クリーネの標準形定理に基づく証明
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2020/07/06 11:41 UTC 版)
「構造化定理」の記事における「クリーネの標準形定理に基づく証明」の解説
f : N n → N {\displaystyle f\colon \mathbb {N} ^{n}\to \mathbb {N} } をフローチャートによって計算可能な(一般には部分的に定義された)関数とする。これは再帰的関数になっている。クリーネの標準形定理(の弱い形)によれば、原始再帰的関数 T : N n + 1 → { 0 , 1 } {\displaystyle T\colon \mathbb {N} ^{n+1}\to \{0,1\}} と U : N → N {\displaystyle U\colon \mathbb {N} \to \mathbb {N} } が存在して、 f ( x → ) = U ( min { y ∈ N | T ( x → , y ) = 1 } ) {\displaystyle f({\vec {x}})=U(\min\{y\in \mathbb {N} |T({\vec {x}},y)=1\})} が成り立つ。ここで T ( x → , y ) = 1 {\displaystyle T({\vec {x}},y)=1} となる y {\displaystyle y} が存在しないとき、右辺は未定義と解釈する。 原始再帰的関数はループプログラムによって計算可能であることが知られている。ループプログラムは、基本的な算術演算、大小比較、条件分岐(if-then-else)、(変数によってループ回数を指定する)計数ループ、からなる言語であり、ジャンプ命令(goto文)やbreak文のような機構を含まない。したがって、ループプログラムで記述されるアルゴリズムは構造化定理の求める条件を満たしている。 したがって、 f {\displaystyle f} を計算するには、次のような手続きを踏めばよい。 y := 0t := 0while t = 0 do begin t := T(x, y); if t = 0 then y := y+1;end;z := U(y). ここで、T と U を計算する箇所は、構造化定理の条件を満たすようなアルゴリズムに置き換えられる。したがって f {\displaystyle f} もまた構造化定理を満たすアルゴリズムによって計算可能である。
※この「クリーネの標準形定理に基づく証明」の解説は、「構造化定理」の解説の一部です。
「クリーネの標準形定理に基づく証明」を含む「構造化定理」の記事については、「構造化定理」の概要を参照ください。
- クリーネの標準形定理に基づく証明のページへのリンク