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