任何非常先进的技术,初看都与魔法无异。
λ-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 就可以理解为后继。这倒是能说得通,但是我要做加法又怎么理解?很简单,只不过是进行多次后继罢了。
正真的 λ 演算比本文所描述的要复杂很多,本文只是简要的介绍。