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)的绑定(即,将参数都写成sz的组合的形式)。

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

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

让我们再进一步看看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”!