停机问题:为什么某些判断没有通用程序
上一篇文章用寄存器机解释器说明了通用性:程序可以编码成数据,解释器可以读取这份数据并模拟执行。通用性带来强大表达能力,也带来一个边界问题:能不能写一个程序,判断任意程序在任意输入上是否会停机。
答案是否定的。停机问题说明,不存在一个对所有程序和输入都正确的通用停机判定器。工程里可以做超时、步数限制、静态分析和资源预算,但这些方法要么不完整,要么会保守拒绝,要么只覆盖有限范围。
本文先用一个可运行的有界检查器展示工程近似,再用自引用反证解释为什么通用判定器不存在。
问题形式
停机问题可以写成一个理想函数:
1 | |
它的承诺是:
| 返回值 | 含义 |
|---|---|
True |
program(input_data) 最终会停机 |
False |
program(input_data) 会一直运行 |
难点在“任意程序”和“任意输入”。判断某个具体程序很容易;判断所有程序则会遇到自引用。
工程里常见的近似:有界执行
最朴素的方法是只运行有限步。如果步数内停机,就返回 True;如果步数用完还没停,就返回 False。
这里用生成器模拟程序执行。每次 yield 代表程序推进一步,生成器结束代表程序停机。
1 | |
有界检查器如下。
1 | |
完整示例
完整代码如下。
1 | |
运行结果:
1 | |
读取结果
stops_quickly 在 10 步内停机,所以返回 True。
stops_slowly 需要 20 步。步数限制是 10 时,它被判为 False;步数限制提高到 30 后,它被判为 True。
loops_forever 在 30 步内没有停机,被判为 False。
这里暴露了有界执行的本质:False 只表示“在给定步数内没有停机”,不能推出“永远不停机”。慢程序和死循环在有限观察窗口里可能无法区分。
为什么通用判定器不存在
设想存在一个完全可靠的函数:
1 | |
它能对任意程序和任意输入给出正确答案。基于它可以构造一个特殊程序 diagonal:
1 | |
diagonal 专门和 halts 的判断反着来。若 halts(program, program) 判断会停机,diagonal 就进入死循环;若判断不会停机,diagonal 就立刻停机。
把 diagonal 自己作为输入:
1 | |
会得到矛盾:
halts(diagonal, diagonal) 的判断 |
diagonal(diagonal) 的行为 |
|---|---|
| 会停机 | 进入死循环 |
| 不会停机 | 立刻停机 |
两种情况都和判定器的承诺相反。所以最初假设不成立:不存在对所有程序和输入都正确的通用停机判定器。
这个反证的核心是自引用。通用解释器让程序可以处理程序本身;一旦程序能把自己的编码作为输入,就能构造出专门反驳判定器的对角程序。
对工程的影响
停机问题不是说所有判断都做不了。它说的是“对任意程序给出完备且正确的停机判断”做不了。工程里的分析工具依然有价值,但需要明确边界。
| 工具 | 能做什么 | 边界 |
|---|---|---|
| 超时 | 控制运行时间 | 超时不等于死循环 |
| 最大步数 | 限制解释器执行 | 慢程序可能被误判 |
| 静态分析 | 发现特定模式 | 无法覆盖所有程序行为 |
| 类型系统 | 排除一类错误 | 不证明所有运行性质 |
| 沙箱 | 限制资源使用 | 不判断语义停机 |
真实系统通常选择保守策略:宁可拒绝某些安全程序,也不要放过高风险程序;或者接受不完整性,只针对已知模式给出告警。
Java 程序员的迁移表
| 理论概念 | Java 工程对照 | 实践含义 |
|---|---|---|
halts(program, input) |
静态分析器 / 规则扫描器 | 试图预测程序行为 |
| 有界执行 | 超时、最大循环次数、测试运行 | 只能观察有限前缀 |
| 自引用程序 | 反射、脚本引擎、自解释器 | 程序可以操作程序 |
| 不可判定 | 分析工具的理论边界 | 不能承诺全覆盖 |
| 保守近似 | 编译器 warning、IDE inspection | 用可接受误报换安全性 |
看到“写一个工具,判断任意代码是否一定安全、一定终止、一定不抛异常”时,需要先问清范围。如果范围是任意程序,承诺就已经越过停机问题的边界。
模式提炼:从判定转向约束
停机问题给工程的启发不是放弃分析,而是改变目标。
1 | |
工程系统通常把“完全判定”改成几类可执行约束:
| 约束 | 示例 |
|---|---|
| 时间约束 | timeout、deadline |
| 空间约束 | heap limit、container memory limit |
| 步数约束 | query cost、VM instruction budget |
| 语言约束 | 禁止反射、禁止无限循环语法 |
| 抽象约束 | 类型、区间、数据流 |
这些约束不解决停机问题本身,但能把风险控制在工程可接受范围内。下一篇抽象解释会继续讲“精确做不到时,怎样做有用近似”。
练习
第一,把 bounded_halts 改成返回三种结果:halts、unknown、error。
第二,给 loops_forever 增加计数输出,观察有限窗口里它和慢程序的相似性。
第三,设计一个只能写 for range(n)、不能写 while 的小语言,思考它为什么更容易判断终止。
第四,列出一个日常项目里的静态检查规则,标注它可能误报还是漏报。
