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