Halt = { f,x | f(x)↓ } is re (semi-decidable) but undecidable
Total = { f | ∀x f(x)↓ } is non-re (not even semi-decidable)
Total問題が再帰的でない (決定可能)ことを証明する助けが必要です。
Halting問題の対角化証明は知っていますが、 Total問題についても同じ種類の証明が必要です。参照用にHalting Problem Proof を投稿しています。
問題の証明の停止
停止問題を決定できると仮定します。次に、次のようないくつかの合計関数 Halt が存在します。
1 if [x] (y) is defined
Halt(x,y) =
0 if [x] (y) is not defined
ここでは、すべてのプログラムに番号を付けており、[x] はこの順序で x 番目のプログラムを指します。入力を one-one 関数を介して 2 つの数値のペアを表す単一の数値として扱うことにより、Halt を ℵ から ℵ へのマッピングと見なすことができます。
pair(x,y) = <x,y> = 2^x (2y + 1) – 1
with inverses
<z>1 = exp(z+1,1)
<z>2 = ((( z + 1 ) // 2^<z>1) – 1 ) // 2
Halt が存在する場合、Disgree も存在します。
0 if Halt(x,x) = 0, i.e, if Φx (x) is not defined
Disagree(x) =
µy (y == y+1) if Halt(x,x) = 1, i.e, if Φx (x) is defined
Disagree は ℵ から ℵ へのプログラムであるため、Disagree は Halt によって推論できます。d を Disagree = Φd とします。
Disagree(d) が定義されている ⇔ Halt(d,d) = 0 ⇔ Φd (d) が定義されていない ⇔ Disagree(d) が定義されていない
しかし、これは、不一致がそれ自体の存在に矛盾することを意味します。元の仮定を除いて、私たちが取ったすべてのステップは建設的だったので、元の仮定が間違っていたと推測しなければなりません. したがって、停止問題は解決できません。