程序能否决定任意程序是否因某些输入而停止？

Question

是否有一个程序(may-halt?p)可以判断是否存在输入使(p input)停止？

我尝试了简单的对角化，但它只告诉我 (may-halt?di​​ag-may-halt) 必须为真。无助于证明程序是否存在

有这样的程序吗？

Answer 1

不，may-halt? 不存在。

（我认为通过对角化的直接证明不会比 Halting problem is undecidable 的证明简单；否则 that 将是标准示例。相反，让我们将您的问题简化为停机问题:)

假设有一个程序 may-halt? p，它决定程序 p 是否因 一些 输入而停止。然后定义：

halt? p x := may-halt? (\y -> if y==x then p x else ⊥)

大括号中的东西是派生程序。让我们分解一下：

halt? p x := may-halt? p'

其中 p' 是 (i) 在输入 x 上计算 p x 的程序，(ii) 在任何其他输入上只是循环而不终止：

p' y := if y==x then p x else ⊥

然后 may-halt? p' 当且仅当 p x 终止时输出 true。

因此，对于任何程序 p 和输入 x，halt? p x 将决定 p x 是否终止。但我们知道那是不可能的，所以 may-halt? 不存在。