クリーネの標準形定理
Kleene's normal form theorem
任意の帰納的関数は、とある原始帰納的関数と、とある原始帰納述語で表せる
定理
任意の$ k引数帰納的関数$ f(\vec{x})は、 適当な
を用いると、
$ fに対して、自然数$ pが存在して、以下のように表せる
$ f(\vec{x})=g(\mu t[T_k(p, \vec{x},t)])
補足
$ tがそれの変数
関数$ g
1引数
状態値の列$ t
output(t) = element(right(element(t, length(t))), 1)
最後の状態値のv1になる
普通にreturnする値のようなもの
原始帰納的述語$ T_k
$ k+2変数
プログラムのコード$ p
$ pの引数$ x_1,\cdots,x_k
状態値の列$ t
$ pを引数$ x_1,\cdots,x_kで実行したときの、最初から最後までの状態値の列
引数で渡された$ tが正しいときに真を返す
$ \mathrm{Trace}_kは「$ tを求めるプログラム」ではないことに注意
状態値
pair(pc, <v1,v2,...,vm>)のこと
pcは次に実行する行番号を示す
vはプログラム中の各変数
証明
証明自体は難しくないが、準備が多いので面倒
『C言語による計算の理論』.iconの6章、wiki2に書いている 参考資料の関数の対応
見ればわかるがmrsekut.icon
table:参考資料の関数の対応
上の定義 C言語の~ wiki1 wiki2
1変数原始帰納的関数 g output U U
k+2変数原始帰納述語 T Trace_k T T_k
補足
ちなみに、上の定義と『C言語による計算の理論』.iconとwiki2の定義はちゃんと一般化されて$ f(\vec{x})について見ているが、wiki1はされていない
参考