直観主義論理のカリー・ハワード対応

「A→B」というのは、Aの証明があったときにBの証明ができることをあらわす。

と解釈した。これをもっと構成的な言い方にすると

「A→B」というのは、Aの証明が与えられたときにBの証明を出力することができることをあらわす。

と読み替えられる。このように読み替えると命題「A→B」は何らかの関数(の存在)を表しているように見えてくる。そうすると、→除去則

$\frac{\large{\begin{array}{c} \vdots \\ A \end{array} } \qquad \large{\begin{array}{c} \vdots \\ A \to B \end{array} }}{\large{B}}$

は、関数に入力を与えて関数を呼び出している(関数適用をしている)ことを表しているように見える。
一方、→導入則

$\frac{\large{\begin{array}{c}[ A ]{}_{\small{1}} \\ \vdots \\ B \end{array}} }{\large{ A \to B}}\small{1}$

は、新しい関数が作られているので、関数抽象(ラムダ抽象)をやっているように見えてくる。
ここまで来ると、各命題は型を表していると考えるのが良いように思える。命題AはAという型を表し、命題A→Bは、A型の引数を取りB型を戻すような関数を表す型を表す、というように。
実際、型付きのラムダ計算と自然演繹の証明とを結びつけることができる。このような型(計算)と証明との対応関係をカリー・ハワード対応という。以下のように対応づけられる。

証明の各式に「項 : 型」の形の式を置く。項は型付きラムダ式で、型は論理式。
証明の始式には、「変数 : 型」の形の式を置く。これは、その型のデータが存在すると仮定してそれに対する変数を宣言している、と読むことができる。例えば「 $x^{\tiny{A}}\quad :A$ 」なら「A型のデータが存在すると仮定して、 $x^{\tiny{A}}$ をA型の変数とする」となる(変数には型を表す添字を付けているけど、以下では型を示す添字は適当に省略する)。

関数についての規則

→導入則は、関数抽象を表す規則になる。

$\frac{\large{\begin{array}{c}[x^{\tiny{A}}\quad : A ]{}_{\small{1}} \\ \vdots \qquad \\ t \qquad : B \end{array}} }{\large{\lambda x^{\tiny{A}} .t \qquad : A \to B}}\small{1}$

「xをA型と仮定してtがB型であることが示されたら、λx.tはA→B型である」ということを表している。例えば、次の証明
$\frac{\frac{\large{[ x^{\tiny{A}} \quad : A ]{\small{1}} }}{\large{x^{\tiny{A}} \quad : A }}}{\large{\lambda x^{\tiny{A}}. x^{\tiny{A}} \quad : A \to A }}\small{1}$
では、A→A型の項「 ${\lambda x^{\tiny{A}}. x^{\tiny{A}} }$ 」が導かれている。この証明は、項 ${\lambda x^{\tiny{A}}. x^{\tiny{A}} }$ がA→A型であることを証明していると読むこともできるし、A→A型のデータが存在することを証明してその型のデータの具体例を示していると読むこともできる。
一方、→の除去則は、関数適用を表す規則になる。

$\frac{\large{\begin{array}{c} \vdots \\ s \qquad : A \end{array} } \qquad \large{\begin{array}{c} \vdots \\ t \quad : A \to B \end{array} }}{\large{(t s) \quad : B}}$

直積型と直和型

含意が関数型に対応していたのと同様に、論理積は直積型に対応し、論理和は直和型に対応する。くわしい説明は略。
直積型はタプルだと思えば良い。

$\frac{\large{s \quad : A \qquad t \quad : B}}{\large{(s,t) \quad : A \wedge B}}$

$\frac{\large{\quad t \quad : A \wedge B}}{\large{{\rm fst}{}_{\tiny{A \wedge B}}\,t \quad : A}} \qquad \qquad \qquad \frac{\large{\quad t \quad : A \wedge B}}{\large{{\rm snd}{}_{\tiny{A \wedge B}}\,t \quad : B}}$

直和型は、複数の型をタグ付けして一つの型としてあつかう。あとでパターンマッチングで場合分けをして使う。

$\frac{\large{t \quad : A}}{\large{{\rm Left}{}_{\tiny{A \vee B}}\,t \quad : A \vee B }} \qquad \qquad \qquad \frac{\large{t \quad : B}}{\large{{\rm Right}{}_{\tiny{A \vee B}}\,t \quad : A \vee B }}$

$\frac{{\large{t \quad : A \vee B}} \qquad \large{\begin{array}{c}[ x \quad : A]_{\small{1}} \\ \vdots \quad \\ p \quad : C \end{array}} \qquad \large{\begin{array}{c}[ y \quad : B]_{\small{1}} \\ \vdots \quad \\ q \quad : C \end{array}}}{ \large{{\rm case\:} x {\:\rm of\;}{\rm Left}{}_{\tiny{A \vee B}} y => p \, | {\rm Right}{}_{\tiny{A \vee B}} z => q \quad : C} }\small{1}$

矛盾

矛盾 $\bot$ をどういう型と解釈するかだけど、これは実行が「その位置に戻ってこない」型だと考える。矛盾からは任意の命題が導けるという規則は、その位置に戻ってこないからその位置をどんな型にしても問題がないことを表していると解釈できる。

$\frac{\large{t \quad : \bot}}{(A)t \quad : A}$

ここではキャストみたいに「(A)」と書いたけど、省略しても文脈的にたぶんわかる。
¬Aは、A→ $\bot$ と同じなので、「A型の引数を受けとるけど、受け取ってそのまま戻ってこない関数」の型を表すことになる。

簡約(リダクション)と証明図の書きかえ

ラムダ計算では、(λx.t)sという項は、t[x←s]という項に書きかえられる(これをβ簡約という)。ただしここでt[x←s]というのは、項tの中にある自由変数xをsに置き換えるという操作を表す。これは関数が引数を受け取って実行を一ステップ進めることにあたる。
ところで、(λx.t)sという項は、次のような証明と対応している。
$\frac{{\large{\begin{array}{c}\vdots \quad \\ s \quad : A \end{array} } } \qquad \frac{\large{\begin{array}{c} [ x \quad : A ]{}_{\small{1}} \\ \vdots \quad \\ t \quad : B \end{array}}}{\large{\lambda x . t \quad : A \to B}}}{ \large{(\lambda x . t)s \quad :B }}\small{1}$

「直観主義論理の「自然さ」(2) シーケント計算」の「カットについて」のところで書いたように、
$\frac{\large{\begin{array}{c} \vdots \\ A \end{array} } \qquad \frac{\large{\begin{array}{c} [ A ]{}_{\small{1}} \\ \vdots \\ B \end{array}}}{\large{A \to B}}}{ \large{\begin{array}{c}B \\ \vdots \end{array} }}\small{1}$ という証明は、→導入則を使った直後に→除去則を使っているので、 $\large{\begin{array}{c} \vdots \\ A \\ \vdots \\ B \\ \vdots \end{array} }$ という証明に書きかえることができる。この書きかえを(λx.s)tの証明についておこなってみる。「x : A」という仮定を置いていたところを「s : A」の証明で置き換えるので、元の証明図で「x : A」から下で「x」だった部分が「s」で置き換わることになる。したがって次のような証明図に書き換わる。
$\large{\begin{array}{c} \vdots \quad \\ s \quad :A \\ \vdots \quad \\ t[x \leftarrow s ] \quad : A \to B \end{array}}$
最後に得られているのは、(λx.s)tをβ簡約して得られるt[x←s]という項である。つまり証明図から導入則・除去則の組を取り除くという書き換えが、型付きラムダ計算でのβ簡約に対応している。これは、直積型・直和型についても成り立つ(また除去則を使った直後に導入則を使う形の回り道の書き換えはη簡約に対応する)。

古典論理の場合

上で述べたように、直観主義論理の自然演繹と型付きラムダ計算との間には対応関係があった。では古典論理の場合はどうか。というと「Schemeでお馴染みのcall/ccを追加すると古典論理と対応関係ができる」といった話があるのだけど、なんでcall/ccとか継続が出てくるのかを考えるとややこしくなってくる。
(「call/ccと古典論理のカリー・ハワード対応」につづく)