形式陈述

简单类型 λ 演算中的每个良类型项都强正规化：不存在无限 β-归约序列。经典证明用 Tait 可归约性或逻辑关系，按类型定义“可计算项”，证明变量替换保持可计算性，再推出良类型项可计算并终止。结论依赖没有一般递归或不受限自引用。

直觉

简单类型阻止函数把自身当作不匹配类型的参数反复应用，从结构上排除无类型演算中的经典发散项。

例子与边界

自应用 $xx$$xx$ 无法在简单类型系统中给 $x$$x$ 同时赋予 $A$$A$ 与 $A\to B$$A\to B$。强正规化比类型安全更强：安全只说不会卡住，不排除无限循环。加入 fix 算子后仍可保持进展与保持性，但强正规化消失。

推论与应用

该定理连接 Curry–Howard 对应、逻辑一致性和可判定的规范化判等，并解释总函数语言的设计基础。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 3–30。
• Andrew K. Wright and Matthias Felleisen, “A Syntactic Approach to Type Soundness,” Information and Computation 115(1), 1994，Full paper。