5.1. 替换算法¶

在本节中，我们将继续探究 lambda 演算的语义。既然我们已经理解了三种 lambda 表达式的含义（参见 lambda 演算的语义 ）、自由变量与绑定变量的含义（参见 自由变量与约束变量 ）以及如何系统地重命名绑定变量（参见 Alpha 转换 ），我们就具备了阐释 lambda 演算中函数调用含义所需的全部工具。请注意，由于函数是 lambda 演算中唯一的实体，解释 lambda 演算程序归根结底就是执行函数调用。

首先，考虑如何在脑海中执行以下函数调用：

f(8)

你首先会查找函数 f 的定义，例如：

var f = function (x) { return  2 * x - 5; };

然后，您可以通过将 8 代入 f 的主体中的 x 并计算其值来求得 f(8) 的值，得到 2*8 - 5 = 11 。这种评估函数调用的直观方法自然地引出了 基于替换的解释模型。在本节中，我们将讨论一种在 lambda 演算中执行替换的著名算法。

由于函数体与函数调用的参数都可以是任意的 lambda 表达式，因此我们需要一种算法，能够将任意 lambda 表达式 \(a\) （参数）代入到 lambda 表达式 \(b\) （函数体）中的变量 \(p\) （函数的形参）。在本节中，我们不再将 \(a\) 、 \(p\) 和 \(b\) 视为函数调用的组成部分。相反，我们将以一般性术语描述该算法，即作为一种在 \(b\) 中将 \(a\) 代入 \(p\) 的算法，记作：

其中 \(a\) 和 \(b\) 是任意 lambda 表达式， \(p\) 是任意变量。

注意 \(subst(a, p, b)\) 表示“在 \(b\) 中将 \(p\) 替换为 \(a\) "，或者等价地说，“在 \(b\) 中用 \(a\) 替换 \(p\) "。无论您选择哪种表述方式， \(b\) 始终是我们执行替换操作所在的表达式， \(p\) 始终是从 \(b\) 中被移除的表达式，而 \(a\) 始终是插入到 \(b\) 中的表达式。

现在，回到替换算法。由于 \(b\) 是任意 lambda 表达式，回顾 BNF 文法（参见 lambda 演算的语法 ），我们看到对于 \(b\) 必须考虑三种情况，即变量、lambda 抽象或应用表达式。因此，我们对该算法的描述被分解为三个编号的情况。

情况 1： 如果 \(b\) 是一个变量，例如 \(x\) ，那么 \(subst(a, p, b)\) 变为 \(subst(a, p,x)\) 。回想一下， \(p\) 和 \(x\) 是通用变量。因此我们需要区分两种子情况。首先，如果 \(p\) 和 \(x\) 是同一个变量，例如 \(v\) ，那么 \(subst(a,p,x)\) 实际上是 \(subst(a,v,v)\) ，其值为 \(a\) ，因为这是将 \(v\) 替换为 \(a\) 后得到的结果。我们将算法的这部分称为 情况 1a。其次，如果 \(p\) 和 \(x\) 是两个不同的变量，那么 \(subst(a,p,x)\) 等于 \(x\) ，因为变量 \(p\) 不出现在 \(x\) 中，不需要也不可能进行替换。我们将算法的这部分称为 情况 1b。

让我们来看两个属于情况 1 的代入示例。首先，在 \(subst(\lambda x.x, u, v)\) 中， \(v\) 是一个不同于 \(u\) 的变量。因此，此示例匹配情况 1b，算法的输出为 \(v\) 。另一方面， \(subst(\lambda y.(y\ x), u, u)\) 属于情况 1a，因为 \(p\) 和 \(b\) 都等于同一个变量 \(u\) 。所以，算法返回 \(\lambda y.(y\ x)\) 。

情况 2： 当在 \(\lambda x.E\) 中将 \(a\) 替换为 \(p\) 时，即 \(subst(a,p,b)\) ，其中 \(b\) 是一个 \(\lambda\) 抽象（此处为 \(\lambda x.E\) ），需要考虑三种子情况：

• 情况 2a： \(p\) 和 \(x\) 是同一个变量，例如 \(v\) ，则 \(subst(a,v,\lambda v.E)\) 应返回 \(\lambda v.E\) 。例如， \(subst(\lambda z.z, x, \lambda x.x)\) 返回 \(\lambda x.x\)

• 情况 2b： \(p\) 和 \(x\) 是两个不同的变量，且 \(x\) 不在 \(a\) 中自由出现，则 \(subst(a,p,\lambda x.E)\) 应返回 \(\lambda x.subst(a,p,E)\) 。例如， \(subst((w \; z), y, \lambda x.y)\) 返回 \(\lambda x.(w \; z)\)

• 情况 2c： \(p\) 和 \(x\) 是两个不同的变量，但 \(x\) 确实在 \(a\) 中自由出现，则应对 \(\lambda x.E\) 进行 alpha 转换，以便应用情况 2b。例如， \(subst((w \; x), y, \lambda x.x)\) 应返回 \(\lambda a.a\) ，其中 \(a\) 是在 alpha 转换过程中选择的合适变量。

情况 3： 如果 \(b\) 是一个应用表达式，例如 \((e_1\ e_2)\) ，其中 \(e_1\) 和 \(e_2\) 是任意 lambda 表达式，那么 \(subst(a,p,b)\) 的值（实际上是 \(subst(a,p,(e_1\ e_2))\) ）为 \((subst(a,p,e_1)\ subst(a,p,e_2))\) ，即通过将 \(a\) 递归替换原始应用表达式各组成部分中的 \(p\) 而得到的应用表达式。

例如，考虑 \(subst(\lambda y.(y\ x), u, (\lambda v.u\ u))\) 。由于我们代入的表达式（即第三个表达式）是一个应用表达式，该算法要求我们返回一个应用，该应用是通过在应用的两个分量中递归地将 \(u\) 替换为 \(\lambda y.(y\ x)\) 而得到的，结果为 \((\lambda v.\lambda y.(y\ x)\ \lambda y.(y\ x))\) 。

5.2. 识别情况 1 的代换子情况¶

以下练习有助于识别在替换算法的每一步中适用情况 1 的哪个子情况。要在此随机问题中获得分数，您必须连续三次正确解答。

5.3. 识别情况 2 的代换子情况¶

以下练习有助于识别在代入算法的每一步中适用情况 2 的哪个子情况。要在此随机问题中获得分数，您必须连续三次正确解答。

5.4. 识别代换情形 3¶

以下练习有助于判断在替换算法的每一步中是否适用情况 3。要在此随机问题中获得分数，您必须连续三次正确解答。

5.5. 识别替换情形与子情形¶

以下练习有助于识别在代入算法的每一步中适用哪个（子）情况。要在此随机问题中获得分数，您必须连续三次正确解答。

5.6. 执行替换算法¶

以下练习将测试您通过严格应用算法来完成完整代换的能力。要获得此随机问题的分数，您必须连续三次正确解答。