我看到了它,却不敢相信它[1]。
——康托尔
计算机是数学家一次失败思考的产物。
——无名氏
哥德尔的不完备性定理震撼了20世纪数学界的天空,其数学意义颠覆了希尔伯特的形式化数学的宏伟计划,其哲学意义直到21世纪的今天仍然不断被延伸到各个自然学科,深刻影响着人们的思维。图灵为了解决希尔伯特著名的第十问题而提出有效计算模型,进而作出了可计算理论和现代计算机的奠基性工作,著名的停机问题给出了机械计算模型的能力极限,其深刻的意义和漂亮的证明使它成为可计算理论中的标志性定理之一。丘齐,跟图灵同时代的天才,则从另一个抽象角度提出了lambda算子的思想,与图灵机抽象的倾向于硬件性不同,丘齐的lambda算子理论是从数学的角度进行抽象,不关心运算的机械过程而只关心运算的抽象性质,只用最简洁的几条公理便建立起了与图灵机完全等价的计算模型,其体现出来的数学抽象美开出了函数式编程语言这朵奇葩,Lisp、Scheme、Haskell… 这些以抽象性和简洁美为特点的语言至今仍然活跃在计算机科学界,虽然由于其本质上源于lambda算子理论的抽象方式不符合人的思维习惯从而注定无法成为主流的编程语言[2],然而这仍然无法妨碍它们成为编程理论乃至计算机学科的最佳教本。而诞生于函数式编程语言的神奇的Y combinator至今仍然让人们陷入深沉的震撼和反思当中…
关系却又有点一头雾水的背后,其实隐隐藏着一条线,这条线把它们从本质上串到了一起,而顺着时光的河流逆流而上,我们将会看到,这条线的尽头,不是别人,正是只手拨开被不严密性问题困扰的19世纪数学界阴沉天空的天才数学家康托尔,康托尔创造性地将一一对应和对角线方法运用到无穷集合理论的建立当中,这个被希尔伯特称为“谁也无法将我们从康托尔为我们创造的乐园中驱逐出去”、被罗素称为“19世纪最伟大的智者之一”的人,他在集合论方面的工作终于驱散了不严密性问题带来的阴霾,仿佛一道金色的阳光刺破乌云,19世纪的数学终于看到了真正严格化的曙光,数学终于得以站在了前所未有的坚固的基础之上;集合论至今仍是数学里最基础和最重要的理论之一。而康托尔当初在研究无穷集合时最具天才的方法之一——对角线方法——则带来了极其深远的影响,其纯粹而直指事物本质的思想如洪钟大吕般响彻数学和哲学的每一个角落[3]。随着本文的展开,你将会看到,刚才提到的一切,歌德尔的不完备性定理,图灵的停机问题,lambda算子理论中神奇的Y combinator、乃至著名的罗素悖论、理发师悖论等等,其实都源自这个简洁、纯粹而同时又是最优美的数学方法,反过来说,从康托尔的对角线方法出发,我们可以轻而易举地推导出哥德尔的不完备性定理,而由后者又可以轻易导出停机问题和Y combinator,实际上,我们将会看到,后两者也可以直接由康托尔的对角线方法导出。尤其是Y combinator,这个形式上绕来绕去,本质上捉摸不透,看上去神秘莫测的算子,其实只是一个非常自然而然的推论,如果从哥德尔的不完备性定理出发,它甚至比停机问题还要来得直接简单。总之,你将会看到这些看似深奥的理论是如何由一个至为简单而又至为深刻的数学方法得出的,你将会看到最纯粹的数学美。
然而,这一切的一切,看似不很相关却又有点相关,认真思考其图灵的停机问题(The Halting Problem)
了解停机问题的可以直接跳过这一节,到下一节“Y Combinator”,了解后者的再跳到下一节“哥德尔的不完备性定理”
一篇关于图灵机的文章,有兴趣的读者可以从那篇开始,那篇主要是从理论上阐述,所以这里我们打算避开抽象的理论,换一种符合程序员思维习惯的直观方式来加以解释。
我们还是从图灵著名的停机问题说起,一来它相对来说是我们要说的几个定理当中最简单的,二来它也最贴近程序员。实际上,我以前曾写过停机问题
不存在这样一个程序(算法),它能够计算任何程序(算法)在给定输入上是否会结束(停机)。
那么,如何来证明这个停机问题呢?反证。假设我们某一天真做出了这么一个极度聪明的万能算法(就叫God_algo吧),你只要给它一段程序(二进制描述),再给它这段程序的输入,它就能告诉你这段程序在这个输入上会不会结束(停机),我们来编写一下我们的这个算法吧:
bool God_algo(char* program, char* input)
{
if(<program>halts on<input>)
return true;
return false;
}
这里我们假设if的判断语句里面是你天才思考的结晶,它能够像上帝一样洞察一切程序的宿命。现在,我们从这个God_algo出发导出一个新的算法:
bool Satan_algo(char* program)
{
if(God_algo(program, program) ){
while(1); // loop forever!
return false; // can never get here!
}
else
return true;
}
正如它的名字所暗示的那样,这个算法便是一切邪恶的根源了。当我们把这个算法运用到它自身身上时,会发生什么呢?
Satan_algo(Satan_algo);
我们来分析一下这行简单的调用:
显然,Satan_algo(Satan_algo)这个调用要么能够运行结束返回(停机),要么不能返回(loop forever)。
如果它能够结束,那么Santa_algo算法里面的那个if判断就会成立(因为God_algo(Santa_algo,Santa_algo)将会返回true),从而程序便进入那个包含一个无穷循环while(1);的if分支,于是这个Satan_algo(Satan_algo)调用便永远不会返回(结束)了。
而如果Satan_algo(Satan_algo)不能结束(停机)呢,则if判断就会失败,从而选择另一个if分支并返回true,即Satan_algo(Satan_algo)又能够返回(停机)。
总之,我们有:
Satan_algo(Satan_algo)能够停机=>它不能停机
Satan_algo(Satan_algo)不能停机=>它能够停机
所以它停也不是,不停也不是。左右矛盾。
拉格朗日所说:“陛下,我们不需要(上帝)这个假设”[4]。
于是,我们的假设,即God_algo算法的存在性,便不成立了。正如这个证明相信每个程序员都能够容易的看懂。然而,这个看似不可捉摸的技巧背后其实隐藏着深刻的数学原理(甚至是哲学原理)。在没有认识到这一数学原理之前,至少我当时是对于图灵如何想出这一绝妙证明感到无法理解。但后面,在介绍完了与图灵的停机问题“同构”的Y combinator之后,我们会深入哥德尔的不完备性定理,在理解了哥德尔不完备性定理之后,我们从这一同样绝妙的定理出发,就会突然发现,离停机问题和神奇的Y combinator只是咫尺之遥而已。当然,最后我们会回溯到一切的尽头,康托尔那里,看看停机问题、Y combinator、以及不完备性定理是如何自然而然地由康托尔的对角线方法推导出来的,我们将会看到这些看似神奇的构造性证明的背后,其实是一个简洁优美的数学方法在起作用。
Y Combinator
了解Y combinator的请直接跳过这一节,到下一节“哥德尔的不完备性定理”。
让我们暂且搁下但记住绕人的图灵停机问题,走进函数式编程语言的世界,走进由跟图灵机理论等价的lambda算子发展出来的另一个平行的语言世界。让我们来看一看被人们一代一代吟唱着的神奇的Y Combinator…
Haskell B.Curry(Haskell语言就是以他命名的,而函数式编程语言里面的Curry手法也是以他命名)“发明”出来的组合算子(Haskell是研究组合逻辑(combinatory logic)的)仿佛有种神奇的魔力,它能够算出给定lambda表达式(函数)的不动点。从而使得递归成为可能。事实上,我们待会就会看到,Y Combinator在神奇的表面之下,其实隐藏着深刻的意义,其背后体现的意义,曾经开出过历史上最灿烂的数学之花,所以MIT的计算机科学系将它做成系徽也就不足为奇了[5]。
关于Y Combinator的文章可谓数不胜数,这个由师从希尔伯特的著名逻辑学家当然,要了解这个神奇的算子,我们需要一点点lambda算子理论的基础知识,不过别担心,lambda算子理论是我目前见过的最简洁的公理系统,这个系统仅仅由三条非常简单的公理构成,而这三条公理里面我们又只需要关注前两条。
以下小节——lambda calculus——纯粹是为了没有接触过lambda算子理论的读者准备的,并不属于本文重点讨论的东西,然而要讨论Y combinator就必须先了解一下lambda(当然,以编程语言来了解也行,但是你会看到,丘齐最初提出的lambda算子理论才是最最简洁和漂亮的,学起来也最省事。)所以我单独准备了一个小节来介绍它。如果你已经知道,可以跳过这一小节。不知道的读者也可以跳过这一小节去wikipedia上面看,这里的介绍使用了wikipedia上的方式
lambda calculus
先来看一下lambda表达式的基本语法(BNF):
<expr> ::= <identifier>
<expr> ::=lambda<identifier-list>. <expr>
<expr> ::= (<expr> <expr>)
前两条语法用于生成lambda表达式(lambda函数),如:
lambdax y. x + y
haskell里面为了简洁起见用“\”来代替希腊字母lambda,它们形状比较相似。故而上面的定义也可以写成:
\ x y. x + y
这是一个匿名的加法函数,它接受两个参数,返回两值相加的结果。当然,这里我们为了方便起见赋予了lambda函数直观的计算意义,而实际上lambda calculus里面一切都只不过是文本替换,有点像C语言的宏。并且这里的“+”我们假设已经是一个具有原子语义的运算符[6],此外,为了方便我们使用了中缀表达(按照lambda calculus系统的语法实际上应该写成“(+ x y)”才对——参考第三条语法)。
那么,函数定义出来了,怎么使用呢?最后一条规则就是用来调用一个lambda函数的:
((lambdax y. x + y) 2 3)
命令式语言(imperative language)惯用的调用形式有点区别,后者是“f(x, y)”,而这里是“(f x y)”,不过好在顺序没变:) )。为了表达简洁一点,我们可以给(lambdax y. x + y)起一个名字,像这样:
以上这一行就是把刚才定义的加法函数运用到2和3上(这个调用语法形式跟let Add = (lambdax 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算子系统中表达这一函数呢?理所当然的想法如下:
lambdan. If_Else n==0 1 n*<self>(n-1)
当然,上面的程序假定了If_Else是一个已经定义好的三元操作符(你可以想象C的“?:”操作符,后面跟的三个参数分别是判断条件、成功后求值的表达式、失败后求值的表达式。那么很显然,这个定义里面有一个地方没法解决,那就是<self>那个地方我们应该填入什么呢?很显然,熟悉C这类命令式语言的人都知道应该填入这个函数本身的名字,然而lambda算子系统里面的lambda表达式(或称函数)是没有名字的。
怎么办?难道就没有办法实现递归了?或者说,丘齐做出的这个lambda算子系统里面根本没法实现递归从而在计算能力上面有重大的缺陷?显然不是。马上你就会看到Y combinator是如何把一个看上去非递归的lambda表达式像变魔术那样变成一个递归版本的。在成功之前我们再失败一次,注意下面的尝试:
let F =lambdan. IF_Else n==0 1 n*F(n-1)
看上去不错,是吗?可惜还是不行。因为let F只是起到一个语法糖的作用,在它所代表的lambda表达式还没有完全定义出来之前你是不可以使用F这个名字的。更何况实际上丘齐当初的lambda算子系统里面也并没有这个语法元素,这只是刚才为了简化代码而引入的语法糖。当然,了解这个let语句还是有意义的,后面还会用到。
一次成功的尝试
在上面几次失败的尝试之后,我们是不是就一筹莫展了呢?别忘了软件工程里面的一条黄金定律:“任何问题都可以通过增加一个间接层来解决”。不妨把它沿用到我们面临的递归问题上:没错,我们的确没办法在一个lambda函数的定义里面直接(按名字)来调用其自身。但是,可不可以间接调用呢?
我们回顾一下刚才不成功的定义:
lambdan. If_Else n==0 1 n*<self>(n-1)
现在<self>处不是缺少“这个函数自身”嘛,既然不能直接填入“这个函数自身”,我们可以增加一个参数,也就是说,把<self>参数化:
lambdaselfn. If_Else n==0 1 n*self(n-1)
上面这个lambda算子总是合法定义了吧。现在,我们调用这个函数的时候,只要加传一个参数self,这个参数不是别人,正是这个函数自身。还是为了简单起见,我们用let语句来给上面这个函数起个别名:
let P =lambdaself 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 =lambdaselfn. If_Else n==0 1 n*self(self, n-1)
请注意,我们在P的函数体内调用self的时候增加了一个参数。现在当我们调用P(P, 3)的时候,展开就变成了: