大三上回顧 ─ Current View about Computer Science

FLOLAC '07 對我顯然是個重大的轉捩點。幸好成行了，不然我不知道會浪費多少時間。那感覺就好像是突然往後一看，一大片閃閃發光的領域就在那裡等著我。之前我雖然對學校教的 CS 有親近之意（相對於其他學門），但始終達不到完全的共鳴。這次不一樣，我看到 program derivation、Curry-Howard isomorphism，馬上就叫出來 "it should be done this way!" 沒意外的話，我就要朝這個方向走下去了。

長久以來困擾 (theoretical) computer scientists 的一個問題，就是 Mathematics 和 Computer Science 的關係。（或許稱後者為 "Computing Science" 更恰當，不過我就先把它們當作同義詞用了。）Knuth 在《Selected Papers on Computer Science》裡面曾經用他獨特的方法尋找這個問題的解答，但也沒能把兩者異同說得足夠清楚。（感覺上 Knuth 對於哲學式論證並不在行 XD。）對一個剛入門的小朋友而言，有時候 CS 和 Math 分得很開，有時候又會出現像 "Mathematics of Program Construction" 這種混合的詞彙，非常混淆。我當然還沒找到終極的答案，不過我發現若採用某種二元論的思維，很多問題就能解釋清楚。正常的大學生應該都已經對「正式與直覺」、「語法和語意」這類的二元概念有一些體會，我這裡想強調的是「純粹概念」和「操作工具、方法」之間的交互關係。從這種觀點來看，CS 和 Math 在「方法工具」上沒有什麼區別（deduction, abstraction, ...），但是兩者操作的「純粹概念」我認為是可以區分的。數學所探討的純粹概念恐怕數學家也很難給一個內涵上（intensional）的界定，但他們顯然不只專注於「有窮的機械式計算步驟」。CS 的各個分支就比較清楚，理路上（至少實作上）大都可以從 "algorithm" 發展出去。（這樣的說法或許是受了 Knuth 的影響。）"Algorithm" 的相關概念是不是數學概念的子集還有待爭辯，不過數學家發展的工具縱深真的很夠，拿過來 CS 這邊試著套套看一定很有意思。

最後以一點關於「證明格式」的討論作結。這學期我寫的圖論證明比較偏向白話敘述和畫圖示意，比較少用 set comprehension 或其他的符號來寫。我個人不覺得這樣比較不嚴謹，因為「嚴謹」應該是在「純粹概念」那邊講的，不一定要訴諸符號（這是「方法工具」的一部份），只是有些時候符號確實能表達得比較好。更何況，如果把嚴謹定義成 "formal"，每篇數學論文都該用 theorem prover 來寫才對，至少也該用 Leslie Lamport 提倡的那種 structural proof 格式，那才有點 "formal" 的味道。我以後會遇到的、要寫的符號顯然不會太少，一般的證明還是寫得白話一點吧。

--
以後記得要趁文思泉湧的時候（i.e., 期末考）一口氣把回顧寫完 XD。