単純型付きラムダ計算 | 数理論理

1 型、項、および文脈

基本型記号の空でない集合を $\mathsf{Base}$ とする。

定義 1.1. 単純型 (simple type) を次の規則で帰納的に定める。

A,B ::= \iota\mid A\to B \qquad(\iota\in\mathsf{Base}).

$A\to B\to C$ は $A\to(B\to C)$ と読む。型の大きさを

|\iota|=1,\qquad |A\to B|=1+|A|+|B|

と定める。

項の構文、自由変数、アルファ同値、および捕獲回避代入には、型なしラムダ計算で定義した§E15.8 定義 1.1、§E15.8 定義 2.2、§E15.8 定義 2.4を用いる。従って項は

M,N ::= x\mid\lambda x.M\mid MN

という構文をもち、束縛変数の名前だけが異なる項を同一視する。型注釈は項の構文には書かず、型は判断の導出が与える。この形式を Curry 形式という。

定義 1.2. 型付け文脈 (typing context) $\Gamma$ は、変数から単純型への有限部分関数である。 $x\notin\operatorname{dom}(\Gamma)$ のとき、 $\Gamma$ を $x:A$ で拡張した文脈を $\Gamma,x:A$ と書く。

判断 $\Gamma\vdash M:A$ を、次の規則から生成される有限導出木の存在として定める。

\frac{\Gamma(x)=A}{\Gamma\vdash x:A}(\mathrm{Var})

\frac{\Gamma,x:A\vdash M:B} {\Gamma\vdash\lambda x.M:A\to B}(\mathrm{Abs}) \qquad \frac{\Gamma\vdash M:A\to B\qquad\Gamma\vdash N:A} {\Gamma\vdash MN:B}(\mathrm{App}).

例 1.3 (恒等関数と合成). 任意の型 $A$ について

\varnothing\vdash\lambda x.x:A\to A

である。また、任意の型 $A,B,C$ について

\varnothing\vdash \lambda f.\lambda g.\lambda x.f(gx): (B\to C)\to(A\to B)\to A\to C

である。後者では、 $x:A$ から $gx:B$ を得て、 $f(gx):C$ を得た後、三つの仮定を逆順に抽象する。

2 文脈に関する補題

補題 2.1. $\Gamma\vdash M:A$ とする。 $\Delta$ が $\Gamma$ のすべての変数へ同じ型を割り当てるならば、 $\Delta\vdash M:A$ である。

証明. $\Gamma\vdash M:A$ の導出に関して帰納法を用いる。 $(\mathrm{Var})$ の場合、 $\Gamma(x)=A$ ならば仮定から $\Delta(x)=A$ である。 $(\mathrm{App})$ の場合は二つの直前の導出へ帰納法の仮定を適用する。 $(\mathrm{Abs})$ の場合、束縛変数を $\operatorname{dom}(\Delta)$ の外の新鮮な変数へアルファ変換してよい。拡張文脈も型の割当てを保つため、本体の導出へ帰納法の仮定を適用し、再び $(\mathrm{Abs})$ を用いる。▨

補題 2.2. $\Gamma,x:A\vdash M:B$ とし、 $z\notin\operatorname{dom}(\Gamma)\cup\operatorname{Var}(M)$ とする。このとき

\Gamma,z:A\vdash\rho_{x\to z}(M):B

である。特に、アルファ同値な項は同じ文脈で同じ型をもつ。

証明. 最初の主張を型付け導出に関して帰納的に示す。変数規則では、項が $x$ ならば改名後の $z$ に型 $A$ が割り当てられ、ほかの変数ならば $\Gamma$ の割当てが保存される。適用規則では二つの直前の導出へ帰納法の仮定を適用する。抽象規則では、内側の束縛変数が $x$ ならば自由変数の改名はその抽象で遮蔽される。束縛変数が $x$ と異なる場合は、必要ならば当該束縛変数をさらに新鮮な変数へ変更してから本体へ帰納法の仮定を適用する。

アルファ同値は、捕獲を起こさない束縛変数の改名と項文脈に関する閉包から生成される。上の改名結果を抽象規則で閉じ、適用と抽象の文脈について導出を持ち上げれば、各生成段階で型付けが保たれる。対称性と推移性を用いると、アルファ同値な任意の二項が同じ型をもつ。▨

型付け判断に現れない自由変数は存在しない。

補題 2.3. $\Gamma\vdash M:A$ ならば $\operatorname{FV}(M)\subseteq\operatorname{dom}(\Gamma)$ である。

証明. 型付け導出に関する帰納法を用いる。変数規則では定義から従う。適用規則では二つの自由変数集合の和を取る。抽象規則では、本体の自由変数から束縛変数を除き、 $\Gamma,x:B$ の定義域から $x$ を除けば $\operatorname{dom}(\Gamma)$ に含まれる。▨

3 型付き代入補題

定理 3.1 (型付き代入補題). $x\notin\operatorname{dom}(\Gamma)$ とする。

\Gamma,x:A\vdash M:B,\qquad \Gamma\vdash N:A

ならば

\Gamma\vdash M[x:=N]:B

である。代入は変数捕獲を避け、アルファ同値類上で行う。

証明方針は、 $\Gamma,x:A\vdash M:B$ の最後の型付け規則に関する帰納法である。抽象の場合には、束縛変数を $N$ の自由変数と文脈の定義域の外へ先に改名する。従って、代入は捕獲を起こさず抽象の本体へ入る。

証明. $\Gamma,x:A\vdash M:B$ の導出に関して帰納法を用いる。

最後が $(\mathrm{Var})$ であるとする。 $M=x$ ならば $B=A$ であり、 $M[x:=N]=N$ なので仮定 $\Gamma\vdash N:A$ から結論を得る。 $M=y\ne x$ ならば $(\Gamma,x:A)(y)=\Gamma(y)=B$ であり、 $M[x:=N]=y$ なので変数規則から $\Gamma\vdash y:B$ を得る。

最後が $(\mathrm{App})$ であるとする。このとき $M=M_1M_2$ であり、ある型 $C$ が存在して

\Gamma,x:A\vdash M_1:C\to B,\qquad \Gamma,x:A\vdash M_2:C

である。二つの導出へ帰納法の仮定を適用すると

\Gamma\vdash M_1[x:=N]:C\to B,\qquad \Gamma\vdash M_2[x:=N]:C

を得る。適用規則と代入の再帰式から $\Gamma\vdash(M_1M_2)[x:=N]:B$ である。

最後が $(\mathrm{Abs})$ であるとする。このとき $M=\lambda y.M_0$ 、 $B=C\to D$ であり、

\Gamma,x:A,y:C\vdash M_0:D \tag{1}

である。文脈の拡張では新しい変数だけを加えるため、(1) から $y\ne x$ および $y\notin\operatorname{dom}(\Gamma)$ が従う。さらに、補題 2.3により $\operatorname{FV}(N)\subseteq\operatorname{dom}(\Gamma)$ であるから、 $y\notin\operatorname{FV}(N)$ である。必要ならば補題 2.2により、 $y$ を

z\notin\operatorname{dom}(\Gamma)\cup\operatorname{Var}(M_0)\cup \operatorname{Var}(N)\cup\{x\}

へ改名することができる。改名後も同じ記号 $y$ を用いる。この代表元では捕獲回避代入が抽象の本体へ入り、

(\lambda y.M_0)[x:=N]=\lambda y.(M_0[x:=N])

である。帰納法の仮定を、文脈 $\Gamma,y:C$ と変数 $x$ に適用する。弱化により $\Gamma,y:C\vdash N:A$ であるため、

\Gamma,y:C\vdash M_0[x:=N]:D

を得る。抽象規則から

\Gamma\vdash\lambda y.(M_0[x:=N]):C\to D

となる。変数、適用、抽象のすべての場合について結論を得た。▨

4 ベータ簡約と型保存

一段ベータ簡約には、型なしラムダ計算で固定した§E15.8 定義 3.1を用いる。すなわち、基本縮約

(\lambda x.M)N\to_\beta M[x:=N]

を抽象の本体、適用の左項、および適用の右項を含むすべての項文脈について閉じる。特定の評価順序には限定しない。

補題 4.1. 次が成り立つ。

$\Gamma\vdash\lambda x.M:C$ ならば、ある型 $A,B$ が存在して $C=A\to B$ かつ $\Gamma,x:A\vdash M:B$ である。
$\Gamma\vdash MN:B$ ならば、ある型 $A$ が存在して $\Gamma\vdash M:A\to B$ かつ $\Gamma\vdash N:A$ である。

証明. 型付け導出の最後の規則を調べる。抽象を結論にもつ規則は $(\mathrm{Abs})$ だけであり、適用を結論にもつ規則は $(\mathrm{App})$ だけである。各規則の直前の判断を読み取ると主張を得る。▨

定理 4.2 (型保存定理).

\Gamma\vdash M:A,\qquad M\to_\beta M'

ならば

\Gamma\vdash M':A

である。

証明方針は、一段ベータ簡約の導出に関する帰納法である。根にあるβ基には型付けの反転と型付き代入補題を用いる。三つの文脈閉包規則には帰納法の仮定を適用し、同じ型付け規則で結論を再構成する。

証明. 基本縮約 $M=(\lambda x.P)N\to_\beta P[x:=N]=M'$ を考える。補題 4.1を二回用いると、ある型 $B$ が存在して

\Gamma,x:B\vdash P:A,\qquad \Gamma\vdash N:B

である。束縛変数 $x$ は $\operatorname{dom}(\Gamma)$ の外へアルファ変換してよい。定理 3.1により $\Gamma\vdash P[x:=N]:A$ を得る。

抽象文脈で $M=\lambda x.P$ 、 $M'=\lambda x.P'$ 、 $P\to_\beta P'$ とする。反転により $A=B\to C$ かつ $\Gamma,x:B\vdash P:C$ である。帰納法の仮定から $\Gamma,x:B\vdash P':C$ を得て、抽象規則から $\Gamma\vdash\lambda x.P':B\to C$ となる。

適用の左文脈で $M=PN$ 、 $M'=P'N$ 、 $P\to_\beta P'$ とする。反転により、ある型 $B$ が存在して $\Gamma\vdash P:B\to A$ かつ $\Gamma\vdash N:B$ である。帰納法の仮定から $\Gamma\vdash P':B\to A$ を得て、適用規則を用いる。

適用の右文脈で $M=PN$ 、 $M'=PN'$ 、 $N\to_\beta N'$ とする。反転により、ある型 $B$ が存在して $\Gamma\vdash P:B\to A$ かつ $\Gamma\vdash N:B$ である。帰納法の仮定から $\Gamma\vdash N':B$ を得て、適用規則を用いる。基本縮約と三つの文脈閉包規則を尽くしたため、任意の一段ベータ簡約が型を保存する。▨

5 型付けすることができない項

命題 5.1. 項 $\lambda x.xx$ には、単純型を付けることができない。従って

\Omega=(\lambda x.xx)(\lambda x.xx)

にも単純型を付けることができない。

証明. $\lambda x.xx$ に型が付くと仮定する。型付けの反転により、ある型 $A,B$ が存在して、文脈 $x:A$ の下で $xx:B$ が型付けされる。適用の反転により、ある型 $C$ が存在して

x:A\vdash x:C\to B,\qquad x:A\vdash x:C

である。変数規則から同じ変数 $x$ の型は $A$ なので、 $A=C\to B$ かつ $A=C$ である。従って $A=A\to B$ となる。しかし型の大きさについて

|A\to B|=1+|A|+|B|>|A|

であり、 $A=A\to B$ は不可能である。ゆえに $\lambda x.xx$ は型付け不能である。 $\Omega$ が型付け可能ならば、適用の反転によって左側の部分項 $\lambda x.xx$ も型付け可能になるため矛盾する。▨

型なしラムダ計算では $\Omega\to_\beta\Omega$ である。上の命題は、単純型がこの特定の自己適用を排除することを示す。ただし、本記事は型付け可能なすべての項について簡約が停止すると結論していない。

6 演習

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

$\varnothing\vdash\lambda f.\lambda x.fx:(A\to B)\to A\to B$ の導出木を書け。
型付き代入補題の抽象の場合に、束縛変数を $\operatorname{FV}(N)$ の外へ取る必要がある理由を述べよ。
型保存定理の基本縮約の場合に、反転補題から得る二つの判断を記せ。

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

1では、 $f:A\to B$ と $x:A$ から適用規則で $fx:B$ を得て、 $x$ と $f$ を順に抽象する。2では、 $N$ の自由変数が $\lambda y$ に捕獲されることを防ぎ、捕獲回避代入の再帰を本体へ適用するためである。3では、 $\Gamma,x:C\vdash P:A$ と $\Gamma\vdash N:C$ を挙げ、代入補題へ接続する。▨

7 境界と次の段階

本記事が証明した動的性質は、一段ベータ簡約に対する型保存だけである。閉項が値または簡約可能であるという進行定理、正規形の存在、弱正規化、および強正規化は扱っていない。型なしラムダ計算の Church–Rosser 性から型付き項の正規化を導くこともできない。後続の記事は、含意の自然演繹と本記事の型付け規則を対応させ、局所的なβ基の縮約だけを証明の迂回除去として解釈する。

§E16.27単純型付きラムダ計算