logic - プログラムは、任意のプログラムが SOME 入力のために停止するかどうかを判断できますか?

Question

(p 入力) が停止するように入力が存在するかどうかを判断できるプログラム (may-halt? p) はありますか?

簡単な対角化を試みましたが、(may-halt? diag-may-halt) が true でなければならないということしかわかりません。プログラムが存在するかどうかを証明するのには役立ちません。

そのようなプログラムは存在しますか？

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) 入力で を計算し、(ii) 他の入力で、終了せずにループするだけp'のプログラムです。xp x

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

次に、終了したmay-halt? p'場合にのみ true を出力しますp x。

したがって、任意のプログラムpと inputxについて、終了halt? p xするかどうかを決定しp xます。しかし、私たちはそれが不可能であることを知っているので、may-halt?存在しません。