不可判定性与停机问题

停机问题询问一个给定程序在给定输入下是否最终停止，图灵证明了没有算法可以对所有情况给出答案，这是不可判定问题的一个开创性例子。

Definition

当没有算法能对每个输入都正确回答时，一个判定问题就是不可判定的；停机问题，即判断任意程序在任意输入下是否停机，是规范的不可判定问题，通过自指对角线论证（self-referential diagonal argument）证明了这一点。

Scope

本主题涵盖了建立停机问题不可判定性的对角线论证，可判定、可识别和共可识别问题之间的区别，莱斯定理（Rice's theorem）表明程序所有非平凡语义属性都是不可判定的，以及逻辑、数学和计算机科学中一系列自然的不可判定问题。

Core questions

• 为什么没有一个算法可以判断每个程序是否停机？
• 一个问题是可判定的和仅仅是可识别的有什么区别？
• 为什么程序行为的几乎所有有趣属性都是不可判定的？
• 不可判定性是如何从停机问题传播到其他问题的？

Key theories

停机问题的不可判定性

假设存在一个判断停机的算法，通过一个当且仅当被预测不停止时才停止的程序，会导致矛盾，因此这样的算法不存在。

莱斯定理

程序所计算函数的每一个非平凡属性——任何基于行为对某些程序成立而对另一些程序不成立的属性——都是不可判定的，将停机结果推广到所有语义属性。

Clinical relevance

由于停机问题以及根据莱斯定理，程序所有非平凡行为属性都是不可判定的，因此没有任何工具可以完美地检测无限循环、验证任意正确性或完全分析每个程序；静态分析器和验证器因此必须进行近似、接受误报或限制其范围。

History

图灵在1936年利用受康托尔（Cantor）和哥德尔（Gödel）启发的对角线论证，确立了停机问题和逻辑判定问题的不可判定性。莱斯在1953年证明了他的普遍性推广，在接下来的几十年里，许多自然问题，包括关于丢番图方程（Diophantine equations）的希尔伯特第十问题，都被证明是不可判定的。

Key figures

• Alan Turing
• Henry Gordon Rice
• Emil Post
• Alonzo Church

Seminal works

• turing1937
• sipser2013

Frequently asked questions

为什么我们不能仅仅运行一个程序来查看它是否停机？

运行它只会在它确实停止时告诉你它停止了；如果它将永远运行，那么任何有限的等待都无法揭示这一点。停机问题要求一种方法，该方法总能在有限时间内对每个程序和输入给出正确答案，而图灵证明了不存在这样的方法。

不可判定性是否让程序分析变得毫无希望？

不，但这解释了为什么完美的分析是不可能的。工具通过保守地标记任何它们无法证明是安全的东西，通过精确处理受限的程序类别，或者通过解决许多实际情况，同时承认它们可能在对抗性或病态情况下失败来应对。