暴走

參加 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。