停机问题不可判定性

假想判断器为什么会被一个普通程序击败 ​

假设存在判定器 $H$，对所有机器编码 $x$ 和输入 $w$ 都在有限时间内结束，并满足

借助这个子程序，构造机器 $D$：收到合法机器编码 $x$ 后，先运行 $H(x,x)$；若答案是 $1$，就进入无限循环；若答案是 $0$，就立即停机。因为假设中的 $H$ 总停机，这是一段定义清楚的有效程序。

现在把 $D$ 自己的编码 $⟨D⟩$ 交给它。机器描述本来就是有限字符串，所以“程序把另一个程序的编码当作输入”没有增加任何超出计算模型的能力。

两种可能都与 $H$ 的正确性矛盾，所以这样的 $H$ 不存在。证明没有要求我们实际等到一次无限循环结束；只需分析两条分支，就排除了“总停机且处处正确”的假设。

这与 Cantor 式对角论证共享“在自己的位置上反转”的结构，这里被反转的是机器的停机行为。自指只是把矛盾对准假想判断器的工具，结论约束的是所有程序和输入组成的整体问题。[1]

具体程序的终止性证明 ​

while True: pass 的不停机和固定次数循环的停机，都可直接证明。若某循环的每一步都严格减少一个非负整数，而且循环体每次都能结束，这个整数就是终止性证书。不可判定性排除的是一种对任意程序都给出正确结论并结束的方法，并没有排除局部证明、特定语言的检查器或覆盖部分程序的分析工具。

带步数上限的问题也不同。给定 $M,w,B$，询问“是否在 $B$ 步内停机”，模拟至多 $B$ 步即可判定。$B$ 用二进制编码时，这个直接算法可能对输入长度很慢；“可判定”和“多项式时间可判定”仍是两个层次。

若程序被限制在一个可有效枚举的有限配置集合中，且其转移确定，那么遇到重复配置就会重复后续行为，可以据此判断是否停机。一般图灵机拥有无界工作带，不能把这个有限状态论证直接搬过去。

为什么“不停机”连通用识别器也没有 ​

假设还存在一个识别器 $N$，专门在 $M(w)$ 不停机时最终接受。我们可以交替推进 $M(w)$ 的模拟和 $N(⟨M,w⟩)$：前者先停机，就回答“停机”；后者先接受，就回答“不停机”。每个输入总属于其中一种情况，因此总有一边给出答案。

这就构造出了不存在的判定器。故 $\overline{\mathrm{HALT}}$ 不可识别。交替推进很重要：若先完整运行一边，再运行另一边，第一边可能永远占住计算而不让另一边开始。

停机问题常作为不可判定性归约公理库映射归约Mapping reduction · Many-one reduction用可计算函数把一个语言成员关系变换为另一个语言成员关系。的起点。例如，给定 $M,w$，构造程序 $P$：先模拟 $M(w)$，等其结束后才执行某条标记语句。于是

若存在适用于所有这类程序的可达性判定器，就能解决停机问题。归约中的程序 $P$ 可从 $M,w$ 的有限描述有效生成，因此它把停机问题的输入统一转换成语句可达性的输入。

Rice 定理公理库Rice 定理Rice's theorem图灵可识别语言的每个非平凡语义性质都是不可判定的。进一步覆盖非平凡的可计算语义性质，但要核对语义对象。两个机器可以识别同一语言，其中一个在非成员输入上拒绝，另一个在同样输入上循环；因此“某次运行是否停机”不能不加说明地当作仅由接受语言决定的性质。直接停机归约没有这种歧义。