λ 演算λ 演算是数理逻辑中的一个形式系统，在函数抽象和应用的基础上，使用变量绑定和替换来表达计算。讨论 λ 演算离不开形式化的表达。在本文中，我们尽量集中在与编程相关的基本概念上，而不拘泥于数学上的形式化表示。λ 演算实际上是对前面提到的函数概念的简化，方便以系统的方式来研究函数。λ 演算的函数有两个重要特征：
- λ 演算中的函数都是匿名的，没有显式的名称。比如函数 sum(x, y) = x + y 可以写成 (x, y)|-> x + y。由于函数本身仅由其映射关系来确定，函数名称实际上并没有意义。因此使用匿名函数是合理的。
- λ演算中的函数都只有一个输入。有多个输入的函数可以转换成多个只包含一个输入的函数的嵌套调用。这个过程就是通常所说的柯里化（currying）。如 (x, y)|-> x + y 可以转换成 x |-> (y |-> x + y)。右边的函数的返回值是另外一个函数。这一限定简化了λ演算的定义。
对函数简化之后，就可以开始定义 λ 演算。λ 演算是基于 λ 项（λ-term）的语言。λ 项是 λ 演算的基本单元。λ 演算在 λ 项上定义了各种转换规则。
λ项λ 项由下面 3 个规则来定义：
- 一个变量 x 本身就是一个 λ 项。
- 如果 M 是 λ 项，x 是一个变量，那么 (λx.M) 也是一个 λ 项。这样的 λ 项称为 λ 抽象（abstraction）。x 和 M 中间的点（.）用来分隔函数参数和内容。
- 如果 M 和 N 都是 λ 项，那么 (MN) 也是一个 λ 项。这样的λ项称为应用（application）。
所有的合法 λ 项，都只能通过重复应用上面的 3 个规则得来。需要注意的是，λ 项最外围的括号是可以省略的，也就是可以直接写为 λx.M 和 MN。当多个 λ 项连接在一起时，需要用括号来进行分隔，以确定 λ 项的解析顺序。默认的顺序是左向关联的。所以 MNO 相当于 ((MN)O)。在不出现歧义的情况下，可以省略括号。
重复应用上述 3 个规则就可以得到所有的λ项。把变量作为λ项是重复应用规则的起点。λ 项 λx.M 定义的是匿名函数，把输入变量 x 的值替换到表达式 M 中。比如，λx.x+1 就是函数 f(x)=x+1 的 λ 抽象，其中 x 是变量，M 是 x+1。λ 项 MN 表示的是把表达式 N 应用到函数 M 上，也就是调用函数。N 可以是类似 x 这样的简单变量，也可以是 λ 抽象表示的项。当使用λ抽象时，就是我们通常所说的高阶函数的概念。
绑定变量和自由变量在 λ 抽象中，如果变量 x 出现在表达式中，那么该变量被绑定。表达式中绑定变量之外的其他变量称为自由变量。我们可以用函数的方式来分别定义绑定变量（bound variable，BV）和自由变量（free variable，FV）。
对绑定变量来说：
- 对变量 x 来说，BV(x) = ∅。也就是说，一个单独的变量是自由的。
- 对 λ 项 M 和变量 x 来说，BV(λx.M) = BV(M) ∪ { x }。也就是说，λ 抽象在 M 中已有的绑定变量的基础上，额外绑定了变量 x。
- 对 λ 项 M 和λ项 N 来说，BV(MN) = BV(M) ∪ BV(N)。也就是说，λ 项的应用结果中的绑定变量的集合是各自 λ 项的绑定变量集合的并集。
对自由变量来说，相应的定义和绑定变量是相反的：
- 对变量 x 来说，FV(x) = { x }。
- 对 λ M 和变量 x 来说，FV(λx.M) = FV(M) − { x }。
- 对 λ 项 M 和 λ 项 N 来说，FV(MN) = FV(M) ∪ FV(N)。
在 λ 项 λx.x+1 中，x 是绑定变量，没有自由变量。在 λ 项 λx.x+y 中，x 是绑定变量，y 是自由变量。
在λ抽象中，绑定变量的名称在某些情况下是无关紧要的。如 λx.x+1 和 λy.y+1 实际上表示的是同样的函数，都是把输入值加 1。变量名称 x 或 y，并不影响函数的语义。类似 λx.x+1 和 λy.y+1 这样的 λ 项在λ演算中被认为是相等的，称为 α 等价（alpha equivalence）。
约简在 λ 项上可以进行不同的约简（reduction）操作，主要有如下 3 种。
α 变换α 变换（α-conversion）的目的是改变绑定变量的名称，避免名称冲突。比如，我们可以通过 α 变换把 λx.x+1 转换成 λy.y+1。如果两个λ项可以通过α变换来进行转换，则这两个 λ 项是 α 等价的。这也是我们上一节中提到的 α 等价的形式化定义。
对 λ 抽象进行 α 变换时，只能替换那些绑定到当前 λ 抽象上的变量。如 λ 抽象 λx.λx.x 可以 α 变换为 λx.λy.y 或 λy.λx.x，但是不能变换为 λy.λx.y，因为两者的语义是不同的。λx.x 表示的是恒等函数。λx.λx.x 和 λy.λx.x 都是表示返回恒等函数的 λ 抽象，因此它们是 α 等价的。而 λx.y 表示的不再是恒等函数，因此 λy.λx.y 与 λx.λy.y 和 λy.λx.x 都不是 α 等价的。
β 约简β 约简（β-reduction）与函数应用相关。在讨论 β 约简之前，需要先介绍替换的概念。对于 λ 项 M 来说，M[x := N] 表示把 λ 项 M 中变量 x 的自由出现替换成 N。具体的替换规则如下所示。A、B 和 M 是 λ 项，而 x 和 y 是变量。A ≡ B 表示两个 λ 项是相等的。
- x[x := M] ≡ M：直接替换一个变量 x 的结果是用来进行替换的 λ 项 M。
- y[x := M] ≡ y（x ≠ y）：y 是与 x 不同的变量，因此替换 x 并不会影响 y，替换结果仍然为 y。
- (AB)[x := M] ≡ (A[x := M]B[x := M])：A 和 B 都是 λ 项，(AB) 是 λ 项的应用。对 λ 项的应用进行替换，相当于替换之后再进行应用。
- (λx.A)[x := M] ≡ λx.A：这条规则针对 λ 抽象。如果 x 是 λ 抽象的绑定变量，那么不需要对 x 进行替换，得到的结果与之前的 λ 抽象相同。这是因为替换只是针对 M 中 x 的自由出现，如果 x 在 M 中是不自由的，那么替换就不需要进行。
- (λy.A)[x := M] ≡ λy.A[x := M]（x ≠ y 并且 y ∉ FV(M)）：这条规则也是针对λ抽象。λ 项 A 的绑定变量是 y，不同于要替换的 x，因此可以在 A 中进行替换动作。
在进行替换之前，可能需要先使用 α 变换来改变绑定变量的名称。比如，在进行替换 (λx.y)[y := x] 时，不能直接把出现的 y 替换成 x。这样就改变了之前的 λ 抽象的语义。正确的做法是先进行 α 变换，把 λx.y 替换成 λz.y，再进行替换，得到的结果是 λz.x。
替换的基本原则是要求在替换完成之后，原来的自由变量仍然是自由的。如果替换变量可能导致一个变量从自由变成绑定，需要首先进行 α 变换。在之前的例子中，λx.y 中的 x 是自由变量，而直接替换的结果 λx.x 把 x 变成了绑定变量，因此 α 变换是必须的。在正确的替换结果 λz.x 中，z 仍然是自由的。
β 约简用替换来表示函数应用。对 ((λV.E) E′) 进行 β 约简的结果就是 E[V := E′]。如 ((λx.x+1)y) 进行 β 约简的结果是 (x+1)[x := y]，也就是 y+1。
η 变换η 变换（η-conversion）描述函数的外延性（extensionality）。外延性指的是如果两个函数当且仅当对所有参数的结果相同时，才被认为是相等的。比如一个函数 F，当参数为 x 时，它的返回值是 Fx。那么考虑声明为 λy.Fy 的函数 G。函数 G 对于输入参数 x，同样返回结果 Fx。F 和 G 可能由不同的 λ 项组成，但是只要 Fx=Gx 对所有的 x 都成立，那么 F 和 G 是相等的。
以 F=λx.x 和 G=λx.(λy.y)x 来说，F 是恒等函数，而 G 则是在输入参数 x 上应用恒等函数。F 和 G 虽然由不同的 λ 项组成，但是它们的行为是一样，本质上都是恒等函数。我们称之为 F 和 G 是 η 等价的，F 是 G 的 η 约简，而 G 是 F 的 η 扩展。F 和 G 互为对方的 η 变换。 |
