图灵机停机问题

能不能写一个程序，判断任意另一个程序在任意输入下会不会停下来？图灵在 1936 年证明：不能。下面用一台可以亲手操控的图灵机，把这个结论"跑"给你看。

可计算性理论 对角化论证 不可判定问题 交互模拟

1公式与参数

停机问题（Halting Problem）问的是：是否存在一个算法，对任意给定的图灵机 $M$ 和输入串 $w$， 都能在有限步内判断 $M$ 在 $w$ 上最终会不会停机？ 先"假装"这样一台万能判定器 $H$ 存在：

$$H(M, w) = \begin{cases} 1, & \text{若 } M \text{ 在输入 } w \text{ 上最终停机} \\[4pt] 0, & \text{若 } M \text{ 在输入 } w \text{ 上永不停机} \end{cases}$$

$H$ 被要求对所有输入都在有限时间内给出 0 或 1 的答案——它自身绝不允许死循环。

接着用对角化构造一台专门与 $H$ 唱反调的"捣乱机器" $D$： 把任意机器的编码喂给它自己，$D$ 先问 $H$ 要答案，然后反着做。

$$D(M) = \begin{cases} \text{无限循环（死循环）}, & \text{若 } H(M, M) = 1 \\[4pt] \text{立即停机}, & \text{若 } H(M, M) = 0 \end{cases}$$

现在把 $D$ 的编码喂给 $D$ 自己——无论 $H(D,D)$ 返回什么，都会立刻自相矛盾：

$$H(D, D) = 1 \;\Longrightarrow\; D(D) \text{ 不停机} \;\Longrightarrow\; H(D, D) = 0 \;\Longrightarrow\; \bot$$

两边互相否定，矛盾成立。因此最初的假设 $H$ 不存在 —— 停机问题是不可判定的。

符号 数学含义 通俗解释
M 图灵机 / 程序 任何一段能被写下来的算法。它可以读取输入、改写纸带、移动读写头，直到停机或永远跑下去。
w 输入串 程序启动时纸带上的初始内容，比如 1011。同一个程序换个输入，可能就从"能停"变成"死循环"。
H(M, w) 假想的判定函数 一个"万能裁判"：扔进去程序和输入，它总能吐出一个 0 或 1，告诉你会不会停。图灵证明这种裁判不存在。
D 对角化机器 反证法里的"内鬼"：裁判说它会停，它偏死循环；裁判说它死循环，它偏立刻停。正是它让 $H$ 无法自洽。
⊥ 矛盾 逻辑上的"不成立"。一旦推出矛盾，说明最初的假设（存在 $H$）是错的。

2交互模拟：亲手把图灵机跑起来

左侧选择程序和输入并调节参数，右侧会实时显示读写头位置、纸带内容与运行轨迹。 请注意：模拟必须设定步数上限——因为现实中我们没有办法知道它到底会不会停下来。 如果跑满上限仍未停机，我们只能诚实地报告"未知"，这正是停机问题的现实困境。

只允许 0 和 1；纸带两端自动补空白格 _。
真实世界没有"步数上限"，但模拟必须有。跑满上限还没停 = 我们无法判定。
数值越小，动画越慢，越容易看清每一步的动作。
当前状态
q0
已执行步数
0
读写头位置
0
模拟进度
0.00%
待运行
当前规则：—

3深入理解

标准介绍

停机问题是可计算性理论中最经典的不可判定问题。它由阿兰·图灵在 1936 年的论文《论可计算数及其在判定问题上的应用》中提出并证明。 问题的形式化表述是：是否存在一个图灵机 $H$，对任意图灵机 $M$ 与输入 $w$，都能在有限步内停机并输出 $M(w)$ 是否停机？ 图灵通过对角化法构造出矛盾，证明了这样的 $H$ 不存在。这一结论等价于：停机问题的特征函数不是可计算函数。

通俗介绍

想象你发明了一台"程序体检仪"，号称能检查任何程序会不会死循环。 那就写一个专门跟它对着干的程序："先用体检仪检查我自己——如果它说我会停机，我就死循环；如果它说我会死循环，我就立刻停下。" 现在把这台程序交给体检仪去检查它自己。体检仪说"会停"？那它就会死循环，说错了。体检仪说"会死循环"？那它就会立刻停下，还是说错了。 不管怎么回答都是错的，所以这台体检仪根本不可能造出来。

解决了什么问题

  • 给出了"算法"的严格数学定义（图灵机），让"可计算"这个概念第一次有了精确含义。
  • 划定了计算的边界：明确存在原则上无解的问题，而不只是"暂时没算出来"。
  • 否定了希尔伯特判定问题（Entscheidungsproblem）的可行性——不存在能判定任意数学命题真假的机械方法。
  • 提供了归约这一强大工具：想证明某个问题是不可判定的，只要证明它能编码停机问题即可。

为什么重要

  • 它是哥德尔不完备定理在计算领域的对应物，共同揭示了形式系统的内在局限。
  • 它终结了"只要算力足够，一切问题都能算"的朴素信念，为计算机科学划出了理论天花板。
  • 它让"不可判定性"成为一门成熟的证明技术，数百个实际问题由此被证明无解。
  • 它反过来推动了可判定子集的研究：既然不能全判，那就找出哪些受限程序可以判。

应用场景

  • 程序静态分析：没有工具能对所有程序都准确判断"会不会死循环"，因此现实中的分析器只能做保守近似（宁可误报，不可漏报）。
  • 编译器优化：彻底的死代码消除、精确的循环优化在一般情况下不可实现。
  • 形式化验证：证明程序终止必须引入人工标注（循环不变式、秩函数、变体表达式），无法完全自动化。
  • 软件工程：它解释了为什么"自动检测所有 Bug"是一个不可能完成的目标。
  • 理论计算机科学：递归论、计算复杂度、程序语言语义学的基石结论。

缺陷与局限

  • 它只说明不存在对所有程序都有效的通用判定法，并不否定某个具体程序可以被证明终止。
  • 实践中大多数程序是可以判断的——不可判定性是一个"存在性"结论，不是"日常必然撞墙"。
  • 结论建立在无限内存、无限时间的图灵机模型上；物理计算机资源有限，边界略有不同。
  • 它是非构造性的：只告诉你"不存在"，却没有给出任何一个具体无法判定的实例。
  • 对工程实践的直接指导有限，更多是警示性的理论边界，提醒人们不要追求不可能的自动化程度。

动手建议

把程序切到 ③ 往返振荡机 或 ④ 无限写入机，把最大步数调到 2000 以上然后点开始： 你会看到机器一路跑下去，图表上的轨迹不断延伸或来回振荡，但永远不会出现"已停机"。 模拟最后会报告 "未判定"——因为在有限步数内没停机，并不能证明它永远不会停。 换一个步数上限、换一个输入，你依然只能得到同样的"未知"。这就是停机问题的核心： 没有任何算法能代替你，对所有程序给出确定答案。