之所以和上一篇文章间隔的时间如此之长, 是因为我发现我没有资格介绍Lambda…遂重新学习
人只有在清楚自己是无知的, 人才会获得成长, 人才是比知晓一切的造物主更高贵的生物.
—— Wharziki Shold
λ演算，是从数理逻辑出发，当今在计算机科学领域大放异彩的形式系统。是由数学家阿隆佐·邱奇(Alonzo Church)发明，由哈斯凯尔·加里(Haskell Brooks Curry)进一步完善的以函数作为核心的计算模型。
如果把汇编(以及后继者C，C++和今天的一系列程序语言)比喻成计算机的躯体，那么以λ演算为基础的Lisp、Haskell等一系列函数语言则就像计算机的灵魂。想要理解计算机，就一定要理解λ。λ作为“最基本的编程语言“其构建在简单的两条规则上。这就是数理逻辑的魅力所在，你可以用砂石堆出城堡，如点滴细流汇聚大江东流，简洁的规则演变成复杂的世界。这两条规则，或者说是世界的起源，就是：
| 语法 | 名称 | 描述 |
|---|---|---|
| (λx.M) | 抽象 | 将x绑定到λ项M中，并返回M。即函数定义。 |
| (M N) | 应用 | 讲λ项N作为参数调用λ项M。即函数应用。 |
以上两条十分直观的规则就是λ的基本规则。对于我们将要深入讨论的λ演算，是邱奇的最初的λ演算，即“无类型的λ演算”。在此之后人们又发展出”有类型的λ演算”，并以之作为邱奇的λ演算的精细化。不过现时代的观点通常认为邱奇的“无类型λ演算”是“有类型λ演算”的一种特殊情况，即有且仅有一种类型——“函数”时的情况。不过都无所谓，不影响我们接下来的讨论。
首先介绍一下λ演算的优点：
它是图灵完全的，你可以用λ演算解决一切图灵机可以解决的问题。
规则简单语义健壮，可被用作数理逻辑推理的基础。
易于读写，便于使用。
具有固定模型(比如本系列会讨论的SKI结合子模型)。
超级好玩！特别有意思！智力游戏一般的推理！
首先从一条计算两数和的λ表达式说起。
λx y . x + y
根据上述的语法，我们可以很清楚的看出这个λ表达式(λ项)是接受x和y作为参数并且返回x+y的数值的一个函数。在λ演算中，每个表达式都代表一个匿名函数，而且这个函数 仅 接受和返回一个参数。等等，那么我们上面计算两数和的函数是错误的吗？非也。这条语句是下列语句的简化：λx . (λy . x + y)。这种将接受多个参数的函数变化为接受一个参数的函数的过程叫做柯里化(Currying，然鹅这个不是柯里发明的=。=)。事实上，柯里化是将多参函数转化为一条由单参函数组成的函数链的过程。
柯里化的结果在λ算式里似乎与柯里化之前并无什么区别。不过要注意柯里化是将单个函数变换成多个函数组成的链的过程。由于λ表达式是左结合的，而且会省略不会引起歧义的括号(数学家们的歧义)。所以对于一个多参函数F := λx y . x + y来说，F x y和我们常用的F(x, y)并无什么两样；而事实上λ演算要求所有函数均为单参的，所以以上的多参函数定义通常会被转化为：F := λx . (λy . x + y)，而调用仍然是F x y，不过如果加上括号，就变成了F(x)(y)，先将x应用到F上，返回一个接受y作为参数的函数，然后再把y应用到这个函数上，取得返回值。这一点在用JavaScript写正宗的λ算式的时候是需要注意的。
上文定义的F，对于λ表达式F 3 2来说，其展开式则为：((λx . (λy . x + y)) 3) 2=>(λy . 3 + y)=>(3 + 2)。这里值得注意的是，这三个表达式显然是等价的。但是根据邱奇利用λ演算对判定性问题的证明，这三个表达式之间的等价性是无法找到一个通用的函数来判定的。我们在应用函数的过程中，实际上是把3、2分别与λ项里面的x和y绑定。然后才返回一个没有未经绑定的具体的数值表达式。这个过程叫做变量的绑定。下面的式子：F 3的结果就是(λy . 3 + y)，我们把3绑定到x上，但是并没有绑定y。这个表达式返回了一个有未知数的表达式：3+y，这里的未知数y，在λ里被称作自由变量，也就是未经绑定的变量。对于表达式中的一组自由变量的规定如下(一般来说，x、y为变量，t、s、r为λ项)：
- x的自由变量只是x
- λx.t的自由变量是t中的自由变量的集合移除了x之后的集合
- ts的自由变量是t的自由变量和s的自由变量的并集。
目前为止，我们已经理解了自由变量和柯里化的概念。相信也一定对λ有了一个感性的认知。下面我们来介绍λ演算里面的另外一个重要的东西——归约。归约是λ表达式求值的基础，其总共有两条规则(是不是很少？)：
下面来详细介绍这两条归约。
α-转换
α-转换指出，一个抽象函数体和其中的变量名是无关的，显而易见，
λx.x和λy.y是同一个函数，根据转换规则，x不光和y是等效的，也和当前条件下其他所有的自由变量是等效的。如果x和y是变量，t是一个λ项，t[x:=y]则是把t中自由出现的x都替换成y，对于这种操作，如果y在t中不是一个自由变量，而且y不会被t中的λ项绑定的情况下，λx.t与λy.t[x:=y]是等效的。即：
λx.(λx.x) x与λy.(λx.x) y是等价的(显而易见的?)。β-归约
β-归约是函数作用的概念，即
((λx.M)E) → (M[x:=E])相当于M(E)。具体的定义是：当s的所有自由出现在t[x:=s]的时候仍然是自由的情况下，((λx.t) s)和t[x:=s]等价且为最小等价(等价关系中减少任意一个映射都不再是等价关系)。即当应用前s中的自由变量为应用后t[x:=s]自由变量的子集时，则可以应用β-归约于λ项。 当一个λ表达式无法继续被使用β-归约，则称呼这个表达式为β范式，且与应用归约前的表达式等价。
这两条规则便是计算λ表达式的基础，至此，λ表达式的基础内容，就全部介绍完毕了。