停机问题 — 有些程序,谁都写不出来
这一章讲三件事: 「不可解」在这里的准确含义(它不是「很难」); 那个谁都写不出来的程序长什么样、为什么写不出来; 以及这条界和第 13 章那条界的区别。
它在全书链条里的位置: 这是全书的最高点。 第 13 章说有些问题跑不完(慢),这一章说有些问题根本写不出程序(不可能)。 而证明它要用第 15 章的反证法和第 16 章的数数结果。 需要的基础: 第 15、16 章。
1. 先把「解不了」这个词说清楚
这一节必须先做减法,因为「解不了」这三个字有太多意思。
原书专门澄清了这个词。不可解问题不是 下面这三种1:
| 不是这个 | 为什么不是 |
|---|---|
| 「要花很长时间才能解的问题」 | 那是第 13 章讲的(跑两千年),它有解 |
| 「本来就无解的问题」 | 那是题目本身没答案 |
| 「目前谁都不知道解法的问题」 | 那是还没被解决,不是不能被解决 |
不可解问题的意思是:原则上不能用程序来解决的问题2。 没人能写出解决它的程序——不是现在写不出,是永远写不出; 和机器有多快、语言有多先进,全都没有关系。
这一章要展示一个具体的例子。
2. 程序的行为只有两种
这一节是准备工作,建立走查要用的语言。
一个程序跑起来,结果只有两种3:
- 在有限时间内结束(是 1 秒还是 100 亿年都算,只要有个头);
- 永远不结束。
注意第一条的宽松:即使程序报错退出,也算「在有限时间内结束」4。
永不结束的程序特别好写5:
while (1 > 0) {
}
1 > 0 永远成立,所以这个循环永远转不完——这就是无限循环。
而且停不停有时还取决于输入的数据6:
while (x > 0) {
}
x 大于 0 就死循环,x 小于 0 就直接跳过。 所以「会不会停」这个问题,必须同时给出程序和数据两样东西。
3. 处理程序的程序,一点都不稀奇
这一节要打消一个可能的疑虑:「一个程序怎么能检查另一个程序?」
能,而且天天在用。程序说到底就是存储设备上的数据, 所以「处理程序的程序」没什么特别的7:
| 它是什么 | 它干什么 |
|---|---|
| 编 译器 | 读人写的源代码,翻译成机器能跑的东西 |
| 源代码检查器 | 读源代码,告诉你哪里用了不该用的指令、哪里可能死循环、哪些代码永远跑不到 |
| 调试器 | 让运行中的程序暂停、重来,并告诉你当前的状态 |
注意中间那一行:源代码检查器已经能报出「这里可能陷入无限循环」了8。 这一章要证的不是「一点都判断不了」,而是「不可能有一个对任意程序都判得准的」。
4. 停机问题,以及那个判断程序的要求
这一节给出这一章的主角。
停机问题就是:判断「某个程序在给定的数据下,会不会在有限时间内结束运行」9。
假设有一个能解决它的判断程序,原书给它取名 HaltChecker10:
程序 p ──┐
├──→ [ HaltChecker ] ──→ true (把 d 喂给 p,p 会停)
数据 d ──┘ false (把 d 喂给 p,p 不会停)
图说:它吃两样东西 —— 一个程序、一份数据,吐一个真假。
全章的主走查就是拿这台机器做实验,最后把它逼死。
这里有两条要求,不写清楚后面就说不通11:
① HaltChecker 自己必须在有限时间内结束。 它可以算很久, 但必须给出答案——永远算不完的判断程序不算判断程序。
② 所以它不能靠「实际跑一遍 p」来判断。 因为如果 p 恰好是不停的那种,跟着跑的 HaltChecker 自己也就永远出不来了12。
5. 主走查:把它逼死
这一节是全章的主走查。用第 15 章的反证法。
步骤 1:假设 HaltChecker 写得出来。
步骤 2:拿它拼一个专门跟它对着干的程序,原书叫它 SelfLoop13:
SelfLoop(p)
{
halts = HaltChecker(p, p); // 问:把 p 自己喂 给 p,p 会停吗
if (halts) { // 如果回答「会停」
while (1 > 0) { // 那我就故意永远不停
}
}
} // 如果回答「不会停」,我什么也不做,立刻结束
读懂这三行是这一章唯一的门槛,所以慢一点14:
| HaltChecker(p, p) 的回答 | SelfLoop(p) 的行为 |
|---|---|
| true(会停) | 进入无限循环,永远不停 |
| false(不会停) | 跳过循环,立刻结束 |
SelfLoop 干的事只有一件:永远和 HaltChecker 的判断反着来。
步骤 3:把 SelfLoop 自己喂给 SelfLoop,看会发生什么。 只有两种可能,我们一个个走15:
可能一:SelfLoop(SelfLoop) 在有限时间内结束了
→ 看代码:它要结束,只能是 halts 为 false 那一支
→ halts 是 HaltChecker(SelfLoop, SelfLoop) 的结果
→ 也就是说,HaltChecker 判定「SelfLoop 喂自己会不停」
→ 可事实是它停了 —— 矛盾
可能二:SelfLoop(SelfLoop) 陷入了无限循环
→ 看代码:它要死循环,只能是 halts 为 true 那一支
→ 也就是说,HaltChecker 判定「SelfLoop 喂自己会停」
→ 可事实是它没停 —— 又矛盾
图说:两种可能穷尽了所有情况(第 02 章的完整性),而两种都矛盾。
所以假设错了 —— HaltChecker 写不出来。
两条路都撞墙,所以「能写出 HaltChecker」这个假设必然产生矛盾16。 结论:HaltChecker 这样的程序无法编写。停机问题是不可解的17。主走查走完 了。
这里要小心一个常见的误读: 这不是说「判断某个具体程序会不会停」做不到。 原书明说:对于个别程序和数据的组合,有时是可以判断的; 做不到的是「给定任意程序和数据都能判准」的那种普遍程序18。
6. 另一条理由:数量级上就不够
这一节把第 16 章那两个结论接上来,它是同一个结论的另一条路。
第 16 章数过两件事19:
| 可数吗 | |
|---|---|
| 所有程序 | 可数(有限种字符排成的有限长串,能一个个编号) |
| 「输入一个整数、输出一个整数」的所有函数 | 不可数(对角论证法) |
可数集合和不可数集合之间不可能一一对应—— 否则不可数的那一堆就能顺着这个对应关系被编上号了20。
所以一定存在某些函数,没有任何程序能把它算出来21。 这不是找到了某个具体的例子,而是数量级上的必然。
两条路的分工要分清:
- 这一条(数数)说的是「一定存在写不出来的东西」,但没告诉你是哪一个;
- 上一节(SelfLoop)给的是一个点名道姓的具体例子。
原书还留了一道很值得做的思考题: 有人会想—— 「所有能用程序生成的整数数列」也可以用对角论证法证明不可数吧? 这是错的。 对角线造出来的那个数列,不能保证它仍然是「能用程序生成的」—— 和第 16 章那个「对有理数不灵」是同一个坑22。
7. 换个感性的理由:它要是存在,数学就太轻松了
这一节另起一处走查。原书说明这不是证明,是「感性地讲解」23。
思路是:如果 HaltChecker 存在,很多悬了几百年的数学难题都能一句话判掉。
例子一:费马大定理。 写一个程序 FermatChecker,让它不停地随便挑整数
x、y、z 、n(n 大于 2),一旦发现 xⁿ + yⁿ = zⁿ 就打印出来并结束;
否则就一直找下去24。
拿 HaltChecker 去问「FermatChecker 会不会停」:
回答「会停」 → 说明存在反例 → 费马大定理是错的
回答「不停」 → 说明找不到反例 → 费马大定理是对的
图说:一句判定,就把一道题结掉了。
这道题有多难?它被提出之后 358 年没人证得出来, 直到 1994 年才由怀尔斯完全证明25。 也就是说,HaltChecker 要是存在,它能一句话判掉一个折磨了人类三个半世纪的问题。
例子二:哥德巴赫猜想(任一大于 2 的偶数都能写成两个质数之和)。 同样写一个程序,从 4 开始一个个偶数试过去,找到反例就停,找不到就一直试; 再拿 HaltChecker 问一句,猜想的真假立刻有了答案26。 而这道题至今没有解决。
原书自己给这条论证挂了个提醒:严格来说 HaltChecker 只判断有没有解, 并不显示有解时的解是什么27。但即便如此,这条路也已经太便宜了。
8. 不止这一个,而且换语言也没用
这一节交代结论的适用范围。
第一,和语言无关。 上面的证明用的是 C 风格的代码, 但停机问题不依赖于特定的编程语言——无论用什么语言都写不出来28。
第二,不可解问题不止这一个。 原书用同样的证法列了几个29:
- 给定两个程序,判断「无论输入什么,它们的行为是否都相同」;
- 给定一个程序,判断「它能不能判断输入的整数是不是质数」;
- 给定一个程序,判断「无论输入什么,是不是都输出 1 」;
- 给定一个程序,在 T 时间内判断「它能不能在 T 时间内结束」。
第三,能判的还是能判。 程序符不符合这门语言的书写规矩(这叫语法),这种问题程序完全能解决; 判不了的是「任意程序的行为」这一类30。
9. 书里只给了年份和篇名:剩下的来历要自己补
这一节把来源分清楚,因为这里最容易把三种东西混成一种。
书里给了的(第一类来源):
- 正文写着:停机问题是不可解的,这已由图灵在 1936 年证明出来了31;
- 脚注里给了那篇论文的完整篇名: 《On computable numbers, with an application to the Entscheidungsproblem》, 而且原书那道「找出证明中的错误」的思考题,就摘自这篇论文里 「Application of the diagonal process」一节32。
书里没给、我们补的(第二类来源,已核对): 那篇论文投给的是《伦敦数学会会刊》第二辑第 42 卷, 1936 年 11 月 12 日收稿,1937 年才正式印出来,页码 230–265; 图灵后来还发过一篇更正33。
书里没给、属于通用背景的(第三类来源): 图灵在同一篇论文里定义了一种极简的计算机器:一条无限长的纸带、 一个能在纸带上读写并左右移动的磁头、一张「当前状态加上读到的字符, 就决定写什么、往哪走、变成什么状态」的表——这台想象出来的机器就叫图灵机34。
在它之上还有一条被广泛接受的主张:凡是直觉上「能机械照做算出来」的东西, 都能用图灵机算出来——这条主张叫邱奇—图灵论题。 注意它是「论题」不是「定理」:因为「直觉上能机械算出来」这一半没法写成严格的定义, 所以它无法被证明,只可能被反例推翻。
为什么要把这三类分开? 因为这一章的结论极硬, 而一个极硬的结论最怕的就是「书里没有的东西被写得像书里有」。
10. 作者的判断、我们的判断,以及这一章的边界
| 说法 | 书里给了什么 |
|---|---|
| 不可解 ≠ 很难 / 无解 / 尚未解决 | 给了三条排除,专门开了一小节澄清 |
| HaltChecker 写不出来 | 给了完整证明(SelfLoop + 两种可能各推一遍) |
| 一定存在写不出来的函数 | 给了另一条独立理由(可数 vs 不可数) |
| 「它要是存在,数学就太轻松了」 | 作者自己声明这不是证明,是感性讲解 |
| 图灵 1936 年证明 | 书里有年份和篇名;刊物、卷期、收稿日期是我们补的 |
| 人类会不会比计算机强 | 作者在课后对话里拒绝下结论,理由是这不属于数学讨论的范畴 |
判断(我们的,不是书里的):这一章对日常工作最实在的用处, 是让你对「写一个能自动检测所有 XX 问题的工具」这类想法保持警惕。 「自动检测所有死循环」「自动判断这段代码有没有副作用」「自动证明这个改动不会改变行为」—— 这些需求的完整版都等价于停机问题,也就是说都写不出来。 能写出来的一定是它们的削弱版:只覆盖一部分情况,或者允许答「不知道」。 现实中的静态检查工具走的正是这条路。 如果错,会错在: 削弱版往往已经够用了—— 「99% 的情况能判、剩下的报个警告」在工程上是完全可接受的。 所以这条界限制的是「完美工具」,不是「有用工具」。判据是: 那个工具允不允许输出「我不确定」。
这一章的边界:
- 没有讲图灵机,也没有讲计算模型的一般理论——我们在第 9 节补了一小段,并标了来源;
- 没有讲可计算性理论里的其他结论(比如 归约、莱斯定理);
- 那几个「同样不可解」的问题只列了名字,没有给证明;
- 没有讨论现实中的静态分析工具怎么绕开这条界(那是我们在判断块里补的);
- 人类是不是也受这条界限制,作者明确拒绝回答——他的理由是: 如果能把人类的能力形式化,同样的论证就能证明存在人类也解不出的问题; 而如果形式化不了,这个问题就不属于数学讨论的范畴35。
11. 可带走的
- 「不可解」在这里的意思是:原则上写不出解决它的程序—— 不是很难、不是无解、不是尚未解决;
- 程序的行为只有两种:有限时间内结束(报错退出也算)、永远不结束;
- 会不会停,还取决于输入的数据,所以判断要同时给程序和数据;
- 处理程序的程序不稀奇:编译器、源代码检查器、调试器都是;
- 停机问题:判断「某程序在某数据下会不会停」;
- 判断程序自己必须停下来给出答案,所以它不能靠「跑一遍看看」;
- SelfLoop 的把戏:永远和判断结果反着来,再把它自己喂给自己,两种可能全矛盾;
- 换任何编程语言都写不出来,而且这类不可解问题不止一个;
- 另一条独立的理由:程序可数、函数不 可数——数量级上就不够;
- 假如它存在,费马大定理(1994 年才被怀尔斯证明,此前 358 年无人能证) 和哥德巴赫猜想都能被一句判定打发;
- 「能自动检测所有 XX」的工具都是写不出来的;能写的都是允许答「不知道」的削弱版。
12. 原文地图
| 主题 | 原书章 | 原文位置 |
|---|---|---|
| 不可解问题不是什么 | 第8章 不可解问题 | text/13-ch08.txt:573(搜「并非「花大量时间求解的问题」」) · :575(搜「原则上不能用程序来解决的问题」) |
| 程序的两种行为 | 第8章 不可解问题 | text/13-ch08.txt:656(搜「程序的行为必是以下两者之一」) · :661(搜「是 1 秒还是 100 亿年都无所谓」) · :675(搜「这就是所谓的无限循环」) |
| 处理程序的程序 | 第8章 不可解问题 | text/13-ch08.txt:688(搜「程序说白了就是计算机存储设备上的数据」) · :692(搜「源代码检查器」) |
| 停机问题与 HaltChecker | 第8章 不可解问题 | text/13-ch08.txt:701(搜「停机问题（halting problem）」) · :710(搜「取名为 HaltChecker」) · :735(搜「自身必须要在有限时间内结束运行」) |
| SelfLoop 与两种矛盾 | 第8章 不可解问题 | text/13-ch08.txt:773(搜「写出如下 SelfLoop 函数」) · :822(搜「会在有限时间内结束运 行的情况」) · :828(搜「陷入无限循环」) · :843(搜「就必然产生矛盾」) |
| 图灵 1936 年 | 第8章 不可解问题 | text/13-ch08.txt:845(搜「这已由图灵在 1936 年证明出来了」) · :637(搜「本 题 摘 自 图 灵」) |
| 数量级上的理由 | 第8章 不可解问题 | text/13-ch08.txt:594(搜「的集合是不可数的」) · :596(搜「所有程序的集合是可数的」) · :600(搜「存在无法用程序表达的」) |
| 费马大定理与哥德巴赫猜想 | 第8章 不可解问题 | text/13-ch08.txt:868(搜「费马大定理」) · :869(搜「1994 年怀尔斯」) · :873(搜「哥德巴赫猜想」) |
| 不止一个、与语言无关 | 第8章 不可解问题 | text/13-ch08.txt:905(搜「并不依赖于特定的编程语言」) · :910(搜「无论输入什么，程序动作是否都相同」) · :915(搜「程序是否存在语法错误」) |