型付きラムダ計算について。
型と構文規則
われわれは、型 (type) の概念をあくまでプリミティブなものとして扱う。 つまり、ここでは型は、（たとえば集合や命題などの）別の何かによってそれ以上解明されることのないものと理解される。
定義 (型)
(1) 記号の集合は、以下のように与えられるとする：
- $T$：変数記号の集合
- $\to$：補助記号
(2) 型 (type) の集合 $\tau(T)$ を以下のように帰納的に定義する：
- 基底型$t \in T$ は型である。
- $A, B$ が型であるならば、$A \to B$ も型である。
BNF記法で表記すると、以下のようになる：
ラムダ項の定義は、型なしラムダ計算 の場合とほぼ同様である：
定義 (ラムダ項)
ラムダ項を以下のように定義する：
定義 (型判断)
(1) 型文脈 (typing context) $\Gamma$ を以下のように帰納的に定義する：
- 空文脈$\langle \rangle$ は型文脈である。
- $\Gamma$ が型文脈であるならば、$x$をまだ $\Gamma$ に現れていない変数、$A$ を型とすると、$\Gamma, x : A$ も型文脈である。
(2) $M$ をラムダ項、$A$ を型、$\Gamma$ を型文脈とするとき、型判断 (typing judgement) とは以下の形式の記号列である：
この型判断は「$M$ は型文脈 $\Gamma$ のもとで型 $A$ を持つ」ということを表す。
ただし、我々が以下考察の対象とするのは、適切に型付けられた (well-typed) 型判断のみである。 この適切な型付けの概念は、これまでと同様に形式体系の形で与えられる：
定義 (型付け規則)
型付け規則を以下の規則により定義する。
型付け公理
型付け規則
構造規則
例 (型判断の例)
(1) $\vdash \lambda x^{A} \lambda y^{B} .x : A \to (B \to A)$
簡約公理
定義 (簡約公理・簡約規則)
(1) ラムダ項に対し、1ステップ簡約 (1-step reduction) を以下の簡約公理と簡約規則によって定義する：
簡約公理
$(\beta_{\to})$
$(\eta_{\to})$
簡約規則
(2) $\lambda(V)$ 上の二項関係 $\overset{*}{\leadsto}$ を1ステップ簡約の反射推移閉包として定義する：すなわち、
- [$\leadsto \subset \overset{*}{\leadsto}$] $M \leadsto N$ ならば $M \overset{*}{\leadsto} N$.
- [反射性] $M \overset{*}{\leadsto} M$.
- [推移性] $M \overset{*}{\leadsto} N$ かつ $M \overset{*}{\leadsto} L$ ならば、$M \overset{*}{\leadsto} L$.
- [最小性] もし $\lambda(V)$ 上の二項関係 $R$ が上記を満たすならば、$\overset{*}{\leadsto} \subset R$.
代入補題と型保存定理
補題 (型に関する代入補題)
$\Gamma, x : B \vdash M : A$ かつ $\Gamma \vdash N : B$ ならば、$\Gamma \vdash M[x := N] : A$ である。
定理 (型保存定理)
$\Gamma \vdash M : A$ かつ $M \overset{*}{\leadsto} N$ ならば、$\Gamma \vdash N : A$ である。
1ステップの簡約 $M \leadsto N$ について、型が保存されることを示せば十分である。というのも、 1ステップの場合を証明できるのであれば、$M \overset{*}{\leadsto} N$ については、簡約ステップ数に関する帰納法によって証明できるからである。
以下、証明には1ステップの簡約 $M \leadsto N$ の導出に関する帰納法を用いる。
(1) [$\beta_{\to}$]
1ステップの簡約が公理 $\beta_{\to}$ からただちに得られる場合、具体的には
- $M = (\lambda x^{B} .L)P$
- $N = L[x:=P]$
と表せるので、$\Gamma \vdash (\lambda x^{B} .L)P : A$ を仮定してよい。 この型判定式の直前の導出図を考えると、
のようになる：すなわち、この仮定の下では $\Gamma, x : B \vdash L : A$ および $\Gamma \vdash P : B$ の導出が存在する。ゆえに、 型に関する代入補題により $\Gamma \vdash L[x:=P] : A$ を得る。これは求める $\Gamma \vdash N : A$ の型判定式である。
(2) [$\eta_{\to}$]
1ステップの簡約が公理 $\eta_{\to}$ からただちに得られる場合、具体的には
- $M = \lambda x^{A'} .Nx$ （ただし$x \notin \text{FV}(N)$）
と表せるので、$\Gamma \vdash \lambda x^{A'} .Nx : A' \to A''$ を仮定してよい（ここで $A = A' \to A''$ とおく）。 この型判定式の直前の導出図を考えると、
のようになる：すなわち、この仮定の下では $\Gamma, x : A' \vdash N : A' \to A''$ の導出 $\pi$ が存在する。 ゆえに、これに対して再び導出図を考えると、仮定より $x \notin \text{FV}(N)$ なので
となり、求める $\Gamma \vdash N : A$ を得る。
(3)[$\text{cong}$]
1ステップの簡約が $\text{cong}$ 規則から得られる場合、 $M = LP$、$N = L'P$ の形で表せて、$M \leadsto N$ は $L \leadsto L'$ から得られているはずなので、 $\Gamma \vdash LP : A$ および $L \leadsto L'$ を仮定する。さらに、ラムダ項 $L$ については、1ステップの型保存定理が成り立つと仮定する（$\because$ 帰納法の仮定）。 いまこの型判定式の直前の導出図を考えると、
のようになる：すなわち、この仮定の下では $\Gamma \vdash L : B \to A$ の導出が存在する。 仮定より $L \leadsto L'$であったので、帰納法の仮定である1ステップの型保存定理により、 $\Gamma \vdash L' : B \to A$ が成り立つ。
ゆえに、これに対して再び導出図を考えると、
となり、求める $\Gamma \vdash N : A$ を得る。
(4)[$\xi$]
1ステップの簡約が $\xi$ 規則から得られる場合、$M = \lambda x^{A'}.L$、$N = \lambda x^{A'}.L'$ の形で表せて、 $M \leadsto N$ は $L \leadsto L'$ から得られているはずなので、$\Gamma \vdash \lambda x^{A'}.L : A$ および $L \leadsto L'$ を仮定する（ただし $A = A' \to A''$ とおく）。 さらに、ラムダ項 $L$ については、1ステップの型保存定理が成り立つと仮定する（$\because$ 帰納法の仮定）。 いまこの型判定式の直前の導出図を考えると、
のようになる：すなわち、この仮定の下では $\Gamma, x : A' \vdash L : A''$ の導出が存在する。 仮定より $L \leadsto L'$ であったので、帰納法の仮定である1ステップの型保存定理により、$\Gamma, x : A' \vdash L' : A''$ が成り立つ。
ゆえに、これに対して再び導出図を考えると、
となり、求める $\Gamma \vdash N : A$ を得る。 $\Box$
参考文献
- [1] Peter Selinger, 2013. "Lecture notes on the lambda calculus". https://doi.org/10.48550/arXiv.0804.3434.
- [2] 横内寛文, 1994. 『情報数学講座7 プログラム意味論』. 共立出版.