(λ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 互为对方的 η 变换。