半決定可能の同値条件の証明

参考

『C言語による計算の理論』 pp.110-113

証明

①→③

①と③をわざわざ分ける必要ないくらいに自明なのでは？mrsekut.icon

「$ \alphaを半決定するプログラム」は、「$ \alphaを定義域とした1変数計算可能部分関数のプログラム」である

f :: α -> 1 | undefined

https://gyazo.com/ecc958fbf4a0506fbb9a3eaf26417dba

③→④

③を満たす部分帰納的関数を$ fとすると、クリーネの標準形定理により

$ f(x)=\mathrm{output}(\mu t [T(x,t)]) となる$ T,\mathrm{output}が存在する

$ \alpha\ne\emptysetのとき、$ \forall a\in\alphaに対し、以下のような原始帰納的関数$ gを定義する

$ g(y) = \left\{ \begin{array}{ll} \mathrm{left}(y) & (T(\mathrm{left}(y), \mathrm{right}(y))) \\ a & (\mathrm{otherwise}) \\ \end{array} \right.

この$ gが、④で言っている関数になるmrsekut.icon

この$ gの定義域は$ \alphaである

つまり、$ \mathrm{left}(y),a\in\alphaであることが以下によって示せる

$ x\in\alpha$ \iff f(x)\downarrow

$ \alphaが$ fの定義域なので。

$ \iff$ T(x,t)が成り立つ$ tが存在する

こういう$ tが存在しないなら、$ f(x)\uparrowになるので。

$ \iff$ T(\mathrm{left}(y),\mathrm{right}(y))が成り立ち、$ x=\mathrm{left}(y)となるような$ yが存在する

逆に考えればいい

$ y=\mathrm{pair}(x,t)とすると、$ x=\mathrm{left}(y)であるmrsekut.icon

よって、$ x\in\alphaならば、$ gの1つ目の条件に該当し、$ x\;\left(=\mathrm{left}(y)\right)が返り値になる

逆に$ x\notin \alphaのときは、$ aが返り値になるので、結局、どっちにしても$ \alphaが値域になる

④→⑤

原始帰納的関数は、計算可能部分関数であるので明らか

#??

$ \alphaが空集合のときは？

空集合を値域とする計算可能部分関数が存在する？

⑤→⑥

⑤を満たすような、$ \alphaを値域とする$ k変数計算可能部分関数$ fが存在するとすると、クリーネの標準形定理により、

$ f(x)=\mathrm{output}(\mu t [T(x,t)]) となる$ T,\mathrm{output}が存在する

ここで、2変数原始帰納的述語$ Aを以下で定義する

$ A(x,y)=A_1\land A_2\land A_3\land A_4　

ここで

$ A_1= (k=\mathrm{length}(y)-1)

$ A_2=(x=\mathrm{output}(y_{k+1}))

$ A_3=T(y_1,y_2,\cdots,y_k,y_{k+1})

$ A_4= \forall z\lt y_{k+1} (\lnot T(y_1,y_2,\cdots,y_k,z))

これらの$ A_1,..,A_4は、以下のように考えるとスッと理解できるmrsekut.icon

まず、$ A_3の$ Tの引数の中身の全ての$ y_iの列のコードを$ yとすると

$ yは、 $ y=\lang e_1,e_2,\cdots,e_k,t\rangのように見ることができる

$ T(..)=\mathrm{Trace}_k(p, ..)のようなカリー化が成されている

https://gyazo.com/36a16c063c4d7146798c801bd0e0ff92

クリーネの標準形定理の$ T_kの中身をコード化したもの

$ xは使用済みで紛らわしいので$ eを使っているmrsekut.icon

そうすると、

$ A_1は$ kの変数定義

$ A_2は、プログラムp<e>の返り値を$ xに束縛していると見れる

$ A_3は、普通に棋譜の検査$ T(p,e_1,\cdots,e_{k-1},t)が成り立つことを見る

$ A_4は、最小化のためにμ演算子の定義に則っていることを確認

つまり、全体として$ f(\vec{x})=\mathrm{output}(\mu t [T(\vec{x},t)]) を論理式で表現した感じに見える

すると、以下が成り立つ

$ a\in\alpha$ \iff$ a=f(\vec{x})となる$ \vec{x}\in\mathbb{N}^kが存在

$ \iff $ a=\mathrm{output}(\mu t[T(\vec{x},t)]) となる$ \vec{x}\in\mathbb{N^k}が存在する

$ \iff$ a=\mathrm{output}(t)かつ$ T(\vec{x},t)かつ$ (\forall t'\lt t)(\lnot T(\vec{x},t'))となる、$ \vec{x}\in\mathbb{N}^kと$ tが存在する

$ a=\mathrm{output}(t)かつ$ T(\vec{x},t)は前式より自明

$ (\forall t'\lt t)(\lnot T(\vec{x},t'))は上の$ A_3の書き換え

$ \iff$ A(a,y)が成り立つ$ yが存在する

$ y=\lang \vec{x},t\rangとすれば良い

⑥→⑦

原始帰納述語は、計算可能述語であるので明らか

⑦→②

$ x\in\alpha\iff(\exist y\in\mathbb{N})(B(x,y))であるような計算可能述語$ Bを使って、$ \alphaを枚挙するプログラムを作ればいい

nで自然数を網羅して、B(left(n), right(n))が真になるときのleft(n)を返す

code:c

alpha(){

int n,x,y;

n=1;

while (n>=1){

x = left(n);

y = right(n);

if (B(x,y)==1)

printf(x); // Bが真になるときに出力

n++

}

pairの作り方を考えれば、nが自然数を網羅すること自体はあまり関係なくて、

(0,0), (0,1), (1,0), (0,2),,,を全網羅していると考えたほうが直感的mrsekut.icon

これ、何をしているのかと言うと

https://gyazo.com/405637f792254d95c7d282c2bdc45af4

この表で、ある$ xについて行を見たときに、どこかで1が出てくるかどうかを知りたいわけだが、

まず$ x=0について、次に$ x=1について、、と見ていくと、

もし$ 0\in\alphaだとすると、無限に$ x=0の行を見ていくことになり永遠に終わらない

なので、枚挙されない

なので、工夫が必要

なので、上のようなプログラムになっている

https://gyazo.com/a998b9a07288bd0bd83a00504faa3b9e

対角線に見ていくことで、そういう事態が起きなくなる

②→①

$ \alphaを枚挙するプログラムを3箇所変えて、半決定するプログラムを作ればいい

引数に、使われていない名前の変数を使う。

例えばv

printf(x)を、if(v==x) printf(1)にする

プログラムの最後尾にwhile(0==0) {}を追加

これ必要なの？

例として上のコードを書き換えてみる

code:ex.c

alpha(v){

int n,x,y;

n=1;

while (n>=1){

x = left(n);

y = right(n);

if (B(x,y)==1)

if(v == x)

return(1);

n++

}

while(0=0) {}

}