The Coq Proof Assistant A Tutorial (9) 排中律の証明
さかい さんからトラックバックをいただきました．
ヒビルテ 2006-04-29 [Haskell] [quiz] (forall x. ((x->r)->r)->x) -> Either a (a->r)
うほっ，いいトラックバック… ありがとうございます．
しかし，何を言っているのすら全然理解不能だぜ，ビバド低能な俺 ☆
とりあえず，Either ってのは，Haskell の言語仕様に組み込みのタグ付き型の一種で，静的強い型付けが強制される Haskell において，2 つの型のどっちかを返す関数を定義する時に使うらしいです．
まず Haskell がわからないから，脳が拒絶反応を起こしてしまう．
とりあえず，Coq 風の記法 + 自然演繹法のスタイルで，証明を書き直してみよう．
まず，非常に美しい体系 NJ (Natural Deduction for Intuitionistic logic) に，忌々しい二重否定除去規則 (Double Negation ; 以下 NNPP と略記) を加えましょう (笑)
構成的論理に基づく Coq のデフォルトでは，古典論理の排中律 (The Law of excluded middle ; EM) はもちろん，NNPP も使用することはできません．
ただし，Classical モジュールを明示的にインポートすると，NNPP を使用することができるようになります．
これまでの直観主義における自然演繹の体系に，NNPP を加えたこの体系を，NK (Natural deduction for classical logic) と呼ぶそうです．
ちなみに，K はドイツ語で，Kalkuel (計算) の意らしいです (J が何の略なのかはよくわかりません．無理矢理 Klassical Logic とか Jntuitionistic とか書いているサイトもありました w)．
# 美しいけどおもちゃに過ぎない体系ではなく，こっちは汚いけどモノホンの「計算」を扱ってんだ ！ っていう気迫が感じられますね．まぁ，どっちにしろ，自然演繹法自体が，直感的にはわかりやすいものの，あまり形式的には整理されていないため (一長一短なので，一概に悪いとは言えない)，シーケント計算の体系とかが本命になってくるのですが．
「二重否定は除去できる (¬ 除去)」 というのは，かなり強力な推論規則で，これと 「もし A と仮定して，*実際に矛盾を作ることができたら* ¬ A を書き加えても良い (¬ 導入)」 を組み合わせると，排中律 (P ∨ ¬ P) が証明できてしまいます．
まず，方針として，せっかく NNPP を手に入れたのですから，おそらく最後は ¬¬ (P ∨ ¬ P) の形に NNPP を apply して，EM を手に入れることになるのだろう，という目星を付けます．
# NNPP を使わないですむならば，NJ で十分 w
ということは，まず ¬ (P ∨ ¬ P) の形を仮定して，そこから矛盾を意図的に作って行く必要がある，という見当が付きます．
んで，上手く contradiction させるためには，(ここはわかりにくくて，混乱しがちですが) P ∨ ¬ P を，一段下がった仮定のスコープの中で導き出してやる必要があります．
はぁ ? P ∨ ¬ P を証明したくてやってきたのに，P ∨ ¬ P を使っちゃったら，循環論法にならなくね ? と，大人社会の体制の嘘臭さに敏感で血気盛んな若者達は思ってしまいがちですが，スコープが違うので問題は無いのです (このようにして上手く丸め込まれながら，青くさい少年ボーイは大人になっていくのです)．
プログラマならば，変数のスコープ (有効範囲規定) はお馴染だと思います．たとえ同じ名前，同じ形の変数名や式が出てきても，スコープが異なれば違うものなので，混乱しないでちゃんと区別しないといけないのです．ここをいい加減にしてしまうと，何でも導けてしまうため，何もかもがナンセンスになってしまいます．グローバル変数が危険なのと同じ理屈です．
基本的に，自然演繹法では，新たな仮定を付け加えるたびに，どんどん右に証明経路がずれていきます．そして，スコープは，現在の経路から見て左側のみになります．
すなわち，右側の，勝手に付け加えたローカルなスコープ内の仮定には，左側からはアクセスできません．ちゃんと勝手に付け加えた仮定を全てキャンセルして，左側にもどってこなければなりません．
というわけで，一段潜った部分で，P ∨ ¬ P の構成を試みていきましょう．
∨ を出す (∨ 導入) ためには，P か ¬ P のどちらかを出せば OK です．ここではとりあえず ¬ P を出すことにしましょう (どっちを選んでも，今回の場合は同じになる)．
¬ P を出すためには，さらにもう一段深く潜って，P を仮定して矛盾を作り， ¬ 導入して戻って来れば良さそうです．
一番最初とは異なり，左側の仮定は，全て自由に使うことができます．というか，使えるものは，どう考えても ~(P \\/ ~P) しかありません．んで，こいつをキャンセルするためには，P \\/ ~P を作れば，うは wwwww おk wwww です．
もちろん，P が仮定されているので，P \\/ ~P はトリビアルに成り立ちます．以上で，じっちゃんの名に賭けて，謎は全て解けた ！ QED です．
あとはこいつを Coq で書き下せば良いだけなのですが… これは，次回と言うことで (笑)
まだようやく CoqIDE の使い方がわかってきたレベルの坊やなので… どんなコマンドや機能があるのかさえ，まだまださっぱり妖精です．
とりあえz，Linux の coqtop は，Windows と異なり，履歴などが遡れなくて不便なので，なるべく coqide を使った方が楽ですよ．
使い方は以外と簡単で，起動して，バッファにテキトーに何か書いて，後は上の方にある， ↓ を押せば，１行ずつ coqtop に入力してリターンを押したのと同じように，対話的にインタプリートしてくれます．
一度読みこまれた行は編集できなくなるので，バックトラックして編集したいときは，↑ ボタンで戻れます．また，→ ◯ で，カーソルが当たっている任意の位置に戻れます．
↓ を押せば，バッファを丸ごとバッチ処理できますし，
--
--
↑ を押せば，一番最初に戻ります．
やっぱり，IDE の方が，慣れればコマンドラインよりも便利だと思います (私は IDE とかの使い方を覚えるのが面倒で面倒でしかたありませんが… orz)．
まだよくわかりませんが，Coq の証明図を，まるごと tex ファイルに変換したり，HTML や ps ファイルとして直接吐かせることもできるみたいです．もしかして，これってかなり凄いんじゃない !?
そのうち，論理系の論文の清書は，エディタ + latex じゃなくて， 直接 Coq などの定理証明器で検証しながら書くのがあたりまえの時代になるのかもしれませんね (笑) そうしたら，本や論文のミスも少なくなるかもしれません．
# 複雑な式を多用する，論理学の本などは，やたら typo やミスが多い．時に致命的な大ハマリにつながる場合もあるので，とても怖い．ミスをミスと見抜けない人に (論理学の自習は) 難しい．
ヒビルテ 2006-04-29 [Haskell] [quiz] (forall x. ((x->r)->r)->x) -> Either a (a->r)
問題の関数はこんな感じで定義できる。
notNotEM :: ((Either a (a->r)) -> r) -> r
notNotEM k = k (Right (\a -> k (Left a)))
dn2EM :: (forall x. ((x->r)->r)->x) -> Either a (a->r)
dn2EM dn = dn notNotEM
で、これが表しているのは何かだが……二重否定除去規則から排中律(The Law of excluded middle)を導く証明の計算的な表現だったりする。型はちょっと一般化してあるので、以下のようにより具体的な型にすると分かり易いかも。
data Absurd
type Not p = p -> Absurd
type Or = Either
notNotEM :: Not (Not (p `Or` Not p))
dn2EM :: (forall x. Not (Not x) -> x) -> p `Or` Not p
で、面倒なので詳しい説明は省略するが、例えばNK(自然演繹の体系NJに二重否定除去規則を追加した体系)で排中律を証明すると、この関数の構造を反映した証明図が得られる。
(省略)
他の体系での証明は誰かにまかせた。あろはさんはこの証明をCoqで表現してみると良い勉強になるかも。ついでに古典論理のうさんくささをもっと感じられるかもw
うほっ，いいトラックバック… ありがとうございます．
しかし，何を言っているのすら全然理解不能だぜ，ビバド低能な俺 ☆
とりあえず，Either ってのは，Haskell の言語仕様に組み込みのタグ付き型の一種で，静的強い型付けが強制される Haskell において，2 つの型のどっちかを返す関数を定義する時に使うらしいです．
まず Haskell がわからないから，脳が拒絶反応を起こしてしまう．
とりあえず，Coq 風の記法 + 自然演繹法のスタイルで，証明を書き直してみよう．
まず，非常に美しい体系 NJ (Natural Deduction for Intuitionistic logic) に，忌々しい二重否定除去規則 (Double Negation ; 以下 NNPP と略記) を加えましょう (笑)
構成的論理に基づく Coq のデフォルトでは，古典論理の排中律 (The Law of excluded middle ; EM) はもちろん，NNPP も使用することはできません．
ただし，Classical モジュールを明示的にインポートすると，NNPP を使用することができるようになります．
Coq < Require Import Classical.
Coq < Check NNPP.
NNPP
: forall p : Prop, ~ ~ p -> p
これまでの直観主義における自然演繹の体系に，NNPP を加えたこの体系を，NK (Natural deduction for classical logic) と呼ぶそうです．
ちなみに，K はドイツ語で，Kalkuel (計算) の意らしいです (J が何の略なのかはよくわかりません．無理矢理 Klassical Logic とか Jntuitionistic とか書いているサイトもありました w)．
# 美しいけどおもちゃに過ぎない体系ではなく，こっちは汚いけどモノホンの「計算」を扱ってんだ ！ っていう気迫が感じられますね．まぁ，どっちにしろ，自然演繹法自体が，直感的にはわかりやすいものの，あまり形式的には整理されていないため (一長一短なので，一概に悪いとは言えない)，シーケント計算の体系とかが本命になってくるのですが．
「二重否定は除去できる (¬ 除去)」 というのは，かなり強力な推論規則で，これと 「もし A と仮定して，*実際に矛盾を作ることができたら* ¬ A を書き加えても良い (¬ 導入)」 を組み合わせると，排中律 (P ∨ ¬ P) が証明できてしまいます．
まず，方針として，せっかく NNPP を手に入れたのですから，おそらく最後は ¬¬ (P ∨ ¬ P) の形に NNPP を apply して，EM を手に入れることになるのだろう，という目星を付けます．
.
.
.
~~ (P ∨ ~ P)
P \\/ ~ P (* ¬ 除去)
(* めでたしめでたし *)
# NNPP を使わないですむならば，NJ で十分 w
ということは，まず ¬ (P ∨ ¬ P) の形を仮定して，そこから矛盾を意図的に作って行く必要がある，という見当が付きます．
| ~ (P \\/ ~ P) (* 仮定 *)
| .
| .
| .
|
| 矛盾発生 ！！！ (contradiction)
~ ~ (P \\/ ~P) (* ¬ 導入 *)
P \\/ ~P (* ¬ 除去 *)
(* 王大人 EM 証明確認 *)
んで，上手く contradiction させるためには，(ここはわかりにくくて，混乱しがちですが) P ∨ ¬ P を，一段下がった仮定のスコープの中で導き出してやる必要があります．
はぁ ? P ∨ ¬ P を証明したくてやってきたのに，P ∨ ¬ P を使っちゃったら，循環論法にならなくね ? と，大人社会の体制の嘘臭さに敏感で血気盛んな若者達は思ってしまいがちですが，スコープが違うので問題は無いのです (このようにして上手く丸め込まれながら，青くさい少年ボーイは大人になっていくのです)．
プログラマならば，変数のスコープ (有効範囲規定) はお馴染だと思います．たとえ同じ名前，同じ形の変数名や式が出てきても，スコープが異なれば違うものなので，混乱しないでちゃんと区別しないといけないのです．ここをいい加減にしてしまうと，何でも導けてしまうため，何もかもがナンセンスになってしまいます．グローバル変数が危険なのと同じ理屈です．
基本的に，自然演繹法では，新たな仮定を付け加えるたびに，どんどん右に証明経路がずれていきます．そして，スコープは，現在の経路から見て左側のみになります．
すなわち，右側の，勝手に付け加えたローカルなスコープ内の仮定には，左側からはアクセスできません．ちゃんと勝手に付け加えた仮定を全てキャンセルして，左側にもどってこなければなりません．
というわけで，一段潜った部分で，P ∨ ¬ P の構成を試みていきましょう．
∨ を出す (∨ 導入) ためには，P か ¬ P のどちらかを出せば OK です．ここではとりあえず ¬ P を出すことにしましょう (どっちを選んでも，今回の場合は同じになる)．
¬ P を出すためには，さらにもう一段深く潜って，P を仮定して矛盾を作り， ¬ 導入して戻って来れば良さそうです．
| ~(P \\/ ~P)
| ------------
| | P
| | ----------
| | .
| | (* ここで，P から矛盾を作る *)
| | .
| | (* contradiction !!! *)
| ~P (* ¬ 導入 *)
| P \\/ ~P (* ∨ 導入 *)
~~ (P \\/ ~P) (* ¬ 導入 *)
P \\/ ~P (* ¬ 除去 *)
(* 勝った ! 第三部完 !! *)
一番最初とは異なり，左側の仮定は，全て自由に使うことができます．というか，使えるものは，どう考えても ~(P \\/ ~P) しかありません．んで，こいつをキャンセルするためには，P \\/ ~P を作れば，うは wwwww おk wwww です．
もちろん，P が仮定されているので，P \\/ ~P はトリビアルに成り立ちます．以上で，じっちゃんの名に賭けて，謎は全て解けた ！ QED です．
| ~(P \\/ ~P) (* 仮定 *)
| ------------
| | P (* 仮定 *)
| | ----------
| | ~(P \\/ ~P) (* 仮定より *)
| | P \\/ ~P (* P が仮定されているので，∨ 導入より構成 *)
| | (* おーっと坊や，捨て牌を良く見てみな． ~(P \\/ ~P)
| | があるじゃねぇか．contradiction だな．罰符 8000 両だ *)
| ~P (* ¬ 導入 *)
| P \\/ ~P (* ∨ 導入 *)
~~ (P \\/ ~P) (* ¬ 導入 *)
P \\/ ~P (* ¬ 除去 *)
(* わるいなぁ… そいつはロンだ． リーチ一発チートイ表表裏裏 24000 *)
あとはこいつを Coq で書き下せば良いだけなのですが… これは，次回と言うことで (笑)
まだようやく CoqIDE の使い方がわかってきたレベルの坊やなので… どんなコマンドや機能があるのかさえ，まだまださっぱり妖精です．
とりあえz，Linux の coqtop は，Windows と異なり，履歴などが遡れなくて不便なので，なるべく coqide を使った方が楽ですよ．
使い方は以外と簡単で，起動して，バッファにテキトーに何か書いて，後は上の方にある， ↓ を押せば，１行ずつ coqtop に入力してリターンを押したのと同じように，対話的にインタプリートしてくれます．
一度読みこまれた行は編集できなくなるので，バックトラックして編集したいときは，↑ ボタンで戻れます．また，→ ◯ で，カーソルが当たっている任意の位置に戻れます．
↓ を押せば，バッファを丸ごとバッチ処理できますし，
--
--
↑ を押せば，一番最初に戻ります．
やっぱり，IDE の方が，慣れればコマンドラインよりも便利だと思います (私は IDE とかの使い方を覚えるのが面倒で面倒でしかたありませんが… orz)．
まだよくわかりませんが，Coq の証明図を，まるごと tex ファイルに変換したり，HTML や ps ファイルとして直接吐かせることもできるみたいです．もしかして，これってかなり凄いんじゃない !?
そのうち，論理系の論文の清書は，エディタ + latex じゃなくて， 直接 Coq などの定理証明器で検証しながら書くのがあたりまえの時代になるのかもしれませんね (笑) そうしたら，本や論文のミスも少なくなるかもしれません．
# 複雑な式を多用する，論理学の本などは，やたら typo やミスが多い．時に致命的な大ハマリにつながる場合もあるので，とても怖い．ミスをミスと見抜けない人に (論理学の自習は) 難しい．
