4.1. Alpha 转换规则¶

现在我们把注意力转回 lambda 演算的语义，聚焦于 lambda 表达式中的 自由变量与约束变量 如何影响它们的含义。我们先考虑约束变量出现。

当一个变量出现 \(x\) 绑定于某个绑定出现时，\(x\) 的含义取决于这样一个事实：它出现在某个函数的函数体内，而且是该函数参数的名字。因此，\(x\) 的值完全由函数被调用时传入的实参决定，并且等于该实参。换句话说，当一个变量出现在一个给定表达式中是约束的时，它的含义在这个表达式内部是良定义的。例如，在下面的 JavaScript 函数中：

function f(x) {
     return 2 + x - y * x;
}

\(x\) 的值在函数被调用之前是未知的，但在运行时刻——比如说当我们运行下面的程序时：

f(12);

\(x\) 的含义是明确的：其值为 12。相比之下，\(y\) 在 f 内部的含义不是良定义的，因为 f 函数体中的 \(y\) 出现是自由的。这个例子说明了自由变量与约束变量在语义上的关键区别。

现在，函数参数的名字由程序员选择，要求简短而又有助于联想到它所代表的值。因此，在上面的例子中，程序员本可以选择把参数命名为 time 或 t，从而得到这个函数的另外两个版本：

function f(time) {                                  function f(t) {
     return 2 + time - y * time;                         return 2 + t - y * t;
}                                                   }

要点在于：函数 f 的三个版本行为完全一致。它们具有相同的含义。约束变量只是一个值的占位符。只要在整个函数体中被一致地使用，占位符叫什么名字并不重要。约束变量可以在不改变函数含义的前提下被重命名，这一事实体现在下面的 lambda 演算规则中。

\(\alpha\)-转换（\(\alpha\) 是小写希腊字母 alpha）是把函数抽象中的参数重命名的过程。

例如，考虑恒等函数：

我们可以使用变量 \(y\) 对这个函数进行 \(\alpha\)-转换，得到语义上相同的函数：

当然，在这种情况下，我们也可以使用其他任何变量来进行 \(\alpha\)-转换，比方说 \(z\)：

然而，务必牢记，\(\alpha\)-转换不能改变它所作用函数的含义。特别是，函数内部的所有自由变量在 \(\alpha\)-转换之后必须仍然是自由的。这意味着，当对 lambda 抽象进行 \(\alpha\)-转换时，我们并不总是可以随便挑选 任何 变量。考虑下面的例子：

这个表达式是一个函数应用：那个总是返回 \(y\) （一个自由变量）的常函数被应用于 \(x\) （也是一个自由变量）。我们能对这个表达式进行 \(\alpha\)-转换吗？不能，因为它是一个函数应用。但是，我们可以对它的第一个组成部分进行 \(\alpha\)-转换，因为它是一个 lambda 抽象。让我们来做。我们该选择哪个变量呢？首先，我们用变量 \(z\) 进行 \(\alpha\)-转换，得到：

这完全是可以接受的。含义没有改变。无论是这个版本还是应用的原始版本，应用的最终值都将是 \(y\)，因为被调用的函数忽略它的实参并且总是返回 \(y\)。

然而，如果我们用变量 \(y\) 对这个 lambda 抽象进行 \(\alpha\)-转换，我们会得到：

这是不可接受的。含义已经改变。在这个版本中，恒等函数被应用于并返回 \(x\)，而不是 \(y\)。回顾一下，在最初的应用中，\(y`（函数体）和 :math:`x`（函数调用的实参）都是自由变量，这意味着它们的含义没有在这个代码片段中被指定，而必须由上下文——即此应用所在的更大程序——来提供。在这个更大的程序中，:math:`x\) 和 \(y\) 很可能被绑定到不同的值。因此，它们含义不同，不能互换。

那么，当我们用变量 \(y\) 对表达式 \(\lambda x.y\) 进行 \(\alpha\)-转换得到 \(\lambda y.y\) 时，出了什么问题呢？抽象函数体中的变量 \(y\) 从自由变成了约束。我们说 \(y\) 经历了 变量捕获，或者更简单地说，它被 捕获 了。

由于变量捕获会改变 lambda 表达式的含义，我们必须不惜一切代价避免它。幸运的是，使用下面的规则很容易做到这一点：

在对 lambda 抽象进行 \(\alpha\)-转换时，始终选择 新的 变量，也就是不出现在被 \(\alpha\)-转换的函数体内的变量。

4.2. 练习：Alpha 转换¶

要练习 \(\alpha\)-转换的过程，请完成下面的练习。要获得学分，你必须连续三次答对。

总之，\(\alpha\)-转换只是把函数参数的名字替换为全新的名字，以避免变量捕获。在下一节中，\(\alpha\)-转换将对我们非常有用，因为我们要在那里描述确定 lambda 演算程序含义的主要算法，即替换（substitution）过程。