作者joshs (Josh Ko)
看板PLT
標題Re: [問題] What does ⊥-elimination do?
時間Wed Mar 6 04:49:41 2013
※ 引述《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
1F：推 xcycl:不要再逃避了 XD 03/06 05:00
※ 編輯: joshs 來自: 86.2.123.53 (03/06 07:03)
2F：推 scwg:樓上不要在逃避了, 快繼續發 blog 03/06 07:36
3F：推 xcycl:禮拜五死線截止再回來補 QQ 03/06 08:57
4F：推 suhorng:逃避呀QQ.. 03/06 22:55