lambda 演算中的数字

引进「全局」函数（即在我写的这些所有的关于lambda演算的介绍里都可以直接使用，而不用在每一个表达式中都声明一次这个函数的办法），我们将使用“let”表达式：

let square = lambda x . x ^ 2
这条表达式声明了一个名为“square”的函数，其定义是lambda x . x ^ 2。如果我们有“ square 4”，则上面的“let”表达式的等效表达式为：

(lambda square . square 4) (lambda x . x ^ 2)
某些例子中，我使用了数字和算术运算。但数字并不真正存在于lambda演算中，我们有的只有函数！因此，我们需要发明某种使用函数来创建数字的方式。幸运的是，邱奇（Alonzo Church），这个发明了lambda演算的天才，找出了做到这一点的办法。他的函数化的数字的版本被称为丘奇数（Church Numerals）。

所有的丘奇数都是带有两个参数的函数：

0是“ lambda s z . z “。
1是“ lambda s z . s z “。
2是“ lambda s z . s (s z)
对于任何数“n”，它的丘奇数是将其第一个参数应用到第二个参数上“n”次的函数。
一个很好的理解办法是将“z”作为是对于零值的命名，而“s”作为后继函数的名称。因此，0是一个仅返回“0”值的函数；1是将后继函数运用到0上一次的函数；2则是将后继函数应用到零的后继上的函数，以此类推。

现在看好了，如果我们想要做加法，x + y，我们需要写一个有四个参数的函数；两个需要相加的数字；以及推导数字时用到的“s”和“z”：

let add = lambda s z x y . x s (y s z)
让我们将其柯里化，看看是怎么回事。首先，它接受两个参数，这是我们需要做加法的两个值；第二，它需要正则化（normalize）这两个参数，以使它们都使用对0（z）和后继值（s）的绑定（即，将参数都写成s和z的组合的形式）。

let add = lambda x y . (lambda s z . (x s (y s z)))
看下这个式子，它说的是，为了将x和y相加，先用参数“s”和“z”创建（正则化的）丘奇数“y”。然后应用x到丘奇数y上，这时候使用由“s”和“z”定义的丘奇数y。也就是说，我们得到的结果是一个函数，这个函数把自己加到另一个数字上。（要计算x + y，先计算 y 是 z 的几号后继，然后计算x 是 y的几号后继。）

让我们再进一步看看2 + 3的运算过程：

add (lambda s z . s (s z)) (lambda s z . s (s (s z))) news newz
为了更容易理解，对数字2和3做alpha变换，“2”用“s2”和“z2”代替，3用“s3”和“z3”代替：

add (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))
用add的定义做替换：

(lambda x y .(lambda s z. (x s y s z))) (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))
对add做beta规约：

lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (lambda s3 z3 . s3 (s3 (s3 z3)) s z)
然后beta规约丘奇数”3”。这步操作其实是“正则化”3：把数字3的定义里的后继函数和零函数替换成add的参数列表里的后继函数和零函数：

lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (s (s (s z)))
现在，到了最精妙的一步了。再对丘奇数”2”做beta规约。我们知道：2是一个函数，它接受两个参数：一个后继函数和0(函数)。于是，要相加2和3，我们用后继函数应用到2的第一个参数；用3的运算结果应用到第二个参数（0函数）！

lambda s z . s (s (s (s (s z))))
于是，我们的结果是：丘奇数”5”！