停机问题是判断某个指定程序在指定输入下运行时，最终会停止还是会无限运行的判定问题。计算机科学的一项基础性结果表明，不存在一种算法，能够对所有可能的程序及其输入都在有限时间内给出正确答案。因此，这个问题是不可判定的：这一限制涉及原则上能计算什么，而不仅仅是能高效计算什么。(courses.cs.cornell.edu)
形式定义
停机问题通常用图灵机来表述。图灵机是一种抽象计算装置，具有有限的描述，其工作存储空间则可以无限扩展。设 (M) 表示这样一台机器，(w) 表示它的输入，(\langle M,w\rangle) 表示将两者有效编码为一个有限字符串。停机语言定义为
[ \mathrm{HALT}={\langle M,w\rangle\mid M\text{ 在输入 }w\text{ 上停机}}. ]
判定器必须对这个集合中的每个成员回答“是”，对每个非成员回答“否”，且无论哪种情况，都必须在有限步内结束。停机既包括接受输入，也包括拒绝输入；它并不意味着程序得到了期望的结果。(cs.cornell.edu)
程序本身也可以表示为数据。通用图灵机能够读取一台机器的编码，并模拟其执行过程。这样，关于程序行为的问题就能转化为普通的计算输入；这些输入甚至可以描述正在检查它们的程序本身。(cs.cornell.edu)
历史背景
艾伦·图灵在其发表于1936—1937年的论文《论可计算数及其在判定问题中的应用》中，确立了若干基础性的不可判定性结果。他提出了自己的机器模型，描述了通用模拟，并证明某些关于机器的问题无法通过机械化的方法判定。这些结果对判定问题给出了否定的答案，即不存在适用于一阶逻辑的一般判定程序。(cs.virginia.edu)
理解历史术语时需要谨慎。图灵最初提出的“无循环”（circle-free）问题，关注的是一台机器是否会输出无限多个指定的输出符号，而不只是它是否会停止。他的论文还证明，判断一台机器是否会在某个时刻打印某个指定符号，是不可判定的。后一问题可以推出现代的停机定理：只需让模拟器恰好在被模拟的计算停机时打印该符号即可。因此，现代定理可以从他的研究中推出，但今天的标准表述和证明并不是对原论文的逐字复述。(cs.virginia.edu)
对角化证明
标准的数学证明将反证法与对角化相结合，后者是一种与康托尔对角线论证相关的技巧。假设存在一个程序 (H(P,x))，它总能在有限时间内结束，并正确判断程序 (P) 在输入 (x) 上是否停机。构造另一个程序 (D)，用伪代码表示如下：
D(p):
如果 H(p, p) 回答“会停机”：
永远循环
否则：
停机
现在，以 (D) 自身的描述 (d) 作为输入运行 (D)。如果 (H(d,d)) 预测这次执行会停机，(D) 就故意永远运行；如果它预测这次执行不会终止，(D) 就停机。无论给出哪个答案，都是错误的，这与假设 (H) 能正确判断相矛盾。因此，不存在通用的停机判定器。(courses.cs.cornell.edu)
这个论证并不要求程序自动获取自己的源代码：程序的描述是作为输入提供的。它也不排除对特定情形作出判定。它排除的是一个同时满足以下三项要求的统一程序：适用于所有情形、判断正确，以及保证终止。(courses.cs.cornell.edu)
可识别性与不终止
停机问题虽然不可判定，却是可计算枚举的，也称可识别或半可判定。识别器模拟 (M) 在 (w) 上的运行，并在模拟停止时回答“是”。每一次会停机的执行最终都能被检测到，但如果执行不会停机，识别器就会无限运行。这正是识别与判定的区别。(cs.cornell.edu)
其补集由不会停机的机器—输入对组成，是不可识别的。如果停机和不停机两种情况都有识别器，就可以交替模拟两者的执行步骤，直到其中一个接受，从而判定停机问题。这种不对称性并不妨碍对个别程序证明其不会终止；它排除的是这样一种识别器：既能最终确认每一种不会停机的情况，又不会接受任何会停机的情况。(cs.cornell.edu)
归约与相关结果
停机定理为可计算性理论提供了一个出发点。通过可计算归约，可以将停机问题的实例转化为另一个问题的实例。如果后一个问题的判定器能够据此构造出停机判定器，那么后一个问题也必然不可判定。归约的方向至关重要：应当将已知不可判定的问题归约到正在研究的问题。(cs.cornell.edu)
赖斯定理将这一限制推广到任意图灵机所识别语言的所有非平凡性质。这里的“非平凡”是指，有些可识别语言具有该性质，而另一些则不具有。它针对的是语义性质，而不是机器的句法或执行过程的所有性质：检查机器的书面描述，或模拟固定数量的步骤，都可以是可判定的。(cs.cornell.edu)
适用范围与软件分析
这一结果适用于具有图灵完备性的计算系统，包括在无界资源假设下解释的通用编程语言。它对形式验证和自动程序分析构成了限制：对于不受限制的程序，终止性分析器不可能总是在有限时间内给出正确而确定的答案。受限的分析方法则可以让某些情况保持未决，或采用保守的近似方法。(cs.cornell.edu)
不可判定性不同于计算复杂性。即使一个判定器极其缓慢，它仍然是判定器；而停机定理排除了所有这样的算法。一个有界的问题——程序是否会在给定的步数内停机——可以通过有限模拟来判定，但程序未在该步数范围内停机，并不能证明它会永远运行。(courses.cs.cornell.edu)