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