※ 引述《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