《康托尔哥德尔图灵——永恒金色对角线.doc》由会员分享，可在线阅读，更多相关《康托尔哥德尔图灵——永恒金色对角线.doc（23页珍藏版）》请在金锄头文库上搜索。
1、康托尔、哥德尔、图灵永久的金色对角线康托尔、哥德尔、图灵永久的金色对角线我看到了它，却不敢相信它。康托尔哥德尔的不齐备性定理震惊了20世纪数学界的天空，其数学意义推翻了希尔伯特的形式化数学的雄伟计划，其哲学意义直到21世纪的今日仍旧不断被延长到各个自然学科，深刻影响着人们的思想。图灵为认识决希尔伯特有名的第十问题而提出有效计算模型，从而作出了可计算理论和现代计算机的奠定性工作，有名的停机问题给出了机械计算模型的能力极限，其深刻的意义和美丽的证明使它成为可计算理论中的标记性定理之一。丘齐，跟图灵同时代的天才，则从另一个抽象角度提出了lambda算子的思想，与图灵机抽象的倾向于硬件性不同，丘齐的l
2、ambda算子理论是从数学的角度进行抽象，不关怀运算的机械过程而只关怀运算的抽象性质，只用最简短的几条公义便成立起了与图灵机完整等价的计算模型，其表现出来的数学抽象美开出了函数式编程语言这朵奇葩，Lisp、Scheme、Haskell这些以抽象性和简短美为特色的语言到现在仍旧活跃在计算机科学界，固然因为其实质上源于lambda算子理论的抽象方式不切合人的思想习惯从而注定无法成为主流的编程语言2，但是这仍旧无法阻碍它们成为编程理论以致计算机学科的最正确教本。而出生于函数式编程语言的奇特的Ycombinator到现在仍旧让人们堕入深邃的震惊和反省中间但是，这全部的全部，看似不很有关却又有点有关，仔
3、细思虑其关系却又有点一头雾水的背后，其实隐约藏着一条线，这条线把它们从实质上串到了一起，而顺着光阴的河流逆流而上，我们将会看到，这条线的终点，不是他人，正是只手扒开被不严实性问题困扰的19世纪数学界阴森天空的天才数学家康托尔，康托尔创建性地将一一对应和对角线方法运用到无量会合理论的成立中间，这个被希尔伯特称为“谁也无法将我们从康托尔为我们创建的乐园中驱赶出去”、被罗素称为“19世纪最伟大的智者之一”的人，他在会合论方面的工作终于遣散了不严实性问题带来的阴霾，忧如一道金色的阳光刺破乌云，19世纪的数学终于看到了真实严格化的曙光，数学终于得以站在了亘古未有的牢固的基础之上；会合论到现在还是数学里最
4、基础和最重要的理论之一。而康托尔当初在研究无量会合时最具天才的方法之一对角线方法则带来了极其深远的影响，其纯粹而直指事物实质的思想如洪钟大吕般响彻数学和哲学的每一个角落3。跟着本文的睁开，你将会看到，方才提到的全部，歌德尔的不齐备性定理，图灵的停机问题，lambda算子理论中奇特的Ycombinator、以致有名的罗素悖论、剪发师悖论等等，其实都源自这个简短、纯粹而同时又是最优美的数学方法，反过来说，从康托尔的对角线方法出发，我们能够易如反掌地推导出哥德尔的不完备性定理，而由后者又能够轻易导出停机问题和Ycombinator，实质上，我们将会看到，后二者也能够直接由康托尔的对角线方法导出。特别
5、是Ycombinator，这个形式上绕来绕去，实质上捉摸不透，看上去神奇莫测的算子，其实不过一个特别自但是然的推论，假如从哥德尔的不齐备性定理出发，它甚至比停机问题还要来得直接简单。总之，你将会看到这些看似高深的理论是怎样由一个至为简单而又至为深刻的数学方法得出的，你将会看到最纯粹的数学美。/图灵的停机问题(TheHaltingProblem)认识停机问题的能够直接跳过这一节，到下一节“YCombinator”，认识后者的再跳到下一节“哥德尔的不齐备性定理”我们还是从图灵有名的停机问题提及，一来它相对来说是我们要说的几个定应中间最简单的，二来它也最切近程序员。实质上，我从前曾写过一篇对于图灵机
6、的文章，有兴趣的读者能够从那篇开始，那篇主假如从理论上论述，所以这里我们打算避开抽象的理论，换一种切合程序员思想习惯的直观方式来加以解说。停机问题不存在这样一个程序（算法），它能够计算任何程序（算法）在给定输入上能否会结束（停机）。那么，怎样来证明这个停机问题呢？反证。假定我们某一天真做出了这么一个极度聪慧的全能算法（就叫God_algo吧），你只需给它一段程序（二进制描绘），再给它这段程序的输入，它就能告诉你这段程序在这个输入上会不会结束（停机），我们来编写一下我们的这个算法吧：boolGod_algo(char*program,char*input)if(haltson)returntru
7、e;returnfalse;这里我们假定if的判断语句里面是你天才情虑的结晶，它能够像上帝相同洞察全部程序的宿命。此刻，我们从这个God_algo出发导出一个新的算法：boolSatan_algo(char*program)if(God_algo(program,program)while(1);/loopforever!returnfalse;/cannevergethere!elsereturntrue;正如它的名字所示意的那样，这个算法即是全部险恶的本源了。当我们把这个算法运用到它自己身上时，会发生什么呢？Satan_algo(Satan_algo);我们来剖析一下这行简单的调用：明显，
8、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_al
9、go)又能够返回（停机）。总之，我们有：Satan_algo(Satan_algo)能够停机=它不可以停机Satan_algo(Satan_algo)不可以停机=它能够停机所以它停也不是，不断也不是。左右矛盾。于是，我们的假定，即God_algo算法的存在性，便不可以立了。正如拉格朗日所说：“陛下，我们不需要（上帝）这个假定”4。这个证明相信每个程序员都能够简单的看懂。但是，这个看似不可以捉摸的技巧背后其实隐蔽着深刻的数学原理（甚至是哲学原理）。在没有认识到这一数学原理从前，起码我当时是对于图灵怎样想出这一绝妙证明感觉无法理解。但后边，在介绍完了与图灵的停机问题“同构”的Ycombinator
10、以后，我们会深入哥德尔的不齐备性定理，在理解了哥德尔不齐备性定理以后，我们从这一起样绝妙的定理出发，就会忽然发现，离停机问题和奇特的Ycombinator不过咫尺之遥而已。自然，最后我们会回溯到全部的终点，康托尔那边，看看停机问题、Ycombinator、以及不齐备性定理是怎样自但是然地由康托尔的对角线方法推导出来的，我们将会看到这些看似奇特的结构性证明的背后，实质上是一个简短优美的数学方法在起作用。YCombinator认识Ycombinator的请直接跳过这一节，到下一节“哥德尔的不齐备性定理”。让我们姑且搁下但记着绕人的图灵停机问题，走进函数式编程语言的世界，走进由跟图灵机理论等价的la
11、mbda算子发展出来的另一个平行的语言世界。让我们来看一看被人们一代一代吟唱着的奇特的YCombinator对于YCombinator的文章堪称不计其数，这个由师从希尔伯特的有名逻辑学家HaskellB.Curry（Haskell语言就是以他命名的，而函数式编程语言里面的Curry手法也是以他命名）“发明”出来的组合算子（Haskell是研究组合逻辑(combinatorylogic)的）忧如有种奇特的魔力，它能够算出给定lambda表达式（函数）的不动点。从而使得递归成为可能。事实上，我们待会就会看到，YCombinator在奇特的表面之下，其实隐蔽着深刻的意义，其背后表现的意义，以前开出过
12、历史上最绚烂的数学之花，所以MIT的计算机科学系将它做成系徽也就不以为奇了5。自然，要认识这个奇特的算子，我们需要一点点lambda算子理论的基础知识，可是别担心，lambda算子理论是我当前见过的最简短的公义系统，这个系统不过由三条特别简单的公义组成，而这三条公义里面我们又只需要关注前两条。以下小节lambdacalculus纯粹是为了没有接触过lambda算子理论的读者准备的，其实不属于本文要点议论的东西，但是要议论Ycombinator就一定先认识一下lambda（当然，以编程语言来认识也行，可是你会看到，丘齐最初提出的lambda算子理论才是最最简短和美丽的，学起来也最省事。）所以我独
13、自准备了一个小节来介绍它。假如你已经知道，能够跳过这一小节。不知道的读者也能够跳过这一小节去wikipedia上边看，这里的介绍使用了wikipedia上的方式lambdacalculus先来看一下lambda表达式的基本语法(BNF)：:=:=lambda.:=()前两条语法用于生成lambda表达式（lambda函数），如：lambdaxy.x+yhaskell里面为了简短起见用“”来取代希腊字母lambda，它们形状比较相像。故而上边的定义也能够写成：xy.x+y这是一个匿名的加法函数，它接受两个参数，返回两值相加的结果。自然，这里我们为了方便起见给予了lambda函数直观的计算意义，而实质上lambdacalculus里面全部都只可是是文本替代，有点像C语言的宏。并且这里的“+”我们假定已经是一个拥有原子语义的运算符6，别的，为了方便我们使用了中缀表达（依据lambdacalculus系统的语法实质上应当写成“(+xy)”才对参照第三条语法）。那么，函数定义出来了，怎么使用呢？最后一条规则就是用来调用一个lambda函数的：(lambdaxy.x+y)23)以上这一行就是把方才定义的加法函数运用到2和3上（这个调用语法形式跟命令式语言
