康托尔哥德尔图灵永恒的金色对角线.docx
《康托尔哥德尔图灵永恒的金色对角线.docx》由会员分享，可在线阅读，更多相关《康托尔哥德尔图灵永恒的金色对角线.docx（35页珍藏版）》请在冰点文库上搜索。
康托尔哥德尔图灵永恒的金色对角线
康托尔、哥德尔、图灵——永恒的金色对角线（rev#2）
By刘未鹏
C++的罗浮宫（
我看到了它，却不敢相信它[1]。
——康托尔
计算机是数学家一次失败思考的产物。
——无名氏
哥德尔的不完备性定理震撼了20世纪数学界的天空，其数学意义颠覆了希尔伯特的形式化数学的宏伟计划，其哲学意义直到21世纪的今天仍然不断被延伸到各个自然学科，深刻影响着人们的思维。
图灵为了解决希尔伯特著名的第十问题而提出有效计算模型，进而作出了可计算理论和现代计算机的奠基性工作，著名的停机问题给出了机械计算模型的能力极限，其深刻的意义和漂亮的证明使它成为可计算理论中的标志性定理之一。
丘齐，跟图灵同时代的天才，则从另一个抽象角度提出了lambda算子的思想，与图灵机抽象的倾向于硬件性不同，丘齐的lambda算子理论是从数学的角度进行抽象，不关心运算的机械过程而只关心运算的抽象性质，只用最简洁的几条公理便建立起了与图灵机完全等价的计算模型，其体现出来的数学抽象美开出了函数式编程语言这朵奇葩，Lisp、Scheme、Haskell…这些以抽象性和简洁美为特点的语言至今仍然活跃在计算机科学界，虽然由于其本质上源于lambda算子理论的抽象方式不符合人的思维习惯从而注定无法成为主流的编程语言[2]，然而这仍然无法妨碍它们成为编程理论乃至计算机学科的最佳教本。
而诞生于函数式编程语言的神奇的Ycombinator至今仍然让人们陷入深沉的震撼和反思当中…
然而，这一切的一切，看似不很相关却又有点相关，认真思考其关系却又有点一头雾水的背后，其实隐隐藏着一条线，这条线把它们从本质上串到了一起，而顺着时光的河流逆流而上，我们将会看到，这条线的尽头，不是别人，正是只手拨开被不严密性问题困扰的19世纪数学界阴沉天空的天才数学家康托尔，康托尔创造性地将一一对应和对角线方法运用到无穷集合理论的建立当中，这个被希尔伯特称为“谁也无法将我们从康托尔为我们创造的乐园中驱逐出去”、被罗素称为“19世纪最伟大的智者之一”的人，他在集合论方面的工作终于驱散了不严密性问题带来的阴霾，仿佛一道金色的阳光刺破乌云，19世纪的数学终于看到了真正严格化的曙光，数学终于得以站在了前所未有的坚固的基础之上；集合论至今仍是数学里最基础和最重要的理论之一。
而康托尔当初在研究无穷集合时最具天才的方法之一——对角线方法——则带来了极其深远的影响，其纯粹而直指事物本质的思想如洪钟大吕般响彻数学和哲学的每一个角落[3]。
随着本文的展开，你将会看到，刚才提到的一切，歌德尔的不完备性定理，图灵的停机问题，lambda算子理论中神奇的Ycombinator、乃至著名的罗素悖论、理发师悖论等等，其实都源自这个简洁、纯粹而同时又是最优美的数学方法，反过来说，从康托尔的对角线方法出发，我们可以轻而易举地推导出哥德尔的不完备性定理，而由后者又可以轻易导出停机问题和Ycombinator，实际上，我们将会看到，后两者也可以直接由康托尔的对角线方法导出。
尤其是Ycombinator，这个形式上绕来绕去，本质上捉摸不透，看上去神秘莫测的算子，其实只是一个非常自然而然的推论，如果从哥德尔的不完备性定理出发，它甚至比停机问题还要来得直接简单。
总之，你将会看到这些看似深奥的理论是如何由一个至为简单而又至为深刻的数学方法得出的，你将会看到最纯粹的数学美。
图灵的停机问题（TheHaltingProblem）
了解停机问题的可以直接跳过这一节，到下一节“YCombinator”，了解后者的再跳到下一节“哥德尔的不完备性定理”
我们还是从图灵著名的停机问题说起，一来它相对来说是我们要说的几个定理当中最简单的，二来它也最贴近程序员。
实际上，我以前曾写过一篇关于图灵机的文章，有兴趣的读者可以从那篇开始，那篇主要是从理论上阐述，所以这里我们打算避开抽象的理论，换一种符合程序员思维习惯的直观方式来加以解释。
停机问题
不存在这样一个程序（算法），它能够计算任何程序（算法）在给定输入上是否会结束（停机）。
那么，如何来证明这个停机问题呢？
反证。
假设我们某一天真做出了这么一个极度聪明的万能算法（就叫God_algo吧），你只要给它一段程序（二进制描述），再给它这段程序的输入，它就能告诉你这段程序在这个输入上会不会结束（停机），我们来编写一下我们的这个算法吧：
boolGod_algo（char*program,char*input）
{
if（haltson）
returntrue;
returnfalse;
}
这里我们假设if的判断语句里面是你天才思考的结晶，它能够像上帝一样洞察一切程序的宿命。
现在，我们从这个God_algo出发导出一个新的算法：
boolSatan_algo（char*program）
{
if（God_algo（program,program））{
while
（1）;//loopforever!
returnfalse;//cannevergethere!
}
else
returntrue;
}
正如它的名字所暗示的那样，这个算法便是一切邪恶的根源了。
当我们把这个算法运用到它自身身上时，会发生什么呢？
Satan_algo（Satan_algo）;
我们来分析一下这行简单的调用：
显然，Satan_algo（Satan_algo）这个调用要么能够运行结束返回（停机），要么不能返回（loopforever）。
如果它能够结束，那么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）不能停机=>它能够停机
所以它停也不是，不停也不是。
左右矛盾。
于是，我们的假设，即God_algo算法的存在性，便不成立了。
正如拉格朗日所说：
“陛下，我们不需要（上帝）这个假设”[4]。
这个证明相信每个程序员都能够容易的看懂。
然而，这个看似不可捉摸的技巧背后其实隐藏着深刻的数学原理（甚至是哲学原理）。
在没有认识到这一数学原理之前，至少我当时是对于图灵如何想出这一绝妙证明感到无法理解。
但后面，在介绍完了与图灵的停机问题“同构”的Ycombinator之后，我们会深入哥德尔的不完备性定理，在理解了哥德尔不完备性定理之后，我们从这一同样绝妙的定理出发，就会突然发现，离停机问题和神奇的Ycombinator只是咫尺之遥而已。
当然，最后我们会回溯到一切的尽头，康托尔那里，看看停机问题、Ycombinator、以及不完备性定理是如何自然而然地由康托尔的对角线方法推导出来的，我们将会看到这些看似神奇的构造性证明的背后，其实是一个简洁优美的数学方法在起作用。
YCombinator
了解Ycombinator的请直接跳过这一节，到下一节“哥德尔的不完备性定理”。
让我们暂且搁下但记住绕人的图灵停机问题，走进函数式编程语言的世界，走进由跟图灵机理论等价的lambda算子发展出来的另一个平行的语言世界。
让我们来看一看被人们一代一代吟唱着的神奇的YCombinator…
关于YCombinator的文章可谓数不胜数，这个由师从希尔伯特的著名逻辑学家HaskellB.Curry（Haskell语言就是以他命名的，而函数式编程语言里面的Curry手法也是以他命名）“发明”出来的组合算子（Haskell是研究组合逻辑（combinatorylogic）的）仿佛有种神奇的魔力，它能够算出给定lambda表达式（函数）的不动点。
从而使得递归成为可能。
事实上，我们待会就会看到，YCombinator在神奇的表面之下，其实隐藏着深刻的意义，其背后体现的意义，曾经开出过历史上最灿烂的数学之花，所以MIT的计算机科学系将它做成系徽也就不足为奇了[5]。
当然，要了解这个神奇的算子，我们需要一点点lambda算子理论的基础知识，不过别担心，lambda算子理论是我目前见过的最简洁的公理系统，这个系统仅仅由三条非常简单的公理构成，而这三条公理里面我们又只需要关注前两条。
以下小节——lambdacalculus——纯粹是为了没有接触过lambda算子理论的读者准备的，并不属于本文重点讨论的东西，然而要讨论Ycombinator就必须先了解一下lambda（当然，以编程语言来了解也行，但是你会看到，丘齐最初提出的lambda算子理论才是最最简洁和漂亮的，学起来也最省事。
）所以我单独准备了一个小节来介绍它。
如果你已经知道，可以跳过这一小节。
不知道的读者也可以跳过这一小节去wikipedia上面看，这里的介绍使用了wikipedia上的方式
lambdacalculus
先来看一下lambda表达式的基本语法（BNF）：
:
:
=
:
:
=lambda.
:
:
=（）
前两条语法用于生成lambda表达式（lambda函数），如：
lambdaxy.x+y
haskell里面为了简洁起见用“\”来代替希腊字母lambda，它们形状比较相似。
故而上面的定义也可以写成：
\xy.x+y
这是一个匿名的加法函数，它接受两个参数，返回两值相加的结果。
当然，这里我们为了方便起见赋予了lambda函数直观的计算意义，而实际上lambdacalculus里面一切都只不过是文本替换，有点像C语言的宏。
并且这里的“+”我们假设已经是一个具有原子语义的运算符[6]，此外，为了方便我们使用了中缀表达（按照lambdacalculus系统的语法实际上应该写成“（+xy）”才对——参考第三条语法）。
那么，函数定义出来了，怎么使用呢？
最后一条规则就是用来调用一个lambda函数的：
（（lambdaxy.x+y）23）
以上这一行就是把刚才定义的加法函数运用到2和3上（这个调用语法形式跟命令式语言（imperativelanguage）惯用的调用形式有点区别，后者是“f（x,y）”，而这里是“（fxy）”，不过好在顺序没变:
））。
为了表达简洁一点，我们可以给（lambdaxy.x+y）起一个名字，像这样：
letAdd=（lambdaxy.x+y）
这样我们便可以使用Add来表示该lambda函数了：
（Add23）
不过还是为了方便起见，后面调用的时候一般用“Add（2,3）”，即我们熟悉的形式。
有了语法规则之后，我们便可以看一看这个语言系统的两条简单至极的公理了：
Alpha转换公理：
例如，“lambdaxy.x+y”转换为“lambdaab.a+b”。
换句话说，函数的参数起什么名字没有关系，可以随意替换，只要函数体里面对参数的使用的地方也同时注意相应替换掉就是了。
Beta转换公理：
例如，“（lambdaxy.x+y）23”转换为“2+3”。
这个就更简单了，也就是说，当把一个lambda函数用到参数身上时，只需用实际的参数来替换掉其函数体中的相应变量即可。
就这些。
是不是感觉有点太简单了？
但事实就是如此，lambda算子系统从根本上其实就这些东西，然而你却能够从这几个简单的规则中推演出神奇无比的Ycombinator来。
我们这就开始！
递归的迷思
敏锐的你可能会发现，就以上这两条公理，我们的lambda语言中无法表示递归函数，为什么呢？
假设我们要计算经典的阶乘，递归描述肯定像这样：
f（n）:
ifn==0return1
returnn*f（n-1）
当然，上面这个程序是假定n为正整数。
这个程序显示了一个特点，f在定义的过程中用到了它自身。
那么如何在lambda算子系统中表达这一函数呢？
理所当然的想法如下：
lambdan.If_Elsen==01n*（n-1）
当然，上面的程序假定了If_Else是一个已经定义好的三元操作符（你可以想象C的“?
:
”操作符，后面跟的三个参数分别是判断条件、成功后求值的表达式、失败后求值的表达式。
那么很显然，这个定义里面有一个地方没法解决，那就是那个地方我们应该填入什么呢？
很显然，熟悉C这类命令式语言的人都知道应该填入这个函数本身的名字，然而lambda算子系统里面的lambda表达式（或称函数）是没有名字的。
95105105
怎么办？
难道就没有办法实现递归了？
或者说，丘齐做出的这个lambda算子系统里面根本没法实现递归从而在计算能力上面有重大的缺陷？
显然不是。
马上你就会看到Ycombinator是如何把一个看上去非递归的lambda表达式像变魔术那样变成一个递归版本的。
在成功之前我们再失败一次，注意下面的尝试：
letF=lambdan.IF_Elsen==01n*F（n-1）
看上去不错，是吗？
可惜还是不行。
因为letF只是起到一个语法糖的作用，在它所代表的lambda表达式还没有完全定义出来之前你是不可以使用F这个名字的。
更何况实际上丘齐当初的lambda算子系统里面也并没有这个语法元素，这只是刚才为了简化代码而引入的语法糖。
当然，了解这个let语句还是有意义的，后面还会用到。
一次成功的尝试
在上面几次失败的尝试之后，我们是不是就一筹莫展了呢？
别忘了软件工程里面的一条黄金定律：
“任何问题都可以通过增加一个间接层来解决”。
不妨把它沿用到我们面临的递归问题上：
没错，我们的确没办法在一个lambda函数的定义里面直接（按名字）来调用其自身。
但是，可不可以间接调用呢？
我们回顾一下刚才不成功的定义：
lambdan.If_Elsen==01n*（n-1）
现在处不是缺少“这个函数自身”嘛，既然不能直接填入“这个函数自身”，我们可以增加一个参数，也就是说，把参数化：
lambdaselfn.If_Elsen==01n*self（n-1）
上面这个lambda算子总是合法定义了吧。
现在，我们调用这个函数的时候，只要加传一个参数self，这个参数不是别人，正是这个函数自身。
还是为了简单起见，我们用let语句来给上面这个函数起个别名：
letP=lambdaselfn.If_Elsen==01n*self（n-1）
我们这样调用，比如说我们要计算3的阶乘：
P（P,3）
也就是说，把P自己作为P的第一个参数（注意，调用的时候P已经定义完毕了，所以我们当然可以使用它的名字了）。
这样一来，P里面的self处不就等于是P本身了吗？
自身调用自身，递归！
可惜这只是个美好的设想，还差一点点。
我们分析一下P（P,3）这个调用。
利用前面讲的Beta转换规则，这个函数调用展开其实就是（你可以完全把P当成一个宏来进行展开！
）：
IF_Elsen==01n*P（n-1）
看出问题了吗？
这里的P（n-1）虽然调用到了P，然而只给出了一个参数；而从P的定义来看，它是需要两个参数的（分别为self和n）！
也就是说，为了让P（n-1）变成良好的调用，我们得加一个参数才行，所以我们得稍微修改一下P的定义：
letP=lambdaselfn.If_Elsen==01n*self（self,n-1）
请注意，我们在P的函数体内调用self的时候增加了一个参数。
现在当我们调用P（P,3）的时候，展开就变成了：
IF_Else3==013*P（P,3-1）
而P（P,3-1）是对P合法的递归调用。
这次我们真的成功了！
不动点原理
然而，看看我们的P的定义，是不是很丑陋？
“n*self（self,n-1）”？
什么玩意？
为什么要多出一个多余的self？
DRY！
怎么办呢？
我们想起我们一开始定义的那个失败的P，虽然行不通，但最初的努力往往是大脑最先想到的最直观的做法，我们来回顾一下：
letP=lambdaselfn.If_Elsen==01n*self（n-1）
这个P的函数体就非常清晰，没有冗余成分，虽然参数列表里面多出一个self，但我们其实根本不用管它，看函数体就行了，self这个名字已经可以说明一切了对不对？
但很可惜这个函数不能用。
我们再来回想一下为什么不能用呢？
因为当你调用P（P,n）的时候，里面的self（n-1）会展开为P（n-1）而P是需要两个参数的。
唉，要是这里的self是一个“真正”的，只需要一个参数的递归阶乘函数，那该多好啊。
为什么不呢？
干脆我们假设出一个“真正”的递归阶乘函数：
power（n）:
if（n==0）return1;
returnn*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_Else3==013*power（3-1）
发生了什么？
？
power（3-1）将会计算出2的阶乘（别忘了，power是我们设想的完美递归函数），所以这个式子将会忠实地计算出3的阶乘！
回想一下我们是怎么完成这项任务的：
我们设想了一个以某种方式构造出来的完美的能够内部自己调用自己的递归阶乘函数power，我们发现把这个power传给P的话，P（power,n）的展开式就是真正的递归计算n阶乘的代码了。
你可能要说：
废话！
都有了power了我们还要费那事把它传给P来个P（power,n）干嘛？
直接power（n）不就得了？
!
别急，之所以设想出这个power只是为了引入不动点的概念，而不动点的概念将会带领我们发现Ycombinator。
什么是不动点？
一点都不神秘。
让我们考虑刚才的power与P之间的关系。
一个是真正可递归的函数，一个呢，则是以一个额外的self参数来试图实现递归的伪递归函数，我们已经看到了把power交给P为参数发生了什么，对吧？
不，似乎还没有，我们只是看到了，“把power加上一个n一起交给P为参数”能够实现真正的递归。
现在我们想考虑power跟P之间的关系，直接把power交给P如何？
P（power）
这是什么？
这叫函数的部分求值（partialevaluation）。
换句话说，第一个参数是给出来了，但第二个参数还悬在那里，等待给出。
那么，光给一个参数得到的是什么呢？
是“还剩一个参数待给的一个新的函数”。
其实也很简单，只要按照Beta转换规则做就是了，把P的函数体里面的self出现处皆替换为power就可以了。
我们得到：
IF_Elsen==01n*power（n-1）
当然，这个式子里面还有一个变量没有绑定，那就是n，所以这个式子还不能求值，你需要给它一个n才能具体求值，对吧。
这么说，这可不就是一个以n为参数的函数么？
实际上就是的。
在lambda算子系统里面，如果给一个lambda函数的参数不足，则得到的就是一个新的lambda函数，这个新的lambda函数所接受的参数也就是你尚未给出的那些参数。
换句话来说，调用一个lambda函数可以分若干步来进行，每次只给出一部分参数，而只有等所有参数都给齐了，函数的求值结果才能出来，否则你得到的就是一个“中间函数”。
那么，这跟不动点定理有什么关系？
关系大了，刚才不是说了，P（power）返回的是一个新的“中间函数”嘛？
这个“中间函数”的函数体我们刚才已经看到了，就是简单地展开P（power）而已，回顾一遍：
IF_Elsen==01n*power（n-1）
我们已经知道，这是个函数，参数n待定。
因此我们不妨给它加上一个“lambdan”的帽子，这样好看一点：
lambdan.IF_Elsen==01n*power（n-1）
这是什么呢？
这可不就是power本身的定义？
（当然，如果我们能够定义power的话）。
不信我们看看power如果能够定义出来像什么样子：
letpower=lambdan.IF_Elsen==01n*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，是指这样的形式：
letP=lambdaselfn.If_Elsen==01n*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具有性质：
升级会员 