2009/01/22

大四上回顧

昨天報告完〈Computing Good Nash Equilibria in Graphical Games〉就直奔火車站,結束本學期。這學期主要的焦點是練習寫數學證明,兼顧 rigor 和 readability。有了型式證明的經驗,rigor 的部份並不太難。Readability 就要下點工夫,這方面 AoP 附加推論理由的推理風格很有幫助,適時使用能非常有效地寫出簡練易讀的證明。更精確地說,我對於證明的希望是「一出手就知道是對的」,而達到這個目標的唯一方法就是以型式證明為本,視情況省略(proof trees)末端的細節,鋪敘成人們比較容易接受的長相。一學期試驗下來,成效相當不錯,我願意視之為 math maturity 成長到一定階段的象徵。

以下分科繼續。

代數導論
這一科是練習證明的主要科目。因為作業難度經過控制,我可以多花時間在改寫證明上面,磨到我滿意為止。小考考的是作業題目,二十分鐘要寫兩題,到中期我差點就寫不完,但別人總是提早交卷。稍後我才想到別人必定是收藏了更多細節或只把符號寫一寫,亦即我眼中的 proof sketch,所以最後幾次我就只寫 proof sketch,負擔果然減輕許多。(當然這絕對不符合我為作業設定的標準。)代數這學期談 group theory,我一方面讚嘆前人了解 groups 的成就(例如 fundamental theorem of finite (-ly generated) abelian groups 徹底掌握了 finite (-ly generated) abelian groups 的結構),一方面也得承認 groups 的性質要比 programs 簡單得多。Group theory 尚且未完全掌握 groups,要以代數方法掌握 programs 只會更難。另一方面,既有代數證明的建構性(constructiveness)相當高,因此可能直接應用到程式上,xcycl 最近寫的一篇〈Why quotient and subset on datatype?〉提供了一個例子。
東坡詞
以往讀東坡的〈定風波〉、〈前赤壁賦〉,都是他曠遠的代表作,對東坡的印象也就停留在此。但這學期比較完整地看東坡的各種詞篇後,東坡作為一個人的形象更加完整了。(當然要了解東坡整個人不能只看他的詞,但相較於以往的印象已經完整許多。)除了曠遠的意境,東坡也思鄉、惜別,偶爾豪放,甚至經常感嘆時間流逝。劉少雄老師成功地讓東坡在我心中活了過來,希望隨著成長我會和東坡愈來愈熟嘍。
賽局理論
隨機客終於如願以償,開了賽局演算法。最有意思的大概是後半段的 market equilibria,涉及 flow network,演算法與其正確性證明都相當複雜。我一方面懷疑 formal approach 對於這麼複雜的證明是否可行,一方面發現裡面仍離不開在 AoP 讀到的一些基礎理論。例如找 balanced flow 的演算法基本上是個展開 binary tree 的 hylomorphism,於是正確性證明就會對中間的 data 做歸納,並需要證明整個 hylomorphism 的 termination。以後如果有什麼 formal framework,應該要拿這種程度的證明來測試合不合用。
線性代數一
坦白講,修這科幾乎純粹是要拿數學系的輔系學分而已,所以沒花什麼心思在上面。而且修大一的課真的是幾無負擔,有點太具象了 XD。
西洋哲學史一上
我一直不習慣苑老師的上課風格,感覺上抓不到重點,如一開學時老師引前人的評鑑所言,似乎淹沒在華麗的口才當中。不過奮力抓到一些關鍵字之後,對柏拉圖和之前的希臘哲學家們算有點認識。柏拉圖回歸理性的主張我相當(但不完全)認同,而實在論(例如理型世界存在)的部份我不予置評。我想這是我大學的最後一門哲學課。對於哲學最重要的部份「辯證」,我的態度是除非解決語言的歧義問題,我不願意對哲學問題多做論辯。這是一個支持 formal languages 的理由,我認為即使 formal languages 仍允許各人持有不同的概念,但概念的「形狀」會受 formal languages 限制而不會相差太多。即便 formal languages 的表達力不夠,至少會是有效的溝通媒介。
高等編譯器設計
這門課看 gcc 源碼,相當程度地改善了我對 C 的印象。以往被 Stroustrup 洗腦說 C macro 有多骯髒多邪惡,但實用上效果確實不錯。同時 gcc 也用上很多 metaprogramming,但用的是原始的方法 — 真的寫 C 程式產生 C 源碼然後編譯,過程以 make 控制。不過我還是認同 Stroustrup 的哲學,這些行為最好歸於編譯器的掌控之下。

由以上回顧,可以發現我的關注焦點已經聚在 PL (in general) 上了。PL 應該是夠大的領域,而且我也已經大四了,這樣的聚焦應該沒什麼壞處吧。

--
迎接大學的最後一學期!

Labels:

<< 回到主頁