Fork me on GitHub

手把手教你做λ(八)替换与归约

本系列教程:

在上一章我们通过引入α变换学习了关于λ表达式的等价关系,准确说,是等价关系之一。但是α变换本身仅仅是替换了变元的名字,并没有改变一个λ表达式的结构,或者变元的绑定关系。如果在不改变变元绑定关系的前提下,还想改变结构的话,那么就需要把“替换(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] 的话则是参数齐全的表达式了。写成 _[_:=_] 其实也可以看作是这个函数的名字,就像三角函数 sincos 这样的名字,只不过是用符号,而不是英文来表示。

第一个例子 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 函数,会发现:

  1. 首先是它们的函数类型不同,因为 subT 是要把 Var 替换成 Term
  2. 其次,它们在对 Term 这个代数类型的三个分支的处理上很类似,主要的差别是当 Lam v e 里面的 v 不等于 u 的时候,如何处理关于子项 e 的递归替换:

    1. 我们先做一个条件检查,当 w 的自由变元中不包括 v 时,不存在原本自由的变元被意外绑定的情况,所以可以直接递归处理子项 e
    2. 而当意外绑定有可能发生时,则需要对 Lam v e 做α变换,用一个新变元 x 来替代 v。选取这样一个 x 需要满足以下两个条件:

      1. x 对于 e 来说是一个“新”的不曾出现过的变元,这个条件和α变换所需的条件是一样的;
      2. w 的自由变元不包括 x,以避免在 w 的自由变元被这里α变换时引入的 x 意外绑定。

鉴于前文已经给出了 freeVars 函数的实现,另外两个辅助函数 boundVarsfreshVar 就留待读者自行定义(见习题一)。

在替换操作的基础上,λ演算定义了一个化简λ表达式的方法,叫做β规约(β-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 函数 boundVarfreshVar。使得 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 这两个函数的过程中,有什么通用的代码是可以复用的?能做得更好吗?

Submitted by at 11 months ago

所有回复

习题所需程序可以去 github 下载 https://github.com/ninegua/lambda-viewer/blob/master/program/prog-08.hs

ninegua 11 months ago