原标题：康托尔、哥德尔、图灵 —— 永恒的金色对角线 原文链接：https://blog.csdn.net/pongba/article/details/1336028 By 刘未鹏 C++ 的罗浮宫 (http://blog.csdn.net/pongba) 我看到了它，却不敢相信它 [1] 。 —— 康托尔 计算机是数学家一次失败思考的产物。 —— 无名氏 哥德尔 的 不完备性定理 震撼了 20 世纪数学界的天空，其数学意义颠覆了 希尔伯特 的形式化数学的宏伟计划，其哲学意义直到 21 世纪的今天仍然不断被延伸到各个自然学科，深刻影响着人们的思维。 图灵 为了解决希尔伯特著名的 第十问题 而提出有效计算模型，进而作出了 可计算理论 和现代计算机的奠基性工作，著名的停机问题给出了机械计算模型的能力极限，其深刻的意义和漂亮的证明使它成为可计算理论中的标志性定理之一。 丘齐 ，跟图灵同时代的天才，则从另一个抽象角度提出了 lambda算子 的思想，与 图灵机 抽象的倾向于硬件性不同，丘齐的 lambda 算子理论是从数学的角度进行抽象，不关心运算的机械过程而只关心运算的抽象性质，只用最简洁的几条公理便建立起了与图灵机 完全等价 的计算模型，其体现出来的数学抽象美开出了 函数式编程语言 这朵奇葩， Lisp 、 Scheme 、 Haskell… 这些以抽象性和简洁美为特点的语言至今仍然活跃在计算机科学界，虽然由于其本质上源于 lambda 算子理论的抽象方式不符合人的思维习惯从而注定无法成为主流的编程语言 [2] ，然而这仍然无法妨碍它们成为编程理论乃至计算机学科的最佳教本。而诞生于函数式编程语言的神奇的 Y combinator 至今仍然让人们陷入深沉的震撼和反思当中 … 然而，这一切的一切，看似不很相关却又有点相关，认真思考其关系却又有点一头雾水的背后，其实隐隐藏着一条线，这条线把它们从本质上串到了一起，而顺着时光的河流逆流而上，我们将会看到，这条线的尽头，不是别人，正是只手拨开被不严密性问题困扰的 19 世纪数学界阴沉天空的天才数学家 康托尔 ，康托尔创造性地将一一对应和对角线方法运用到无穷集合理论的建立当中，这个被希尔伯特称为 “ 谁也无法将我们从康托尔为我们创造的乐园中驱逐出去 ” 、被罗素称为 “19 世纪最伟大的智者之一 ” 的人，他在 集合论方面的工作 终于驱散了不严密性问题带来的阴霾，仿佛一道金色的阳光刺破乌云， 19 世纪的数学终于看到了真正严格化的曙光，数学终于得以站在了前所未有的坚固的基础之上；集合论至今仍是数学里最基础和最重要的理论之一。而康托尔当初在研究无穷集合时最具天才的方法之一 —— 对角线方法 —— 则带来了极其深远的影响，其纯粹而直指事物本质的思想如洪钟大吕般响彻数学和哲学的每一个角落 [3] 。 随着本文的展开，你将会看到，刚才提到的一切，歌德尔的不完备性定理，图灵的停机问题， lambda 算子理论中神奇的 Y combinator 、乃至著名的罗素悖论、理发师悖论等等，其实都源自这个简洁、纯粹而同时又是最优美的数学方法，反过来说，从康托尔的对角线方法出发，我们可以轻而易举地推导出哥德尔的不完备性定理，而由后者又可以轻易导出停机问题和 Y combinator ，实际上，我们将会看到，后两者也可以直接由康托尔的对角线方法导出。尤其是 Y combinator ，这个形式上绕来绕去，本质上捉摸不透，看上去神秘莫测的算子，其实只是一个非常自然而然的推论，如果从哥德尔的不完备性定理出发，它甚至比停机问题还要来得直接简单。 总之，你将会看到这些看似深奥的理论是如何由一个至为简单而又至为深刻的数学方法得出的，你将会看到最纯粹的数学美。 1. 图灵的停机问题 (The Halting Problem) 了解停机问题的可以直接跳过这一节，到下一节“Y Combinator”，了解后者的再跳到下一节“哥德尔的不完备性定理” 我们还是从图灵著名的停机问题说起，一来它相对来说是我们要说的几个定理当中最简单的，二来它也最贴近程序员。实际上，我以前曾写过 一篇关于图灵机的文章 ，有兴趣的读者可以从那篇开始，那篇主要是从理论上阐述，所以这里我们打算避开抽象的理论，换一种符合程序员思维习惯的直观方式来加以解释。 1.1. 停机问题 不存在这样一个程序（算法），它能够计算任何程序（算法）在给定输入上是否会结束（停机）。 那么，如何来证明这个停机问题呢？反证。假设我们某一天真做出了这么一个极度聪明的万能算法（就叫 God_algo 吧），你只要给它一段程序（二进制描述），再给它这段程序的输入，它就能告诉你这段程序在这个输入上会不会结束（停机），我们来编写一下我们的这个算法吧： bool God_algo(char* program, char* input) { if(<program> 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) 不能停机 => 它能够停机 所以它停也不是，不停也不是。左右矛盾。 于是，我们的假设，即 God_algo 算法的存在性，便不成立了。正如 拉格朗日 所说： “ 陛下，我们不需要（上帝）这个假设 ”[4] 。 这个证明相信每个程序员都能够容易的看懂。然而，这个看似不可捉摸的技巧背后其实隐藏着深刻的数学原理（甚至是哲学原理）。在没有认识到这一数学原理之前，至少我当时是对于图灵如何想出这一绝妙证明感到无法理解。但后面，在介绍完了与图灵的停机问题 “ 同构 ” 的 Y combinator 之后，我们会深入哥德尔的不完备性定理，在理解了哥德尔不完备性定理之后，我们从这一同样绝妙的定理出发，就会突然发现，离停机问题和神奇的 Y combinator 只是咫尺之遥而已。当然，最后我们会回溯到一切的尽头，康托尔那里，看看停机问题、 Y combinator 、以及不完备性定理是如何自然而然地由康托尔的对角线方法推导出来的，我们将会看到这些看似神奇的构造性证明的背后，其实是一个简洁优美的数学方法在起作用。 下接第二部分《Y Combinator、Lambda算子和不动点原理》 Reference [1] 《数学——确定性的丧失》 [2] 也有观点认为函数式编程语言之所以没有广泛流行起来是因为一些实际的商业因素。 [3] Douglas R.Hofstadter的著作《Godel, Escher, Bach: An Eternal Golden Braid》（《哥德尔、艾舍尔、巴赫——集异璧之大成》）就是围绕这一思想写出的一本奇书。非常建议一读。 [4] 《数学——确定性的丧失》 [5] 虽然我觉得那个系徽做得太复杂，要表达这一简洁优美的思想其实还能有更好的方式。 [6] 关于如何在lambda calculus系统里实现“+”操作符以及自然数等等，可参见 这里， 这里，和 这里。 [7] g9的blog（负暄琐话） http://blog.csdn.net/g9yuayon/ 上有一系列介绍lambda calculus的文章（当然，还有其它好文章:)），非常不错，强烈推荐。最近的两篇就是介绍Y combinator的。其中有一篇以javaScript语言描述了迭代式逐步抽象出Y Combinator的过程。 [8] 实际上这只是第一不完备性定理，它还有一个推论，被称为第二不完备性定理，说的是任一个系统T内无法证明这个系统本身的一致性。这个定理的证明核心思想如下：我们前面证明第一不完备性定理的时候用的推断其实就表明 Con/T -> G(g) （自然语言描述就是，由系统T的无矛盾，可以推出G(g)成立），而这个“Con/T -> G(g)”本身又是可以在T内表达且证明出来的（具体怎么表达就不再多说了）——只需要用排中律即可。于是我们立即得到，T里面无法推出Con/T，因为一旦推出Con/T就立即推出G(g)从而推出UnPr(G(g))，这就矛盾了。所以，Con/T无法在T内推出（证明）。 |
