※ 引述《noctem (noctem)》之銘言： : 解釋得很棒！真是感謝... : ※ 引述《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. _|_ (\bot) 是任意 type 的 proof term 是甚麼意思呢？ _|_ 應該是對應 logic 上的 false 或稱 absurdity, 雖然 \bot 也用在 denotational semantics 上, 作為 information order 上"沒有資訊"的意思，也就是最小元素， 而 Haskell 也用這個作為所有 type 的 term，因此可以說 Haskell 是 不一致的系統。若用 Heyting algebra 來看 logic 的話， _|_ 的確也是最小元素。 但這兩個 \bot 還是不同吧？ : 補充一下，這裡操作上的意思是我們能寫出不會中斷的程式。 : 用 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）。 雖然是這樣說，不過其實可以設計一個給 domain 的邏輯系統， 有語意，語法以及對應的sequent calculus, 這角度來看就算有 \bot 還是 consistent 的啦。 : : 不過寫了這麼多都沒提到 Kind. : 其實我是不太知道 kind 在這邊的意義哩。說說看吧？ : : (Note: 這段對 user defined data type 的解釋很狹隘, 僅限之後夠用而已, : : data type 的理論 Robert Harper 還在寫的新書裡寫了整整兩章) : 喔喔，這個有草稿可以抓嗎？ : （其實回這篇是為了要問這個 XD） 既然說到這個，我一直想說 FP 對應的邏輯都是構造性的， 但是 wiki 看到的資料寫, 加入 Call-with-current-continuation 對應 Peirce's law 就會是古典邏輯了。但我不曉得實際拿來作證明， 會長甚麼樣子呢？ --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 82.36.219.50