※ 引述《xcycl (XOO)》之铭言： : ※ 引述《noctem (noctem)》之铭言： : : 解释得很棒！真是感谢... : : 这个讲法不错（笔记）。 : _|_ (\bot) 是任意 type 的 proof term 是甚麽意思呢？ 应该说, 因为我们假设操作的 logic system 包含 ex false quodlibet 那麽对任何 type, 从 \bot 出发都写得出 proof term : _|_ 应该是对应 logic 上的 false 或称 absurdity, : 虽然 \bot 也用在 denotational semantics 上, 作为 : information order 上"没有资讯"的意思，也就是最小元素， : 而 Haskell 也用这个作为所有 type 的 term，因此可以说 Haskell 是 : 不一致的系统。若用 Heyting algebra 来看 logic 的话， : _|_ 的确也是最小元素。 : 但这两个 \bot 还是不同吧？ 不是很确定两个 \bot 是不是一样的东西 确实, 两者的来源是不同的. 不过存在任何 context C[] 把两个 \bot 放进去会不同吗? 也就是说, C[\bot_1] 和 C[\bot_2] 可以有不同的 interpretation 吗? 如果不存在这样的 C[] 的话两者应该可以认定为无法区分的吧? : 既然说到这个，我一直想说 FP 对应的逻辑都是构造性的， : 但是 wiki 看到的资料写, 加入 Call-with-current-continuation : 对应 Peirce's law 就会是古典逻辑了。但我不晓得实际拿来作证明， : 会长甚麽样子呢？ 可以参考我推的 Harper 那本书 27, 29, 31 章 以及 http://flint.cs.yale.edu/cs430/assignments/as7.html -- -----BEGIN GEEK CODE BLOCK----- Version: 3.12 GCS/M d- s:++(+) a- C++$ UL++B+ P+(++++) L+ E-@ W++ N? o? K? w(++) !O !M !V PS++(+++) PE++(+++) !Y PGP t+++ 5? !X R !tv b++ DI+++ D++ G e++>++++ h-- r++ y+ ------END GEEK CODE BLOCK------ --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 128.36.229.73