2012/09/28

FLOLAC'12

四月 scm 老師寄信給我,問我有沒有意願接下 Max 的棒子,教 FLOLAC'12 的邏輯。這對我自然意義重大:踏入程式語言理論是因為參加 FLOLAC'07, 接著 '08 和 '10 兩次海洋年擔任助教,現在第一次正式授課也在 FLOLAC'12. 邏輯在兩週的 FLOLAC 課程裡扮演開天闢地的角色,讓學生第一次親密接觸型式系統,並擁有特權與義務點出 Curry–Howard correspondence, 連結數學與計算、證明與程式(這層非型式的連繫其實需要另外命名,例如 propositions-as-types principleBrouwer's dictum),講授這門課的責任相當重大。不僅如此,數理邏輯本身有豐富的歷史脈絡,並有不少科普宣傳,學生勢必會對這塊很有興趣。我接下棒子,如臨大敵。

備課

五月底交出 WGP'11 paper 的期刊版,六月我便著手準備課程內容,直到八月初才大致底定。這樣的時程完全超出我的預期 — 我最先的計劃是花一個月連同最後的打磨拋光全部完成。七月中我和 Jeremy 見面,很慚愧地告訴他我都在準備 FLOLAC,博士論文要用的材料全無進度,Jeremy 卻出乎意料地笑著說「我能夠理解」,並說他的經驗是一小時的課至少得花十小時準備,如果對材料不熟還需要更多時間。Natural deduction 那些基本的東西我自然很熟,但是進一步的結果如 soundness, completeness, Gödel–Gentzen negative translation, canonicity 我並沒有真的證過,二十世紀初數學基礎大論戰的各流派與概念我也還沒理出足夠清晰的脈絡,這些都必須先自己補齊(我在課程網頁列的參考資料有不少是這段時間才第一次讀)。各主題的取捨、呈現、與串接都費了我不少工夫,一個小例子是 completeness 證明快寫完的時候決定換成結構化證明,前面寫好的十七世紀證明只能全部扔掉重寫。最終設計特別有趣的大概是下列幾點:強調直構主義(intuitionism)、解釋迭構法(induction)的立論基礎並操作之、緊扣數學與計算之間的連結。

我參考的是 '07 年 Max 的架構,一次講 intuitionistic logic 和 natural deduction, 一次講 classical logic 和 formal semantics, 最後一次講 Curry–Howard 並提點 languages, deduction systems, 和 semantics 的相對關係。(Max 在 '07 年第三次上課還有講 equational logic, 不過那算是 bonus, 我認為重點還是在 Curry–Howard 和整門課的架構提點。)與往年最大的差異是我特別把直構邏輯拉到第一次上課講(辦公室有位同事看到我的授課大綱,還很驚訝地說「你從直構邏輯開始耶」),因為 de Bruijn 在〈Type-theoretical checking and philosophy of mathematics〉諄諄告誡

[...] [N]atural deduction [...] follows the way people reasoned before it was tried to explain logic by means of an algebra of truth values. Such Boolean logic is the metatheory of classical reasoning. It does not show what that reasoning is. It is silly that education in elementary logic so often takes truth values as the point of departure.

The idea that truth values are the basis of logic may have been one of the reasons why Brouwer's rejection of the law of the excluded middle was so little understood in his time. If one starts from Boolean logic instead of from natural deduction it is impossible to understand what that rejection means.

古典語意被我刪減到差不多只剩基本定義,最後還收尾在 Gödel–Gentzen negative translation, 把古典邏輯嵌入直構邏輯,藉以說明前者的表達能力從某個角度來看其實弱於後者。這麼偏袒直構邏輯,我的辯解是:反正到其他地方都是古典數學說了算,直構數學根本連露個臉都沒機會,就只在 FLOLAC 這裡讓我們聚焦於直構數學吧。

邏輯從第一個定義(propositional formulas)開始就大量使用迭構法(induction),但很少有人真的從迭構定義(inductive definitions)開始解釋迭構法為何有效,頂多只是給一些型式原則。我對北京清華第二屆 Coq summer school 印象最深的是他們特地設計一門課來講迭構法的精神和各種型式,我認為這是非常恰當的設計,因為程式語言理論有一大半的根基是迭構法,沒好好解釋迭構法相當於沒紮好根基。但是我沒有時間從自然數的迭構法開始慢慢講,所以我選擇只在介紹 propositional formulas 的時候一併交代一下迭構法。另外我希望展示迭構法的有趣應用,在邏輯的話,最適當的應用應該非 soundness & completeness 這類性質莫屬了,但這是在 derivations 上的迭構,而 derivations 用一般的迭構法造不好,得用上 inductive families 或是 induction-recursion 之類的手法。我當時設計到這裡猶豫了一陣,不知道該不該深入至此,但最後還是把 derivations 寫成一個 inductive family 然後真的下去用迭構法證 soundness & completeness, 因為我猜測 Coq 真的想證點東西的話不可能不用 inductive families, 先講的話,到 Coq 那邊應該就比較不怕了。(結果我錯了,Arthur 只有展示 Coq 的火力,沒真的帶著學生用 Coq 寫各種迭構定義。)

我堅持要講 soundness & completeness 證明的另一個理由是,最後我希望把 induction 和函式編程的 fold 連結在一起,為此我採用和函式編程相近的語法,從一開始就強調 induction 的計算意義,並給一些證明,希望學生到最後能從這些例子隱約體會到證明與程式確實是同一件事。習題裡面還放一題請學生自己跑一次 completeness 的證明。(這計劃也以失敗告終。一個外在理由是:我預期函式編程是莊老師教,照莊老師的速度,fold 最慢到第二次上課就會出現,我第三天講這連結,剛好能銜接上。結果函式編程換成 scm 老師教,scm 老師又剛好決定要大幅簡化課程,只在他的課最後很快提一下有 fold 這種東西,所以連結失敗。)我一直覺得資訊系學生成天寫程式卻排斥證明,這種情況從 propositions-as-types principle 來看實在很不健康。要是我的邏輯課只是敘述一堆定理都不證明,那就又讓他們多看到一個壞榜樣。造成這種情況的原因大概是他們對程式的認識不夠健全,以及古典數學證明一般不具建構性,以至於難以發現程式其實和證明一樣,都是在描述如何建構具所需性質的物件(而不只是指引機器操作符號的腳本)。「補全對程式的認識」會是 FLOLAC 其他課程的目標,但最後想把程式和證明這兩條經脈打通的話,大概只能從邏輯這裡補上一指了。

整體設計我相信立意良好,但九小時要達成預定目標,無論對講者和學生都非常困難。我的設想是盡可能不要把東西直接丟給學生要他不假思索接受(所以比方說要下迭構定義之前最好先把迭構講清楚),但學生還是要自己掙扎一番才能納為己有。但掙扎需要時間。隨著投影片製作告一段落、實地演練授課之後(倒楣的 housemate 被我抓來上了好幾小時的課),時間不足的問題更是明顯。如果我有一學期的時間,我根本不會從邏輯開始 — 我一定先講基礎的函式編程和迭構證明,並搭配 Agda 之類的語言,悄悄引進 propositions-as-types principle. 等到對「程式/證明建構」培養出足夠的直覺之後,才開始講邏輯和 Curry–Howard. 這樣的順序呼應直構數學「邏輯是數學一部份」的看法,講邏輯的時候也才有更多具體經驗支持。但我只有九小時。最後我想,學生能聽多少就聽多少吧,反正真正有興趣的學生大可日後慢慢研究(掙扎)。

課程準備大致完成,八月 27 號逐漸逼近,但這時天坪颱風也逼近了⋯

食衣住行育樂

今年台灣颱風特別多。原本我預定八月 22 號倫敦起飛、於香港轉機、23 號傍晚抵達台北,但突然殺出一個天坪颱風。20 號看天坪的預測路徑,竟然正好在 23 號籠罩台灣,並繼續往香港推進,最壞情況我說不定得滯留香港機場不只一天。我於是決定改期,提早在 20 號當天晚上出發,搶在颱風抵達前回台。21 號原先有一場家庭音樂會,我準備蕭邦離別曲和 Op. 17 No. 4 馬厝卡等曲子要歡送拿到學位即將返台的 housemates, 也草草取消。FLOLAC 開始前幾天,天坪掠過南部,緊跟在後面的布拉萬也北偏撲向韓國。正當我以為逃過一劫,颱風們竟又發動速攻魔法「藤原效應」,布拉萬牽引下,天坪迴轉再次往北掃過台灣!眼看第三天的邏輯課就要泡湯,幸好最後天坪東偏,沒對台北造成什麼影響。

兩週的課程於是順利進行。回憶當年,FLOLAC'07 前夕我左手鷹嘴突骨折,吊著一隻手去中研院資訊所上課。Yen3 義務擔任書僮,和我住在中研院活動中心兩週,生活全賴 Yen3 打理。晚上寫完作業躺到床上,兩人胡亂閒聊,不亦樂乎。這次 Yen3 找到價格低廉的短期租屋再與我合住(不過這次聊的話題都比較沈重 – 我們已經不是當年無憂無慮的大學生了啊)。第一週我忘了帶睡衣,向 Yen3 借一條極其寬鬆的褲子,週末我回家重整行李,第二週輪到我借他浴巾。我們每天早上走一小段路去吃古亭站出口處的弘爺漢堡(「宮保鐵板麵」不錯)然後搭捷運到台大,晚上通常和一群人吃飯,然後帶著飲料回去。Yen3 每天要跟女友柔言細語一番,另選幾天外出和女友共度甜蜜時光。這次完全沒回 118 巷,因為認識我的兩家餐館都關了,只到台大牛肉麵和資管系對面巷子裡的平價拉麵重溫一下熟悉口味。Yen3 在拉麵店附近發現一家最近從師大夜市搬過來的店,賣綠色臭豆腐和蘭陽米粉羹,相當好吃,讓我回去好幾次。FLOLAC 的優良傳統「美味便當」仍然延續,好幾天讓我在不同便當菜色之間猶豫不決。雖然台北食物的 CP 值大勝,但習慣了中興新村和牛津的小鎮風光,對台北無止盡的水泥叢林不由得感到厭倦。唯一令人懷念的大概只有國家音樂廳,水準完全不輸倫敦。上次進國家音樂廳是兩年前,FLOLAC'10 進行中,我即將赴英,和奇特裸子植物(現於 UT Southwestern 攻讀博士)一塊聽的是 Garrick Ohlsson 的鋼琴獨奏會。這次我選 FLOLAC 中間那個週日下午和 Yen3 一塊去聽 Eldar Nebolsin 的鋼琴獨奏會,進場前還先席地坐在國家音樂廳的飛簷下改了一陣子作業。坐到離舞台這麼近的位子還是第一次,好像要帶領全場聽眾衝進 Nebolsin 捲起的旋風之中。

講課

不過重頭戲當然是邏輯課。要一言以蔽之的話,可以用英國人的說法 "could be worse". 第一天早上緊張得連喝杯豆漿都很勉強。很快共同教室 203 就坐滿人,蔡老師帶著資管系主任來開場。scm 老師今年沒放「煉獄與海灘」投影片,交代一點行政事項後就換資管系主任,後者還很有興致地講一大段。好不容易輪到我啦,第一段 propositional formulas & induction 講得還行,可是講完就下課了,和我「只使用半小時」的目標相差甚遠。下課時 Jaiyalas (or Yen3?) 偷偷跟我說 scm 老師聽到一半就狂皺眉搖頭,覺得內容太難。(我想:蛤,那明天還有 inductive families 怎麼辦⋯)第二段上 natural deduction, 已經講到有點昏了,速度愈飆愈快,例子除了前一兩個以外全部略過,到爆炸原理還絆了一下。第三段是我最不拿手也最討厭的 first-order logic, 撐到 variable capture 終於崩潰了,完全想不到該怎麼解釋「binding structure 改變」有什麼不好,結果硬生生斷開繼續往下講。到了 natural deduction for first-order logic, 這裡 forall-introduction 和 exists-elimination 的 side conditions 也相當棘手,我倒是有給解釋,只不過抽象得應該沒什麼人聽懂。第一天的課就這麼連滾帶跑,最後突兀地停在 natural deduction 的符號海當中。事前設計是第一天用 Heyting arithmetic & Hilbert's program 收尾,讓學生知道前面那套符號是因應什麼樣的問題而發展出來。現在糟啦,沒頭沒腦扔給學生一大堆符號卻沒交代清楚這是幹嘛用的;如果只是這樣那還算了,但我連關鍵技能 natural deduction 也沒講好。我覺得好對不起 scm 老師,把 FLOLAC 開宗明義的第一門課全搞砸了。中午只吃幾條海帶,下午精力耗盡,坐在教室後面倒頭就睡。

第一天晚上準備隔天的課時,心裡已經坦然許多:今早已經上得奇差無比,明天講再差也不會比今天差。傷害已經造成,現在該做的是損害控制,後面課程的難度也要下修。隔天早餐成功吃下一份玉米蛋餅配冰奶茶。第一堂課先重新講解 induction principle 為何有效(稍後將推廣到 inductive families 的 induction principle)和 natural deduction 由下而上和由上而下兩種方向的解讀方式(稍後的 soundness 其實就是由上而下的解讀),然後把 Heyting arithmetic & Hilbert's program 講完,講得出乎意料地順,特別是 Hilbert 將古典數學區分為真實、理想兩部分,然後舉射影幾何「無窮遠處的點和線」為例,這一段我還挺滿意的。第二堂課講 classical semantics 和 derivations as an inductive family, 也講得不錯,特別在解釋後者時行雲流水,從不能用一般 inductive definition 的原因到 inductive family 的直覺解讀方式都妥善交代了。這節下課我在回答問題時 scm 老師走來拍拍我的肩,似乎很滿意,不過我忙著回答問題沒細看,說不定只是跟我打招呼 XD。第三堂講 soundness & completeness, 並稍微提一下 Gödel–Gentzen negative translation 的意義。照原先計劃,我在實際的 derivation 上大略說明 soundness & completeness 是怎麼跑的,然後提點一下證明的架構如何和我講的實例對應,停在我認為滿適當的抽象層級。或許是一開始沒抱什麼期望,第二天講完覺得表現出乎意料地好,信心瞬間恢復。或許因為這樣,第三天太過放心,結果又講得零零落落。

第三天的備課是半夜在床上突然醒來,索性就躺著全程想一遍,想到不少好說法。事後證明這種備課模式極不可取,既沒有養精蓄銳,想到的東西又容易忘掉。下午換一間教室,草草把討厭的 classical semantics of first-order logic 結束掉,趕快進入 Curry–Howard correspondence. 半夜想到的說法重現比較成功的大概只有最一開始,把 natural deduction derivation 變成 typing derivation、然後把 lambda term 直接畫在 derivation 上,從而能直接觀察到 derivation 和 lambda term 的結構確實一樣。接下來 simply typed lambda calculus with constants 就只是一板一眼講過去(這次比較聰明,直接跳過 abort)。「Detours 講得不是很順,不過隨便啦,趕快跟 redexes 扯上關係,帶到 underivability.」講到一半,已經覺得精神不夠集中,不太能隨心控制講話內容,前面那句大致上是當時的想法。終於,到 propositions-as-types principle 又崩潰了,但這次是不自覺的崩潰:把直構數學和編程拉在一起的時候還好(可是請 Dijkstra 出來露臉的時候我忘記講投影片頁碼的字體是 Dijkstra 手寫體!),進入 type families 時竟然忘了闡述關鍵 "type = set = proposition",證明程式直接全部摻一塊講得不亦樂乎,把台下學生甩到不知哪裡去,下課學生問問題,我才發現失誤得有多離譜。最後留下一點時間檢討第一次 natural deduction 的作業,效果也不好:早上收作業但看得不夠細,後來幾天改作業看到不少常見錯誤,檢討時都沒能提出來。第三天基本上也是失敗的。

讀了 Boris Berman 的《Notes from the Pianist's Bench》之後,我更加確定授課(演講)和音樂演奏有很多原則是共通的 — 兩者本質都是在時間上堆砌出某種結構(在音樂是情感的跌宕,在數學則是概念的排列連結),而且這結構有不同尺度的內容要呈現(在音樂必須兼顧每個樂句的語氣乃至整首曲子的分段,在數學則是從證明細節到重要概念的相對關係都必須說明清楚)。不過,相對於演奏,講課技巧上還是比較簡單,對語言精準程度的要求遠不如音樂家對於每個音強弱長短的拿捏;一句話說得不好,再說一次一般沒什麼大礙,但從沒聽過哪位鋼琴家彈到一半停下來說「抱歉我這段重彈」。如果把這次講課比作演奏,只能形容為荒腔走板,頂多聽得出大概是什麼曲子而已。不過真的獲得不少寶貴的實戰經驗,以後會講得更好。

順便提一下兩次作業。第一次全是 natural deduction, 我出題時不小心畫太多雙箭號,每畫一個就讓 derivation 變成兩倍大,學生痛苦完之後,就輪到我面對幾十份飽滿的作業,足足改了好幾天。不過大部份人都做得不錯,還有些導法是我沒想過的。(考試最後一題 admissibility 有人想到不用 weakening lemma 的導法,也出我意料之外。)第二次請大家寫證明,情況就很慘烈。尤其第一題 "Γ ⊧ φ iff (Γ, ¬φ) is unsatisfiable",我出的時候完全認為是暖身題,連接詞和量詞小心弄清楚就行了(natural deduction 做了這麼多,應該能觸類旁通吧),結果收來一看,大部份都不知所云,想修補還不知道從何修補起。雖然我上課的確沒細講證明,也沒給多少時間消化吸收,但來修課的不乏大學高年級和研究所學生,這種程度的證明都寫不周全,很明顯反映出工科的數學教育輕忽證明訓練。這樣的教育方向真的好嗎?

聽課

scm 老師臨危受命,除了本來的 program construction 以外又接下 functional programming. 不知道 scm 老師在資管系受到什麼樣的打擊(或啓示),上課速度慢得不可思議。我私下向人解釋 Church numerals 的時候順便講了一下 fold, 以為破了 scm 老師的哏,結果十八小時的課別說 fold fusion, 連 fold 都沒真的講。Fold 算是學 FP 必撞的一道牆,既然如此不是應該編入課程幫助學生跨越嗎?而且我還是覺得沒有講 fold 的 FP 只是讓人稍微嘗鮮,跳不到全新的角度看編程。不過在意見調查表上 scm 老師的課得到一致好評,讓學生容易聽懂的設計確實有成功。另外邪教說已經成為 FLOLAC(海洋年?)傳統,今年邪教檢查表堂堂進佔意見調查表最後一頁,scm 老師更正式坐上邪教教主大位,可喜可賀 XD。

本次最期待、聽完也最滿足的是 Favonia 推銷直構數學的特別演講。Favonia 的演講風格在正經和玩笑之間取得巧妙平衡,而且有種現在已經很少見的誠懇。整場演講把直構數學的特點鋪敘得很成功,並引發 FLOLAC 史上最熱烈的討論。有不少說法(比方說爆炸盒!)是我往後打算一再引用的。陳恭老師、陳郁方老師、和董世平老師講的都是舊東西。今年外國講者 Arthur Charguéraud 負責介紹 Coq, 安排一次上課教 separation logic, 最後講他博士論文做的 characteristic formulae. 我本來很懷疑 Arthur 如何在九小時內教完 separation logic 而且還在 Coq 裡面驗證 imperative programs — 北京清華的 Coq summer school 是到第二週最後才有一個很簡單的 imperative programs 驗證練習。答案揭曉,原來 Arthur 給的比較像是火力展示,重點擺在「Coq 能做什麼」而不是「Coq 怎麼用」。Separation logic 就有細講,但對於剛接觸這一切的學生 Arthur 的速度應該算滿快的(我的課也差不多?)。Arthur 的英文沒什麼法國腔,有問 Arthur 問題的學生也能流暢溝通,但教學回饋一如往年還是有很多人說自己英文太爛聽不懂,甚至有人建議不要找外國講者。欸,要聽 Coq 這種主題想從國內找人講還真的找不到耶⋯

教與學

我在大學最狂妄的時期對老師的要求極其嚴格,現在自己上台才更真切了解那時的要求有多苛刻。教與學有某種關係是我以往沒有真正察覺的,一個有趣(但不深)的比喻是線性代數裡 linear forms 和 vectors 的關聯,兩者看似截然不同,深層卻有完美的對稱性。老師備課和回答問題,不妨看作是學生交作業和應試的升級版:備課是交出一份規模龐大又得精心雕琢的作業,回答問題則相當於應對五花八門甚至毫無預警的試題。備課不妨比喻作設立一套場景供學生跑跳,這套場景是否能讓學生輕易找到前進方向、是不是所有細節都設置妥當沒留下邏輯上的空白、有沒有呈現美感、啓發,諸般複雜考量若要兼顧,需要大量創意。至於學生問的問題,在這種入門課一般不需要太艱深的答案(反而應該避免),考驗的是老師是否已經為基本概念建立一套體系並能夠完善、白話地說明。說明的深度可以比科普難一點(多用一點術語)但還是接近科普 — 這不見得比直接技術上的討論簡單,往往需要回到概念的本質,從那裡開始重新打造易懂的說詞。整個對稱關係不光是師生一同研討一門知識學會新東西而已,學生和老師各有自己的工程要建構並接受檢驗,在「教學」這種互動模式下一起成長。這麼早被放到「教」這個位置倒是沒料到,有種被強迫長大的感覺。被叫老師很不習慣,可是中文的輩份表示又根深蒂固。英文這方面的規定輕鬆很多啊。

打從一開始我就決定要待滿兩週,希望見到很多熱情的學生、回答很多有趣的問題、參與很多深入的討論。事實證明我果然押對寶了。今年 FLOLAC 似乎因為口碑慢慢打響(還是因為開成暑修課程有正式學分?),修課席次供不應求,一掃往年「告急」的窘況,若計入旁聽席次更讓整體聽課人數翻倍,光從這種態勢就可預期今年會擦出很棒的火花。我後來一直說,這次邏輯課其實是被學生救回來的:我講得這麼不周全,學生卻能自己領會那麼多,課後又不吝於發問,讓我有機會好好重講一次。光邏輯一門課,來問我問題的人就比我想像的還多(其中真的去讀 soundness & completeness 證明或至少有興趣的人不算少,令我很欣慰),廣度和深度也令我驚嘆。事前花那麼多時間準備沒有白費!我應該是最常在場的講師,所以也得以回答一些其他課的問題,稍微復習一下基礎。最令我印象深刻的一幕當屬 Favonia 演講後那個場景,眾人自發形成數個圈圈熱力十足地討論起來。身處其中一個圈圈,我好像又變回熱情單純的大學生,和一群同樣熱情的同學討論超級有趣的學問。(這種盛大場景嚴格說來在我大學時期沒發生過 — 我大學時人際關係處理不佳,總是獨來獨往。)想到日後有更多與熱情學生切磋的機會,我就又燃起把博士讀完的動力。(殘酷事實先不用告訴我沒關係 XD。)這大概是我在 FLOLAC'12 最大也最意想不到的收穫吧。

--
28 Sep 2012: 抵英兩週年紀念日。

Blogger yen39/29/2012 2:40 am 說:

糟糕,我被提到的部分都不怎麼好啊 XDXD

我今天晚上再細看 ... 剛回來 XD。

 

<< 回到主頁