规范化性质

在数理逻辑和理论计算机科学中，一个重写系统有规范化性质，如果所有项都是强规范化的；就是说所有重写序列都最终终止于规范形式的项。

纯粹无类型 lambda 演算不是强规范化的。考虑项 ${\displaystyle \lambda x.xxx}$。它有如下重写规则: 对于任何项 t，

${\displaystyle (\mathbf {\lambda } x.xxx)t\rightarrow ttt}$

但是考虑在应用 ${\displaystyle \lambda x.xxx}$ 于自身时所发生的:

${\displaystyle (\mathbf {\lambda } x.xxx)(\lambda x.xxx)}$	${\displaystyle \rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)}$
	${\displaystyle \rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)}$
	${\displaystyle \rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)}$
	${\displaystyle \ldots \,}$

所以项 ${\displaystyle (\lambda x.xxx)(\lambda x.xxx)}$ 不是规范化的。

各种有类型 lambda 演算系统包括简单类型 lambda 演算，Jean-Yves Girard 的系统F，和 Thierry Coquand 的构造演算都有规范化性质。

带有规范化性质的 lambda 演算系统可以被看作带有所有程序都终止性质的编程语言。尽管这是一个非常有用的性质，它也有缺点: 带有规范化性质的编程语言不可能是图灵完全的。这意味着有可计算函数不能在简单类型的 lambda 演算中定义(类似的有可计算函数不能在构造演算或系统 F 中计算)。

• lambda 演算
• 有类型 lambda 演算
• 重写系统
• 构造演算