想請問一下, 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)