Fork me on GitHub

手把手教你做λ(七)从形式语义到等价关系

本系列教程:

之前我们只是从语法角度解决了如何打印与识别λ表达式,现在我们可以进一步学习它所表达的含义,也即λ表达式的语义。所谓语义(semantics),简单讲就是如何来理解一件事情。而我们这里说的“事情”,就是λ表达式,在研究语义的时候,我们称之为目标语言(object language)。

形式化语义(formal semantics)就是通过形式化的方法(formal methods)来明确和制定一个目标语言所表达的语义。常用的方法有三种:

  1. 操作语义(operational semantics):通过将目标语言分解成一系列的操作步骤来理解它是做什么的。这里隐含的一个条件是,先要假定有一个抽象机(abstract machine),以及与之伴随的一系列操作指令,这样才能够通过理解目标语言所对映的操作来理解它在计算什么。

  2. 指称语义(denotational semantics):将目标语言翻译成元语言(meta language),通常这个元语言是我们用的数学语言,比如函数啊集合啊之类的。假定我们已经理解了元语言,那么通过指称语义就可以理解目标语言所表达的是什么了。这里重要的是弄清楚所指称的到底时什么。

  3. 公理语义(axiomatic semantics):我们先假定针对目标语言有几条恒真的公理,然后通过数理逻辑来进一步理解这个目标语言里面都能够证明些什么。公理能够给出的一种最基本判断,就是等价关系(equivalence)。以公理和衍生的定理为基础,我们就可以进一步判断两种在字面上不同的表达是否等价,从而理解在这个目标语言里什么是相同的什么是不同的。

通常而言,从操作到指称到公理,理解或者定义一个目标语言所需要的辅助工具越来越少,也意味着语义越来越抽象。最后在公理语义里,只剩下基于公理的命题判断,而将计算的细节(比如时间空间复杂度)全部忽略掉了。从语义学的角度,越是能够发现不同之处,就越具体(concrete),而反之,则越抽象(abstract)。

举一个极端 concrete 的例子,我们可以说两个表达式看起来字面上(lexical)不一样,那它们就不一样。但这样一来,所有的理解就都停留在字面上,没有价值(trivial)。反方向极端 abstract 例子,则是所有表达式都等价,都是一个意思。那这样的话,这个语言存在大量冗余(redundant),只留下一个符号不就好了吗?所以,对其中不同分寸的把握,也促成了不同的语义定义。而通过采用不同的形式化方法,则能够从多个层面来解释我们的目标语言,帮助理解。

回到λ表达式,在正式介绍它的公理语义之前,我们首先引入两个概念,用于进一步分析它的结构。第一个概念是关于变元的绑定(binding)。在 λx.M 中,紧跟λ符号之后的 x,叫形式参数(formal parameter)简称形参。所有出现在 M 里的 x,都被当前这个λ的形参 x 所绑定,除非还有内层的λ抽象也绑定了 x。例如在 λx.(x (λy.(x (λx.x)))) 里面,只有第二和第三个 x 是被第一个 x(形参)绑定。

绑定的概念也可以换一种说法:一个变元只被当前或外层离它最近的同名形参所绑定。被绑定有时候也叫做被捕捉(captured)。与绑定相对应的是自由变元(free variable):一个λ项中没有被任何形参绑定的变元就是自由的。我们可以定义一个函数,来找出一个λ项中所有的自由变元:

freeVars :: Term -> [Var]
freeVars = aux []
  where
    aux env (Var v) | elem v env = [] 
                    | otherwise  = [v]
    aux env (Lam v e) = aux (v:env) e
    aux env (App f e) = aux env f ++ aux env e

在上面这个程序里,我们定义了一个辅助函数 aux 来遍历整个λ项的结构,并把其中所有自由变元作为一个列表返回。这有点类似我们在第三章里学习的 show 函数,同样是基于归纳法的递归函数。与 show 函数不同,aux 还传递了一个 env 变量,用于记录已经被绑定的变元们,当然这相对于当前遍历位置而言的。我们可以看到,在 Var 分支的时候,只要是没有被当前的 env 记录,就被作为自由变元返回;而在 Lam 分支里,当前抽象结构所引入的行参,被加入到 env 里面去遍历下一层的λ项;对 App 分支的处理,则是简单地把两个子项的自由变元合并返回,这里用的是 ++ 列表衔接,所以最终结果可能会有同一个变元多次出现,如果要避免这种情况,可以改用 union 函数,它是 Prelude 里面给出的并集操作。

另外值得一提的是,我们用于记录绑定变元集合的变元取名叫 env,意指环境,而不是用状态(state)命名。这是一种在函数编程中约定俗成的风格,环境随递归改变,但环境的改变仅影响关于子项的递归;状态也随递归改变,但状态的改变直接影响之后所有的递归过程。因此状态不能仅仅作为参数传递,还必须作为返回值的一部分从子递归返回到当前的层级。能够正确区分实现一个函数所需的环境和状态,是函数编程当中重要的一环,也是必不可少的训练。

有了变元绑定和自由的概念,接下来我们将引入一个概念叫做α变换(α-conversion)。它是对λ项进行如下操作,把某个形参以及所有它绑定的变元全都替换成一个“新”的变元。比如 (λx.y x) x 就可以通过α变换得到 (λz.y z) x,这个变换的过程简写为 (λx.y x) => (λz. y z) x,其中 => 代表做一次α变换。 α变换不改变λ项代表的意思,这也叫做α等价(α-equivalence),这是我们接触到的第一条关于λ项的等价关系。

α变换涉及到一个相关的操作,就是如何对一个λ项里面某个自由变元做替换操作。在这个操作过程中,我们只要注意不要把被绑定的变元替换掉就好了:

subV :: Var -> Var -> Term -> Term
subV u w (Var v)   | v == u    = Var w
                   | otherwise = Var v
subV u w (Lam v e) | v == u    = Lam v e
                   | otherwise = Lam v (subV u w e)
subV u w (App f e) = App (subV u w f) 
                         (subV u w e)

同样,subV 是一个基于归纳法的递归操作,在遇到 Lam 分支时,如果需要替换的变元 u 与此时被引入的型参 v 同名,那么根本不需要对子项进行替换操作,因为子项里的同名变元都被当前的λ绑定了。

最后,我们回到公理语义上来,我们可以把α等价当做是一条公理,这样我们就有了判别等价关系的依据。我们也可以先给出等价关系的定义,然后试图证明α变换满足等价关系。常见的等价关系(用 = 表示),就是满足三个条件,自反 reflexive (M=M),对称symmetric(可以由 M=N 推导出 N=M),传递transitive(可以由 L=MM=N 推导出 L=N)。而α变换则可以被证明满足对称性和传递性。

α等价的一个引申意义是说,λ项中变元的命名不重要,重要的是它的绑定关系。绝大多数的结构化现代程序语言,都符合这个规律,但鲜少有语言正式给出相应的规则和定义。我们通过学习λ演算,正是要借由公理语义,等价关系,以及α变换,来厘清其中的来龙去脉。

习题

一、判断以下λ项中,从左往右第一个抽象里的形参都绑定了哪些变元?请用引号标出,比如 (λx.y "x") x

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

二、判断以下λ项中,哪些变元是自由的?请用引号标出,比如 (λx."y" x) "x"

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

三、判断以下的λ项是否为α等价?实现一个函数 alphaEq :: Term -> Term -> Bool 来完成这件事。

  λx.λx.x 和 λy.λx.y
  λf.λx.f (λy.f x) 和 λf.λy.f (λy.f x) 
  λx.λy.x y 和 λy.λx.y x 
  λx.x λx.(λx.x) x 和 λx.x λy.(λx.x) y

四、在本章给出的α变换的定义中,我们注意到有一个条件就是要替换为“新”(也即原λ项中没有出现过)的变元,实际上这个条件其实过于严格(充分非必要),什么才是一个恰到好处的(充要)条件呢?

Submitted by at a year ago

所有回复

同样,文章和习题源码可以从 github: lambda-viewer 下载。

ninegua a year ago

或者到 pastie 获取本章所需程序 http://pastie.org/10369840

ninegua a year ago

新添加了程序自动测试,比如将 prog-07.hs 录入 GHCi :

ghci prog-07.hs
*Main> quickCheck propAlpha 
*** Failed! Exception: 'Expect False, but alphaEq (((λa.l) k)) (((λl.l) k)) is True' (after 3 tests and 2 shrinks): 
0
0
((λw.l) k)

ninegua a year ago

相隔有点久,前面的内容都忘的差不多。 --|

wuhaisheng a year ago