turing-machines - 为什么不能有一个程序检查另一个程序

Question

我试图找到逻辑上的艾伦图灵解释为什么不能有一个程序来检查另一个程序。

我记得我们在计算课程上学过，但现在我找不到解决方案，我需要向工作中的某个人解释。

感谢帮助。

score 3 · Accepted Answer

您正在寻找停机问题。

Alan Turing 在 1936 年证明，不可能存在解决所有可能的程序输入对的停止问题的通用算法。我们说停机问题在图灵机上是不可判定的。

score 2 · Accepted Answer

有这方面的维基百科条目...

但基本上，为了确定任何足够复杂的程序是否可以停止，您必须运行它以跟踪执行路径。这意味着你回到一个程序运行另一个程序，如果该程序没有停止，正在观看它的程序也不会停止。

这就像计算 pi 的数字——它会停止吗？你怎么能说它在运行时是无限的，而不是遭受一些计算问题？我们知道那个特定的问题是无限的，但其他类似的问题还没有被证明。

score 2 · Accepted Answer

“检查另一个程序”非常广泛。实际上，可以检查程序的某些特性，例如是否检查Java程序类型。但是，对 Java 程序进行类型检查也会拒绝一些在运行时实际上不会产生类型错误的程序，例如：

int foo() {
    if (true) return 5;
    else return null;
}

此方法永远不会真正返回null，但类型检查器看不到这一点。但是我们不能做一个更智能的类型系统吗？

不幸的是，答案是否定的。考虑以下程序：

int bar() {
    if (infiniteComputation()) return 5;
    else return null;
}

由于停止问题，类型检查器无法检查是否infiniteComputation会返回 false 。

另一个相关定理是Rice's Theorem，它可能比停止问题更接近您的问题。

值得指出的是，该定理仅说明没有可以准确检查的程序属性，对于实际目的，仍然可以很好地近似此类检查。一个例子是类型系统，我们接受一些“正确”的程序被拒绝，就像上面的代码片段一样。编译器还可以在很多情况下消除死代码，即使不可能在所有情况下都这样做。

score 0 · Accepted Answer

拜伦的回答应该为您指出重要信息。顺便说一句，您可以拥有一个检查特定程序的程序。你不能拥有一个检查任意程序是否正确的程序。

4 回答 4