Re: [問題] What does ⊥-elimination do?
※ 引述《suhorng ( )》之銘言：
: 另外請問這個 "沒有程式" 的⊥跟 denotational semantics 中的那個 "最少資訊"、
: 或是 non-terminating computation 的關係是什麼呢...？
應該只有型式上的關聯 — 兩者都是某個 category 下的 initial object:
Empty type ⊥ 是 sets & (total) functions 這個 category 下的 initial object,
因為從 ⊥ 到任意一個 set 都恰有一個 function (up to extensional equality).
Least information ⊥ 是將 preordered set 視為 category 後
其中的 initial object, 因為 ⊥ 小於等於任意元素。
: → suhorng:另外..Haskell中好像沒有這個 "⊥" type? 03/05 23:36
: 推 CindyLinz:Haskell 用 data Bottom (後面沒有 =) 03/05 23:39
: → suhorng:CindyLinz: 喔喔好酷! 原來可以不給它 constructor 03/05 23:41
但這個 Bottom 裡面還是有 ⊥ (least info) 這個元素，所以不是 ⊥ (empty type).
: 那我覺得應該存在函數 bottomEliminate :: Void -> a
^^^^ 把這個視為 Bottom
: 不過想不到該怎麼寫XD (雖然說 bottomEliminate = undefined 也是...er...)
或是 bottomEliminate = bottomEliminate.
順帶一提：若我們固定 a 為 Int, 那麼 bottomEliminate 可以是任意常函式，
包括 bottomEliminate _ = 0, bottomEliminate _ = 1, ...
故 Bottom -> Int 之函式不只一個，從而推得
Bottom 不是 DCPOs & conti. functions 這個 category 下的 initial object.
: 然後下面就有人拿出 Agda 了....
不要再逃避了... XD
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 86.2.123.53
推
03/06 05:00, , 1F
03/06 05:00, 1F
※ 編輯: joshs 來自: 86.2.123.53 (03/06 07:03)
推
03/06 07:36, , 2F
03/06 07:36, 2F
推
03/06 08:57, , 3F
03/06 08:57, 3F
推
03/06 22:55, , 4F
03/06 22:55, 4F
討論串 (同標題文章)
本文引述了以下文章的的內容：
完整討論串 (本文為第 3 之 3 篇)：