[問題] What does ⊥-elimination do?
想請問一下, 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)
→
03/05 23:36, , 1F
03/05 23:36, 1F
推
03/05 23:39, , 2F
03/05 23:39, 2F
→
03/05 23:41, , 3F
03/05 23:41, 3F
推
03/05 23:53, , 4F
03/05 23:53, 4F
→
03/05 23:53, , 5F
03/05 23:53, 5F
不是耶, 當時 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)
推
03/06 13:18, , 6F
03/06 13:18, 6F
討論串 (同標題文章)
以下文章回應了本文 (最舊先)：
完整討論串 (本文為第 1 之 3 篇)：
PLT 近期熱門文章
PTT數位生活區 即時熱門文章
