単純型付きラムダ計算の強正規化定理

(タイトの被還元性の方法。)型の構造に関する帰納法により、各型 $A$ に対して「被還元項」の集合 $\mathrm{RED}_A$ を定義する:基本型 $o$ については、$\mathrm{RED}_o$ をすべての強正規化可能な項からなる集合 $SN$ とする;関数型については、$\mathrm{RED}_{A\to B} = \{t : \text{for every } u \in \mathrm{RED}_A,\ t\,u \in \mathrm{RED}_B\}$ とする。

まず $A$ に関する帰納法により、3つの技術的性質をまとめて証明する:(CR1) $\mathrm{RED}_A$ のすべての項は強正規化可能である;(CR2) $\mathrm{RED}_A$ は $\beta$簡約について閉じている($t\in\mathrm{RED}_A$ かつ $t\to t'$ ならば $t'\in\mathrm{RED}_A$);(CR3) 1段階簡約先がすべてすでに $\mathrm{RED}_A$ に属する「中立的な」項(抽象ではなく変数または適用)は、それ自身も $\mathrm{RED}_A$ に属する。基本の場合は $SN$ の定義から直ちに従う;関数型の場合は $\mathrm{RED}_{A\to B}$ の定義を展開し、より小さい型 $A$、$B$ に関する帰納法の仮定を用いる。

次に、自由変数に被還元項を代入したとき、あらゆる型付けされた項が被還元であることを示す:$\Gamma \vdash t:A$ の型付け導出に関する帰納法により、$\sigma$ が $\Gamma$ の各変数 $x$ に項 $\sigma(x)\in\mathrm{RED}_{\Gamma(x)}$ を割り当てるならば、$t\sigma \in \mathrm{RED}_A$。変数の場合は直ちに従う。適用の場合は $\mathrm{RED}_{A\to B}$ の定義から直接従う。抽象の場合が最も注意を要する:$(\lambda x.\,t)\sigma$ を任意の $u\in\mathrm{RED}_A$ に適用すると、項は1回の $\beta$ステップで $t(\sigma,x{:=}u)$ に簡約され、これは(拡張された代入に適用した)帰納法の仮定により $\mathrm{RED}_B$ に属する;性質(CR3)——簡約先がすべてすでに被還元である項の「展開」についての閉性——により、$(\lambda x.\,t)\sigma\,u$ 自身が $\mathrm{RED}_B$ に置かれ、したがって定義により $(\lambda x.\,t)\sigma \in \mathrm{RED}_{A\to B}$。

最後に、これを恒等代入に適用する:各変数 $x{:}A$ はそれ自身が中立的であり簡約先を一切持たないので、(CR3) により自明に $\mathrm{RED}_A$ に属する。したがって任意の閉じた導出 $\Gamma \vdash t:A$ について、$\sigma$ が各 $x$ をそれ自身へ送るとすれば $t = t\sigma \in \mathrm{RED}_A$ が得られる。(CR1) により $\mathrm{RED}_A \subseteq SN$ なので $t \in SN$:あらゆる型付けされた項は強正規化可能である。$\blacksquare$