lambda演算系列搬运cgnail的blog，源blog连接为这里。

所以，现在，让我们用lambda演算干点有趣的事。首先，为了方便起见，我将介绍些语法糖（syntactic sugar）来命名函数，以便下面遇到某些复杂的事情的时候方便我们阅读。

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

1
let square = lambda x . x ^ 2

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

1
(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”：

1
let add = lambda s z x y . x s (y s z)

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

1
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的运算过程：

1
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”代替：

1
add (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))

用add的定义做替换：

1
(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规约：

1
lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (lambda s3 z3 . s3 (s3 (s3 z3)) s z)

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

1
lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (s (s (s z)))

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

1
lambda s z . s (s (s (s (s z))))

于是，我们的结果是：丘奇数”5”！