logic - 程序可以决定任意程序是否因某些输入而停止？

Question

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

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

有这样的程序吗？

Answer 1

不，may-halt?不存在。

（我认为对角化的直接证明不会比停止问题不可判定的证明更简单；否则这将是标准示例。相反，让我们将您的问题简化为停止问题：）

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

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

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

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

（i）在输入上计算p'的程序在哪里，（ii）在任何其他输入上只是循环而不终止：xp x

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

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

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