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

高塔收到一项看似合理的需求：写一个总能判断任意程序是否停止的检查器。

馆长把问题写得很像一项普通静态检查：“给定任意程序和输入，判断它最终是否停止。”如果存在这样的工具，死循环似乎能在运行前一次清除。真正的障碍不是工具还不够聪明，而是这种对所有程序都正确且总会停机的判定器不存在。

本课目标

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

1. 停机语言

定义：

$$ HALT_{TM}={\langle M,w\rangle\mid M\text{ 在输入 }w\text{ 上停机}}. $$

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

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

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

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\iff f(x)\in B. $$

记作：

$$ A\le_m B. $$

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

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

5. 一个接受问题归约

定义：

$$ A_{TM}={\langle M,w\rangle\mid M\text{ 接受 }w}. $$

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

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

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

归约证明必须交代构造本身可计算、yes/no 实例双向对应，不能只说“两个问题看起来差不多”。

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

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

“非平凡”表示有些机器具有该性质，有些没有；“语义”表示只看机器识别的语言或计算行为，不看源代码拼写。

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

• 程序是否接受至少一个输入；
• 两个程序是否计算相同函数；
• 程序是否对所有输入返回固定值。

而“源代码是否包含 100 个状态”是语法性质，不由 Rice 定理直接覆盖，并且对有限编码显然可数出来。

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

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

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

术语方向会随分析目标表述改变。工具文档必须明确 sound 是针对“安全证明”还是“错误报告”。

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

常见误区

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

练习

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

小结

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

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