任何非常先进的技术，初看都与魔法无异。
λ-calculus
这篇博客我们简单说说 λ-calculus。 在 λ 演算中，每个表达式均代表一个函数，这个函数有一个参数，并返回一个值。故 λ 演算只有一种“类型”，即单参函数。（这也是为什么上一篇博客里说柯里化给予 λ 演算一个理论模型）而函数由 λ 表达式匿名定义，如：f(x) = x * 2 可以写为 λx.x * 2 而 f(4)的值即可表示为(λx.x * 2) 4。 看上去怪怪的，突然冒出来一个孤零零的数字 4，如果有强迫症的话简直不能忍啊！那么我们还可以把它写成下面这个样子： (λf.f 4)(λ.x x * 2)这回看着规整了一些。(λf.f 4)表示的是这个函数接受一个函数作为参数，并作用在 4 上。 就如同任何编程语言都有语法一样，λ 演算也需要语法。λ 演算将符合这些语法的表达式也称作“lambda 项”其语法可归纳成三条规则：
- 变量 x 本身就是一个有效的 lambda 项
- 如果 t 是一个 lambda 项，而 x 是一个变量，则(λx.t) 是一个 lambda 项（称为 lambda 抽象）
- 如果 t 和 s 是 lambda 项，那么(ts)是一个 lambda 项（称为应用） 等等，这样一来，我写下这种式子(λx.x x)(λx.x x)也是对的，但是貌似计算不出来一个确定的值啊。然而这是可以接受的，因为 lambda 表达式并不要求必须归约到一个确定的值上。 接下来我们来看一个有趣的东西：
Church 数
Church 数 0, 1, 2, ...在 lambda 演算中被定义如下：
0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x
...
这是什么？怎么凭空就能冒出来 0 ≡ λf.λx. x，1 ≡ λf.λx. f x 这种奇怪的东西？我们先回想一下自然数是怎么定义的？ 额，像是 0，1，2，3······这种数叫自然数？这种定义太不严谨，我们要用皮亚诺公理定义自然数：
- 0 是一个自然数。
- 0 不是任何其他自然数的继数。
- 每一个自然数 a 都有一个继数。
- 如果 a 与 b 的继数相等则 a 与 b 亦相等。
- 若一个由自然数组成的集合 s 包含有 0，又若当 s 包含有某一数 a 时，它一定也含有 a 的继数，则 s 就包含有全体自然数。
看上去好多了，但是这又和上面的 church 数有什么关系呢？我们可以这么理解：
我们先定义了一个零作为基础，又定义了后继这个概念（计算方法），我们现在只不过在用 λ 表达式来表示罢了，其中的 f 就可以理解为后继。这倒是能说得通，但是我要做加法又怎么理解？很简单，只不过是进行多次后继罢了。
正真的 λ 演算比本文所描述的要复杂很多，本文只是简要的介绍。