2008/12/30

暴走

參加 scan33scan33 主辦的 seminar on theory of computation。最後提意見的時候,我說似乎看過 Gödel 喜歡 Turing machine 不喜歡 lambda-calculus,覺得很不解,因為前者定義繁複、幾乎不可能型式地論證,後者至少定義簡單很多。結果我就從 lambda-calculus 的 term syntax 講到 alpha-conversion、beta-reduction,拐到 Haskell(應該是為了展示「這種脈絡下有實用的東西」)又繞回 Church-Rosser theorem,再迅速飆到 Curry-Howard correspondence 把 ∀P. ∀x. P(x) ∨ ¬P(x) 和 decidability 拉上關係,最後還天外飛來一筆 complete partial orders 和 continuous functions,驚險地在這裡煞住車 XD。

突然這樣來一次有點像隨機考試。當我敘述 Church-Rosser theorem 和 corollary "normal form is unique" 的時候其實被自己嚇到 ─ 我沒預料可以講得這麼順 XD。

--
這種 lightweight seminar 偶爾辦還挺不錯的 XD。

Labels:

Blogger Nanro1/07/2009 12:39 am 說:

我也喜歡這種討論會

感謝學長,真是讓我開了眼界XD

 

<< 回到主頁