形式系统是一套符号化的系统，
这些符号，遵循了某些规则，
模型化了待研究的现实世界。
例如：
(lambda (x) x)
是由符号“(”，“)”，“lambda”和“x”构成的。
它们符合“S表达式”的语法规则，
以及Lisp函数调用的推导规则，
表示了一个数学函数f(a)=a。
区分符号和它指称的事物，
是很重要的。
我们要研究的这些符号构成了一种语言，
称为目标语言。
而符号所指称的事物也构成了一种语言，
称为元语言。
例如：
符号1，我们通常认为它是自然数1。
但这只是通俗的说法。
事实上，符号1，符号2，符号3，...属于目标语言范围，
而自然数1，自然数2，自然数3，...属于元语言范围。
符号1和自然数1是不同的，
如果愿意，我们当然可以用符号a表示自然数1。
λ演算——形式语法
λ演算系统，是一个形式系统，
用来研究编程语言。
在内容上，大体分为几个部分。
形式语法，公理语义，不动点，操作语义，指称语义。
形式语法，
用来说明合法表达式的组成方式。
定义如下：
M ::= x | MM | λx.M
这是一个递归定义，
它表示，在λ演算系统中，合法的表达式，
要么是一个变量x，
要么是一个函数调用（application），
要么是一个函数抽象（lambda abstraction）。
例如：如下表达式就是合法的，
x，变量x
(λx.x)5，函数调用
λx.y，函数抽象
我们看到合法的lambda表达式，
在语法上和Lisp中的S表达式很相似。
x <=> x
(λx.x)5 <=> ((lambda (x) x) 5)
λx.y <=> (lambda (x) y)
事实上，Lisp语言的语法，
确实受到了λ演算的影响。
在不影响歧义的情况下，
我们将采用Lisp语言来讨论λ演算。
因为，他们可以看做只是语法不同的两套形式系统。
λ演算——公理语义
公理语义，
是一套等式证明系统，
用来区分一个形式系统中的两个表达式，
是不是等价。
正如不同的语法规则，给出了不同的形式语言，
不同的等价性条件，给出了有不同公理语义的形式系统。
给λ演算添加不同的等价性规则，
会导致不同的λ演算系统。
最常用的两种等价规则是，
α等价，和β等价。
α等价指出，
函数的形参只是占位符，
替换形参和函数体中相应名字的符号，
所产生的新表达式与原表达式等价。
例如：
(lambda (x) x)和(lambda (y) y)
是等价的。
这里还没有谈到这两个表达式的指称语义。
无论这些符号指称什么，
在公理语义的约束下，都是等价的。
β等价指出，
函数调用表达式，等价于，
把函数体中的形参替换成实参后的表达式。
例如：
((lambda (x) (+ a x)) y)等价于(+ a y)
需要注意的是，
实参含有自由变量，
可能会与替换后环境中的绑定变量冲突。
例如：
(
(lambda (x)
(lambda (y)
(+ x y)))
(- a y)
)
如果我们单纯把形参x替换成(- a y)
结果如下：
(lambda (y)
(+ (- a y) y))
其中，函数体(+ (- a y) y)中，
第一个y就会被绑定的符号y所捕获。
这容易引起歧义，
因此，在这种情况下，我们需要为绑定变量更名。即，
(lambda (z)
(+ (- a y) z))
λ演算——不动点
我们看到λ演算中，所有函数都是匿名的，
这样在函数体内部引用函数本身，是很困难的事情。
例如，阶乘函数，
(define fact
(lambda (n)
(if (= n 1)
1
(* n (fact (- n 1))))))
函数内部引用了函数本身。
改写成等式形式，
fact = (lambda (n)
(if (= n 1)
1
(* n (fact (- n 1)))))
我们发现，在等式两边都出现了fact。
这使得我们回忆起了代数学中，
求解以下方程式。
x = G(x)。
其中，
G(f) = (lambda (n)
(if (= n 1)
1
(* n (f (- n 1)))))
或，
G = (lambda (f)
(lambda (n)
(if (= n 1)
1
(* n (f (- n 1))))))
待求取的函数fact，是这个方程的解。即，
fact = G(fact)。
我们称，方程x = G(x)的解为函数G的不动点。
那么这个方程有解吗？
幸运的是，人们已经找到了求解不动点的办法。
方法如下：
人们发现存在一个称为Y组合子（Y combinator）的函数，
可以得到任意函数G的不动点。即，
令x = YG，则x = G(x)
因此，上例中，
fact = YG
其中，
Y = (lambda (k)
((lambda (g) (g g))
(lambda (f)
(lambda (n)
((k (f f))
n)))))
这里需要注意，Y本身不是G的不动点，
YG才是。
λ演算——操作语义
操作语义，
是一套推导规则，
据此表达式可以规约成更简单的形式。
与等式证明系统不同的是，
推导规则具有方向性。
相同之处在于，
在不同个数规约规则的限制下，
得到了不同的λ演算系统。
最常用的规约规则，称为β规约。
它是β等价的有向形式。
记法如下：
((lambda (x) (+ a x)) y) -> (+ a y)
另外，某些表达式，β规约不可终止的。
例如：
(
(lambda (x)
(x x))
(lambda (x)
(x x))
)
->
(
(lambda (x)
(x x))
(lambda (x)
(x x))
)
-> ...
对于β规约可终止的表达式，人们发现，
按不同的次序，对表达式进行规约，
总是可以得到相同的最终表达式，
称为范式（normal form）。
这种性质，称为汇聚性（confluence）。
λ演算——指称语义
指称语义，
是通过为每一个表达式指定一个数学对象，
作为该表达式的指称，
来说明表达式语义的一种办法。
能这样做，是建立在语义合成性（compositionality）前提之下的。
即，表达式的语义，只由它的子表达式语义决定。
例如：
对于加法表达式，
(+ 1 2)
符号+，指称数学函数，加法函数，
符号1，指称自然数1，
符号2，指称自然数2。
整个表达式指称，自然数1与自然数2的加法操作。
记为： E[[+]] = 加法函数
E[[1]] = 自然数1
E[[2]] = 自然数2
E[[e1+e2]] = E[[e1]]+E[[e2]]
其中，等式右边的+表示自然数加法操作。
结语
λ演算虽然语法简单，但是内涵丰富，
这很符合Scheme语言的设计哲学。
从模型论的角度来看，
如果说物理学是对现实世界的建模，
那么程序设计语言，就是对计算的建模。
λ演算和其他编程语言一样，采用形式方法，
用满足特定规则的一组符号，
建立了计算模型。
图灵机，递归函数论等，采用了其他方式建模，
虽然复杂一些，但是与λ演算具有相同的计算能力。
λ演算很值得学习，
会了解到很多数学上的基础问题，
集合论，证明论，递归论，模型论，
都有不同程度的应用。