半決定可能の同値条件
参考
『C言語による計算の理論』 p.110
集合\alphaに関する以下の条件は全て同値
①\alphaは半決定可能である
\alphaを半決定するプログラムが存在する
②\alphaは帰納的枚挙可能である
\alphaを枚挙するプログラムが存在する
③\alphaを定義域とする1変数計算可能部分関数が存在する
これ、「半決定可能」そのものて感じするな
⑤\alphaを値域とする計算可能部分関数が存在する
⑥ある2変数原始帰納述語Aが存在して以下が成り立つ
x\in\alpha\iff(\exist y\in\mathbb{N})(A(x,y))
上図はAの出力を全網羅した表
あるxの行を見たときに、どこかに1が存在すれば、x\in\alphaだということ
x\notin\alphaの場合は、どこまでいっても0が続き1が出てこない
⑦ある2変数計算可能述語Bが存在して以下が成り立つ
x\in\alpha\iff(\exist y\in\mathbb{N})(B(x,y))
証明
部分的に一般化した同値条件
\mathbb{N}^kの要素からなる集合\alphaに関する以下の4条件はすべて同値である
ただしkは1以上の任意の自然数
①' 以下のようなk入力プログラムQが存在する
Qを入力値\vec{x}で実行すると、
\vec{x}\in\alphaの場合は1を返して実行が終了
\vec{x}\notin\alphaの場合は実行が永久に終了しない
③' \alphaを定義域とするk変数計算可能部分関数が存在する
⑥' あるk+1変数原始帰納的述語Aが存在して、以下が成り立つ
\vec{x}\in\alpha \iff (\exist y)A(\vec{x},y)
⑦' あるk+1変数計算可能述語Bが存在して、以下が成り立つ
\vec{x}\in\alpha \iff (\exist y)B(\vec{x},y)
これらは、半決定可能の同値条件の①③⑥⑦の一般化にあたる
逆に言えば、①'③'⑥'⑦'でk=1にしたものが、①③⑥⑦
証明
①'→③'
Qは\alphaを定義域とするk変数計算可能部分関数を計算するプログラムになっている
③'→⑥'
\alphaがfの定義域でfを計算するジャンププログラムのコードがpのとき
A(\vec{x},y)\iff\mathrm{Trace}_k(p,\vec{x},y)
と、すればいい
標準形定理とかは関係なく
⑥'→⑦'
原始帰納述語は、計算可能述語であるので明らか
⑦'→①'
k=2のとき、Bの特性関数を計算するプログラムを
B とすると以下のプログラムが\alphaを半決定するcalpha(x1, x2){
int n;
n = 0;
while (n>=0) {
if (B(x1, x2, n) == 1)
return(1);
n++;
}
}