此文章来源于网络，是学习lambda演算过程的总结与复习，着重于探讨“为什么(Why)”与“怎么做(How)”，也希望能对看到它的人学习了解这个形式系统有些微帮助。由于之前看了不少wiki、tutorial、introduction之流，绝大多数读过之后仅知其然而不知其所以然，我不知道为什么它们都不解释为什么要这么做，为什么要有这些东西，这些东西是怎么得来的，但这个事实让我非常苦恼，因此才有了这个系列。我试图将自己的浅薄理解稍作阐释梳理，知之尚浅，如有错漏不妥之处请不吝指出，欢迎交流讨论批评建议。
NOTE: 在lambda演算中，函数是一等公民。即对函数做一般的基本操作都是合法的，比如把函数作为参数传入或返回，赋给一个变量等等。
lambda | λ 定义
要描述一个形式系统，我们首先需要约定用到的基本符号，对于本系列所介绍的lambda演算，其符号集包括λ . ()和变量名(x, y, z, etc.)。
- λ 表达式/项
在lambda演算中只有三种合法表达式（也可以称之为项：λ-expression or λ-term）存在：
变量(Variable)
形式：x
变量名可能是一个字符或字符串，它表示一个参数（形参）或者一个值（实参）。
e.g. z var
抽象(Abstraction)
形式：λx.M
它表示获取一个参数x并返回M的lambda函数，M是一个合法lambda表达式，且符号λ和.表示绑定变量x于该函数抽象的函数体M。简单来说就是表示一个形参为x的函数M。
e.g. λx.y λx.(λy.xy)
前者表示一个常量函数(constant function)，输出恒为y与输入无关；后者的输出是一个函数抽象λy.xy，输入可以是任意的lambda表达式。
注意：一个lambda函数的输入和输出也可以是函数。
应用(Application)
形式：M N
它表示将函数M应用于参数N，其中M、N均为合法lambda表达式。简单来说就是给函数M输入实参N。
e.g. (λx.x) y, (λx.x) (λx.x)
前者表示将函数λx.x应用于变量y，得到y；后者表示将函数λx.x应用于λx.x，得到λx.x。函数λx.x是一个恒等函数(identity function)，即输入恒等于输出，它可以用 I 来表示。
这时候可能就有人纳闷儿了，(λx.x) y意义很明确，但λy.xy为什么代表函数抽象而不是将函数λy.x应用于y的函数应用呢？为了消除类似的表达式歧义，可以多使用小括号，也有以下几个消歧约定可以参考：
一个函数抽象的函数体将尽最大可能向右扩展，即：λx.M N代表的是一个函数抽象λx.(M N)而非函数应用(λx.M) N。
函数应用是左结合的，即：M N P意为(M N) P而非M (N P)。
2. 自由变量和绑定变量
前面提到在函数抽象中，形参绑定于函数体，即形参是绑定变量，相对应地，不是绑定变量的自然就是自由变量。咱们来通过几个例子来理解这个关系：
λx.xy：其中x是绑定变量，y是自由变量；
(λy.y)(λx.xy)：这个表达式可以按括号划分为两个子表达式M和N，M的y是绑定变量，无自由变量，N的x是绑定变量，y是自由变量且与M无关；
λx.(λy.xyz)：这个表达式中的x绑定于外部表达式，y绑定于内部表达式，z是自由变量。
由于每个lambda函数都只有一个参数，因此也只有一个绑定变量，这个绑定变量随着形参的变化而变化。
我们用FV来表示一个lambda表达式中所有自由变量的集合，如：
FV(λx.xy) = {y}
FV((λy.y)(λx.xy)) = FV(λy.y) ∪ FV(λx.xy) = {y}
FV(λx.(λy.xyz)) = FV(λy.xyz) \ x = {x,z} \ x = {z}
3. 柯里化(Currying)
有时候我们的函数需要有多个参数，这太正常不过了，但是lambda函数只能有一个参数怎么办？解决这个问题的方法就是柯里化(Currying)。
柯里化是用于处理多参数输入情况的方法，我们已经知道一个lambda函数的输入和输出也可以是函数，那么基于它，可以把多参数函数和单参数函数做以下转换：
currying: λx y.xy = λx.(λy.xy)
外层函数接受一个参数x返回一个函数λy.xy，这个返回函数（内层函数）又接受一个参数y返回xy，x绑定于外层函数，y绑定于内层函数，这样我们就在满足lambda函数只接受一个参数的约束下实现了多参数函数的功能，这就是柯里化，而λx y.xy称为λx.(λy.xy)的缩写，为了方便表达，后续会常常出现λx y.xy这样的书写方式，需要谨记它只是缩写写法。
lambda | λ 归约
我们已经知道了lambda表达式的基本定义与语法，下面将介绍如何对一个lambda表达式进行归约(reduction)。
- beta | β 归约
对于一个函数应用(λx.x) y，它意为将函数应用λx.x应用于y，等价于x[x:=y]，即结果是y。在这个过程中，(λx.x) y ≡ x[x:=y]一步就叫做beta归约，x[x:=y] ≡ y一步称作替换(substitution)，[x:=y]意为将表达式中的自由变量x替换为y。
替换
形式：E[V := R]
意为将表达式E中的所有 “自由变量” V替换为表达式R。对于变量x,y和lambda表达式M,N，有以下规则：
x[x := N] ≡ N
y[x := N] ≡ y //注意 x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N] ≡ λx.M //注意 x 是绑定变量无法替换
(λy.M)[x := N] ≡ λy.(M[x := N]) //注意 x ≠ y, 且表达式N的自由变量中不包含 y 即 y ∉ FV(N)
beta归约
形式：β: ((λV.E) E′) ≡ E[V := E′]
其实就是用实参替换函数体中的形参，也就是函数抽象应用(apply)于参数的过程啦，只不过这个参数除了是一个变量还可能是一个表达式。
细心的话可以注意到，替换规则中特别标注了一些x ≠ y或者y ∉ FV(N)等约束条件，它们的意义在于防止lambda表达式的归约过程中出现歧义。
比如以下过程：
(λx.(λy.xy)) y
= (λy.xy)[x:=y] //beta归约：注意 y ∈ FV(y) 不满足替换的约束条件
= λy.yy //替换：绑定变量y与自由变量y同名出现了冲突
可以看出在不满足约束条件的情况强行替换造成了错误的结果，那么对于这种情况该如何处理呢？那就需要alpha转换啦。
- alpha | α 转换
这条规则就是说，一个lambda函数抽象在更名绑定变量前后是等价的，即：
α: λx.x ≡ λy.y
其作用就是解决绑定变量与自由变量间的同名冲突问题。
那么对于上面的那个错误归约过程就可以纠正一下了：
(λx.(λy.xy))y
= (λy.xy)[x:=y] //beta归约：注意 y ∈ FV(y) 不满足替换的约束条件
= (λz.xz)[x:=y] //alpha转换：因为绑定变量y将与自由变量x（将被替换为y）冲突，所以更名为z
= λz.yz
Perfect！这样对于lambda演算最基础的定义与归约规则已经介绍完毕了，虽然内容很简单，但是却很容易眼高手低，要试着练习喔。
- eta | η 归约
灵活运用alpha和beta已经可以解决所有的lambda表达式归约问题，但是考虑这样一个表达式：
λx.M x
将它应用于任意一个参数上，比如(λx.M x) N，进行beta归约和替换后会发现它等价于M N，这岂不是意味着
λx.M x ≡ M
没错，对于形如λx.M x，其中表达式M不包含绑定变量x的函数抽象，它是冗余的，等价于M，而这就是eta归约，它一般用于清除lambda表达式中存在的冗余函数抽象。