規範化性質

在數理邏輯和理論計算機科學中，一個重寫系統有規範化性質，如果所有項都是強規範化的；就是說所有重寫序列都最終終止於規範形式的項。

純粹無類型 lambda 演算不是強規範化的。考慮項 $\lambda x.xxx$。它有如下重寫規則: 對於任何項 t，

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

但是考慮在應用 $\lambda x.xxx$ 於自身時所發生的:

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

所以項 $(\lambda x.xxx)(\lambda x.xxx)$ 不是規範化的。

各種有類型 lambda 演算系統包括簡單類型 lambda 演算，Jean-Yves Girard 的系統F，和 Thierry Coquand 的構造演算都有規範化性質。

帶有規範化性質的 lambda 演算系統可以被看作帶有所有程序都終止性質的編程語言。儘管這是一個非常有用的性質，它也有缺點: 帶有規範化性質的編程語言不可能是圖靈完全的。這意味着有可計算函數不能在簡單類型的 lambda 演算中定義(類似的有可計算函數不能在構造演算或系統 F 中計算)。

參見

• lambda 演算
• 有類型 lambda 演算
• 重寫系統
• 構造演算