规范化性质 在数理逻辑和理论计算机科学中一个重写系统有规范化性质如果所有项都是强规范化的就是说所有重写序列都最终终止于规范形式的项 纯粹无类型 lambda 演算不是强规范化的考虑项 λ x  x x x displaystyle lambda xxxx 它有如下重写规则 对于任何项 t  λ x  x x x  t  t t t displaystyle mathbf lambda  xxxxtrightarrow ttt 但是考虑在应用 λ x  x x x displaystyle lambda xxxx 于自身时所发生的 所以项  λ x  x x x   λ x  x x x  displaystyle lambda xxxxlambda xxxx 不是规范化的 各种有类型 lambda 演算系统包括简单类型 lambda 演算JeanYves Girard 的系统F和 Thierry Coquand 的构造演算都有规范化性质 带有规范化性质的 lambda 演算系统可以被看作带有所有程序都终止性质的编程语言尽管这是一个非常有用的性质它也有缺点 带有规范化性质的编程语言不可能是图灵完全的这意味着有可计算函数不能在简单类型的 lambda 演算中定义类似的有可计算函数不能在构造演算或系统 F 中计算