形式陈述

令

$$ HALT_{TM}=\{\langle M,w\rangle:M\text{ 在输入 }w\text{ 上停机}\}. $$$$HAL{T}_{TM}=\{⟨M,w⟩:M\text{ 在输入 }w\text{ 上停机}\}.$$

语言 $HALT_{TM}$$HAL{T}_{TM}$ 不可判定。

直觉

若存在通用停机判定器，就可构造一个程序：当判定器预测它会停机时故意循环，预测它循环时立即停机；把程序自身作为输入便产生矛盾。

例子与边界

具体的有限状态程序或受限循环可以分析停机；定理否定的是覆盖任意程序与输入的统一完备算法，不是否定所有局部终止性证明。

推论与应用

许多程序语义性质可由停机问题归约证明不可判定；Rice 定理进一步推广了这一边界。

参考资料

• Alan M. Turing, “On Computable Numbers, with an Application to the Entscheidungsproblem,” 1936.
• Michael Sipser, Introduction to the Theory of Computation, 3rd ed., §5.1.