帰納的であることと、計算可能であることは同値である

定理

自然数上の部分関数$ fに関する以下の2条件は同値である

①$ fは帰納的である

②$ fは計算可能である

証明

①→②

帰納的部分関数の定義に基づく帰納法で示す。

部分帰納的関数の4定義のそれぞれが計算可能であることを示せばいい

例えば3番目などはこう言い換える

計算可能部分関数から原始帰納法で得られるものはまた計算可能部分関数である

上3つは/mrsekut-private/C言語による計算の理論 5章レクチャー資料#5f8861c2198270000001abbbと同じ様に示せばいい

4つめの最小化についてはwhile文を使うと書くことができる

例えば$ f(x_1,x_2)=\mu y[(g(x_1,x_2,y)=0)\land (\forall z\lt y) (g(x_1,x_2,z)\downarrow)] という関数なら、以下のように書ける

code:c

f(x1, x2) {

int y;

y = 0;

while (g(x1, x2, y) != 0)

y++;

return(y);

}

②→①

$ pが$ k変数部分関数$ fを計算するジャンププログラムのコードであるならば、以下が成り立つので、これによって示される

$ f(\vec{x})=\mathrm{output}(\mu t [\mathrm{Trace}_k(p,\vec{x},t)])

各関数の定義は以下に示す

用語の整理

本体コード

ジャンププログラムの本体部分のコード

$ \lang \sharp S1,..,\sharp S_{n-1} \rang

#SはSのコード

状態値

pair(pc, <v1,v2,...,vm>)のこと

pcは次に実行する行番号を示す

vはプログラム中の各変数

関数の準備

next(s, q)

2変数原始帰納的関数

sは本体コード

qは状態値

sの中の, q+1の状態値を返す

Trace_k

k+2変数原始帰納的述語

プログラムのコード$ p

プログラムの引数$ x_1,\cdots,x_k

状態値の列$ t

$ pを引数$ x_1,\cdots,x_kで実行したときの、最初から最後までの状態値の列

#ToDo 実装の中身の理解

output

1引数

状態値の列$ t

output(t) = element(right(element(t, length(t))), 1)

最後の状態値のv1になる

普通にreturnする値のようなもの

参考

『C言語による計算の理論』 6章