規範化性質

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

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

但是考慮在應用 於自身時所發生的:

所以項 不是規範化的。

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

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

參見