简单类型化λ演算的强正规化定理

(泰特的可归约性方法。)对类型的结构做归纳,为每个类型 $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$ 做归纳,一并证明三条技术性质:(CR1) $\mathrm{RED}_A$ 中每个项都是强正规化的;(CR2) $\mathrm{RED}_A$ 对 $\beta$ 归约封闭(若 $t\in\mathrm{RED}_A$ 且 $t\to t'$,则 $t'\in\mathrm{RED}_A$);(CR3) 任何"中性"项(变量或应用,而非抽象),若其所有一步归约结果都已在 $\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$,该项经一步 $\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$