排中律やPeirce's lawの挙動 - chiguriの生態（嘘や誇張アリ）

これは、Theorem Proving Advent Calendarの四日目の記事である。
ぱっと見ではあまりTheorem Provingらしくないかと思われるかもしれないが、たまにはこういう話もよいだろう、ということで。

お題

今回使う道具は、Curry-Howard同型対応、直観主義で失われる二重否定除去、そして栄光のcall/cc*1である。
ただ、これらの背景を説明すると滅茶苦茶に長くなるので、あとで解説用のスライドを作成しようと思う。
今回はこれらがわかっている前提で話を進める。

着眼点1：二重否定除去以外の規則群

直観主義論理と二重否定除去の組み合わせは古典論理と同じ計算能力を有する。
つまり、二重否定除去をつけると「直観主義論理で証明できなかったもの（のうち古典論理で正しいもの）が証明できる」こととなる。
また、同時にこれは逆が言える場合もあり、その規則を直観主義論理に付け加えると二重否定除去が導ける。
有名どころでは排中律（常に、命題Pは成り立つか、または成り立たないかのどちらかである）や、変なところでは*2Peirse's lawなどがある。
ちなみにPeirce's lawは((P -> Q) -> P) -> Pという論理式である。

着眼点2：二重否定除去とcall/ccの関係

これこそがCurry-Howard同型対応の本骨頂だろう。
これらはそれぞれ論理と関数という場所は違えど一対一の対応が取れるものなのである。
call/ccの型は、実際にみるとまるで二重否定除去のようになる。

内容：規則群は何と対応しますか？

ならば、排中律やPeirse's lawは何と対応するのだろうか？
どうやったらそれを見つけられるのだろうか？
これが今回のお話である。

Coqで項を作ろう

そうは言っても、むやみやたらにこんな項、なんていわれても（自他共に）無理があるので、Curry-Howard同型でcall/ccから作ってしまおう、という話である。
つまり、二重否定除去を使って排中律とPeirce's lawを証明し、その証明の項を元に動きを解釈しよう、ということだ。
というわけで、以下排中律とPeirce's lawの証明*3。
どこにでもある程度のものなので説明はしないが、Peirce's lawの証明は別の形として、最初に二重否定除去を使う方法もある。
だが、その場合項は複雑化するのでお勧めしない。

Variable dne : forall P : Prop, ~~P -> P.
Implicit Arguments dne [P].
Variable P : Prop.

Definition em : P \/ ~P.
apply dne; intro H; apply H.
 right; intro l; apply H.
  left; apply l.
Defined.

Variable Q : Prop.
Definition peirce : ((P -> Q) -> P) -> P.
intro H; apply dne.
 intro H0; apply H0.
  apply H; intro H1.
   destruct (H0 H1).
Defined.

あとは出力を見るだけ。ではそれぞれ見てみよう。

排中律の項

Printしてみよう。

> Print em.
em = 
dne
  (fun H : ~ (P \/ ~ P) =>
   H (or_intror P (fun l : P => H (or_introl (~ P) l))))
     : P \/ ~ P

さすがにいろいろ型があって読みづらい。
少しOCaml風に直してみよう。
あくまで擬似コードなので、こんなの書けない、といわれても困る。

type a (* declaration *)
type 'a not (* declaration *)
type 'a or = Left of 'a | Right of 'a not
val dne : ('a not) not -> 'a

let em = dne (fun k ->
                k (Right (fun x -> k (Left x))))

ほう、なんとも奇妙な項だ。
ちなみに'a notは'aの値をとってどこかへ飛んでいく継続の型である。
kの型は(a or) notである。aの値かaをとる継続（と同じ型の値）をとる継続。わかりにくい。
さて、動きを確かめよう。

emを作ると、最初の（左側の）kによって、Right (fun x -> k (Left x))が返される。
パターンマッチで展開すると、Rightなので、aの値をとる関数が出てくる。
こいつにaの値tを入れると、Leftにtを包んで（orにして）継続kを呼び出す。
emを定義した場所の値がLeft tになる。
次にパターンマッチをするとtが出てくる。

はて。なんのこっちゃ。
何かに使えないかと思ったが、結局思いつかず断念。
世界全体がtを知らなかった世界にtを持ち込むようなものなのだが・・・

と思ったら5年半前にさかいさんがこれに関するblogを書いていた。
今気づくとは・・・

Peirce's lawの項

気を取り直して、ではPeirce's lawに移ろう。

peirce = 
fun H : (P -> Q) -> P =>
dne
  (fun H0 : ~ P =>
   H0 (H (fun H1 : P => let f := H0 H1 in match f return Q with
                                          end)))
     : ((P -> Q) -> P) -> P

やはり読めないので、OCaml風に。

type a (* declaration *)
type b (* declaration *)
type 'a not (* declaration *)
val dne : ('a not) not -> 'a

let peirce cl = dne (fun k ->
                      k (cl (fun t -> match k t with (* nothing returned *))))

何か、引っかかるものがある。が、とりあえず動きを追おう。

peirceは一引数をとる関数である。この引数をclとしよう。これは関数であり、「aの値tを受け取るとbの値を返す・・・ことを期待された関数」を受け取る。
peirceの呼び出しの結果、clに対して関数の適用が行われた結果が（渡された継続kによって）返される。
clに適用される関数は、bを返すといいながら何も返してない。が、aの値tが「継続で」返されるので、つまり「大丈夫だ、問題ない」。どうせこの処理は終わる。かわいそうに無視されてしまう型b。

clは何かを処理する関数・・・で、たとえば渡された関数を使わないと、普通に値が返される（継続で飛ぶとはいえ、見かけ上は普通に返すのと同じ）。
渡された関数を使うと、その結果が返ってくる。
・・・これ、なんてcall/cc？

call/ccの型

まずはじめに。

最初に二重否定除去とcall/ccの型は対応すると書いたな、あれはウソだ。

否定を継続による大域ジャンプによる結果としてみた場合、二重否定除去に対応する値dneは以下のような挙動を示す。

一引数clをとる。
clはaの値をとる継続を渡される。当然そこにaの値を渡すとdneの呼ばれた場所へ飛んでいく。
clは値を返してはならない。なぜならclの型はa not notであり、cl自身が、何らかの形で大域ジャンプを果たす必要がある。

一方、call/ccは普通に値を返していい。これはおかしい。
ここを考慮したうえで、実際にcall/ccの型を考えてみる。

一引数clをとる。
clはaの値をとる継続を渡される。そこにaの値を渡すとcall/ccの呼ばれた場所に飛んでいく。
clはaの値を返していい。その場合、返した値はcall/ccを呼んだ結果になる。

型はどうなるか。

val cl : 'a not -> 'a
val call/cc : ('a not -> 'a) -> 'a

notを'a->bottom（falsehood）だと思うことにすると、

val call/cc : (('a -> bottom) -> 'a) -> 'a

これはPeirce's lawのb=bottomのときである。
つまり、call/ccと本当に対応するのは二重否定除去規則ではなく、Peirce's lawだったということである。
でもかわいそうなbは置いていくように。

今日のまとめ

call/ccのつもりで進めていたら、本物のcall/ccが出てきやがった。
何を言ってるのかわからねえと思うが(ry

おまけ

このcall/ccだが、実際Coq上でcall/ccから二重否定除去規則は導ける。そのくらい強い。
以下が証明である。

Variable call_cc : forall P : Prop, (~P -> P) -> P.
Variable P : Prop.
Definition dne : ~~P -> P.
intro H; apply call_cc.
intro H0; destruct H.
apply H0.
Defined.

OCaml風の翻訳結果は以下の通り。

type a (* declaration *)
type 'a not (* declaration *)
val call_cc : ('a not -> 'a) -> 'a

let dne cl = call_cc (fun k
                       match cl k with (* nothing returned *))

つまり、絶対普通には戻ってこないでkで飛ぶ、という制限をかけたものがdneでありました、と。
shift/resetには（call/ccよりむしろ）こちらの方が近く見えるけど、気のせいかな？*4

*1:正式にはcall-with-current-continuation

*2:というと指導教員に怒られそうだが。

*3:dneはdouble negation elimination、emはexcluded middleの略。

*4:絶対に継続を呼ぶと決まっているため、スタックを残す必要がない。shift/resetも必ずスタックから一度消す。