问题包括程序与输入
同一个程序可能对某些输入很快返回,对其他输入持续循环,因此停机问题的对象是一对程序与输入。所问的是最终是否停止,而不是在一分钟内有没有结果。一个程序目前尚未结束,只能说明它已经运行到现在,不能据此直接判断它以后永远不会停止。
参考:[1]
通用判定会产生矛盾
经典反证假设有一个总能正确判断停机的程序,再构造一个根据它的判断反向行动的程序:预测会停就循环,预测不会停就立即结束。让这个构造检查自身对应的描述,会迫使预测与实际行为冲突。由此排除的是适用于所有程序与输入的统一判定器,而非某一个样本的分析。
参考:[2]
模拟只能证明一部分
直接运行一个程序,一旦它停止,就能确认这次执行会停;若它不停,模拟却可能永远无法给出否定答案。循环检测也只能处理能够识别或完全覆盖的状态范围,不能自动推广到任意存储与输入。实际工具因此会采用限制、近似或人工约束,明确自己能保证的范围。
参考:[1]
具体程序依然能证明
倒数到零的有限循环、某些结构递归和受限语言,都可能有可证明的终止性质。通用不可能性不意味着程序验证没有意义,也不意味着所有运行错误都无法发现。正确结论是,不能要求一个单一算法对无限广泛的所有程序都完整且正确地解决停机判断。
参考:[2]