此系列文章是我学习lambda演算过程的总结与复习，着重于探讨“为什么(Why)”与“怎么做(How)”，也希望能对看到它的人学习了解这个形式系统有些微帮助。由于之前看了不少wiki、tutorial、introduction之流，绝大多数读过之后仅知其然而不知其所以然，我不知道为什么它们都不解释为什么要这么做，为什么要有这些东西，这些东西是怎么得来的，但这个事实让我非常苦恼，因此才有了这个系列。我试图将自己的浅薄理解稍作阐释梳理，知之尚浅，如有错漏不妥之处请不吝指出，欢迎交流讨论批评建议。

部分参考：
Wikipedia
SEP(Stanford Encyclopedia of Philosophy)
Brilliant
Cornell Recitation Course
一个有翻译的tutorial：[翻译] [原文]
一个完全how to的introduction

NOTE: 在lambda演算中，函数是一等公民。即对函数做一般的基本操作都是合法的，比如把函数作为参数传入或返回，赋给一个变量等等。

lambda | λ 定义

要描述一个形式系统，我们首先需要约定用到的基本符号，对于本系列所介绍的lambda演算，其符号集包括λ . ()和变量名(x, y, z, etc.)。

1. λ 表达式/项

在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)。

1. 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转换啦。

2. 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演算最基础的定义与归约规则已经介绍完毕了，虽然内容很简单，但是却很容易眼高手低，要试着练习喔。

3. 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表达式中存在的冗余函数抽象。

To be continued...