本文介绍了 'lambda 演算'.
演算的概念
在Lambda演算中，我们所做的演算是通过一定的机械规则将一个lambda term 转化为另一个lambda term，这个转化过程就称为lambda calculus广义上来说，对于任何一个发展变化的数学(或物理)系统，只要赋于它的状态以一定的语义，将它从一个状态变换到另一个状态，这个变化过程就是一个演算过程。
比如我们经常做的加法运算：2+13=15,这就是在PA系统中做的演算。我们做数学证明，就是在形式化的公理系统中进行逻辑推导的演算。我们写程序，就 是在图灵机上做演算。一段程序的指令序列就描述了一个演算过程。我们说话，写字，就是在自然语言上做演算。强人工智能主义者认为：人类思考问题，也是在做 某种演算。
在经典的计算理论中，演算的最重要的性质就是机械性，这是“演算”的强大威力所在，也是其局限性所在。但是如果把演算的概念扩展到物理世界中，有可能能突破机械性的局限(量子图灵机)。
起源
在十八世纪初，现代数学取得了辉煌的成果。其中G. W. Leibniz (1646 -- 1716)是当时的杰出者，他是微积分学的创始人之一。作为数学家和哲学家，他为推动现代逻辑的发展也作出过重大的贡献。 Leibniz曾有一个宏伟的理想：（1）建立一个通用语言，使得所有的问题能在其中表述；以及（2）找出一种判定方法，解答所有在通用语言中表述的问 题。
人们为实现这一理想付出了很多努力，直至二十世纪才出现一些重要成果。谓词逻辑和集合论的建立实际上完成了Leibniz的第一条理想，这归功于一些一流的数学家，Frege, Cantor, Russell, Hilbert 和 Godel。Leibniz的第二个理想成为了一个哲学问题：“是否存在一个通用的判定方法求解所有用通用语言表述的问题呢？”这就是所谓的Entscheidungsproblem（德语，意思是“判定问题”）。
在1936年，A Church（这家伙就是McCarthy的导师）和Alan Turing独立地给出了这个问题的否定答案。为了解决此问题，他们以 不同的方式形式化定义了“可判定”的概念（或者“可计算”的概念）。事实上他们给出了两种不同的计算模型：Turing发明了一组机器---Turing 机，并以此定义可计算性；Church发明了一个形式系统---lambda演算，并以此定义了可计算性。后来证明，图灵机和lambda演算其实是等价 的。就这样，λ-演算问世了。
Lambda 演算对函数式程序设计Functional Programming有巨大的影响，特别是Lisp语言的精髓。
非形式化描述
在 lambda 演算中，每个表达式都代表一个只有单独参数的函数，这个函数的参数本身也是一个只有单一参数的函数，同时，函数的值是又一个只有单一参数的函数。函数是通过 lambda 表达式匿名地定义的，这个表达式说明了此函数将对其参数进行什么操作。lambda演算所以不考虑多元函数的情况，因为多元函数可通过重复作用一元函数的运算而得到。
λ-演算有两种基本运算：“作用(Application)”与“抽象(Abstract)”。
作用：表达式 FA 表示对象 F 作用于对象 A，FA 既可被理解为计算 FA 的过程， 也可被理解为此过程的输出。λ-演算是无类型系统，从而自作用 FF 是合 法的，这将模拟递归。
抽象：在抽象运算中，记号λ将被引入。对于数学式x^2，λx. x^2 表示函数 x |→ x^2，通俗一点的表示，λx.x^2就是函数f(x)=x^2,当然，也可以认为是f(y)=y^2，参数的取名并不重要。
一般来说，若 M[x] 为表达式，则 λx. M[x] 表示函数 x |→ M[x]。
把作用与抽象结合起来就有如下方程 (λx. M[x])N = M[N]
这一方程便是所谓的β-变换。这里 M[N] 通常写成 M[x:=N]，表示在M中将所有“自由出现”的 x 替换为 N 所得到的结果（事实上替换过程中 N 的表达式也可能要改变，这一点将在后面详细说明）。
形式化定义（这一节是完全的数学方式的表达，很头痛的东西，我不太能够认真地看下去，所以这部分我完全摘抄其它文章：P）
【定义1】λ-演算的字母表由以下组成：
●变元集合：Δ = {v, v', v'', v''', …}, Δ无穷
●抽象算子：λ
●括号：(, )
【定义2】λ-项的集合Λ归纳定义为满足以下条件的最小集合：
● x ∈Δ → x ∈ Λ
● M, N ∈Λ → (MN) ∈ Λ
● M ∈Λ, x ∈Δ → (λx M) ∈ Λ
若用BNF(Backus Normal Form)表示，则有
Δ ::= v | Δ'
Λ ::= Δ | (ΛΛ) | (λΔΛ)
【定义3】我们做以下约定：
● x, y, z, … 表示任意变元；
● M, N, L, … 表示任意λ项；
● M ≡ N 表示M和N语法恒同；
● 通常采用以下省略括号表示法：
(i) F M_1 M_2 … M_n ≡ (…((F M_1) M_2)…M_n) (左结合)
(ii) λx_1x_2…x_n. M ≡ (λ x_1 (λ x_2 (…(λx_n M)…) ) )
● 设 P ≡ M N_1 N_2 … N_k (k ≥ 0)，当k=0时，P ≡ M;
设 P ≡ λx_1x_2…x_k. M (k ≥ 0)，当k=0时，P ≡ M。
【定义4】设M ∈ Λ，M的长度ρ(M)被定义为M中变元出现的次数，即
● ρ(x) = 1, x ∈Δ
● ρ(MN) = ρ(M) + ρ(N)
● ρ(λx. M) = ρ(M) + 1
以后我们说对M的结构作归纳是指对M的长度ρ(M)作归纳，这是自然数上的归纳。
【定义5】设M∈Λ，对M的结构作归纳，定义M的子项集合Sub(M)如下：
● Sub(x) = {x} , x ∈Δ
● Sub(N_1 N_2) = Sub(N_1) ∪ Sub(N_2) ∪ { N_1N_2 }
● Sub(λx.N ) = Sub(N) ∪ {λx.N }
若N ∈ Sub(M)，则称N为M的子项。
例如：y为 λx.yy 的子项，但是x不是 λx.yy 的子项。
【定义6】设M ∈Λ，
● M 的自由变元集合 FV(M) 归纳定义如下：
FV(x) = {x}
FV(N_1N_2) = FV(N1) ∪ FV(N_2)
FV(λx.N ) = FV(N) - {x}
● 若x出现于M中，且x不属于FV(M)，则称x是约束的。
● 若FV(M)为空集，则称M为闭λ-项（或组合子），且记全体闭λ-项的集合为 Λ* 。
例如 M ≡ λx. yxy ，则其中x 是约束变元，y是自由变元。N ≡ λxy. yxy 是一个闭λ-项。
事实上约束变元和自由变元的概念在数学的其他领域也出现过，例如在微积分中
∫(3xy+x-y) dx
这里dx其实就表明在3xy+x-y中x是约束变元。
【定义7】上下文(Contexts)
λ上下文集合C[]定义为满足下列条件的最小集合：
● x ∈C[]
● [] ∈ C[]
● C_1[], C_2[] ∈ C[] → (C_1[]C_2[]) ∈ C[]
● C_1[] ∈ C[] → (λx. C_1[]) ∈ C[]
上下文中的空白用一个[]表示。引入上下文的概念是为了方便以后的讨论。
例如
C_1[] = (λx. []x) M
则
C_1[λy.y] = (λx. (λy.y) x) M
换句话说，C_1[N] 就是把 C_1[] 中的 [] 出现的地方都填入 N。这种填入替换和前面说的 M[x:=N] 不同，M[x:=N] 要把M中所有自由出现的x替换成N， 并且N本身可能也会适当地改变。但是C_1[N]的替换则是把所有的[]都换成N，且N不做任何改变。
另外需要注意的是，FV[M]中的变元在 C[M] 中可能会变成约束变元。
lambda演算的公理化系统
形式理论λβ由以下的公理和规则组成。这7条规则是lambda演算中最重要的部分，体现了演算的逻辑性和机械性。我们可以把lambda的函数看作是一 个有机体，这些规则就类似于有机体中分子与分子结合的方式，有机体通过这些组合方式可以无限的繁衍，并且无论如何繁衍，最终都还是这种有机体。因此，对于 一个可计算的问题，无论它有多么困难，理论上都有一个足够长的函数能够把它表示出来。
公理：
(ρ) M ＝ M
(β) (λx. M) N = M[x:=N]
规则：
M = N
(σ) ---------------
N = M
M = N, N = L
(τ) ---------------
M = L
M = N
(μ) ---------------
ZM = ZN
M = N
(ν) ---------------
MZ = NZ
M = N
(ξ) ---------------
λx.M = λx.N
公式 M = N 在λβ中可记为λβ|- M = N，有时简记为 M = N，
这时称M可β转换于N。
上面的公理和规则的名称来源于 Curry[1958]。
β变换
β替换有两个基本原则：
1。M[x:=N] 只能把M中自由出现的x替换为N；
2。原来在N中自由出现的变元，在M[x:=N] 的结果中也应该保持自由。
下面将分别对这两个原则进行描述。
1。M[x:=N] 只能把M中自由出现的x替换为N
上述公理系统中的β公理其实就是λ演算中的作用（Application）过程。从计算机程序设计的角度来看，任何一个λ项都可以看作是一段子程序，λx. M 就表示该子程序的输入参数是x，而 (λx. M) N 则表示把N作为参数x带入到子程序M中进行计算。M本身的语法形式描述了M的计算过程，因而只需要把M中所有“自由出现”的x替换成N即可得到计算结果。注意，这里一直强调要替换“自由出现”的x，下面我们举一个例子来说明这一点。
假设我们已经在λ演算中定义了加减乘除运算，设
L ≡ λx. (y + x)
M ≡ L (x * x)
则
(λx. M) t ≡ (λx. L(x*x) ) t
≡ (λx. (λx. (y + x)) (x*x) ) t
= (λx. (y + x))(t*t)
= y + t*t
注意其中第一个＝号处不能把(λx. (y + x))中的x替换成t，因为(λx. (y + x))中的x是约束的，如果把(λx. (y + x))中的x也换成t的话，将得到
(λx. M) t ≡ (λx. (λx. (y + x)) (x*x) ) t
= (λx. (y + t)) (t*t)
= y + t
在计算第二个等号的时候约束变元x在 (y + t)中没有出现，所以实际上并没有做任何替换，只是简单地浪费掉一个参数(t*t)，最后得到结果y+t。但这个替换的结果并非我们所希望的。
从程序设计的角度来看，λx. M 相当于一段子程序，"λx."说明了子程序M的输入参数是x，M中除了x以外的其他自由变量都相当于子程序中的全局变量。
因此在λ演算中规定 M[x:=N] 只能把M中“自由出现”的x换成N。
2。原来在N中自由出现的变元，在M[x:=N] 的结果中也应该保持自由（俺不懂PASCAL，所以这里完全照抄了）
请看下面的例子：
设
L ≡ y + x
M ≡λy. L ≡ λy. (y + x)
则
(λx.M)y = M[x:=y] ≠ λy. y + y
我们还是用PASCAL语言为例来说明这点。
M就相当于以下的函数（在下面例子中我们扩展一下PASCAL的语法，让其函数返回值也可以为一个函数）：
program Example_2;
var
y, z: integer;
function M(x: integer): function; // M的返回值也是一个function
function L(y: integer): integer; // L是M的子函数
begin
L := y + x;
end;
begin
M := L;
end;
begin
readln(y, z);
writeln( M(y)(z) );
end.
上面例子中M的返回值也是一个function，因此M(y)得到的是一个函数，M(y)(z)得到的才是一个函数值。
上述程序的正确输出应该是z+y。在调用了M(y)以后，函数M返回的是一个函数L，且因为L是M的子函数，L中的x就是M的参数x，他的值应该等于y，不过L本身的参数名字也叫做y，如果不加区分就会搞混淆。一种错误的计算过程如下：先计算M(y)，得到一个函数
function L(y: integer): integer;
begin
L := y + y;
end;
然后计算L(z)，得到z+z。这个结果是错误的，这就是对局部变元和全局变元不加区分的结果。
当然如果让计算机来执行这个程序它是不会搞错的，因为编译器采用了一个叫做“名字空间”的方法，每个变元名前面都会加上名字空间。具体而言，在编译器看来，函数M应该是下面这个样子的
function M(M_x : integer): function;
function M_L(M_L_y: integer): integer;
begin
M_L := M_L_y + M_x ;
end;
begin
M := M_L;
end;
计算机计算M(y)(z)的时候，先计算M(y)，得到一个函数
function M_L(M_L_y: integer):integer;
begin
L := M_L_y + y
end;
然后计算 M_L(z)，得到 z + y。这个结果是正确的。
其实编译器所采用的这个方法就是把函数中所有出现过的变元名，函数名都加上一个前缀，这个前缀是这个函数本身的名字空间。主程序的名字空间就是空字符串， 主程序的子函数M的名字空间就是"M_"，M的子函数L的名字空间是L的父函数M的名字空间加上L自己的名字，即"M_L_"。这样就永远不会出现局部变 元和全局变元同名的问题了。
不过作为程序员来说，为了让程序更便于理解，需要自己来手工地给函数L的参数改名。例如可以把M改为下面的形式
function M(x: integer): function;
function L(y1: integer): integer; // 把L的参数命名为y1
begin
L := y1 + x;
end;
begin
M := L;
end;
这样在计算M(y)(z)的时候就不会搞错了。
下面我们回到λ演算中来。在λ演算中也会有这种问题。
设
L ≡ y + x
M ≡λy. L ≡ λy. (y + x)
则
(λx.M)y = M[x:=y] ≡ (λy. (y + x))[x:=y] ≠ λy. y + y
这就和刚才的计算过程一样，如果不做任何处理地直接将(λy. (y + x))中的x换为y，则会导致原来自由的y在替换后变为约束的，这就产生了错误。
原来自由出现的变元在β替换以后变成了约束的，这种现象就叫做“variable capture”。
解决“variable capture”的方法也和程序设计中一样，只要把M中的约束变元y改一个名字就可以了。这其实是基于这样一种思想：把函数中的参数或局部变元名字改变， 函数的功能仍然保持不变。但在λ-演算，我们需要把这种思想形式化地定义出来。在Curry的著作以及其他一些λ-演算的著作中，公理
(α) λx.M = λy. M[x:=y] 这里y不出现于M中
被加入形式理论λβ中。这条α公理就是为了处理变元改名而引入的。
