停机问题与不可判定性

停机问题，即判断给定程序在给定输入下是否停机，是算法不可判定问题的典型例子，通过将其归约可以证明许多其他问题的不可判定性。

Definition

如果不存在图灵机能在所有输入上正确判定某个判定问题，则该问题是不可判定的；停机问题询问任意机器是否在任意输入下停机，它是原型性的不可判定问题，其他问题通过归约被证明是不可判定的。

Scope

本主题涵盖停机问题的精确表述、通过对角线法证明其不可判定性、用于转移不可判定性的多一归约技术、关于程序非平凡性质的莱斯定理，以及诸如判定问题（Entscheidungsproblem）和群的字问题等经典不可判定问题。

Core questions

• 为什么没有算法可以判断程序是否停机？
• 如何使用归约来证明一个问题从另一个问题中不可判定？
• 莱斯定理对判断程序性质有何阐述？
• 哪些著名的数学问题最终被证明是不可判定的？

Key theories

停机问题的不可解性

对角线论证表明，假设存在一个停机判定器会导致矛盾，因此没有算法可以判断所有程序和输入的停机性。

归约与不可判定性转移

如果一个已知的不可判定问题可以归约到目标问题，则目标问题也是不可判定的，这使得归约成为确立不可判定性的标准工具。

莱斯定理

程序所计算函数的每一个非平凡性质都是不可判定的，因此，程序本质上没有有趣的行为性质可以通过算法来判定。

Clinical relevance

不可判定性结果为自动化推理和程序分析设定了严格的限制：它们表明，用于验证终止或程序性质的完美通用工具不可能存在，并且解释了为什么逻辑学、代数学和数论中的许多问题没有算法解决方案。

History

图灵和丘奇在1936年证明了判定问题（Entscheidungsproblem），即判断一阶有效性的算法问题是不可解的，停机问题是图灵论证的核心。莱斯在1953年概括了这一现象，后来，诺维科夫证明了群的字问题，马蒂亚谢维奇证明了希尔伯特第十问题等具体问题是不可判定的。

Key figures

• Alan Turing
• Alonzo Church
• Henry Gordon Rice
• Pyotr Novikov

Seminal works

• sipser2013
• turing1936
• rogers1987

Frequently asked questions

为什么更快的计算机无法解决停机问题？

不可判定性与速度或内存无关：对角线论证排除了任何算法的可能性，无论给予多少时间。停机问题原则上是不可解的，而不仅仅是不切实际。

我们能判断程序是否停机吗？

对于特定程序，通常可以，通过分析或运行它们。不可能的是存在一个单一算法，能正确回答每个程序和输入的这个问题。因此，实际的终止检查器仅在受限类别上成功，或者可能无法给出答案。