lambda calculus
先来看一下lambda表达式的基本语法(BNF):
<expr> ::= <identifier>
<expr> ::= lambda <identifier-list>. <expr>
<expr> ::= (<expr> <expr>)
前两条语法用于生成lambda表达式(lambda函数),如: lambda x y. x + y haskell里面为了简洁起见用“\”来代替希腊字母lambda,它们形状比较相似。故而上面的定义也可以写成: \ x y. x + y
这是一个匿名的加法函数,它接受两个参数,返回两值相加的结果。当然,这里我们为了方便起见赋予了lambda函数直观的计算意义,而实际上lambda calculus里面一切都只不过是文本替换,有点像C语言的宏。并且这里的“+”我们假设已经是一个具有原子语义的运算符[sup][6][/sup],此外,为了方便我们使用了中缀表达(按照lambda calculus系统的语法实际上应该写成“(+ x y)”才对——参考第三条语法)。
那么,函数定义出来了,怎么使用呢?最后一条规则就是用来调用一个lambda函数的:
((lambda x y. x + y) 2 3)
以上这一行就是把刚才定义的加法函数运用到2和3上(这个调用语法形式跟命令式语言(imperative language)惯用的调用形式有点区别,后者是“f(x, y)”,而这里是“(f x y)”,不过好在顺序没变 )。为了表达简洁一点,我们可以给(lambda x y. x + y)起一个名字,像这样:
let Add = (lambda x y. x + y)
这样我们便可以使用Add来表示该lambda函数了:
(Add 2 3)
不过还是为了方便起见,后面调用的时候一般用“Add(2, 3)”,即我们熟悉的形式。
有了语法规则之后,我们便可以看一看这个语言系统的两条简单至极的公理了: Alpha转换公理:例如,“lambda x y. x + y”转换为“lambda a b. a + b”。换句话说,函数的参数起什么名字没有关系,可以随意替换,只要函数体里面对参数的使用的地方也同时注意相应替换掉就是了。 Beta转换公理:例如,“(lambda x y. x + y) 2 3”转换为“2 + 3”。这个就更简单了,也就是说,当把一个lambda函数用到参数身上时,只需用实际的参数来替换掉其函数体中的相应变量即可。
就这些。是不是感觉有点太简单了?但事实就是如此,lambda算子系统从根本上其实就这些东西,然而你却能够从这几个简单的规则中推演出神奇无比的Y combinator来。我们这就开始!
递归的迷思
敏锐的你可能会发现,就以上这两条公理,我们的lambda语言中无法表示递归函数,为什么呢?假设我们要计算经典的阶乘,递归描述肯定像这样:
f(n):
if n == 0 return 1
return n*f(n-1)
当然,上面这个程序是假定n为正整数。这个程序显示了一个特点,f在定义的过程中用到了它自身。那么如何在lambda算子系统中表达这一函数呢?理所当然的想法如下: lambda n. If_Else n==0 1 n*<self>(n-1)
当然,上面的程序假定了If_Else是一个已经定义好的三元操作符(你可以想象C的“?:”操作符,后面跟的三个参数分别是判断条件、成功后求值的表达式、失败后求值的表达式。那么很显然,这个定义里面有一个地方没法解决,那就是<self>那个地方我们应该填入什么呢?很显然,熟悉C这类命令式语言的人都知道应该填入这个函数本身的名字,然而lambda算子系统里面的lambda表达式(或称函数)是没有名字的。
怎么办?难道就没有办法实现递归了?或者说,丘齐做出的这个lambda算子系统里面根本没法实现递归从而在计算能力上面有重大的缺陷?显然不是。马上你就会看到Y combinator是如何把一个看上去非递归的lambda表达式像变魔术那样变成一个递归版本的。在成功之前我们再失败一次,注意下面的尝试:
let F = lambda n. IF_Else n==0 1 n*F(n-1)
看上去不错,是吗?可惜还是不行。因为let F只是起到一个语法糖的作用,在它所代表的lambda表达式还没有完全定义出来之前你是不可以使用F这个名字的。更何况实际上丘齐当初的lambda算子系统里面也并没有这个语法元素,这只是刚才为了简化代码而引入的语法糖。当然,了解这个let语句还是有意义的,后面还会用到。
一次成功的尝试
在上面几次失败的尝试之后,我们是不是就一筹莫展了呢?别忘了软件工程里面的一条黄金定律:“任何问题都可以通过增加一个间接层来解决”。不妨把它沿用到我们面临的递归问题上:没错,我们的确没办法在一个lambda函数的定义里面直接(按名字)来调用其自身。但是,可不可以间接调用呢?
我们回顾一下刚才不成功的定义: lambda n. If_Else n==0 1 n*<self>(n-1)
现在<self>处不是缺少“这个函数自身”嘛,既然不能直接填入“这个函数自身”,我们可以增加一个参数,也就是说,把<self>参数化: lambdaself n. If_Else n==0 1 n*self(n-1)
上面这个lambda算子总是合法定义了吧。现在,我们调用这个函数的时候,只要加传一个参数self,这个参数不是别人,正是这个函数自身。还是为了简单起见,我们用let语句来给上面这个函数起个别名:
let P = lambda self n. If_Else n==0 1 n*self(n-1)
我们这样调用,比如说我们要计算3的阶乘: P(P, 3)
也就是说,把P自己作为P的第一个参数(注意,调用的时候P已经定义完毕了,所以我们当然可以使用它的名字了)。这样一来,P里面的self处不就等于是P本身了吗?自身调用自身,递归!
可惜这只是个美好的设想,还差一点点。我们分析一下P(P, 3)这个调用。利用前面讲的Beta转换规则,这个函数调用展开其实就是(你可以完全把P当成一个宏来进行展开!):
IF_Else n==0 1 n*P(n-1)
看出问题了吗?这里的P(n-1)虽然调用到了P,然而只给出了一个参数;而从P的定义来看,它是需要两个参数的(分别为self和n)!也就是说,为了让P(n-1)变成良好的调用,我们得加一个参数才行,所以我们得稍微修改一下P的定义:
let P = lambdaself n. If_Else n==0 1 n*self(self, n-1)
请注意,我们在P的函数体内调用self的时候增加了一个参数。现在当我们调用P(P, 3)的时候,展开就变成了:
IF_Else 3==0 1 3*P(P, 3-1)
而P(P, 3-1)是对P合法的递归调用。这次我们真的成功了!
不动点原理
然而,看看我们的P的定义,是不是很丑陋?“n*self(self, n-1)”?什么玩意?为什么要多出一个多余的self?DRY!怎么办呢?我们想起我们一开始定义的那个失败的P,虽然行不通,但最初的努力往往是大脑最先想到的最直观的做法,我们来回顾一下:
let P = lambda self n. If_Else n==0 1 n*self(n-1)
这个P的函数体就非常清晰,没有冗余成分,虽然参数列表里面多出一个self,但我们其实根本不用管它,看函数体就行了,self这个名字已经可以说明一切了对不对?但很可惜这个函数不能用。我们再来回想一下为什么不能用呢?因为当你调用P(P, n)的时候,里面的self(n-1)会展开为P(n-1)而P是需要两个参数的。唉,要是这里的self是一个“真正”的,只需要一个参数的递归阶乘函数,那该多好啊。为什么不呢?干脆我们假设出一个“真正”的递归阶乘函数:
power(n):
if(n==0) return 1;
return n*power(n-1);
但是,前面不是说过了,这个理想的版本无法在lambda算子系统中定义出来吗(由于lambda函数都是没名字的,无法自己内部调用自己)?不急,我们并不需要它被定义出来,我们只需要在头脑中“假设”它以“某种”方式被定义出来了,现在我们把这个真正完美的power传给P,这样:
P(power, 3)
注意它跟P(P, 3)的不同,P(P, 3)我们传递的是一个有缺陷的P为参数。而P(power, 3)我们则是传递的一个真正的递归函数power。我们试着展开P(power, 3):
IF_Else 3==0 1 3*power(3-1)
发生了什么??power(3-1)将会计算出2的阶乘(别忘了,power是我们设想的完美递归函数),所以这个式子将会忠实地计算出3的阶乘!
回想一下我们是怎么完成这项任务的:我们设想了一个以某种方式构造出来的完美的能够内部自己调用自己的递归阶乘函数power,我们发现把这个power传给P的话,P(power, n)的展开式就是真正的递归计算n阶乘的代码了。
你可能要说:废话!都有了power了我们还要费那事把它传给P来个P(power, n)干嘛?直接power(n)不就得了?! 别急,之所以设想出这个power只是为了引入不动点的概念,而不动点的概念将会带领我们发现Y combinator。
什么是不动点?一点都不神秘。让我们考虑刚才的power与P之间的关系。一个是真正可递归的函数,一个呢,则是以一个额外的self参数来试图实现递归的伪递归函数,我们已经看到了把power交给P为参数发生了什么,对吧?不,似乎还没有,我们只是看到了,“把power加上一个n一起交给P为参数”能够实现真正的递归。现在我们想考虑power跟P之间的关系,直接把power交给P如何?
P(power)
这是什么?这叫函数的部分求值(partial evaluation)。换句话说,第一个参数是给出来了,但第二个参数还悬在那里,等待给出。那么,光给一个参数得到的是什么呢?是“还剩一个参数待给的一个新的函数”。其实也很简单,只要按照Beta转换规则做就是了,把P的函数体里面的self出现处皆替换为power就可以了。我们得到:
IF_Else n==0 1 n*power(n-1)
当然,这个式子里面还有一个变量没有绑定,那就是n,所以这个式子还不能求值,你需要给它一个n才能具体求值,对吧。这么说,这可不就是一个以n为参数的函数么?实际上就是的。在lambda算子系统里面,如果给一个lambda函数的参数不足,则得到的就是一个新的lambda函数,这个新的lambda函数所接受的参数也就是你尚未给出的那些参数。换句话来说,调用一个lambda函数可以分若干步来进行,每次只给出一部分参数,而只有等所有参数都给齐了,函数的求值结果才能出来,否则你得到的就是一个“中间函数”。
那么,这跟不动点定理有什么关系?关系大了,刚才不是说了,P(power)返回的是一个新的“中间函数”嘛?这个“中间函数”的函数体我们刚才已经看到了,就是简单地展开P(power)而已,回顾一遍:
IF_Else n==0 1 n*power(n-1)
我们已经知道,这是个函数,参数n待定。因此我们不妨给它加上一个“lambda n”的帽子,这样好看一点: lambda n. IF_Else n==0 1 n*power(n-1)
这是什么呢?这可不就是power本身的定义?(当然,如果我们能够定义power的话)。不信我们看看power如果能够定义出来像什么样子:
let power = lambda n. IF_Else n==0 1 n*power(n-1)
一模一样!也就是说,P(power)展开后跟power是一样的。即: P(power) = power
以上就是所谓的不动点。即对于函数P来说power是这样一个“点”:当把P用到power身上的时候,得到的结果仍然还是power,也就是说,power这个“点”在P的作用下是“不动”的。
可惜的是,这一切居然都是建立在一个不存在的power的基础上的,又有什么用呢?可别过早提“不存在”这个词,你觉得一样东西不存在或许只是你没有找到使它存在的正确方法。我们已经看到power是跟P有着密切联系的。密切到什么程度呢?对于伪递归的P,存在一个power,满足P(power)=power。注意,这里所说的“伪递归”的P,是指这样的形式:
let P = lambda self n. If_Else n==0 1 n*self(n-1) // 注意,不是self(self,n-1)
一般化的描述就是,对任一伪递归F(回想一下伪递归的F如何得到——是我们为了解决lambda函数不能引用自身的问题,于是给理想的f加一个self参数从而得到的),必存在一个理想f(F就是从这个理想f演变而来的),满足F(f) = f。
那么,现在的问题就归结为如何针对F找到它的f了。根据F和f之间的密切联系(F就比f多出一个self参数而已),我们可以从F得出f吗?假设我们可以(又是假设),也就是说假设我们找到了一根魔棒,把它朝任意一个伪递归的F一挥,眼前一花,它就变成了真正的f了。这根魔棒如果存在的话,它具有什么性质?我们假设这个神奇的函数叫做Y,把Y用到任何伪递归的函数F上就能够得到真正的f,也就是说:
Y(F) = f
结合上面的F(f) = f,我们得到:
Y(F) = f = F(f) = F(Y(F))
也就是说,Y具有性质: Y(F) = F(Y(F))
性质倒是找出来了,怎么构造出这个Y却又成了难题。一个办法就是使用抽象法,这是从工程学的思想的角度,也就是通过不断迭代、重构,最终找到问题的解。然而对于这里的Y combinator,接近问题解的过程却显得复杂而费力,甚至过程中的有些点上的思维跳跃有点如羚羊挂角无迹可寻。然而,在这整个Y combinator介绍完了之后我们将会介绍著名的哥德尔不完备性定理,然后我们就会发现,通过哥德尔不完备性定理证明中的一个核心构造式,只需一步自然的推导就能得出我们的Y combinator。而且,最美妙的是,还可以再往下归约,把一切都归约到康托尔当初提出的对角线方法,到那时我们就会发现原来同样如羚羊挂角般的哥德尔的证明其实是对角线方法的一个自然推论。数学竟是如此奇妙,我们由简单得无法再简单的lambda calculus系统的两条公理居然能够导出如此复杂如此令人目眩神迷的Y Combinator,而这些复杂性其实也只是荡漾在定理海洋中的涟漪,拨开复杂性的迷雾我们重又发现它们居然寓于极度的简洁之中。这就是数学之美。
让我们先来看一看Y combinator的费力而复杂的工程学构造法,我会尽量让这个过程显得自然而流畅[sup][7][/sup]:
我们再次回顾一下那个伪递归的求阶乘函数:
let P = lambda self n. If_Else n==0 1 n*self(n-1)
我们的目标是找出P的不动点power,根据不动点的性质,只要把power传给P,即P(power),便能够得到真正的递归函数了。
现在,关键的地方到了,由于:
power = P(power) // 不动点原理
这就意味着,power作为一个函数(lambda calculus里面一切都是函数),它是自己调用了自己的。那么,我们如何实现这样一个能够自己调用自己的power呢?回顾我们当初成功的一次尝试,要实现递归,我们是通过增加一个间接层来进行的:
let power_gen = lambda self. P(self(self))
还记得self(self)这个形式吗?我们在成功实现出求阶乘递归函数的时候不就是这么做的?那么对于现在这个power_gen,怎么递归调用?
power_gen(power_gen)
不明白的话可以回顾一下前面我们调用P(P, n)的地方。这里power_gen(power_gen)展开后得到的是什么呢?我们根据刚才power_gen的定义展开看一看,原来是: P(power_gen(power_gen))
看到了吗?也就是说:
power_gen(power_gen) => P(power_gen(power_gen))
现在,我们把power_gen(power_gen)当成整体看,不妨令为power,就看得更清楚了:
power => P(power)
这不正是我们要的答案么?
OK,我们总结一下:对于给定的P,只要构造出一个相应的power_gen如下:
let power_gen = lambda self. P(self(self))
我们就会发现,power_gen(power_gen)这个调用展开后正是P(power_gen(power_gen))。也就是说,我们的power_gen(power_gen)就是我们苦苦寻找的不动点了! 铸造Y Combinator
现在我们终于可以铸造我们的Y Combinator了,Y Combinator只要生成一个形如power_gen的lambda函数然后把它应用到自身,就大功告成:
let Y = lambda F.
let f_gen = lambda self. F(self(self))
return f_gen(f_gen)
稍微解释一下,Y是一个lambda函数,它接受一个伪递归F,在内部生成一个f_gen(还记得我们刚才看到的power_gen吧),然后把f_gen应用到它自身(记得power_gen(power_gen)吧),得到的这个f_gen(f_gen)也就是F的不动点了(因为f_gen(f_gen) = F(f_gen(f_gen))),而根据不动点的性质,F的不动点也就是那个对应于F的真正的递归函数!
如果你还觉得不相信,我们稍微展开一下看看,还是拿阶乘函数说事,首先我们定义阶乘函数的伪递归版本:
let Pwr = lambda self n. If_Else n==0 1 n*self(n-1)
让我们把这个Pwr交给Y,看会发生什么(根据刚才Y的定义展开吧):
Y(Pwr) =>
let f_gen = lambda self. Pwr(self(self))
return f_gen(f_gen)
Y(Pwr)的求值结果就是里面返回的那个f_gen(f_gen),我们再根据f_gen的定义展开f_gen(f_gen),得到:
Pwr(f_gen(f_gen))
也就是说:
Y(Pwr) => f_gen(f_gen) => Pwr(f_gen(f_gen))
我们来看看得到的这个Pwr(f_gen(f_gen))到底是不是真有递归的魔力。我们展开它(注意,因为Pwr需要两个参数,而我们这里只给出了一个,所以Pwr(f_gen(f_gen))得到的是一个单参(即n)的函数):
Pwr(f_gen(f_gen)) => If_Else n==0 1 n*f_gen(f_gen) (n-1)
而里面的那个f_gen(f_gen),根据f_gen的定义,又会展开为Pwr(f_gen(f_gen)),所以: Pwr(f_gen(f_gen)) => If_Else n==0 1 n* Pwr(f_gen(f_gen)) (n-1)
看到加粗的部分了吗?因为Pwr(f_gen(f_gen))是一个接受n为参数的函数,所以不妨把它令成f(f的参数是n),这样上面的式子就是: f => If_Else n==0 1 n*f(n-1)
完美的阶乘函数!
哥德尔的不完备性定理 了解哥德尔不完备性定理的可以跳到下一节,“大道至简——康托尔的天才”
然而,漫长的Y Combinator征途仍然并非本文的最终目的,对于Y combinator的构造和解释,只是给不了解lambda calculus或Y combinator的读者看的。关键是马上你会看到Y combinator可以由哥德尔不完备性定理证明的一个核心构造式一眼瞧出来!
让我们的思绪回到1931年,那个数学界风起云涌的年代,一个名不经传的20出头的学生,在他的博士论文中证明了一个惊天动地的结论。
在那个年代,希尔伯特的数学天才就像太阳的光芒一般夺目,在关于数学严格化的大纷争中希尔伯特带领的形式主义派系技压群雄,得到许多当时有名望的数学家的支持。希尔伯特希望借助于形式化的手段,抽掉数学证明中的意义,把数学证明抽象成一堆无意义的符号转换,就连我们人类赖以自豪的逻辑推导,也不过只是一堆堆符号转换而已(想起lambda calculus系统了吧:))。这样一来,一个我们日常所谓的,带有直观意义和解释的数学系统就变成了一个纯粹由无意义符号表达的、公理加上推导规则所构成的形式系统,而数学证明呢,只不过是在这个系统内玩的一个文字游戏。令人惊讶的是,这样一种做法,真的是可行的!数学的意义,似乎竟然真的可以被抽掉!另一方面,一个形式系统具有非常好的性质,平时人们证明一个定理所动用的推导,变成了纯粹机械的符号变换。希尔伯特希望能够证明,在任一个无矛盾的形式系统中所能表达的所有陈述都要么能够证明要么能够证伪。这看起来是个非常直观的结论,因为一个结论要么是真要么是假,而它在它所处的领域/系统中当然应该能够证明或证伪了(只要我们能够揭示出该系统中足够多的真理)。
然而,哥德尔的证明无情的击碎了这一企图,哥德尔的证明揭示出,任何足够强到蕴含了皮亚诺算术系统(PA)的一致(即无矛盾)的系统都是不完备的,所谓不完备也就是说在系统内存在一个为真但无法在系统内推导出的命题。这在当时的数学界揭起了轩然大波,其证明不仅具有数学意义,而且蕴含了深刻的哲学意义。从那时起这一不完备性定理就被引申到自然科学乃至人文科学的各个角落…至今还没有任何一个数学定理居然能够产生这么广泛而深远的影响。
哥德尔的证明非常的长,达到了200多页纸,但其中很大的成分是用在了一些辅助性的工作上面,比如占据超过1/3纸张的是关于一个形式系统如何映射到自然数,也就是说,如何把一个形式系统中的所有公式都表示为自然数,并可以从一自然数反过来得出相应的公式。这其实就是编码,在我们现在看来是很显然的,因为一个程序就可以被编码成二进制数,反过来也可以解码。但是在当时这是一个全新的思想,也是最关键的辅助性工作之一,另一方面,这正是“程序即数据”的最初想法。
现在我们知道,要证明哥德尔的不完备性定理,只需在假定的形式系统T内表达出一个为真但无法在T内推导出(证明)的命题。于是哥德尔构造了这样一个命题,用自然语言表达就是:命题P说的是“P不可在系统T内证明”(这里的系统T当然就是我们的命题P所处的形式系统了),也就是说“我不可以被证明”,跟著名的说谎者悖论非常相似,只是把“说谎”改成了“不可以被证明”。我们注意到,一旦这个命题能够在T内表达出来,我们就可以得出“P为真但无法在T内推导出来”的结论,从而证明T的不完备性。为什么呢?我们假设T可以证明出P,而因为P说的就是P不可在系统T内证明,于是我们又得到T无法证明出P,矛盾产生,说明我们的假设“T可以证明P”是错误的,根据排中律,我们得到T不可以证明P,而由于P说的正是“T不可证明P”,所以P就成了一个正确的命题,同时无法由T内证明!
如果你足够敏锐,你会发现上面这番推理本身不就是证明吗?其证明的结果不就是P是正确的?然而实际上这番证明是位于T系统之外的,它用到了一个关于T系统的假设“T是一致(无矛盾)的”,这个假设并非T系统里面的内容,所以我们刚才其实是在T系统之外推导出了P是正确的,这跟P不能在T之内推导出来并不矛盾。所以别担心,一切都正常。
那么,剩下来最关键的问题就是如何用形式语言在T内表达出这个P,上面的理论虽然漂亮,但若是P根本没法在T内表达出来,我们又如何能证明“T内存在这个为真但无法被证明的P”呢?那一切还不是白搭?
于是,就有了哥德尔证明里面最核心的构造,哥德尔构造了这样一个公式: N(n) is unprovable in T
这个公式由两部分构成,n是这个公式的自由变量,它是一个自然数,一旦给定,那么这个公式就变成一个明确的命题。而N则是从n解码出的货真价实的(即我们常见的符号形式的)公式(记得哥德尔的证明第一部分就是把公式编码吗?)。”is unprovable in T”则是一个谓词,这里我们没有用形式语言而是用自然语言表达出来的,但哥德尔证明了它是可以用形式语言表达出来的,大致思路就是:一个形式系统中的符号数目是有限的,它们构成这个形式系统的符号表。于是,我们可以依次枚举出所有长度为1的串,长度为2的串,长度为3的串… 此外根据形式系统给出的语法规则,我们可以检查每个串是否是良构的公式(well formed formula,简称wff,其实也就是说,是否符合语法规则,前面我们在介绍lambda calculus的时候看到了,一个形式系统是需要语法规则的,比如逻辑语言形式化之后我们就会看到P->Q是一个wff,而->Q则不是),因而我们就可以枚举出所有的wff来。最关键的是,我们观察到形式系统中的证明也不过就是由一个个的wff构成的序列(想想推导的过程,不就是一个公式接一个公式嘛)。而wff构成的序列本身同样也是由符号表内的符号构成的串。所以我们只需枚举所有的串,对每一个串检查它是否是一个由wff构成的序列(证明),如果是,则记录下这个wff序列(证明)的最后一个wff,也就是它的结论。这样我们便枚举出了所有的可由T推导出的定理。然后为了表达出”X is unprovable in T”,本质上我们只需说“不存在这样一个自然数S,它所解码出来的wff序列以X为终结”!这也就是说,我们表达出了“is unprovable in T”这个谓词。
我们用UnPr(X)来表达“X is unprovable in T”,于是哥德尔的公式变成了:
UnPr( N(n) )
现在,到了最关键的部分,首先我们把这个公式简记为G(n)——别忘了G内有一个自由变量n,所以G现在还不是一个命题,而只是一个公式,所以谈不上真假:
G(n): UnPr( N(n) )
又由于G也是个wff,所以它也有自己的编码g,当然g是一个自然数,现在我们把g作为G的参数,也就是说,把G里面的自由变量n替换为g,我们于是得到一个真正的命题:
G(g): UnPr( G(g) )
用自然语言来说,这个命题G(g)说的就是“我是不可在T内证明的”。看,我们在形式系统T内表达出了“我是不可在T内证明的”这个命题。而我们一开始已经讲过了如何用这个命题来推断出G(g)为真但无法在T内证明,于是这就证明了哥德尔的不完备性定理[sup][8][/sup]。
哥德尔的不完备性定理被称为20世纪数学最重大的发现(不知道有没有“之一”:) )现在我们知道为真但无法在系统内证明的命题不仅仅是这个诡异的“哥德尔命题”,还有很多真正有意义的明确命题,其中最著名的就是连续统假设,此外哥德巴赫猜想也有可能是个没法在数论系统中证明的真命题。