3.1. 自由变量与约束变量¶

在 lambda 演算中，如同在其他编程语言中一样，存在两种变量出现形式：变量声明和变量使用。例如，在以下 JavaScript 代码片段中：

function (x) {
   return x + y;
}

变量 \(x\) 出现了两次。 \(x\) 的第一次出现（在括号内）是参数 \(x\) 的 声明，即该变量首次被引入程序的位置。相比之下， \(x\) 的第二次出现是对变量 \(x\) 的 使用 （更准确地说， \(x\) 被用作加法运算的操作数）。此程序中 \(y\) 的出现是变量声明还是变量使用？

每个变量声明都为该变量定义了一个 作用域 ，即程序中该变量被定义并可使用的部分。在上面的示例中，变量 \(x\) 的作用域是函数体。当一个变量（例如 \(x\) ）的使用出现在 \(x\) 的声明作用域内时，我们称前者被 约束 到后者，而后者是该变量的 绑定出现 。因此，在上面的示例中，括号中对 \(x\) 的声明是该变量的绑定出现，而下一行中对 \(x\) 的使用则绑定到此绑定出现。未被绑定的变量称为 自由 。在上面的示例中， \(y\) 的出现于函数体内是自由的，因为该函数不包含任何 \(y\) 的绑定出现（即声明）。

由于给定程序中可能存在变量 \(x\) 的多个声明，因此该变量的每次使用绑定到哪个声明必须毫无歧义。这就是为什么每种编程语言都必须定义一种绑定方案。λ 演算与 JavaScript 及大多数其他现代编程语言一样，采用静态绑定（也称为“静态作用域”或“词法绑定”；参见 作用域、闭包、高阶函数 ），这意味着变量的每次使用都绑定到包含该使用的最小 λ 抽象中同名的变量声明。

我们现在准备在 lambda 演算的上下文中讨论变量的声明/使用、绑定出现、自由变量与约束变量以及词法作用域的概念。考虑以下示例：

此 lambda 表达式是一个 lambda 抽象，其参数为 \(y\) ，其主体是将恒等函数应用于表达式 \((y\ x)\) 。因此， \(\lambda\) 之后的 \(y\) 是变量 \(y\) 的绑定出现。此声明的作用域是 \((\lambda x.x\ (y\ x))\) ，这意味着最右侧的 \(y\) 出现绑定到最左侧的绑定出现。相比之下， \(\lambda x.x\) 中 \(x\) 的绑定出现的作用域仅是其中的第二个 \(x\) （即，一如既往，lambda 抽象的主体）。因此，上述表达式中第三个、最右侧的 \(x\) 出现是自由的：它是对 \(x\) 的一次使用，不属于任何 \(x\) 声明的作用域。

总结本例，从左到右， \(x\) 的第一次出现是其绑定出现，第二次出现绑定到第一次出现，而第三次出现是自由的。此例说明，任何变量都可能在同一表达式中既自由出现又绑定出现。因此，询问某个变量在 lambda 表达式中是自由的还是绑定的可能会引起混淆。更可取的做法是针对变量的每次 出现 提出这个问题，并牢记绑定出现永远不会是自由的，因为其作用是定义一个新变量。

3.2. 识别自由变量¶

本练习将有助于识别 lambda 表达式中的自由变量。要获得这道随机题目的分数，您必须连续三次正确解答。

3.3. 识别约束变量¶

本练习将有助于识别 lambda 表达式中的约束变量。要获得这道随机题目的分数，您必须连续三次正确解答。

3.4. 自由变量的形式化定义¶

在本节中，我们尽可能保持直观和非正式。然而，系统地定义自由变量和约束变量的概念是可行的。对于任何涉及 lambda 演算的精确定义，我们只需考虑 lambda 演算的 BNF 语法中定义的三种 lambda 表达式类型（参见 lambda 演算的语法 ）。

例如，我们说任何变量 \(x\) 在任何 lambda 表达式 \(E\) 中出现 自由 次，当且仅当：

1. \(E\) 是一个变量，且 \(E\) 与 \(x\) 相同，或者

2. \(E\) 的形式为 \((E_1\ E_2)\) ，且 \(x\) 在 \(E_1\) 或 \(E_2\) （或两者）中自由出现，或者

3. \(E\) 的形式为 \(\lambda y.E'\) ，其中 \(y\) 不同于 \(x\) ，且 \(x\) 在 \(E'\) 中自由出现。

请注意，上述情况 2 和 3 中的递归反映了 lambda 演算语法中的递归（为了便于理解下面的示例，这两种情况的顺序进行了交换）。下表说明了该定义的所有情况。

我们专门用一整节来讨论自由变量和约束变量的概念，是因为从下一节开始，我们将在本章中反复使用它们。