FLOLAC’14 參與後感

FLOLAC 全名是「邏輯、語言與計算暑期研習營」,主旨是介紹電腦科學基礎,奇偶數年的主題不同,今年 14 年偶數年大約是數理邏輯,程式語言理論,以及函數式程式設計為主。往年因為地域的關係沒有參與過。今年恰逢畢業回國加入講者群,課程安排比以往連貫,配合第一周的型別理論展開。另一方面我也希望經由這次機會了解台灣資工學生的理論背景如何(結果恰好與開課前,拜訪東京大學的學生們形成強烈的對比,有機會再談)。以往從來沒作為學生參加過研習營,首次正式參與便是擔任講師一職以及其他課程助教,事前有些許不安。

一般語意課程中,常選用 While 語言作為示範,這是一個有條件判斷以及 while loop 的 imperative language。但配合第一周的課程 Haskell, Agda 以及 Type Theory,改選擇 Plotkin 在 1977 年介紹的 PCF(Programming Computable Functionals)。此語言是 simply typed lambda calculus 加上自然數,if 判斷式跟 Y combinator,足以表達所有自然數上所有可計算的函數,萃取出常見的程式語言當中必要的構件,程式語言的學術研究也經常用 PCF 為基礎討論。從定義程式語言「如何計算」的操作語意,連結到「計算的內容」的指稱語意。透過此連結,還可以從數學證明在程式語言層面上加入平行計算的確豐富了語言的表達能力。

之前雖然大略看過研究所級的教科書,像是 Thomas Streicher 的 Domain-Theoretic Foundations of Functional Programming 前半部分從語言的基本定義一直講到解 domain equations 等較深的問題,但一直都沒有把每個細節搞清楚寫下來。直到要上陣教學的時候,才仔細看過細節,另外參考 Robert Harper 的 Practical Foundations for Programming Languages 換成較為精簡但少用的語法,修改成較適合教學的內容,像是以歸納法定義程式語言的「值」以及 one-step semantics (另稱 small-step semantics)跟 big-step semantics 的等價性。準備期間才發現不管是兩種操作語意的等價性,或是與指稱語意間的聯繫,都是極為精巧的設計,沒有多餘累贅的操作定義,指稱語意的則是提供極為直覺簡單的數學意涵。指稱語意對於操作語意的正確性,由操作語意上的歸納證明得知,而兩者透過 logical relation ——而不只是單純的歸納證明——巧妙地連結合併,證明了 computational adequacy 性質,說明指稱語意確實導出操作上的計算結果,無需經過冗長的計算。

準備教材方面,感謝今年的助教們尤其是王柔心跟游書泓指出講義上的錯誤,以及蘇健元在安排流程上的建議。比起一開始的版本,應該是相對順暢許多,雖然講義的數學風格對一般的學生還是不大容易接受。不過習題內容需要多琢磨,如何能有效地引導學生熟悉知識並且發展理解,還是需要再多花時間設計。

實際教學上課比起研討會口頭報告相比,內容簡單許多,但卻有「對著空氣講話」不知道學生反應的恐慌。一般學生聽不懂或是講太快的時候通常就開始晃神意識飄移,並不會有具體反應,在台上很難察覺。適時地暫停給學生課堂練習,下場巡視可以幫助他們回過神來,也有比較多的時間跟學生對話,這點往後可以多加參考。最後要不要在課堂間解釋證明,也是往後要好好考慮的,這次在課堂上其中一個證明完全想不出來為什麼(雖然都是自己寫的),學生也毫無興趣的樣子,是這次課程最糟糕的一部份。證明細節該怎麼解說,或是否乾脆列入課後閱讀資料也得好好琢磨。最後考試成果,跟原先預期的分佈情況差不多,大致跟一般數學系課程一樣,少數幾人將近滿分其它落在及格之後。作答情況撇開零分的答案不談,有抓到方向的大多能正確回答,而且成績與平常談話印象來說非常接近。

這次的教學也襯托出台灣(大多為台大高年級與研究所學生),日本(東大某實驗室下)與英國學生(Bham 大學低年級)的差異,英國學生的積極互動但背景略微不足,日本學生積極主動而且背景知識相當豐富但排外不善於溝通,台灣學生上課普遍沒有反應,但接觸不深樣本也不足還不能下定論。回想起大學時代也是如此,老師沒有問之前很少會主動發表意見。

整體來說收獲豐富,接下來要在國外上課不知道情況又是如何 …

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s