単純型付きラムダ計算 (1) の続き。 単純型（パラメータのない型）の範囲でのさまざまな型構成子について。
直積型
定義 (直積型)
(1) 型の集合 $\tau(T)$ を以下の規則により拡張する：
- $A, B$ が型であるならば、$A \times B$ も型である。
(2) ラムダ項の集合 $\lambda(V)$ を以下の規則により拡張する：
- $M, N$ がラムダ項であるならば、ペアリング(pairing) $\langle M, N \rangle$ もラムダ項である。
- $M$ がラムダ項であるならば、 射影(projection) $\pi_{1} M$, $\pi_{2} M$ もラムダ項である。
型 $A \times B$ を 直積型 (product type) という。
定義 (直積型の型付け規則)
直積型の型付け規則として、以下の規則を追加する：
定義 (直積型の簡約公理)
直積型の簡約公理として、以下の簡約公理を追加する：
$(\beta_{\times})$
$(\eta_{\times})$
直和型
定義 (直和型)
(1) 型の集合 $\tau(T)$ を以下の規則により拡張する：
- $A, B$ が型であるならば、$A + B$ も型である。
(2) ラムダ項の集合 $\lambda(V)$ を以下の規則により拡張する：
- $M$ がラムダ項であるならば、入射(injection) $\textsf{in}_{1}M$, $\textsf{in}_{2}M$ もラムダ項である。
- $x, y$ が変数、$M, N, L$ がラムダ項であるならば、 $\textsf{ case } M \textsf{ of } x \Rightarrow N \mid y \Rightarrow L$ もラムダ項である。
型 $A + B$ を直和型 (sum type) という。
定義 (直和型の型付け規則)
直和型の型付け規則として、以下の規則を追加する：
定義 (直和型の簡約公理)
直和型の簡約公理として、以下の簡約公理を追加する：
$(\beta_{+})$
直積型と直和型の型構成子 $\times$, $+$ を加えた体系においても、型保存定理が成り立つ。 これは、追加した簡約公理が「その公理に則って簡約を行っても型が保存される」という意味で正当なものであることの証でもある。
命題 (型保存定理：直積型・直和型)
$\Gamma \vdash M : A$ は直積型と直和型を追加して拡張した体系における型判断であるとする。 このとき、$M \overset{*}{\leadsto} N$ ならば、$\Gamma \vdash N : A$ である。
新しく追加した簡約公理が型を保存することを示せばよい。
(1) [$\beta_{\times}$]
第一射影 $\pi_{1}$ の場合のみ示す。1ステップの簡約が公理 $\beta_{\times}$ からただちに得られる場合、具体的には $M = \pi_{1} \langle N, L \rangle$ と表せるので、$\Gamma \vdash \pi_{1} \langle N, L \rangle : A$ と仮定する。このとき、直前の導出を考えると、
のようになる：すなわち、この仮定の下では $\Gamma \vdash N : A$ の導出が存在する。
(2) [$\eta_{\times}$]
1ステップの簡約が $\eta_{\times}$ からただちに得られる場合、具体的には $M = \langle \pi_{1}N, \pi_{2}N \rangle$ と表せるので、 $\Gamma \vdash \langle \pi_{1}N, \pi_{2}N \rangle : A' \times A''$ と仮定する（$A = A' \times A''$）。このとき、直前の導出を考えると、
のようになる：すなわち、この仮定の下では $\Gamma \vdash N : A' \times A''$ の導出が存在するので、$\Gamma \vdash N : A$ である。
(3) [$\beta_{+}$]
$\textsf{in}_{1}$ の場合のみ示す。1ステップの簡約が $\beta_{+}$ からただちに得られる場合、具体的には
- $M = \textsf{ case } \textsf{in}_{1}L \textsf{ of } x \Rightarrow P \mid y \Rightarrow Q$
- $N = P[x:=L]$
と表せるので、$\Gamma \vdash \textsf{case } \textsf{in}_{1}L \textsf{ of } x \Rightarrow P \mid y \Rightarrow Q : A$ と仮定する。 このとき、直前の導出を考えると、
のようになる：すなわち、この仮定の下では $\Gamma \vdash L : A'$ および $\Gamma, x : A' \vdash P : A$ の導出が存在する。 ゆえに、型に関する代入補題により、$ \Gamma \vdash P[x:=L] : A$ が成り立つ。 これは求める $\Gamma \vdash N : A$ の型判断である。 $\Box$
トップ型とボトム型
定義 (トップ型・ボトム型)
(1) 型の集合 $\tau(T)$ を以下の規則により拡張する：
- $\textsf{1}$ は型である。
- $\textsf{0}$ は型である。
(2) ラムダ項の集合 $\lambda(V)$ を以下の規則により拡張する：
- $*$ はラムダ項である。
- $M$ がラムダ項、$A$ が型であるならば、$\epsilon_{A} M$ はラムダ項である。
定義 (トップ型・ボトム型の型付け規則)
トップ型とボトム型の型付け規則として、以下の規則を追加する：
参考文献
- [1] Peter Selinger, 2013. "Lecture notes on the lambda calculus". https://doi.org/10.48550/arXiv.0804.3434.
- [2] Jean-Yves Girard, Paul Taylor, Yves Lafont. 1989. Proofs and Types. Cambridge : Cambridge University Press.
- [3] Greg Restall. 2000. An Introduction to Substructural Logics. London : Routledge.