4.2 停机问题、归约与 Rice 定理：证明不存在通用判定器

本课目标

• 准确陈述停机问题及其可识别性；
• 理解自指反证的结构；
• 掌握映射归约的正确方向；
• 把不可判定性转化为静态分析中的保守取舍。

1. 停机语言

定义：

$$HAL{T}_{TM}=\{⟨M,w⟩\mid M\text{ 在输入 }w\text{ 上停机}\}.$$

$HAL{T}_{TM}$ 是图灵可识别的：通用机直接模拟 $M(w)$，若模拟停机就接受。若 $M(w)$ 永不停止，模拟也永不停止。

但它不可判定：不存在一台机器对所有 $⟨M,w⟩$ 都停机，并正确回答“会停”或“不会停”。

“这次运行一小时还没停”不能证明它永远不停；“许多实际程序可被分析”也不构成对所有程序的通用判定器。

2. 自指反证

假设存在判定器 halts(program, input)。构造程序：

contradict(program):
    if halts(program, program):
        loop forever
    else:
        return

再运行 contradict(contradict)：

• 若 halts 判断它会停，程序按定义进入无限循环；
• 若 halts 判断它不停，程序按定义立即返回。

两种回答都与自身相反，因此假设的通用判定器不存在。

证明依赖程序可以被编码成数据，并传给模拟器或分析器。实际语言的语法细节不重要；只要系统具有足够的通用计算和自解释能力，编码可以完成。

3. “不可判定”不是“没有任何有用工具”

不可判定性否定的是同时满足以下条件的算法：

1. 覆盖所有合法程序与输入；
2. 每次都在有限时间结束；
3. 每次答案都正确。

工程工具可以放弃其中一项：

• 只处理受限语言或有限状态模型；
• 设置超时并返回 unknown；
• 做保守近似，允许误报或漏报中的一种；
• 让用户提供不变量、类型标注或证明。

模型检查器能完全分析有限状态系统；终止性检查器能证明某些循环；类型系统能排除一类错误。这些成果与停机问题并不矛盾。

4. 映射归约的方向

若要证明新问题 $B$ 很难，从已知困难问题 $A$ 出发，构造对所有输入都停机的可计算函数 $f$，满足：

$$x\in A⟺f(x)\in B.$$

记作：

$$A{\le }_{m}B.$$

含义是“若会解 $B$，就能借它解 $A$”。因此已知 $A$ 不可判定，可推出 $B$ 不可判定。

方向写反是常见错误。把未知问题归约到停机问题，只说明未知问题不比停机问题更难，不能据此证明它不可判定。

5. 一个接受问题归约

定义：

$$A_{TM}=\{⟨M,w⟩\mid M\text{ 接受 }w\}.$$

先确认 $A_{TM}$ 也不可判定：给定停机问题实例，让一台新机器模拟 $M(w)$，只要模拟以接受或拒绝方式停机，新机器就接受固定输入。若能判定接受，就能借此判定停机。

要从 $A_{TM}$ 归约到“某机器是否接受固定字符串 hello”，可以根据 $⟨M,w⟩$ 构造新机器 $N$：

N(input):
    忽略 input
    模拟 M(w)
    若 M 接受，则接受
    若 M 拒绝，则拒绝
    若 M 不停机，则继续模拟

于是 $N$ 接受 hello 当且仅当 $M$ 接受 $w$。如果“$N$ 接受 hello”这一性质存在判定器，就能判定 $A_{TM}$，产生矛盾。

构造 $N$ 时只需把 $M$ 和 $w$ 的编码写进新程序，不能先跑完 $M(w)$ 再决定怎样生成 $N$。伪代码最后一行描述持续模拟的行为，不是在调用一个检测“不停机”的函数。

归约要求 yes/no 答案双向对应，不要求 $f$ 是一一映射或满射。构造本身必须总能结束，不能只说“两个问题看起来差不多”。

6. Rice 定理概括程序语义性质

Rice 定理指出：对图灵可识别语言的任何非平凡语义性质，判定对应机器是否具有该性质都是不可判定的。

这里的“非平凡”表示有些可识别语言具有该性质，有些没有；“语义”表示两台机器只要识别同一个语言，就必须对该性质给出同样答案。具体状态数量、运行步数或输出日志不由这个语言版本的定理概括。

例如一般情况下不可判定：

• 程序是否接受至少一个输入；
• 程序识别的语言是否有限；
• 程序识别的语言是否包含固定字符串 hello。

也有针对部分可计算函数的 Rice 定理版本，可用来讨论“是否对所有输入返回固定值”等外延性质。两个程序的函数等价问题也不可判定，但需要进一步归约：若通用比较器存在，把其中一个程序固定为已知函数的实现，就能判定相应的非平凡函数性质。

而“机器的编码是否列出恰好 100 个状态”是语法性质，不由 Rice 定理直接覆盖，并且对有限编码显然可数出来。

7. 对静态分析的实际影响

静态分析常在 soundness 与 completeness 之间取舍。以“报告所有可能空指针”为例：

• sound 分析不漏掉真实风险，但可能报告实际上不可达的路径；
• complete 分析不误报，但可能漏掉某些真实风险；
• 对足够通用的程序语义，想同时覆盖所有程序、终止且无误报无漏报通常不可能。

这里采用“安全分析覆盖全部可能错误”的约定。术语方向会随分析目标表述改变。工具文档必须明确 sound 是针对“安全证明”还是“错误报告”。

编译器仍能可靠判断大量局部性质：未声明名称、常量类型不匹配、某些结构化控制流后的不可达语句。不可判定的是对任意程序的完整语义问题，不应把它夸大成“静态分析都不可靠”。

常见误区

• 运行足够久就能判定不停机：任何固定超时都可能截断一个稍后会停止的程序。
• 不可判定等于随机猜测：可使用保守分析、交互证明和受限模型得到可靠结论。
• 归约方向不重要：错误方向无法传递困难性。
• Rice 定理覆盖所有源代码属性：它针对非平凡语义性质，不是简单语法统计。

参考资料

• Cornell CS 4820: Limits of Computability

练习

1. 解释 $HAL{T}_{TM}$ 为什么可识别但不可判定。
2. 若已知 $A$ 不可判定，要证明 $B$ 不可判定，应构造 $A{\le }_{m}B$ 还是 $B{\le }_{m}A$？说明理由。
3. 判断“程序源文件是否含 while”和“程序是否会执行某个 while”哪一个是语法问题。
4. 为终止性分析器设计 terminates / does-not-terminate / unknown 三值结果，说明每种证据要求。

小结

停机问题不可判定，原因是通用程序可以模拟并反转关于自身的预测。归约把这条边界传递给其他问题，Rice 定理则覆盖广泛的非平凡程序语义性质。工程分析器的出路不是假装边界不存在，而是缩小语言、返回 unknown 或选择可解释的保守近似。

unknown 也是一个诚实的结果。超时应带着证据和限制退场，不能换个名字就冒充“不会停机”。

下一课讨论另一条正交边界：一个问题即使可判定，所需时间也可能随输入增长得太快而无法实际求解。