能写一个判断所有程序会不会结束的程序吗

先修：02 命题与条件；04 循环不变量与终止度量；07 有限状态的计数

持续集成页面上的一项检查一直显示“运行中”。日志没有新增，进度条也没动。它是在做一段很慢的计算，还是已经进入永不结束的循环？再等十分钟，能不能就此下结论？

超时规则很容易写：超过预算便中止任务，报告失败。但另一个愿望更强：在运行前读一遍代码和输入，准确告诉我们，这次执行最终会不会结束。假如能把这项工作交给一个通用检查器，许多排障工作似乎都能提前完成。

第04章已经证明过一个扫描程序必然结束。本章追问的是：能否把这种能力推广到所有程序，并保证检查器自己也总能给出答案？答案是否定的。要理解这个结论，关键是把“所有”“正确”“总能结束”三个要求同时写清楚。

先说明我们要判断什么

固定一种足够通用的计算模型。程序按明确规则一步步执行，输入是有限字符串；运行开始后没有未建模的外部消息，也没有随机选择。程序可以不断申请更多存储，整数可以用越来越长的字符串表示，事先不设统一的时间或内存上限。每个有限时刻只做过有限步，但资源允许继续扩展。

这里问的是程序P在给定输入x上的一次运行：它是否在某个有限步骤后停止？不要求它算对业务答案，也不要求所有程序都应该停下。长期提供服务的程序可以本来就设计为持续运行。

程序为什么能成为另一个程序的输入？它的指令与规则只有有限长，可以按约定编码成有限字符串。编码、解析以及检查语法是否合法，都有明确可执行的步骤。解释器正是读取这种描述，再模拟其中的指令。程序作为代码执行，与它的编码作为数据传递，是两个角色。

下面为了少写括号，用P同时指程序及其约定编码；H(P,x)的第一个参数实际收到的是字符串。P(P)则表示“运行程序P，把P自己的编码作为输入”，没有要求P会自动读懂自己。MIT的可判定性讲义第34—35页也先建立机器编码，再定义程序与输入组成的停机问题。

给万能检查器一份完整合同

假设存在程序H。对每个有效程序P和每个有限输入x，它都满足：

1. H(P,x)自己一定在有限步内结束
2. 它只回答“会停”或“不会停”
3. 回答“会停”当且仅当P(x)最终停止，回答“不会停”当且仅当P(x)永远运行

这样的H叫作停机判定器。“判定”包括检查器总结束，不能遇到难题就一直思考。H可以很慢，也可以不真正执行P，甚至可以采用我们尚未想到的分析技巧；证明不会限制它的具体方法。

直接模拟P是个有用办法：若某一步看到P停止，就有了“会停”的证据。但P一直运行时，模拟也一直运行，无法满足第一条。等待没有给出一个能完成的否定答案。

因此我们不是先认定某种检查技术失败，再推测所有技术都失败。接下来只使用H的三条承诺，构造它必须处理、却不可能正确处理的一个输入。

用它的回答决定相反的动作

在“确实存在H”的假设下，写一个新程序D：

程序 D(P)：
    如果 P 不是有效程序编码：
        立刻结束
    回答 ← H(P, P)
    如果 回答 = “会停”：
        永久重复一个空操作
    否则：
        立刻结束

D的第一步只是处理无效编码。对有效编码，它问的是“P拿自己的编码作输入，会不会停”，然后作相反的动作：预测会停就循环，预测不会停就结束。

如果H存在，这些动作完全可以写成有限程序：调用一个子程序、判断返回值、进入循环或退出。D不需要预知未来，也没有得到任何神秘能力。它的构造依赖于假设中的H；证明结束后，不能把这段含有不存在组件的伪代码当作真实万能装置。

图1：实线表示一次调用中的信息流。虚线把“被判断的D(D)”与“按规则行动的D(D)”对上，表示它们是同一次运行，不表示程序在运行时沿虚线反复调用自己。

现在把D自己的编码交给D，也就是考察D(D)。因为D是有效程序，H的承诺必须覆盖这一对参数。H(D,D)又保证会结束，只能返回两个答案之一。

如果H(D,D)回答“会停”。 按H的正确性承诺，D(D)应该最终结束；但D的代码规定，收到这个回答就永久循环，所以D(D)不会结束。承诺与执行规则矛盾。

如果H(D,D)回答“不会停”。 按H的正确性承诺，D(D)应该永远运行；但H已经在有限步内返回，D随即走进“立刻结束”分支，所以D(D)会结束。仍然矛盾。

图2：两行覆盖H允许的全部答案。“H一直不回答”不能作为第三条出路，因为这直接违反了判定器总结束的要求。

于是，满足三条承诺的H不可能存在。这就是通用停机问题的不可判定性。反证没有制造一个既停又不停的真实程序，而是证明我们不能同时保留关于H的全部假设。

尤其不要漏掉第一条。若H(D,D)可以永远不返回，D便未必进入任何分支，第二种情况中“随后立刻结束”的推导也就失去前提。一个可能一直运行的分析过程，与本章排除的总判定器，承担的是不同合同。

这与图灵原论文是什么关系

上面使用的是现代常见的程序与输入表述。图灵1936年论文第2、8节研究了机器能否持续输出无穷多个数字，以及是否会打印某个指定符号，不能把其中的“circular”简单翻译成“程序停机”：机器继续运行、却不再输出数字，也属于原文所说的circular。

这些问题与本章有具体联系。例如，要问一台机器是否最终打印0，可以构造一个模拟器：一旦观察到它打印0便停止；若它先停止而没有打印0，模拟器转入永久循环。模拟器停机恰好对应原机器打印过0。若通用停机判定器存在，就能解决原文证明无通用算法的打印问题。本章的D(D)证明则直接在现代停机问题上完成反证，无须照搬原文整套机器记号。

固定的有限电脑为什么是另一个边界

有人可能提出：真实电脑的内存有限，运行足够久总会重复状态，记录下来不就能判断了吗？在合适的模型里，这个办法成立。

设一个封闭、确定系统的完整状态只有N种，下一步怎样变化可以有效计算。完整状态包括指令位置、寄存器、全部可变存储及其他影响下一步的量。给定初始状态，逐步模拟并保存见过的完整状态：先遇到终止状态就回答“会停”；先遇到重复状态就回答“不会停”。

重复为什么够用？假如第i步与第j步状态相同，i＜j，由确定性可知，它们的下一步相同，再下一步也相同。若i到j之间没有终止，后面便不断重走这一段，永远遇不到新的终止状态。若一直未终止，最多检查N＋1个状态记录就必有重复，因为只有N种可能。这说明判定过程也会结束。

图3：上方再次出现B，就重复B、C、D这一段。下方每步给精确整数加1，完整状态始终不同；这只说明有限状态论证不适用，这个具体循环本身仍容易证明永不结束。

因此，不能声称前面的反证也禁止判断所有固定有限状态系统。无界模型中的程序描述虽有限，运行状态却可以靠不断扩展的存储增长。有限长代码与有限个完整状态不是一回事。

实际做状态重复检查，还有两个代价。第一，第07章的计数提醒我们，仅b位存储就可能有2ᵇ种内容，完整状态空间通常更大；理论上有限，计算与保存成本仍可能无法承受。第二，若下一步还受外部输入、时钟或随机源影响，就必须把相关状态和演化规则纳入模型，才能使用“相同状态必有相同后续”的推理。只见到同一行日志或同一内存快照，并不足够。

工程检查仍然能作出有用承诺

不可判定说的是不存在全范围、始终正确、始终结束的通用算法。它与“有算法，但运行太贵”不同，也没有证明P与NP的关系；复杂度讨论计算代价，本章讨论的这一通用算法根本无法满足合同。

对个别程序，我们仍能证明很多事。第04章找最大值的循环，以非负整数n－i作终止度量，每轮严格减少，每轮内部操作也会结束，因此整体必然终止。Dafny官方终止教程展示了用decreases标注检查这类证明的方法。证明某个程序有某项性质，与找出能判定所有程序的万能方法，范围不同。

工程上还可以改变合同：限制语言只表达已知会终止的结构；让静态分析在无法证明时报告“未知”；或者只问“给定执行是否在B步之内停止”。最后一个问题可以模拟至多B步得出答案，每步本身也必须可完成。但“B步内没停”不能升级成“永远不停”。有限资源模型中的性质，也可以在模型完整且状态有限的条件下逐项检查。

仅把输入集合变小还不够。即使只允许空字符串输入，任意程序仍可把原输入x写进代码，启动后模拟P(x)。因此，“给任意代码，判断它在这个唯一输入上是否停机”的通用任务仍包含原来的困难。有限输入数量没有限制单次执行的长度。

AI可以帮助寻找终止度量、发现可疑循环或提出测试，也可以提供带误差的预测。但更多样本或更高预测准确率没有兑现H的全称承诺。只要最终仍是本模型中的算法，并要求对每个程序与输入都必定结束、必定判对，同一个反证仍然适用。允许猜错或报告未知，就是采用另一份合同，应当明确标出来。

顺手试一下

题目1：一百万步够不够

工具T最多模拟一百万步；看到程序停止就回答“会停”，否则回答“未知”。甲说：“T自己总结束，而且已给出的确定答案都正确，所以推翻了本章。”乙把“未知”改成“不会停”，认为这样就补齐了判定器。两人的论证成立吗？假定一次模拟步骤可以完成。

**提示：**逐项检查H的三条承诺，再考虑一个先执行两百万次空操作、随后结束的程序。

**参考答案：**都不成立。T满足自身终止与确定答案可靠，但允许“未知”，未解决每个输入上的二选一问题。乙的修改虽只输出两种答案，却把稍后会结束的程序误判为永不结束。超时可以触发中止策略，不能单凭等待长度证明不终止。

题目2：重复状态就是证明吗

系统A最多有1000个完整状态，封闭、确定，转移规则可计算。系统B只记录任务的局部内存，还会读取外部消息。两者都在未终止时看到了重复记录。分别能否据此证明永不结束？这是否否定了通用停机问题不可判定？

**提示：**检查“记录相同”是否保证下一步相同，再检查完整状态的有限性。

**参考答案：**A可以。重复的是完整状态，确定性保证同一段轨迹反复出现；至多观察1001个状态记录便会终止或发现重复。B不能仅凭局部记录下结论，下一条外部消息可能不同并使任务结束。A属于明确受限的有限状态模型，没有否定无界通用模型下的结论。

回到持续集成页面，可靠的说法可以是“这项任务已超过预算”“这个循环有终止证明”或“在给定模型的这些状态中没有发现问题”。每句话都带着可检查的范围。最后一章会把这些范围带回一个真实系统：规则、数据、数值计算与运行约束分别能保证什么，又该怎样把各层保证接起来。

作者：Jiancheng Wang · 数学之美（独立原创）