6.1. Beta-归约式¶

既然我们在上一节中严格定义了替换，现在就可以定义 求值函数应用 的规则，这是任何 \(\lambda\) 演算解释器的主要操作。该规则称为 \(\beta\) -归约 。可应用此规则的表达式称为 \(\beta\) -可归约式 （简称 \(\beta\) -归约表达式 ）。因此， \(\beta\) -可归约式 在形式上被定义为具有特定形式的 \(\lambda\) 表达式，即第一个项为函数抽象的应用。

例如， \((\lambda x.(x \; v) \;\; (z \; (v \; u)))\) 是一个 \(\beta\) -归约项，因为 \(\lambda x.(x \; v)\) 是一个函数抽象。另一方面， \(((\lambda x.(x \; v) \;\; y) \;\; (z \; (v \; u)))\) 不是，因为它的第一项是一个函数应用而不是函数抽象。然而，构成该表达式第一项的应用是一个 \(\beta\) -归约项。这说明，即使表达式本身可能不是 \(\beta\) -归约项，它也可能包含是归约项的子表达式。

分析任何语言如何求值函数调用的一个关键部分，是从 \(\beta\) -归约的视角来考察其语义。

6.2. 识别 Beta-归约式¶

以下随机问题将帮助你识别 \(\beta\) -redex。要获得该题的分数，你必须连续三次正确解答。

6.3. Beta-归约是一种替换¶

如果我们有一个形式为 \((\lambda x.E \;\; E')\) 的 \(\beta\) -归约式，那么对该表达式进行 \(\beta\) -归约意味着使用上一节开发的替换算法，将 \(E'\) 代入 \(E\) 中的 \(x\) 。

换句话说，要计算形如 \(\beta\) -redex 的表达式

仅仅意味着执行以下替换：

同样，这只是你在 替换算法 中学到的算法。请注意， \(\beta\) -归约的结果是：先剥离 \(\lambda\) -抽象的绑定出现，仅保留其函数体，然后在该函数体中将 \(E'\) 代入 x。

例如，要对 \((\lambda x.(x \; v) \;\; (z \; (v \; u)))\) 进行 \(\beta\) -归约，您首先会剥离 \(\lambda x.\) 以得到 \((x \; v)\) （即 \(\lambda\) -抽象的主体），然后在该主体中将 \((z \; (v \; u))\) 替换为 \(x\) ，从而产生表达式 \(((z \;\; (v \;\; u)) \;\; v)\) 。

6.4. 某些 Beta-归约需要 Alpha-转换¶

下列随机问题将帮助你识别 \(\beta\) -redex，并通过判断是否需要 \(\alpha\) -conversion 来为归约它们做好准备。要获得该题的分数，你必须连续三次正确解答。

6.5. 执行 Beta 归约¶

下列随机问题将提供执行 \(\beta\) -归约的练习。要获得此题的分数，您必须连续三次正确解答。注意：请记住，由于 \(\beta\) -归约使用替换算法，可能有必要执行 \(\alpha\) -转换。例如，对 \((\lambda x. \lambda u.(u \;\; x) \;\; (v \;\; u))\) 进行 \(\beta\) -归约会得到 \(\lambda a.(a \;\; (v \;\; u))\) ，此时我们必须执行 \(\alpha\) -转换以避免捕获自由变量 \(u\) 。