排中律の証明ってどんなプログラム？

はじめに

ある日研究室にいたら助教からこんなことを言われました。
助教：「カリーハワード同型対応って知ってるよね？　排中律を導く証明ってどういうプログラムに対応すると思う？」
私：「...」

カリーハワード同型対応

詳しく説明していると、これだけで何本分かの記事になってしまうので、詳しくは説明しませんが、命題をプログラムの型に対応づけられるというものです。

論理	記号	型	プログラム(TypeScript)
含意(AならばB)	A → B	A → B	(a: A) => B
連言	A ∧ B	A × B (直積)	{ a: A; b: B }
選言	A ∨ B	A ＋ B (直和)	{ tag: "left"; value: A } | { tag: "right"; value: B }
矛盾	⊥	⊥(値が1つもない型)	never
否定	¬A	A → ⊥	(a: A) => never

この対応表に基づいて、命題論理をプログラムの世界の型に対応づけようというものです。最近話題のLeanやRocqなどの定理証明支援系もこの対応関係を利用したものです。

ところで、今表に載っているのは直観主義命題論理の対応関係です。
これは古典論理の対応関係から、「二重否定除去」or「排中律」を除いたものです。

二重否定除去とは¬¬A → Aという命題で、排中律とはA ∨ ¬Aという規則です。どちらも直観主義命題論理では証明することができません。しかし、直観主義命題論理にどちらか片方を加えると、もう片方も証明できるようになります。つまり、二重否定除去と排中律は同値です。

ここでもう一つこれらの規則と同値な規則を紹介します。それがPeirceの法則です。これは((A → B) → A) → Aという規則です。
実はこれらの規則の中でプログラムの世界で対応するものが綺麗に存在するのは、Peirceの法則なので、Peirceの法則について詳しく説明します。

Peirceの法則

まずは、直観主義論理＋Peirceの法則((A → B) → A) → Aを元にして排中律 A ∨ ¬Aを証明してみようと思います。

左側の証明で導入しているのがPeirceの法則で、AをP ∨ ¬P、Bを⊥にしたものです。

助教に出された問題は排中律を証明するプログラムを書けとのことだったので、あとはこの証明をカリーハワード同型対応によってプログラムの世界に持って行きたいのですが、まだわかっていないことがあります。
それはPeirceの法則がプログラムの世界では何に対応するのかということです。型と→で構成されているので何らかの関数ではあるのですが、これは一体どんな関数なんでしょうか？

継続渡しスタイル(CPS)

それにはCPSというものを知る必要があります。
これは継続というのがキーワードになります。あまり聞き馴染みがないかもしれませんが、知らず知らずのうちに使っている機能です。
例えば、JavaScriptのPromiseです。Promiseの実行が終わったら、thenの中の計算を実行するといったコードをかけます。ここでいうthenの中の処理が継続です。
継続とは「ある式の値が決まったあとに、残っている計算全部」のことです。

継続の例

function addCPS(a: number, b: number, k: (r: number) => void): void {
    k(a + b);  // a+bをした後に継続kを実行する
}
function mulCPS(a: number, b: number, k: (r: number) => void): void { 
    k(a * b);  // a*bをした後に継続kを実行する
}

addCPS(1, 2, (s) =>          // 継続:「s に 3 を掛けて表示する」
  mulCPS(s, 3, (r) =>        // 継続: 「r を表示する」
    console.log(r)));        // 9

継続を使わない例

function add(a: number, b: number): number { return a + b; }
function mul(a: number, b: number): number { return a * b; }

console.log(mul(add(1, 2), 3)); // 9

この二つは等価な処理を行なっていますが、継続を関数の引数に渡すようなプログラミングのスタイルのことを継続渡しスタイル(Continuation-Passing Style、以降CPS)と言います。

call/cc

このようなCPSの書き方はPromiseのthenチェーンのように長くなってしまい、毎回継続を書き出すのはとても面倒です。そこで、勝手にプログラム全体の継続を取り出すことができないか？　というのがこのcall/ccになります。
call/ccがサポートされているSchemeで実例を見て見ましょう。先ほどの例をSchemeで書いてみます。

先ほどの足し算と掛け算の例

(define (addCPS a b)
  (call/cc
    (lambda (k)
      (k (+ a b))  ; a+bをした後に継続kを実行する
    )
  )
)
(define (mulCPS a b)
  (call/cc
    (lambda (k)
      (k (* a b))  ; a*bをした後に継続kを実行する
    )
  )
)
(display (mulCPS 3 (addCPS 1 2)))  ; 9
(newline)

Schemeでは(define (名前 引数1 引数2 ...)本体)で関数を定義することができます。
また、(lambda (引数1 引数2 ...)本体)は無名関数になります。
この例ではaddCPS関数はa,bを受け取ると、call/ccによってその後の計算が継続kに束縛され、a+bを計算した後にkが呼び出されるという形になっています。

この書き方だとプログラマが継続を明示的に書かずとも勝手にcall/ccが継続をkに代入してくれるので、通常のスタイルでプログラムを書くことができます。
最後の呼び出しの部分はTypeScriptのconsole.log(mul(add(1, 2), 3));と同じですよね？

ここで、call/ccの型を考えて見ましょう。

1. call/ccは、継続を受け取る関数bodyを受け取り、値を返します。型をA → Bと置きます。
2. bodyは継続を受け取る関数なので、A = C → Dとしましょう。
3. 継続は呼ばないで終わると、bodyの戻り値の型がそのまま返るのでB = Dです。
4. 継続Cも一引数の関数なのでC = E → Fです。
5. 継続Cに渡した値はcall/ccの戻り値にもなる必要があるので、E = Bです。
   これを整理すると次のような型になります。

call/cc : ((B → F) → B) → B

これは前の章で出てきたPeirceの法則((A → B) → A) → Aと同じ形です。
なので、Peirceの法則をcall/ccに対応づければ排中律の証明をプログラムの世界に持っていくことができます。

TypeScriptで書いてみる

まずは簡単なところから始めましょう。¬Pとなる型とP | Qとなる型を定義します。
Either<P,Q>は左と右を区別できるようにラベルを付与しています。Left関数は左側だけを返す関数で、Right関数はその逆です。

type Not<P> = (t:P) => never;

type Either<P, Q> = { type: "left"; value: P } | { type: "right"; value: Q }

function Left<P>(value: P): Either<P, never> {
    return { type: "left", value };
}
function Right<Q>(value: Q): Either<never, Q> {
    return { type: "right", value };
}

これを元にして排中律の証明をプログラムにすると次のようになります。
callccはTypeScriptでは直接は存在しない関数なので、一旦型だけを書いて中身の実装を空にしています。

function callcc<P, Q>(callback: (cont: (ret: P) => Q) => P): P {
    throw new Error("callcc is not implemented yet");
}

function excludedMiddle<P>(): Either<P, Not<P>> {
    function cont (func : (p: Either<P, Not<P>>) => never): Either<P, Not<P>> {
        return Right((k:P) => {return func(Left(k));})
    }

    return callcc(cont);
}

少しづつ考えて行きましょう。
まずcallcc<P,Q>は先ほど説明したcall/ccの型をそのまま書いただけなので良いでしょう。問題はexcludedMiddle<P>の方です。

一番内側にはこのような式があります。

Right((k:P) => {return func(Left(k));})

よーく目を凝らして見てみると、これは次の証明木に対応しています。

Left(k)が$[P]^2$に対応していて、func()が$[(P \lor \lnot P) \to \bot]^1$に対応しているので、return func(Left(k));は$\bot$に対応します。
そうすると(k:P) => return func(Left(k));は$\lnot P$(=$P\to \bot$)になります。
あとはRightで周りを囲めば出来上がりです。

ここがわかってしまえば、あとは明らかでしょう。

Schemeで書き直す

上のコードでTypeScriptの型チェックが通ります。つまり証明としては正しいということがわかりました。
それではこれをcall/ccが存在するような言語で書き下して見ましょう。今回はSchemeを用います。意外とcall/ccをそのまま対応している言語ってなかなか無いんです...

これが先ほどのTypeScriptをそのままSchemeに変換したものになります。

(define left (lambda (value) (cons 'left value)))
(define right (lambda (value) (cons 'right value)))

(define (either e on-left on-right)
  (cond
    ((eq? (car e) 'left) (on-left (cdr e)))
    ((eq? (car e) 'right) (on-right (cdr e)))
    (else (error "Invalid either value"))))

(define (excluded-middle)
    (call/cc
        (lambda (k)
            (right (lambda (p) (k (left p))))
        )
    )
)

(define left (lambda (value) (cons 'left value)))
(define right (lambda (value) (cons 'right value)))

この最初の2行がLeft関数とRight関数に対応しています。cons 'left valueというのは'leftとvalueによるLinked Listを作るという意味です。Schemeでは'leftはleftというシンボル(記号)を意味します。

(define (either e on-left on-right)
  (cond
    ((eq? (car e) 'left) (on-left (cdr e)))
    ((eq? (car e) 'right) (on-right (cdr e)))
    (else (error "Invalid either value"))))

次にここの部分は、eを受け取ると、それが'leftなのか'rightなのかを判別に、続きの処理(継続)を実行するというものです。Schemeは動的型付け言語でパターンマッチのようなものがないのでこのように書いてます。

carというのはlistの先頭を抜き出す関数で、cdrはlistの先頭以降を返すような関数です。

(define (excluded-middle)
    (call/cc
        (lambda (k)
            (right (lambda (p) (k (left p))))
        )
    )
)

最後にこの部分はTypeScriptで書いた関数と同じで、excluded-middle関数を定義しています。
Schemeでは関数呼び出しは(関数名 引数)で呼び出します。また、lambda (引数) (本体)で無名関数を定義することができます。

これは一体どんなプログラムなのでしょうか。試しに次のようなコードを実行して見ましょう。

(define left (lambda (value) (cons 'left value)))
(define right (lambda (value) (cons 'right value)))

(define (either e on-left on-right)
  (cond
    ((eq? (car e) 'left) (on-left (cdr e)))
    ((eq? (car e) 'right) (on-right (cdr e)))
    (else (error "Invalid either value"))))

(define (excluded-middle)
    (call/cc
        (lambda (k)
            (right (lambda (p) (k (left p))))
        )
    )
)

(let ((number-or-not-number (excluded-middle)))
  (either number-or-not-number
          (lambda (n)
            (display "number: ")
            (display n)
            (newline))
          (lambda (not-n)
            (display "not number")
            (newline)
            (not-n 42))))

実行結果

not number
number: 42

まず、Schemeのletは次のように変数を式の評価結果で束縛し、本体を評価するというものです。

let文法

(let ((変数1 式1)
      (変数2 式2))
  本体)

either関数にexcluded-middleの評価結果を渡し、その結果がleftなのかrightなのかで分岐をし、出力を行うというプログラムです。
すると奇妙なことにnot numberとnumber:42のどちらもが表示されました。

それではこのプログラムの実行を追って見ましょう

1. number-or-not-numberが(excluded-middle)の評価値に束縛されます。この時、excluded-middle関数ではこの後の計算(eitherの方の処理)が継続としてkに代入され、評価値として (right (lambda (p) (k (left p))))を返します。
2. number-or-not-numberがeither関数に渡されると、これはrightなので、(lambda (not-n) ...)の方の処理が実行されます。
3. (diplay "not number")で表示をした後に(not-n 42)が実行されます。これは(lambda (p) (k (left p))に42が渡されるということです。
4. 42が渡され、(k (left 42))を実行します。
5. kは先ほどの捕捉した継続で、あの時点に戻ります。つまり、number-or-not-numberに(left 42)が束縛されて、今度は(lambda (n)...)の処理が実行されます。

このように排中律をプログラムで再現すると「とりあえず適当に右を返して、違うと言われたらやっぱり左でしたと処理をやり直す」いい加減なプログラムを書くことができました。

終わりに

最後まで読んでくださりありがとうございました。
継続呼び出しっていうのはPromiseやAsync、 Await、generatorなど色々なところで実は使われているんですが、その核となるのはcall/ccという継続を取り出す機能です。
これがあるといろんなことが書けて楽しいので、是非もっと面白いプログラムを作って行きましょう。
もし誤植があったら教えてください🙇

参考記事