Re: [心得] Y Combinator 與 Mutual Recursion

看板PLT (程式語言與理論)作者noctem (noctem)時間14年前 (2010/06/04 15:21)推噓1(1推 0噓 1→)

留言2則, 1人參與討論串4/6 (看更多)

解釋得很棒！真是感謝... ※ 引述《scwg ( )》之銘言： : Unification 是在說: "現在看起來這個 proof term 你既用來證第一個 proposition, : 又用來證第二個 proposition, 那麼要不這兩件事是同一件事 : ( unify (a :-> b) (c :-> d) = unify a c +++ unify b d ) : 要不某個 proposition 不能太 general, 只能是特定形式 : ( unify (Var a) e = a |-> e where e /= (Var a) )" 這個講法不錯（筆記）。 : 在沒有 Y 之前的 typed lambda calculus 是沒有 divergence 的. : 所有的 function 都是 total function, 給了 input 一定有 output. : 但是 recursive 給了我們造出 divergence 的空間, function 不一定是 total 了. : 事實上這表示我們證得出 "False" 了! 因為 _|_ 是任何 type 的 proof term. : 這個 logic 不再 consistent, proof term 不再是 valid proof. 補充一下，這裡操作上的意思是我們能寫出不會中斷的程式。用 untyped lambda calculus 我們能寫出可以一直 reduce 下去，不會終止的 term (例如 Y, 和很多其他的). 它的表達能力和 Turing machine 一樣。加上 type 的 lambda calculus 通常有 strong normalisation 的性質: 任何 reduction 都會停在某個 normal form. 也就是說用它來寫程式的話，可以確定所有程式都會終止。這樣聽起來很好，代價則是可以寫的程式變少了（但，有人似乎是認為這樣也夠了，詳後述），這語言不再是 Turing complete 了。那個用 Fix 的做法則是用了 type system 開的後門，讓我們又可以定義 Y combinator. 但這麼一來優缺點又顛倒了：你開始可以寫不會中斷，有任何 type 的程式，例如 "y id". : 但是在一些 proof assistant 裡, 因為主要功能就是證明, : 所以上面的 Fix 通常是不合法的. : 要 recursive 可以, 通常只給 primitive recursion, : 這樣還是只寫得出 total function, logic is still consistent. 其實應該比 primitive recursion 強一點（欸，其實是很多）啦。前面的推文有說到 fold/cata, 所以我想這邊可以提一下.. 用 System F 就可以模擬 inductive type 了，做法和 Church encoding 一樣，一個 type 就是它的 fold. (有我不認識的人到現在還知道我在說什麼嗎？那就應該認識一下了 XD) 另外也可以模擬 coinductive type, 例如無限長的 list 或 tree, 基本上一個 coinductive type 就直接用它的 unfold 來表示。這樣你就有了一個語言，有 inductive type (可以做 fold), 也有 coinductive type (可以 unfold), 但是 unfold 出來的東西和 fold 吃的東西的 type 不一樣，因此不能做 hylomoprhism. 這樣一來所有程式都還是會終止的。現在大多 proof assistant 只要能表達 second-order logic 就可以這樣做。有人是認為這樣就很夠了。只是你每寫一個長得比較奇怪的程式，就得付一個它會終止的證明（這個證明當然就表達成某個 inductive type）。 : 不過寫了這麼多都沒提到 Kind. 其實我是不太知道 kind 在這邊的意義哩。說說看吧？ : (Note: 這段對 user defined data type 的解釋很狹隘, 僅限之後夠用而已, : data type 的理論 Robert Harper 還在寫的新書裡寫了整整兩章) 喔喔，這個有草稿可以抓嗎？（其實回這篇是為了要問這個 XD） -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 140.109.20.217