图灵著名的停机问题对于软件开发者而已是非常熟悉的。下面简单描述停机问题:
假设给你一个计算机程序的源代码,也给你所有程序要用的数据,文件,硬盘,DVD等等,所有它需要处理的东西。你能告诉我程序最终是否能够输出我们需要的结果吗,并且在工作完成之后,程序是就退出,还是会永远运行下去不会停止呢?换句话所就是,对于它会不会停止这个问题, 检查程序和数据,是不是足以能够让你回答是或否呢?
图灵对于停机问题不可解决的证明是决定性的。没有一个软件仅靠检查另一个软件的源代码,就能够决定它是否会停止运行,还是会永远运行。这是从软件领域对哥德尔证明的重新表述。很多程度上这个证明与哥德尔的是相同的,只是更容易理解,这个证明可以表示成简单的软件代码,而不是令人费解的运行在逻辑语法上的函数。停机问题的证明对开发人员是很容易理解的,但对其它人来讲并没有太大用处,因此,我们这里就不去讲述了。可以自己去读。
不用枯燥的证明,我们用一个实际的例子来展示。比如我向你要一个预言,下面这个程序会不会停止呢?
从$x=4$开始。给我第一个素数$p$,$p$小于$x$。如果$x-p$也是素数,把$x$加2然后继续。如果不是,让$p$作为下一个小的素数然后重新开始。重复以上直到$p=2$。如果$x-p$还不是素数,打印$x$然后退出。
问题并不复杂,而且对于任何现代的计算机语言来讲都很简单。假设我们不知道停机问题,那很可能会想这样简单的问题应该是容易预测的。
迷惑之处在于,我没有说是任何程序。上面的语句描述的是著名的哥德巴赫猜想,300年来都是不可证明的。软件仅仅检查这个语句“每个大于2的偶数能够用2个素数之和表示”是否为真,然后移到下一个偶数。对所有前4,000,000,000,000,000,000个数检查下来,我们仍然没有得到一个真正的数学证明。
关键在于,知道这几行代码是否停止等于证明哥德巴赫猜想!如果猜想是真则软件不会停止,检查所有直到无穷大的数,都不会发现任何一个破坏这个规则的数。如果猜想为假,那软件就会在找到第一个破坏规则的数之后停止。
有些有趣的东西正在发生。很明显软件只是另一个写逻辑形式系统的方法。我们能用语言或者软件,甚至更低级别的纯粹的哥德尔风格的逻辑算符,如果想的话。然而,基本上,几行语句就能够表示数学上最基础的问题。知道什么时候程序会停止-给出我们想要的结果-和证明难以置信的难题一样困难。我们甚至可以重新用哥德尔的递归函数来写这个软件,然后写这样一个语句“这个函数在某个数之后停止是否为真”。同样是又一次证明这个语句和证明哥德巴赫猜想是一样的。
哥德巴赫猜想目前是数学上一个很大的不可解问题。或者某天有人会真正找到证明;但很可能是某人不用其他公理,证明这个猜想是不可决定的。这样的证明不可思议地难,但类似的问题以前也曾经被证明过。
即使形式系统中最简单的表达式,比如几行软件代码,都能表示非常难的语句,对于我们目前的数学知识,其中一些是不能决定的。软件限制不了其他软件。软件又是如此普遍的存在,以至于行为完全不可预测。另一个软件不能预先告诉你结果会是什么。得到结果的唯一的办法,只有等他运行完毕-可能几小时,或者永远运行下去。
停机问题显示出硬币的另一面。如果一个语句是不可判定的,你不能作弊,只能写一个软件去检查它。软件轻易就可以表示那个语句,但它可能会用无尽的时间去完成它的工作。只要语句的不可判定无法证明,你就证明不了软件是不是会停止。无穷的知识,更多的证明就在那里:然而这些知识却触摸不到,只要我们受限于当前的系统。
既然现在我们开始处理无穷,就是时候了解更多了。大概40年前哥德尔打开大门时,另一个辉煌的思想正在分析关于无穷的问题。
我们思考无穷的时候,第一个想到的就是无穷大。但比起一行简单递增的数字来讲,无穷变得更加有趣。我们考察自然数和实数。我们知道自然数是$1,2,3$这样的序列,用于计数。我们用实数来衡量真实世界里面的元素,-即,两点间的距离是1.23米之类。无穷的自然数和无穷的实数一样显而易见。
格奥尔格.康托尔证明了一个惊人的结论,称为康托尔对角证明,即就算用无穷的自然数,我们仍然不能对实数进行计数!不知道怎么了,无穷多个自然数其实不够“无穷”!而且有不同类型的无穷;由实数组成的无穷,要比自然数组成的无穷更强大。这个证明惊人地简单。
【证明略...对角引理】
很明显连续无穷更强大。那是属于我们周围真实世界的无穷,我们世界里的每个东西都是实数描述的。然而我们永远不知道任意这些实数的准确数字。我们永远局限在我们仪器的误差之中。我们的测量工具在某个地方舍弃了数据,包含无穷的数字的实数被截断。
【...】
这篇文章其实是一篇非常好的引入计算理论和lambda calculus的文章。读者可以知道图灵机实际上是数学问题,而lambda其实是一个逻辑系统。能够在二者之间建立起初步的概念。然后在Reducibility和NP之类的主题,就可以选择角度,互相参照。
哥德尔,图灵和康托尔 part 2 停机问题,布布扣,bubuko.com
原文地址:http://www.cnblogs.com/mlnlp/p/3774138.html