停机问题不可判定性

自指构造抓住的不是某种编程语言的漏洞，而是任何足够通用的程序分析器都会面临的对角冲突。假想的通用停机判定器把程序行为压成可靠的二值预测，反转程序则在判定器预测它会停机时故意循环、预测它循环时立即停机；将反转程序自身的编码作为输入后，预测与行为无法同时成立。这个论证也说明，增加测试样例或延长模拟时间永远只能覆盖更多实例，不能变成全域判定。

为了看到矛盾本身，先假设 $H(M,w)$ 总能判断 $M$ 在 $w$ 上是否停机。

构造 $D(x)$：若 $H(x,x)$ 回答“停机”，则无限循环；若回答“不停机”，则立即停机。考察 $D(D)$：无论 $H$ 给哪种答案，$D$ 都作出相反行为，形成矛盾。

这并不否定所有局部终止性证明：对有限状态机、固定循环上界的程序或带可证明递减度量的递归函数，停机仍可判定。不可判定性否定的是对任意程序与输入都正确且总停机的统一完备算法；静态分析器可以选择保守近似，代价是报告假阳性或放弃某些实例。

图灵机公理库图灵机Turing machine通过有限控制、可读写纸带和移动读写头刻画一般算法计算能力的模型。 的停机问题是构造其他不可判定性结果的标准源头：通过 映射归约公理库映射归约Mapping reduction · Many-one reduction用可计算函数把一个语言成员关系变换为另一个语言成员关系。，可把停机行为编码进等价性、可达性或其他程序语义性质，证明它们不可判定。Rice 定理公理库Rice 定理Rice's theorem图灵可识别语言的每个非平凡语义性质都是不可判定的。 进一步把这种现象概括为所有非平凡语义性质；终止性证明器、模型检查器和类型系统则通常通过限制语言或接受不完备性来获得可用算法。