前言
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)的概念。其中M＝λx.x+2，N＝2，所以MN＝（λx.x+2）2。
说明4：注意说明3只是为了方便理解，但是还存在很多与直观理解不符合的地方。例如xy也是一个合法的λ-项，它们也是MN形式的，不过x和y都仅仅是一个变量而已，谈不上函数代入。
上面是λ-项的形式化定义，有一些是可以与函数理论直观联系的，而另一些只是说明这个λ-项是合法的，不一定有直观的字面意义。
公式
若M，N是λ-项，则MàN，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) = x
2. 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的约束出现），我们得到另一个λ-项，记为M[x/N]。
α-变换规则如下：
λx.M=λy.M[x/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 à M[x/N] 如果N中所有变量的自由出现都在M[x/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 à M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现
2. MàM
3. MàN, NàL => MàL （原书中此处错误）
4. MàM’=>ZMàZM’
5. MàM’=>MZàM’Z
6. MàM’=>λx. M àλx. M’
7. MàM’=>M=M’
8. M=M’=>M’=M
9. M=N,N=L=>M=L
10. M=M’ => ZM = ZM’
11. M=M’ => MZ = M’Z
12. M=M’ =>λx. M =λx. M’
如果某一公式MàN或者M=N可以用以上的公理推出，则记为λ├MàN和λ├M＝N。
范式
如果一个λ-项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)，则Màλx.(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。
证明：定义w＝λx.F(xx)，又令M＝ww，则有λ├M＝ww＝(λx.F(xx))w＝F(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，λ├MàZ并且λ├NàZ。
与之等价的定理如下，
Diamond Property定理：如果MàN1,MàN2，则存在某一Z，使得N1àZ，N2àZ。
后记
最后两个定理的证明没有怎么看懂，所以没有在笔记中记下。另外，前天在网上订购的《程序设计语言：概念和结构》第二版刚刚拿到手，其中有关于λ演算的一章。应该也对我大有帮助，待看完再说。
学习λ演算的初衷是了解一些程序设计的最基本原理，没想到最后还是绕到形式系统和数理逻辑这儿来了。不过，形式化表达的λ演算更清晰。
国内大学虽然也开程序设计的课程，不过好像都是pascal，c/c++之类，关于程序设计的本质基础的程序好像并不多。随着大学扩招，中国有望在很短的时间内成为世界上程序员最多的国家，如果仅仅只学命令式和面向对象的程序设计，一定是不够的。函数式和逻辑式程序设计语言也是要学学的啊。
文中肯定有很多错漏，希望看出来的人给我留言。
参考文献
School of Computer Science and Software Engineering, Faculty of Information Technology, Monash University, Australia 3800
这个大学的FP课程中的Lambda演算相关部分
http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/
wikipedia中lambda演算相关介绍
http://en.wikipedia.org/wiki/Lambda_calculus
《数理逻辑与集合论》第二版 清华大学出版社