[問題] What does ⊥-elimination do?

[suhorng ( )]

想請問一下, 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)
→ suhorng:另外..Haskell中好像沒有這個 "⊥" type?
推 CindyLinz:Haskell 用 data Bottom (後面沒有 =)
→ suhorng:CindyLinz: 喔喔好酷! 原來可以不給它 constructor
推 CindyLinz:這個「abort」名子聽起來很可怕,其實是個exception
→ CindyLinz:handle 嗎? XD
不是耶, 當時 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)
推 Favonia:建議不要用 Haskell 了解這麼嚴謹的東西 xDDDD