“不存在一个总能结束的通用算法，正确判断任意程序在任意输入上是否最终结束。 对图灵机的可计算编码，停机语言定义为”
形式陈述
标准确定性单带图灵机可同时视为三种推广模型的特例：在非确定性图灵机中每个配置只保留一个选择，在预言机图灵机中从不调用预言机，在多带图灵机中只使用一条工作带。这里陈述的是语法包含。在可识别语言与可判定语言两种表达能力上，确定性单带机与非确定机、固定有限多带机分别等价；相应模拟可能增加时间成本。任意预言机则不同：若允许不可计算的预言机，它可以严格增加计算能力，不能把三种推广一概视为表达力相同。
以下选择双向无限纸带，以避免额外规定左边界行为。确定性单带图灵机可写为
其中
纸带内容可写成函数
配置是三元组
其中
若
若
直觉
图灵机把算法压缩为三个要素：有限控制、可读写的无界纸带，以及一次只访问一个格子并做局部修改的转移规则。配置是计算在某一瞬间的完整快照，一步语义则把有限转移表真正解释为运行。纸带的无界只表示可以按需要继续使用新格子，不代表某次有限计算会访问无限区域；运行
有限状态集并不使图灵机退化为有限自动机。即使控制状态相同，纸带内容或头位置不同也会形成不同配置；图灵机的配置集合无限。自动机只有固定多个状态可区分历史，图灵机则能把历史写到新纸带格中。
例子与边界
一台判定回文的机器可以反复标记最左未处理符号，移动到最右未处理符号比较，再返回继续；虽然效率不高，但每个动作都能写成有限转移表。用 X 标记处理过的位置，0110 的两轮纸带摘要是 0110 → X11X → XXXX，随后接受。0100 第一轮外层两个 0 相同，得到 X10X；第二轮比较 1 与 0 才拒绝。奇数长度时若只剩一个未标记符号，它就是中点，无需再找配对符号；空输入也直接接受。
每轮至少消去两个未标记位置，或处理唯一中点后结束；每次来回扫描只穿过有限输入区间。因此这个过程不仅识别回文，而且对所有输入停机。有限控制只需记住本轮选中的是 0 还是 1，无界的处理进度由纸带上的标记承担。
改用单向无限带、允许“停留不动”、增加有限条带或引入非确定性，通常只改变描述便利性、编码与效率，不改变可计算语言类；讨论精细时间复杂度时，模拟开销仍须单独计算。接受、拒绝和不停机是三种不同结果：可识别性只要求成员最终被接受，可判定性还要求非成员最终被拒绝。
推论与应用
输入字、有限状态、纸带符号与转移函数先定义机器本身；机器接受哪些输入字，随后才导出它识别的形式语言。把对象层和语言层分开，可以避免把“某台机器停机”与“某个语言可判定”混成同一句话。
Church–Turing 论题把图灵机视为有效计算的标准形式化之一。通用图灵机进一步说明，机器描述本身可以编码成输入，由另一台机器解释执行；程序与数据之间因此没有不可跨越的形式边界。
若把非确定机器的可访问带区限制为输入长度的常数倍，就得到线性有界自动机，其语言刻画见CSL–LBA 等价定理。可计算函数、可判定性、可识别性和资源复杂度类，则分别在图灵机模型上增加输出、全停机或资源上界要求。
参考资料
- Michael Sipser, Introduction to the Theory of Computation, 3rd ed., Cengage, 2013, Chs. 0–10。
- Alan M. Turing, “On Computable Numbers, with an Application to the Entscheidungsproblem,” Proceedings of the London Mathematical Society, 1936, Full paper。