形式陈述

归约系统的弱正规化要求每个考察项至少存在一条有限归约到正规形的路径；强正规化要求不存在无限归约序列。强正规化蕴含弱正规化，反之不成立。该性质总是相对于项集合与归约关系而言；改变允许的规则、类型或求值策略会改变结论。

直觉

弱正规化说“有路可到终点”，强正规化说“无论怎么走都不可能永远绕下去”。

例子与边界

$(\lambda x.y)\Omega$$(\lambda x.y)\mathrm{\Omega }$ 对全 β-归约弱正规化但不强正规化。简单类型 λ 演算对 β-归约强正规化；加入一般递归后通常失去该性质。确定性求值策略的终止性只涉及唯一执行轨迹，不能自动推出整个重写系统强正规化。

推论与应用

正规化用于证明逻辑一致性、决定类型项等价、保证编译期计算终止，并刻画语言表达能力与发散之间的边界。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Parts I–XVIII。
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 3–30。