Curry–Howard 対応 | 数理論理 | 天游ヶ丘数理学院

1 含意断片と仮定ラベル

命題変数の集合を $P$ とし、含意断片の論理式を

A,B ::= p\mid A\to B \qquad(p\in P)

によって定める。同じ集合 $P$ を単純型付きラムダ計算の基本型記号の集合として用い、論理式 $A$ と単純型 $A$ を同じ帰納的構文で表す。

定義 1.1. 仮定文脈 (assumption context) $\Gamma$ は、変数から含意断片の論理式への有限部分関数である。判断 $\Gamma\vdash_{\to} A$ を、次の三規則から生成される有限導出木とする。

\frac{\Gamma(x)=A}{\Gamma\vdash_{\to} A}(\mathrm{Hyp}_x)

\frac{\Gamma,x:A\vdash_{\to} B} {\Gamma\vdash_{\to} A\to B}(\to I_x) \qquad \frac{\Gamma\vdash_{\to} A\to B\qquad \Gamma\vdash_{\to} A} {\Gamma\vdash_{\to} B}(\to E).

導出木の各仮定出現には、その仮定を表す変数ラベルを付ける。 $(\to I_x)$ はラベル $x$ の仮定出現を解除する。束縛された仮定ラベルの名前だけが異なる導出をアルファ同値とみなす。

通常の含意断片の自然演繹は、同じ論理式を複数回仮定することを許す。仮定ラベルによって出現を区別すれば、どの導入規則がどの仮定を解除するかが明確になる。文脈を有限部分関数としたことは、解除されるラベルを新鮮に選ぶ規約であり、論理式そのものの重複を禁じない。

2 導出から証明項を作る

定義 2.1. 仮定ラベル付き導出 $\pi$ の証明項 (proof term) $\lvert\pi\rvert$ を、最後の規則に関して次のように定める。

\begin{aligned} \lvert\mathrm{Hyp}_x\rvert&=x,\\ \left\lvert\frac{\pi}{A\to B}(\to I_x)\right\rvert &=\lambda x.\lvert\pi\rvert,\\ \left\lvert\frac{\pi\qquad\rho}{B}(\to E)\right\rvert &=\lvert\pi\rvert\,\lvert\rho\rvert. \end{aligned}

定理 2.2. $\pi$ が $\Gamma\vdash_{\to} A$ の導出ならば

\Gamma\vdash\lvert\pi\rvert:A

は単純型付きラムダ計算の型付け判断として導出可能である。

証明. $\pi$ の導出木に関して帰納法を用いる。最後が $(\mathrm{Hyp}_x)$ ならば $\Gamma(x)=A$ であり、型付けの変数規則から $\Gamma\vdash x:A$ である。

最後が $(\to I_x)$ ならば、直前の導出は $\Gamma,x:A\vdash_{\to} B$ である。帰納法の仮定から $\Gamma,x:A\vdash\lvert\pi_0\rvert:B$ を得る。型付けの抽象規則により

\Gamma\vdash\lambda x.\lvert\pi_0\rvert:A\to B

である。

最後が $(\to E)$ ならば、直前の二導出に対する帰納法の仮定から

\Gamma\vdash\lvert\pi_1\rvert:A\to B,\qquad \Gamma\vdash\lvert\pi_2\rvert:A

を得る。型付けの適用規則から $\Gamma\vdash\lvert\pi_1\rvert\lvert\pi_2\rvert:B$ である。三規則のすべてについて対応する型付け規則を得た。▨

3 型付けから導出を復元する

型付け規則は、仮定ラベル付き自然演繹の三規則と同じ木構造をもつ。

定理 3.1. $\mathcal D$ が単純型付きラムダ計算の型付け導出

\Gamma\vdash M:A

ならば、 $\Gamma\vdash_{\to}A$ の仮定ラベル付き自然演繹 $\pi_{\mathcal D}$ が存在して

\lvert\pi_{\mathcal D}\rvert\equiv_\alpha M

となる。

証明. $\mathcal D$ の最後の型付け規則に関して帰納法を用いる。

変数規則の場合、 $M=x$ かつ $\Gamma(x)=A$ である。自然演繹の $(\mathrm{Hyp}_x)$ を用いると、証明項は $x$ になる。

抽象規則の場合、 $M=\lambda x.N$ 、 $A=B\to C$ であり、直前の導出は $\Gamma,x:B\vdash N:C$ である。帰納法の仮定から $\Gamma,x:B\vdash_{\to}C$ の導出 $\pi$ を得る。 $(\to I_x)$ を適用すると $\Gamma\vdash_{\to}B\to C$ を得て、その証明項は $\lambda x.\lvert\pi\rvert\equiv_\alpha\lambda x.N$ である。

適用規則の場合、 $M=PQ$ であり、ある型 $B$ が存在して

\Gamma\vdash P:B\to A,\qquad \Gamma\vdash Q:B

である。二つの直前の導出へ帰納法の仮定を適用し、得られた自然演繹へ $(\to E)$ を適用する。証明項は、アルファ同値を除いて $PQ$ である。三つの型付け規則を尽くしたため結論を得る。▨

系 3.2 (含意断片の Curry–Howard 対応). 仮定ラベル付き自然演繹の導出木と、単純型付きラムダ計算の型付け導出木は、アルファ同値を除いて相互に変換することができる。対応は次の表で与えられる。

論理	ラムダ計算
仮定 $x:A$	変数 $x:A$
含意導入	ラムダ抽象
含意除去	関数適用
命題 $A$	型 $A$
$A$ の導出	型 $A$ の項

証明.定理 2.2と定理 3.1の構成を比較する。各構成は、変数規則を仮定規則へ、抽象規則を含意導入へ、適用規則を含意除去へ写す。従って、一方の導出木へ二つの構成を順に適用すると、各節点で元と同じ規則が復元される。束縛変数と解除仮定のラベルは新鮮な名前へ変更される場合があるため、同一性はアルファ同値を除いて成り立つ。▨

例 3.3 (恒等命題の証明項). 仮定 $x:A$ から $A$ を得て、 $x$ を解除すると $\vdash_{\to}A\to A$ となる。対応する証明項は

\lambda x.x:A\to A

である。

例 3.4 (含意の合成). $f:B\to C$ 、 $g:A\to B$ 、 $x:A$ を仮定する。含意除去を二回用いると $gx:B$ と $f(gx):C$ を得る。三つの仮定を解除すると

\vdash_{\to}(B\to C)\to(A\to B)\to A\to C

を得る。対応する項は $\lambda f.\lambda g.\lambda x.f(gx)$ である。

4 証明の代入

含意導入で解除する仮定を、別の導出によって置き換える操作を定義する。ラムダ項側では捕獲回避代入が同じ役割を担う。

補題 4.1. $\pi$ が $\Gamma,x:A\vdash_{\to}B$ の導出であり、 $\rho$ が $\Gamma\vdash_{\to}A$ の導出であるとする。 $\pi$ に現れるラベル $x$ の未解除仮定を $\rho$ で置き換えると、 $\Gamma\vdash_{\to}B$ の導出 $\pi[x:=\rho]$ が存在し、

\lvert\pi[x:=\rho]\rvert \equiv_\alpha \lvert\pi\rvert[x:=\lvert\rho\rvert]

である。

証明. $\pi$ の最後の規則に関して帰納法を用いる。最後が仮定規則でラベルが $x$ ならば、導出全体を $\rho$ で置き換える。証明項の両辺は $\lvert\rho\rvert$ である。別の仮定ラベルならば導出を変更せず、証明項の代入も当該変数を変更しない。

最後が含意除去ならば、二つの直前の導出へ帰納法の仮定を適用し、得られた二導出へ再び含意除去を適用する。証明項の等式は、適用に対する代入の再帰式から従う。

最後が $(\to I_y)$ ならば、 $y$ を $\lvert\rho\rvert$ の自由変数、 $\Gamma$ の定義域および $x$ の外へ改名する。この代表元では $y\ne x$ であるため、直前の導出へ帰納法の仮定を適用し、再び $(\to I_y)$ を用いる。証明項側でも、捕獲回避代入は抽象の本体へ入る。従って、すべての規則で導出の置換と証明項の捕獲回避代入が一致する。▨

5 局所的な迂回とベータ簡約

含意を導入した直後に同じ含意を除去すると、導入で一時的に置いた仮定を、除去に用いた証明で直接置き換えることができる。

定義 5.1. 次の形の導出を考える。

\frac{ \dfrac{\pi}{\Gamma,x:A\vdash_{\to}B} \ (\to I_x) \quad \dfrac{\rho}{\Gamma\vdash_{\to}A} }{\Gamma\vdash_{\to}B}(\to E).

この導出を、補題 4.1が与える $\pi[x:=\rho]$ へ置き換える操作を、含意の局所的な迂回除去 (local detour reduction) という。導出木の任意の部分木で同じ置換を許す。

定理 5.2. 含意の局所的な迂回除去を一回行う前後の導出を $\mathcal D,\mathcal D'$ とする。このとき

\lvert\mathcal D\rvert\to_\beta\lvert\mathcal D'\rvert

である。逆に、型付け導出の証明項に現れるβ基は、対応する自然演繹導出における含意導入の直後の含意除去を表し、そのβ基の縮約は局所的な迂回除去に対応する。

証明. 根にある局所的迂回の証明項は、証明項抽出の定義から

(\lambda x.\lvert\pi\rvert)\lvert\rho\rvert

である。ベータ簡約の基本規則と補題 4.1により

(\lambda x.\lvert\pi\rvert)\lvert\rho\rvert \to_\beta \lvert\pi\rvert[x:=\lvert\rho\rvert] \equiv_\alpha \lvert\pi[x:=\rho]\rvert

となる。

迂回が導出木の内部にある場合、証明項では対応するβ基が抽象の本体、適用の左項、または適用の右項の内部にある。ベータ簡約は全項文脈について閉じているため、同じ一段簡約を項全体へ持ち上げることができる。

逆向きを示す。型付け可能なβ基 $(\lambda x.M)N$ の型付け導出を反転すると、左項の最後の規則は抽象規則であり、項全体の最後の規則は適用規則である。対応する自然演繹では、前者が $(\to I_x)$ 、後者が $(\to E)$ なので、含意導入の直後に同じ含意を除去している。縮約後の $M[x:=N]$ は導出の代入が与える証明項である。従って両方向の局所対応が成り立つ。▨

注意 5.3 (局所対応から正規化は従わない).定理 5.2は、一つの局所的な迂回と一段のベータ簡約の対応を述べる。任意の導出が有限回の迂回除去で正規形へ到達することや、任意の簡約列が停止することは主張していない。自然演繹の正規化と単純型付きラムダ計算の強正規化には、別の証明が必要である。

6 演習

問題 6.1. 次の問いに答えよ。

$x:A,y:A\to B\vdash_{\to}B$ の自然演繹と対応する証明項を書け。
$(\lambda x.x)N\to_\beta N$ に対応する局所的な迂回を、仮定導出、含意導入、含意除去の順に記述せよ。
定理 5.2だけでは強正規化を結論することができない理由を述べよ。

解答 (確認問題の解答).

1では、仮定 $y:A\to B$ と $x:A$ へ含意除去を適用し、証明項 $yx:B$ を得る。2では、仮定 $x:A$ から $A$ を得て $x$ を解除し $A\to A$ を導き、 $N:A$ の導出へ適用した後、仮定 $x$ の出現を $N$ の導出で置換する。3では、定理が各β基の一段対応だけを示し、すべての簡約列の有限性や正規形の存在を証明していないことを述べる。▨

7 境界と次の段階

本記事の対応は含意断片だけに限定される。連言と積型、選言と和型、偽と空型の対応は扱っていない。また、局所的な迂回除去を定義して一段対応を証明したが、自然演繹の正規化、ラムダ項の正規化、および強正規化は扱っていない。これらの結果は証明論で別に証明される。

§E16.28Curry–Howard 対応

1 含意断片と仮定ラベル

2 導出から証明項を作る

3 型付けから導出を復元する

4 証明の代入

5 局所的な迂回とベータ簡約

6 演習

7 境界と次の段階

参考文献

前提記事