查看“︁规范化性质”︁的源代码

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

纯粹无类型 [[lambda 演算]]不是强规范化的。考虑项 <math>\lambda x . x x x</math>。它有如下重写规则: 对于任何项 ''t''，

: <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math>

但是考虑在应用 <math>\lambda x . x x x</math> 于自身时所发生的:
{|
| <math>(\mathbf{\lambda} x . x x x) (\lambda x . x x x)</math>
| <math> \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>\ldots\,</math>
|}

所以项 <math>(\lambda x . x x x) (\lambda x . x x x)</math> 不是规范化的。

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

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

==参见==
* [[lambda 演算]]
* [[有类型 lambda 演算]]
* [[重写系统]]
* [[构造演算]]

{{logic-stub}}

[[Category:Lambda演算]]