作者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