作者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)