停机问题不可判定定理

概述

停机问题不可判定定理（Undecidability of the Halting Problem）：不存在算法（图灵机）能够判定任意给定的程序在给定的输入上是否最终停机。这是可计算性理论中最基本的不可判定结果。

定理陈述

形式化陈述

定理（Turing, 1936）：停机语言 $H_{ALT}=\{⟨M,w⟩\mid M\text{ 是图灵机且 }M\text{ 在输入 }w\text{ 上停机}\}$ 是不可判定的（undecidable），即不存在图灵机 $H$ 使得对任意输入 $⟨M,w⟩$：

• 若 $M$ 在 $w$ 上停机，则 $H$ 输出 “接受”
• 若 $M$ 在 $w$ 上不停机（死循环），则 $H$ 输出 “拒绝”

术语说明

• 可判定：存在算法在有限步骤内对每个输入给出正确的是/否答案
• 不可判定：不存在这样的算法
• 半可判定：停机问题实际上是半可判定的（可以枚举所有停机的计算），但不可判定

证明概要

证明思路

证明采用对角线论证法（diagonalization），这是Cantor创立的经典技巧：

第一步：假设存在停机判定器

假设存在图灵机 $H$ 能够判定停机问题： $H(⟨M,w⟩)=\{\begin{array}{ll}\text{"接受"}& \text{若 }M\text{ 在 }w\text{ 上停机}\\ \text{"拒绝"}& \text{若 }M\text{ 在 }w\text{ 上不停机}\end{array}$

第二步：构造对角线机器 $D$

基于 $H$，构造一个新的图灵机 $D$，其行为定义为：

$D(⟨M⟩)=\{\begin{array}{ll}\text{死循环}& \text{若 }H(⟨M,⟨M⟩⟩)=\text{"接受"}\\ \text{停机（接受）}& \text{若 }H(⟨M,⟨M⟩⟩)=\text{"拒绝"}\end{array}$

直观地说：$D$ 在输入 $⟨M⟩$ 上，先用 $H$ 判断” $M$ 在自身编码 $⟨M⟩$ 上是否停机”，然后做相反的事情。

第三步：导出矛盾

现在考虑将 $D$ 应用于自身编码：$D(⟨D⟩)$。

情况一：若 $D$ 在 $⟨D⟩$ 上停机，则 $H(⟨D,⟨D⟩⟩)=$ “接受”。但根据 $D$ 的定义，$H$ 输出”接受”时 $D$ 应死循环。矛盾。

情况二：若 $D$ 在 $⟨D⟩$ 上不停机，则 $H(⟨D,⟨D⟩⟩)=$ “拒绝”。但根据 $D$ 的定义，$H$ 输出”拒绝”时 $D$ 应停机。矛盾。

两种情况都导致矛盾，因此假设不成立：停机判定器 $H$ 不存在。

对角线论证的直觉

将所有图灵机排列为 $M_1,M_2,M_3,\dots$，构造一个”对角线表格”：

	$⟨M_1⟩$	$⟨M_2⟩$	$⟨M_3⟩$	…
$M_1$	?	?	?	…
$M_2$	?	?	?	…
$M_3$	?	?	?	…
…	…	…	…	…

其中第 $(i,j)$ 格记录 $M_i$ 在 $⟨M_j⟩$ 上是否停机。机器 $D$ 的行为恰好是沿着对角线取反——它读取对角线上的值并翻转。但 $D$ 本身也是一台图灵机，必然出现在某一行中，导致自指矛盾。

参考文献

• Turing, A. M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc., s2-42(1), 230-265.
• 证明详解: GMU - Diagonalization, Halting Problem
• 教学讲义: UMD - The Halting Problem
• IIT Delhi讲义: Undecidable Languages

关键推论

• 推论1（Rice定理）：任何关于图灵机所识别语言的非平凡语义性质都是不可判定的。例如：“这个程序是否接受空字符串？""这个程序的语言是否有限？“等都是不可判定的
• 推论2：不存在通用的程序验证器——无法编写一个程序来判断任意程序是否正确
• 推论3：不存在通用的程序优化器——无法判断一个优化是否改变了程序的行为
• 推论4：许多数学问题不可判定，如Post对应问题（PCP）、希尔伯特第十问题（Diophantine方程的可解性）

应用场景

• 程序验证：停机问题的不可判定性表明，不可能存在完美的自动化程序验证工具
• 软件工程：理解不可判定性有助于设定合理的测试和验证目标
• 病毒检测：精确检测任意程序是否为恶意软件是不可判定的（因为需要判断程序行为）
• 编译器设计：编译器的某些优化（如死代码消除）在理论上受到不可判定性的限制
• 人工智能：停机问题与AI安全中的”对齐问题”有深层联系——无法用算法完全预测一个智能系统的行为

参见

• 算法
• 递归定义
• Kleene定理
• 递归关系式
• 可满足性