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