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