大四上回顧

昨天報告完〈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 應該是夠大的領域，而且我也已經大四了，這樣的聚焦應該沒什麼壞處吧。

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