作者joshs (Josh Ko)
看板PLT
標題Re: [問題] What does ⊥-elimination do?
時間Wed Mar 6 02:11:56 2013
※ 引述《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
: 但是這能寫出什麼有趣的程式嗎……？
這東西在 Agda 才有完整意義。
常見的用例是在 case analysis 時排除不可能的情況。
如果是在 Haskell, 分析出（我們認為）不可能發生的情況時，
我們會用 error "some complaint", 像
head :: [a] -> a
head [] = error "head accepts only non-empty lists"
head (x : xs) = x
甚至直接省略不寫。
head :: [a] -> a
head (x : xs) = x
但在 Agda 所有程式都必須完全定義 (total),
由此條件可推知 pattern matching 時必須列出所有可能情況，不得省略，
因此在 Agda 更需要處理不可能發生的情況。
但 Agda 不應該有 error 這種函式，否則邏輯系統會不一致，取而代之的正是 ⊥-elim.
error 可任意調用，但 ⊥-elim 不同：
以 ⊥-elim 解消不可能的情況時必須證明這情況真的不可能，
亦即從當下有的假設導出矛盾。
我設法舉個簡單但又不完全無聊的例子。
（其實 (A \/ B) -> (A -> ⊥) -> B 的證明就是一個解消不可能情況的例子，
不過讓我們看另一個稍微具體一點的。）
定義 Booleans 為
data Bool : Set where
false : Bool
true : Bool
並用以下函式將 Booleans 詮釋為自然數：
value : Bool -> Nat
value false = 0
value zero = 1
現設想我們需要定義某個函式，其型態為
-- P : Bool -> Bool -> Set
f : (b : Bool) (b' : Bool) -> (value b <= value b') -> P b b'
白話地講，在 value b 小於等於 value b' 的前提下，
f 須構造出型態為 P b b' 之物件。
我們於是對 b 和 b' 做 pattern matching.
因為 f 必須是 total, 我們完整列出四個情況：
f : (b : Bool) (b' : Bool) -> (value b <= value b') -> P b b'
f false false leq = ?0
f false true leq = ?1
f true false leq = ?2
f true true leq = ?3
這四個情況下 leq 的型態並不一樣：?0 處因假定 b 和 b' 皆為 false,
leq 的型態化簡為
value b <= value b' = value false <= value false = 0 <= 0
同理，leq 在 ?1, ?2, 和 ?3 的型態分別為 0 <= 1, 1 <= 0, 和 1 <= 1.
有意思的是 ?2 這裡：1 <= 0 不應該有證明，我們卻假設 leq 是 1 <= 0 的證明。
若 P true false 下有物件就罷了，
但常見狀況是根本不可能構造出 P true false 的物件。
（否則當初 f 的型態也不用特意多加一個前提了。）
這時我們只能在 ?2 處填入 ⊥-elim p : P true false,
其中 p : ⊥ 是某個從 leq : 1 <= 0 構造出的矛盾證明。
於是 f 的定義基本上就只剩三個情況（?0, ?1, 和 ?3），
只有在這三個情況下我們才真的需要構造出 P b b' 之物件。
若 Agda 的形態系統一致，只考慮這三個情況完全合理，
因為程式實際執行時不可能出現 q : value true <= value false 這種型態的物件，
也就不可能出現 f true false q 這種算式，從而不可能需要求算 ⊥-elim p.
--
所以 FLOLAC'12 跳過 abort 不講實在是明智決定 XD。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 86.2.123.53
※ 編輯: joshs 來自: 86.2.123.53 (03/06 07:21)