本系列教程：

在上一章我们通过引入α变换学习了关于λ表达式的等价关系，准确说，是等价关系之一。但是α变换本身仅仅是替换了变元的名字，并没有改变一个λ表达式的结构，或者变元的绑定关系。如果在不改变变元绑定关系的前提下，还想改变结构的话，那么就需要把“替换（substitution）”的操作做一下扩展。

在正式定义这个广义上的替换操作前，我们先来看几个例子：

  x [ x := λy.y ] 
= λy.y

  (λx.z x) [ x := λy.y ] 
= λx.z x

  (x (λz.x)) [ x := (λy.y) z ] 
= (x (λa.x)) [ x := (λy.y) z ] 
= ((λy.y) z) (λa.(λy.y) z)

首先需要解释一下这里用到的标记方法（notation），像 _[_:=_] 这样的写法通常被用来定义多元函数。广为人知的二元表达式分为前缀（+ 1 2）、中缀（1 + 2）、后缀（1 2 +）三种写法，但它们在多元的情况则不再适用。像 E[x:=e] 这种写法，所表达的是把某个（被定义的）函数，作用于三个参数：E, x, e。既然我们是讨论替换操作，它的意思是将λ表达式 E 里面的所有名叫 x 的自由变元，替换成表达式 e。如果写成 _[_:=_] 的话，其中下划线表示的是参数缺失，也就是有待填入具体参数，而写成 E[x:=e] 的话则是参数齐全的表达式了。写成 _[_:=_] 其实也可以看作是这个函数的名字，就像三角函数 sin，cos 这样的名字，只不过是用符号，而不是英文来表示。

第一个例子 x [ x := λy.y ]，是将 x 替换成 λy.y。既然原λ项是单个变元 x，那么替换结果就是 λy.y。

第二个例子 (λx.z x) [ x := λy.y ]，也是要把 x 替换成 λy.y。但在原λ项里出现的两个 x，第一个是形参，第二个是被这个形参绑定的，非自由变元。所以这里并没有可被替换的自由变元，结果是维持原λ项不变。

第三个例子 (x (λz.x)) [ x := (λy.y) z ]，是要把 x 替换成 (λy.y) z。值得注意的是，替换项里的 z 是自由变元，如果直接替换到 λz.x 里面成为 λz.(λy.y) z 的话，那么替换项里的自由变元 z 将被原λ项里面的 λz 绑定，不再自由。为了避免这种情况的发生，我们可以先把 (x (λz.x)) 做一个α变换，写成 (x (λa.x))，接下来再替换 x 就没问题了。

从这三个例子里面可以看到，做替换操作的主要原则就是不要改变原λ项和替换项里面的变元绑定关系，这个原则在α变换中已经得到了体现（见前一章的 subV 函数），而在扩展后的替换操作中则需要更加小心的对待。用 Haskell 实现如下：

subT :: Var -> Term -> Term -> Term
subT u w (Var v)   | v == u    = w
                   | otherwise = Var v
subT u w (App f e) = App (subT u w f) 
                         (subT u w e)
subT u w (Lam v e)
     | v == u    = Lam v e
     | v `notElem` fvsW = Lam v (subT u w e)
     | otherwise = Lam x (subT u w (subV v x e))
  where
    bvsE = boundVars e
    fvsE = freeVars e
    fvsW = freeVars w
    x    = freshVar (bvsE ++ fvsE ++ fvsW)

我们比较一下这个 subT 和前一章实现的 subV 函数，会发现：

首先是它们的函数类型不同，因为 subT 是要把 Var 替换成 Term。
其次，它们在对 Term 这个代数类型的三个分支的处理上很类似，主要的差别是当 Lam v e 里面的 v 不等于 u 的时候，如何处理关于子项 e 的递归替换： a. 我们先做一个条件检查，当 w 的自由变元中不包括 v 时，不存在原本自由的变元被意外绑定的情况，所以可以直接递归处理子项 e。 b. 而当意外绑定有可能发生时，则需要对 Lam v e 做α变换，用一个新变元 x 来替代 v。选取这样一个 x 需要满足以下两个条件： i. x 对于 e 来说是一个“新”的不曾出现过的变元，这个条件和α变换所需的条件是一样的； ii. w 的自由变元不包括 x，以避免在 w 的自由变元被这里α变换时引入的 x 意外绑定。

鉴于前文已经给出了 freeVars 函数的实现，另外两个辅助函数 boundVars 和 freshVar 就留待读者自行定义（见习题一）。

在替换操作的基础上，λ演算定义了一个化简λ表达式的方法，叫做β规约（β-reduction）：

    (λx.e) e' => e [ x := e' ]

这里我们用的符号 => 代表规约关系。比如 A=>B 代表的就是λ项 A 可以β规约成为λ项 B。所有满足 ((λ_._) _) 这种结构的λ项都可以被规约，我们把它们叫做 redex（reducible expression）。一个复杂的λ项可能有多个子项符合这个结构，也就是有多个 redex。而当一个λ项当中不存在任何 redex 的时候，它被叫做范式（Normal Form）。换句话说，范式就是（所有子项都）不可以继续被规约的λ项。

β规约讲的是这样一个规则：当一个函数作用于它的参数时，原表达式等价于在函数体里将所有行参（parameter）出现的地方都替换为实参（argument）。有中学代数基础的朋友会说：“这不就是把参数代入到函数里去吗？搞这么复杂干嘛？” 没错，道理是相通的。直觉有助于理解，但只有严格的定义才能铺下牢靠的基石，奠定新的起点。中学的代数显然不曾考虑过高阶函数，人们自然也没有机会深入思考这背后隐藏的秘密，直到 Alonzo Church 把相关的规则做了形式化的整理，在这个基础上才发展出了一整套λ演算的理论。

那么β规约是否和α变换一样是一种等价关系呢？如果我们套用最常见的等价的定义，就会发现β规约并不满足自反／对称／传递这三个条件，比如 A => B 并不能推导出 B => A。所以通常的做法是直接把β规约当作是一条公理，也即β等价（β-equivalence）:

    (λx.e) e' = e [ x := e' ]

建立在α和β这两个等价关系上的λ演算满足自恰性（soundness），换句话说，在这套公理系统中不存在相互矛盾的结论。而满足自恰性几乎是一切有意义的公理理论的前提。是的，这一切仅仅是一个起点。

习题

一、实现本章节提到的 Haskell 函数 boundVar 和 freshVar。使得 boundVar e 返回 e 中所有被绑定的变元，freshVar fvs 返回一个不属于 fvs 列表的任意变元。

  boundVars :: Term -> [Var]
  freshVar :: [Var] -> Var

二、以下λ项各有多少个 β-redex？这些λ项都可以被规约到范式吗？如果可以，那么范式分别是什么？

  f (λx.x y) 
  λy.(λf.x x) y 
  (λx.x x)(λx.x x) 
  (λx.(λy.λz.z y) x) p (λx.x) 
  (λf.λx.f (f x)) (λf.λx.f (f x)) f x

三、实现下面这个 Haskell 函数，返回λ项中所有满足 redex 条件的子项；如果不存在 redex，则返回空表。

  redexes :: Term -> [Term]

四、对一个λ项 M 或其子项进行零或多次β归约得到 N，可以简写为 M =>* N。请实现以下 Haskell 函数，对给定的λ项进行多次规约，直到结果不存在 redex 为止，返回最终的λ项。

  reduce :: Term -> Term

五、在实现 redexes 和 reduce 这两个函数的过程中，有什么通用的代码是可以复用的？能做得更好吗？

HaskellCNOrg / haskellcn

手把手教你做λ（八）替换与归约 by ninegua #137

习题