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}

3 導出と型付け導出の相互変換

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

定理 3.1 (含意断片の Curry–Howard 対応). 次が成り立つ。

$\pi$ が $\Gamma\vdash_{\to} A$ の導出ならば $\Gamma\vdash\lvert\pi\rvert:A$ は単純型付きラムダ計算の型付け判断として導出可能である。
$\mathcal D$ が単純型付きラムダ計算の型付け導出 $\Gamma\vdash M:A$ ならば、 $\Gamma\vdash_{\to}A$ の仮定ラベル付き自然演繹 $\pi_{\mathcal D}$ が存在して $\lvert\pi_{\mathcal D}\rvert\equiv_\alpha M$ となる。
仮定ラベル付き自然演繹の導出木と、単純型付きラムダ計算の型付け導出木は、アルファ同値を除いて相互に変換することができる。

対応は次の表で与えられる。

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

証明.主張 (1)を示す。 $\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$ である。三規則のすべてについて対応する型付け規則を得た。

主張 (2)を示す。 $\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)を示す。主張 (1)と主張 (2)の構成を比較する。各構成は、変数規則を仮定規則へ、抽象規則を含意導入へ、適用規則を含意除去へ写す。従って、一方の導出木へ二つの構成を順に適用すると、各節点で元と同じ規則が復元される。束縛変数と解除仮定のラベルは新鮮な名前へ変更される場合があるため、同一性はアルファ同値を除いて成り立つ。▨

例 3.2. 仮定 $x:A$ から $A$ を得て、 $x$ を解除すると $\vdash_{\to}A\to A$ となる。対応する証明項は

\lambda x.x:A\to A

である。

例 3.3. $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では、一つの局所的な迂回と一段のベータ簡約の対応が述べられる。任意の導出が有限回の迂回除去で正規形へ到達することや、任意の簡約列が停止することは主張していない。自然演繹の正規化と単純型付きラムダ計算の強正規化には、別の証明が必要である。

注意 5.4. 本記事の対応は含意断片だけに限定される。連言と積型、選言と和型、偽と空型の対応は扱っていない。

6 演習

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

$x:A,y:A\to B\vdash_{\to}B$ の自然演繹と対応する証明項を書け。
$(\lambda x.x)N\to_\beta N$ に対応する局所的な迂回を、仮定導出、含意導入、含意除去の順に記述せよ。
β 基を部分項として含まない項を β 正規形という。β 正規形の項は、ある $n,k\geq0$ 、変数 $x_1,\ldots,x_n,y$ 、および β 正規形の項 $N_1,\ldots,N_k$ を用いて $\lambda x_1.\cdots\lambda x_n.\,yN_1\cdots N_k$ と書くことができることを示せ。これを用いて、 $p\in P$ について $\varnothing\vdash M:p\to p$ を満たす β 正規形の項 $M$ は $\lambda x.x$ とアルファ同値であることを示し、 $\vdash_{\to}p\to p$ の導出で局所的な迂回を含まないものの証明項がすべて $\lambda x.x$ であることを結論せよ。

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

仮定 $y:A\to B$ と $x:A$ へ含意除去を適用し、証明項 $yx:B$ を得る。
仮定 $x:A$ から $A$ を得て $x$ を解除し $A\to A$ を導き、 $N:A$ の導出とともに含意除去を適用する。この迂回を除去すると、仮定 $x$ の出現が $N$ の導出で置換され、 $N:A$ の導出そのものが残る。
前半を項の構造帰納法で示す。変数 $y$ は $n=k=0$ の場合である。 $\lambda x.M_0$ が β 正規形ならば $M_0$ も β 正規形であり、帰納法の仮定により $M_0$ は表示した形をもつので、先頭に $\lambda x$ を加えればよい。 $PQ$ が β 正規形ならば $P$ と $Q$ も β 正規形である。 $P$ が抽象ならば $PQ$ 自身が β 基となるので、 $P$ は抽象でない。帰納法の仮定により $P=yN_1\cdots N_k$ （ $n=0$ ）であり、 $PQ=yN_1\cdots N_kQ$ は表示した形をもつ。

$\varnothing\vdash M:p\to p$ とし、 $M$ を β 正規形とする。 $M=\lambda x_1.\cdots\lambda x_n.\,yN_1\cdots N_k$ と書く。 $n=0$ ならば、§E19.27 補題 2.3により $y\in\operatorname{FV}(M)\subseteq\operatorname{dom}(\varnothing)$ となり矛盾するので、 $n\geq1$ である。§E19.27 補題 4.1 (1)により $p\to p=A\to B$ 、すなわち $A=B=p$ であり、 $x_1:p\vdash\lambda x_2.\cdots\lambda x_n.\,yN_1\cdots N_k:p$ である。 $n\geq2$ ならば同じ反転により $p$ が $\to$ の形の型となり矛盾するので、 $n=1$ である。§E19.27 補題 2.3により $y\in\{x_1\}$ 、すなわち $y=x_1$ であり、 $x_1$ の型は $p$ である。 $k\geq1$ ならば、§E19.27 補題 4.1 (2)を $k$ 回用いると $x_1$ が $\to$ の形の型をもつことになり、変数規則と矛盾する。よって $k=0$ であり、 $M=\lambda x_1.x_1\equiv_\alpha\lambda x.x$ である。

$\pi$ を $\vdash_{\to}p\to p$ の導出で局所的な迂回を含まないものとする。定理 5.2の逆向きの主張により、 $\lvert\pi\rvert$ に β 基があれば $\pi$ に含意導入の直後の含意除去が現れるので、 $\lvert\pi\rvert$ は β 正規形である。定理 3.1 (1)により $\varnothing\vdash\lvert\pi\rvert:p\to p$ であるから、前段により $\lvert\pi\rvert\equiv_\alpha\lambda x.x$ である。

▨

§E19.28Curry–Howard 対応

1 含意断片と仮定ラベル

2 証明項の抽出

3 導出と型付け導出の相互変換

4 証明の代入

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

6 演習

参考文献

前提記事