Lambda演算学习笔记.doc

前言blog好久没有更新了，上次更新还是4月28号。这段时间实在是很忙，4月的最后一周为了赶一篇论文，累死累活，最后在tom的帮助下总算在4月30号截稿之前完成了。4月29号的晚上一直改到了第二天凌晨3点才睡。4月30号下午回家，可是没有料到长沙的八一路修路，路上堵车。打的从学校到火车站花了40分钟，平时只要15分钟的。于是在最后10分钟一路狂奔，终于在开车前1分钟上车了。五一长假的第一天去了双峰山，云雾缭绕之中真的颇有几分气势，可惜数码照片全部都拍得很模糊，早知道我就自己动手好了。五一归来马上开始整理软件工程相关资料，一共花了3天时间，还剩软件标准化的部分没有整理完毕。接下来的三天，一直在学习lambda演算的相关内容，由于资料不全，学习的过程很是痛苦。国内的大学好像基本上不开设Functional Programming课程，因此FP的基础知识lambda演算也讲得很少。不过好歹在网上找到了一些资料，加上数理逻辑中的少量介绍，明白了一个大致。相关资料网址会列在最后。Lamda演算简介Wikipedia（维基百科全书）中关于lambda演算的解释如下：The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what a computable function is. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.Lambda演算是一个形式系统，它被设计出来用来研究函数定义，函数应用和递归。它是在二十世纪三十年代由Alonzo Church 和 Stephen Cole Kleene发明的。Church在1936年使用lambda演算来证明了判定问题是没有答案的。Lambda演算可以用来清晰的定义什么是一个可计算的函数。两个lambda演算表达式是否相等的问题不能够被一个通用的算法解决，这是第一个问题，它甚至排在停机问题之前。为了证明停机问题是没有答案的，不可判定性能够被证明。Lambda演算对于函数式编程语言（例如lisp）有重大的影响。同时，数理逻辑中对于lambda演算的介绍就简单得多：-演算可以说是最简单、最小的一个形式系统。它是在二十世纪三十年代由Alonzo Church 和 Stephen Cole Kleene发明的。至今，在欧洲得到了广泛的发展。可以说，欧洲的计算机科学是从-演算开始的，而现在仍然是欧洲计算机科学的基础，首先它是函数式程序理论的基础，而后，在-演算的基础上，发展起来的-演算、-演算，成为近年来的并发程序的理论工具之一，许多经典的并发程序模型就是以-演算为框架的。这里不由得想起一位我尊敬的老师的博士毕业论文就是关于-演算的，可惜这位老师已经去别的学校了。Lambda演算表达了两个计算机计算中最基本的概念“代入”和“置换”。“代入”我们一般理解为函数调用，或者是用实参代替函数中的形参；“置换”我们一般理解为变量换名规则。后面会讲到，“代入”就是用lambda演算中的-归约概念。而“替换”就是lambda演算中的-变换。Lambda演算系统的形式化定义维基百科全书上面的对于lambda演算的定义不是很正规，但是说明性的文字较多。而数理逻辑中的定义很严密，不过没有说明不容易理解。我尽可能把所有资料结合起来说明lambda演算系统的定义。字母表lambda演算系统中合法的字符如下：1. x1，x2，x3，变元（变元的数量是无穷的，不能在有限步骤内穷举，这个很重要，后面有定理是根据这一点证明的）2. 归约3. 等价4. ，（，） （辅助工具符号，一共有三个，和左括号右括号）所有能够在lambda演算系统中出现的合法符号只有以上四种，其他符号都是非法的。例如x.x+2，如果没有其他对于符号的说明，那么这就是一个非法的演算表达式。-项-项在一些文章中也称为表达式（lambda expression），它是由上面字母表中的合法字符组成的表达式，合法的表达式组成规则如下：1. 任一个变元是一个项2. 若M，N是项，则（MN）也是一个项 （function application，函数应用）3. 若M是一个项，而x是一个变元，则（x.M）也是一个项 （function abstraction，函数抽象）4. 仅仅由以上规则归纳定义得到的符号串是项说明1：-项是左结合的，意思就是若f x y都是-项，那么f x y(f x) y说明2：(x.M)这样的-项被称为函数抽象，原因是它常常就是一个函数的定义，函数的参数就是变量x，函数体就是M，而函数名称则是匿名的。用一个不恰当的比喻来说，我们通常认为的函数f(x)=x+2，可以被表达为x.x+2。因为是未定义的，所以这个比喻只是为了方便理解而已。说明3：MN这样的-项被称为函数应用，原因是它表达了将M这个函数应用到N这个概念。沿用上面的例子f(x)=x+2，那么f(2)=2+2；同样的x.x+2表达了f(x)的概念，那么（x.x+2）2表达了f(2)的概念。其中Mx.x+2，N2，所以MN（x.x+2）2。说明4：注意说明3只是为了方便理解，但是还存在很多与直观理解不符合的地方。例如xy也是一个合法的-项，它们也是MN形式的，不过x和y都仅仅是一个变量而已，谈不上函数代入。 上面是-项的形式化定义，有一些是可以与函数理论直观联系的，而另一些只是说明这个-项是合法的，不一定有直观的字面意义。公式 若M，N是-项，则MN，M=N是公式。-项中的变量自由出现法则在一个-项中，变量要么是自由出现的，要么是被一个符号绑定的。还是以函数的方式来理解变量的自由出现和绑定。例如f(x)=xy这个函数，我们知道x是和函数f相关的，因为它是f的形参，而y则是和f无关的。那么在x.xy这个-项中，x就是被绑定的，而y则是自由出现的变量。直观的理解，被绑定的变量就是作为某个函数形参的变量，而自由变量则是不作为任何函数形参的变量。Lambda变量绑定规则：1. 在表达式x中，如果x本身就是一个变量，那么x就是一个单独的自由出现。2. 在表达式 x. E中，自由出现就是E中所有的除了x的自由出现。这种情况下在E中所有x的出现都称为被表达式中x前面的那个所绑定。3. 在表达式(MN )中，变量的自由出现就是M和N中所有变量的自由出现。另一种关于变量的自由出现的规则也许更直接：1. free(x) = x2. free(MN) = free(M) free(N) 3. free(lx M) = free(M) x为什么要花大力气来给出变量自由出现的规则，是因为后面的很多地方要用到变量的自由出现的概念。例如-变换和-归约。例子：分析f.x.fx中变量的自由出现和绑定状况。f.x.fx =f.E, E=x.fx E=x.A, A=A1A2, A1=f, A2=x所以在A中f和x都是自由出现的，所以E中x是绑定 x所以整个公式中f是绑定第一个 f的。 x的控制域来看两个-项，x.xx和x.(xx)有何不同？根据左结合的法则，x.xx(x.x)x，其中第一个x是被绑定的，而第二个x则是自由出现的。而x.(xx)中两个x都是被绑定的。这表明了两个-项中x的控制域是不同的。我们知道谓词演算中量词也是有控制域的，x的控制域与它们类似，这里就不给出详细的定义了。其实也很直观。-变换（-conversion）-变换规则试图解释这样一个概念，演算中约束变量的名称是不重要的，例如x.x和y.y是相同的函数。因此，将某个函数中的所有约束变量全部换名是可以的。但是，换名需要遵循一些约束。首先是一个说明：如果M，N是-项，x在M中有自由出现，若以N置换M中所有x的自由出现（M中可能含有x的约束出现），我们得到另一个-项，记为Mx/N。-变换规则如下：x.M=y.Mx/y 如果y没有在M中自由出现，并且只要y替换M中的x，都不会被M中的一个绑定。例子：x.( x.x)x = y(x.x)y-变换主要用来表达函数中的变量换名规则，需要注意的是被换名的只能是M（函数体）中变量的自由出现。-归约-归约表达的是函数应用或者函数代入的概念。前面提到MN是合法的-项，那么MN的含义是将M应用到N，通俗的说是将N作为实参代替M中的约束变量，也就是形参。-归约的规则如下：(x.M)N Mx/N 如果N中所有变量的自由出现都在Mx/N中保持自由出现-归约是演算中最重要的概念和规则，它是函数代入这个概念的形式化表示。一些例子如下：(lx.ly.y x)(lz.u) ly.y(lz.u)(lx. x x)(lz.u) (lz.u) (lz.u)(ly.y a)(lx. x)(lz.(lu.u) z) (ly.y a)(lz.(lu.u) z)(ly.y a)(lx. x)(lz.(lu.u) z) (ly.y a)(lx. x)(lz. z)(ly.y a)(lx. x)(lz.(lu.u) z) (lx. x)(lz.(lu.u) z) a需要多加练习才能习惯这种归约。-变换（-conversion）-变换表达了“外延性”（extensionality）的概念，在这种上下文中，两个函数被认为是相等的“当且仅当”对于所有的参数，它们都给出同样的结果。我理解为，对于所有的实参，通过-归约都能得到同样的-项，或者使用-变换进行换名后得到同样的-项。例如x.fx与f相等，如果x没有在f中自由出现。演算的公理和规则组成这一段来自数理逻辑与集合论（第二版 清华大学出版社）。还修正了其中的一个错误。1. (x.M)N Mx/N 如果N中所有变量的自由出现都在Mx/N中保持自由出现2. MM3. MN, NL = ML （原书中此处错误）4. MM=ZMZM5. MM=MZMZ6. MM=x. M x. M7. MM=M=M8. M=M=M=M9. M=N,N=L=M=L10. M=M = ZM = ZM11. M=M = MZ = MZ12. M=M =x. M =x. M如果某一公式MN或者M=N可以用以上的公理推出，则记为MN和MN。范式如果一个-项M中不含有任何形为(x.N1)N2)的子项，则称M是一个范式，简记为n.f.。如果一个-项M通过有穷步-归约后，得到一个范式，则称M有n.f.，没有n.f.的-项称为n.n.f.。 通俗的说法是，将一个-项进行-归约，也就是进行实参代入形参的过程，如果通过有穷步代入，可以得到一个不能够再进行代入的-项，那么这就是它的范式。如果无论怎样代入，总存在可以继续代入的子项，那么它就没有范式。例子M = x.(x(y.y)x)y，则M y(y.y)y) yy。M有一个n.f.。例子M =x.(xx) x.(xx)，则Mx.(xx) x.(xx)=M。注意到M的归约只有唯一的一个可能路径，所以M不可能归约到n.f.。所以M是n.n.f.。注意这个x.(xx) x.(xx)在演算的协调性研究中是一个比较经典的项。( x. x x) ( x. x x)被称为, ( x. x x x) ( x. x x x)被称为 2。不动点理论表示所有的-项组成的集合。定理：对于每一个F，存在M，使得FM=M。证明：定义wx.F(xx)，又令Mww，则有Mww(x.F(xx)wF(ww)=FM。证明是非常巧妙的，对于每个F，构造出的这个ww刚好是可以通过一次-归约得到F(ww)FM，如果再归约一次就得到F(FM)，这样可以无限次的归约下去得到F(F(F(F(FM)。Church-Rosser定理及其等价定理这两个定理告诉我们这样一个事实：如果M有一个n.f.，则这个n.f.是唯一的，任何-归约的路径都将终止，并且终止到这个n.f.。Church-Rosser定理：如果M=N，则对某一个Z，MZ并且NZ。与之等价的定理如下，Diamond Property定理：如果MN1,MN2，则存