4.7 关于Lambda演算的一些事实

什么时候一个表达式是完全还原的？几乎所有的表达式可以用 →_n^α 将变量名重命名来约化，所以 →_n^α 不能被算在定义内。因此，一个完全还原的表达式是无法再由 →_n^β →_n^η 约化的表达式。

概念：

• 如果一个表达式无法再由 →_n^β →_n^η 约化，则它被称为范式。

• M 有范式 N 如果 M =_n N 并且 N 是范式。

范式的作用与Lambda演算表达式的结果一样。如果一个表达式有范式，则它有且仅有唯一的范式（可能通过很多不同的约化得到）。更准确地说， →_n^α 重命名取模只能得到一个范式。

定理 4.2 [范式] : 如果 L =_n M，L =_n M，并且 M 和 N都是范式，则 M =_α N

如往常一样， =_α 为由 α 兼容闭合生成的等价关系。定理 4.2 易由 Church-Rosser 性质证明：

***定理 4.3 [ =_n 代表 Church-Rosser 关系]***: 如果 M =_n N，则存在一个L’ 使得 M →→_n L’ 且 N →→_n L’

至于 =_r ，这个定理的证明取决于 →→_n 的棱形性质。

定理 4.4 [ →→_n 代表棱形性质] : 如果 L →→_n M 且 L →→_n N，则存在一个表达式 L’ 使 M →→_n L’ 且 N →→_n L’

单步关系 →_n 并不满足棱形性质，甚至不满足轻微的扭曲关系，比如 →_r 的类-棱形性质。原因是→_n^β 可以重复可约表达式。比如：

对于上述的两个约化表达式，没有一个单步关系能够将他们约化为同一个表达式。在下一节我们会知道，解决这个问题的方式是围绕子关系式定义一个平行约化的概念，这样左边的两个((λy.y) (λz.z))子表达式可以被同时约化。现在，我们暂时不会尝试证明定理 4.4。在下一章我们会演示关联语言的棱形性质。

不像 B 中的关系式，每一个表达式的结果不是 f 就是 t，并不是每一个Lambda表达式都有范式。比如，Ω 不存在范式：

即使一个表达式存在范式，也有可能存在一个无限约化顺序使其永远无法变成范式，例如：

因此，定理 4.2 只保证最多只存在一个范式，但是我们目前为止并没有找到它的方法。直观上来说，上述这个无限约化的问题使，我们计算一个函数的参数，但是这个参数再函数体中并不会被使用。这提示我们应用最左边的 β 或 η 约化来达到范式：
KaTeX parse error: Got function '\overline' with no arguments as subscript at position 3: →_\̲o̲v̲e̲r̲l̲i̲n̲e̲{G} 关系被称为 良序约化 关系，它会在范式存在的前提下找到范式。

定理 4.5 [良序约化] : 当且仅当 M →→_{$\overline{G}$} N 的时候，N 为 M 的范式。

良序约化（normal-order reduction）也被称作 名称调用（call-by-name）。

尽管一个 良序约化 会在范式存在时找到范式，但几乎没有编程语言使用这种约化关系。因为良序虽有效但是非常缓慢，比如在上个段落中证明非棱形性质的 →_n 关系中，左边的约化对应良序，右边的约化则会在更少的步骤下得到同样的函数。

在任何情况下，因为我们有唯一范式的概念，问题来到了我们能不能用定义 eval_r 的方式设法定义一个 eval_n 函数：
$$eva{l}_n(M)\stackrel{\text{?}}{=}NifM{=}_{n}NandNisanormalform$$
上述定义对于 α-重命名 是不准确的，但是还有一个更深层次的问题。正如我们所看到的，类似 mk和 Y这样的函数，它们的行为方式相同，但不能相互约化。在下一章中，我们将探讨解决这个问题的方法。

练习 4.15

证明 ((λx.x x) (λx.x x)) 不存在范式。

题解

对 ((λx.x x) (λx.x x)) 应用 β 良序约化：

((λx.x x) (λx.x x)) β ((λx.x x) (λx.x x))

由于进行 β 良序约化之后，我们得到相同的表达式，这一约化将无所循环下去，因此我们无法得到一个范式表达式。所以 ((λx.x x) (λx.x x)) 不存在范式。

4.8 历史

在Turning发明Turning machines略微之前，Church发明了Lambda演算。

Barendregt将Church的Lambda演算作为一个逻辑系统进行了全面的研究，许多处理术语的公约都起源于Barendregt。尽管他没有将Lambda演算看作为编程语言的微积分，他的书提供了许多适用于微积分的技术。