图灵著名的停机问题对于软件开发者而已是非常熟悉的。下面简单描述停机问题：

假设给你一个计算机程序的源代码，也给你所有程序要用的数据，文件，硬盘，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之类的主题，就可以选择角度，互相参照。