Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
freizl opened this Issue Apr 30, 2018 · 1 comment

Comments

Projects
None yet
1 participant
@freizl
Copy link
Member

freizl commented Apr 30, 2018

本系列教程:

在上一章我们通过引入α变换学习了关于λ表达式的等价关系,准确说,是等价关系之一。但是α变换本身仅仅是替换了变元的名字,并没有改变一个λ表达式的结构,或者变元的绑定关系。如果在不改变变元绑定关系的前提下,还想改变结构的话,那么就需要把“替换(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 的递归替换:
    a. 我们先做一个条件检查,当 w 的自由变元中不包括 v 时,不存在原本自由的变元被意外绑定的情况,所以可以直接递归处理子项 e
    b. 而当意外绑定有可能发生时,则需要对 Lam v e 做α变换,用一个新变元 x 来替代 v。选取这样一个 x 需要满足以下两个条件:
    i. x 对于 e 来说是一个“新”的不曾出现过的变元,这个条件和α变换所需的条件是一样的;
    ii. 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 这两个函数的过程中,有什么通用的代码是可以复用的?能做得更好吗?

@freizl freizl added the migration label Apr 30, 2018

@freizl

This comment has been minimized.

Copy link
Member Author

freizl commented Apr 30, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.