想请问一下, NJ deduction system 中有这条规则 Γ |- ⊥ ---------- (⊥E) Γ |- A 而对应过去的程式是 Γ |- e : ⊥ -------------------- (⊥E) Γ |- abort(e) : A 其中 abort 是 Dijkstra's abort operator. http://en.wikipedia.org/wiki/Guarded_Command_Language#Skip_and_Abort 但是这能写出什麽有趣的程式吗……？ 按照⊥的规则, 我们应该写不出任何型态是⊥的程式, 而许多含有⊥的 proposition 实际给出 term 时往往都有更一般的型别, 如 (a → b) → (﹁b) → (﹁a) 就只是 flip (.) 的一个特例. 我想到比较不无聊的程式为 λx. λf. case x of Inl a → abort(f a) | Inr b → b 是 (AＶB) → (﹁a) → b 的证明 (x 的型态是 AＶB; f 的型态是 a →⊥) 但是这程式感觉看起来超没说服力的说 orz 尤其 abort 那边虽然我们可以推出 f 的型态是 a →⊥, 但是根本不可能有⊥的程式, 那能不能有这种 f 传进来当参数我很怀疑... 好吧, 拿来当证明的程式本来就不打算拿来跑, 不过还是希望能搞清楚它到底是什麽>< 另外请问这个 "没有程式" 的⊥跟 denotational semantics 中的那个 "最少资讯"、 或是 non-terminating computation 的关系是什麽呢...？ - 之前看到那个 ⊥-elimination 的对应是在 FLOLAC'12, 不过在 Harper 的 PFPL 中 也有出现@@ 最早在 Ch 12. Sum Types 就有出现了（Harper把它叫做 void），说是「没有选择的 sum type」，因此没有 introductory form 只有 eliminatory form abort(e), 是相对 於「没有东西的 product type」-- unit 的对偶观念。 可是这样还是写不出什麽有趣的程式吧……？ 另外我所不懂的是, 既然有 abort, 那为什麽 Harper 还会说(Theorem 12.1, Safety) 这样的语言是 safe...? (指 1.If e:τ and e |-> e', then e':τ 2.If e:τ, then either e is a value or e |-> e' for some e'.) - 然後还是不太懂这个到底在做什麽orz --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 118.166.44.132 ※ 编辑: suhorng 来自: 118.166.44.132 (03/05 23:16) 不是耶, 当时 flolac 是说这个函数是 "一旦被用任何值呼叫, 就让程式当机" 维基上则是说 abort 就是 do anything = =||| Harper 写的书的描述是这样: "The nullary sum represents a choice of zero alternatives, and hence admits no introductory form. The eliminatory form, abort(e), aborts the computation in the event that e evaluates to a value, which it cannot do." 然後给的语义为 e |-> e' ------------------------ abort(e) |-> abort(e') 接着就没有其他任何有关 abort 的东西了, i.e. 若 abort(e) 且 e val 那整个计算 会卡住 (got stuck!) 忽然好像有点懂 safety 的意思...因为它的 typing rules 只有 ⊥-elimination 的 上面有出现 void, 所以一个程式若 type check, 一定不可能呼叫到 abort.. (呃, 或是 abort 里面的 e 可以一直算下去不会停) 另外, 假设 data Void 那我觉得应该存在函数 bottomEliminate :: Void -> a 不过想不到该怎麽写XD (虽然说 bottomEliminate = undefined 也是...er...) http://stackoverflow.com/a/10212828/2013713 然後下面就有人拿出 Agda 了.... ※ 编辑: suhorng 来自: 118.166.44.132 (03/06 00:13) ※ 编辑: suhorng 来自: 118.166.44.132 (03/06 00:54)