6

众所周知，停止问题没有明确的解决方案，a) 返回 true <==> 程序确实停止了，b) 处理任何输入，但我想知道是否有足够好的解决方案来解决这个问题，那些可能可以完美处理某些类型的程序流，或者能够识别何时无法正确解决问题的程序，或者正确率很高的程序，等等......

如果是这样，它们有多好，它们依赖什么想法/限制？

4

6 回答 6

4

通常的方法是将程序行为限制为有效可计算的算法。例如，简单类型的 lambda 演算可用于确定算法总是停止。这意味着简单类型的 lambda 演算不是图灵完备的，但它仍然足够强大，可以表示许多有趣的算法。

于 2010-03-18T01:16:04.577 回答
1

可以完美处理某些类型的程序流的那些

这很容易，而且你的“某些类型”越窄越容易。原始示例：确定以下代码是否终止，对于任意起始值x：

void run(int x)
{
    while(x != 0)
    {
        x = x > 0 ? x-2 : x+2;
    }
}

该解决方案比代码本身要短。

或能够识别何时无法正确解决问题

再次简单：使用上面的程序，当程序不符合固定的窄模式时，让它回复“否”。

或者正确率很高的那个

您如何在无限的可能输入集上定义“高”百分比？

于 2010-03-18T00:11:55.213 回答
1

证明循环停止的一种方法是识别一些整数变量（不一定在程序中明确显示），每次执行循环时该变量总是减小，并且一旦该变量小于零，循环将终止。我们可以称这个变量为循环变量。

考虑以下小片段：

var x := 20;
while (x >= 0) {
    x := x - 1
}

在这里，我们可以看到每次执行循环时 x 都会减小，并且一旦 x < 0，循环就会退出（显然，这不是很严格，但你明白了）。因此，我们可以使用 x 作为变体。

一个更复杂的例子呢？考虑一个有限的整数列表，L = [L[0], L[1], ..., L[n]]。in(L, x)如果 x 是 L 的成员，则为真。现在考虑以下程序：

var x := 0;
while (in(L, x)) {
    x := x + 1
}

这将搜索自然数 (0, 1, 2, ...)，并在找到不在 L 中的 x 值时停止。那么，我们如何证明这会终止？L 中必须有一个最大值——称之为 max(L)。然后我们可以将我们的变体定义为max(L) - x。为了证明终止，我们首先必须证明max(L) - xx 总是在减少——不是太难，因为我们可以证明 x 总是在增加。然后我们要证明循环将在 时终止max(L) - x < 0。如果max(L) - x < 0，则max(L) < x，这意味着 x 不可能在 L 中，因此循环将终止。

于 2010-03-18T00:33:40.803 回答
0

是的，只需使状态空间有限，并且（理论上）所有输入都是可能的。（简单地遍历所有可能性。）

所以理论上任何程序都可以在真实计算机上运行。（您可能必须使用比执行程序的 RAM 更大的计算机来进行分析。当然，分析会花费非常长的时间。）

可能你想要一些更实用的东西。在这种情况下，请考虑语言。尽管您可以提供无限多的程序作为输入，但可以很快确定语法正确/不正确的问题（取决于语言的种类和输入长度）。（注意：我们不是在谈论执行输入程序，只是确定它在语法上是否正确。）

于 2010-03-18T00:51:11.363 回答
0

有时机器是否会停止是显而易见的，即使它非常大。一旦你确定了一个模式，比如存在一个“倒计时”变量，你就可以编写一个小型机器，它适用于任何拥有它的机器。那是一个无限大的家庭，但在所有可能的机器中微不足道。大多数人工编写的机器对于它们的大小都有非常简单的行为，所以如果其中很多可以在实际时间/空间中解决，我不会感到太惊讶，但我不知道如何衡量这一点。

为了让您了解“他们有多好”的问题有多难，这里有一个非常具有理论意义的问题：对于给定的尺寸 N，有多少台尺寸为 N 的机器停机？这是不可计算的（因为可以计算它的机器可以用来解决停机问题）并且对于 N>4 是未知的。

于 2010-03-18T00:49:40.410 回答
0

请参阅与终结者项目相关的论文：

http://research.microsoft.com/en-us/um/cambridge/projects/terminator/

于 2010-03-18T00:08:35.147 回答