原始再帰関数とは
原始再帰関数とは、３つの基本関数から、合成と原始再帰の操作によって組み立てた、和や積のように有限手順で計算できる（計算可能な）関数です。原始再帰関数により、証明や文字列操作、ゲーデル数化など全て機械的に表現することができます。
尚、再帰関数は、原始再帰関数に無制限探索（ループ型） を加えたもので、有限手順とは限らない関数も含みます。例えば、アッカーマン関数は再帰関数（ $\mu$ 再帰関数）ですが、原始再帰関数ではありません。
以下、基本関数・合成・原始再帰について具体的に説明します。
基本関数
原始再帰関数の基本関数は以下の３つになります。
- ゼロ関数：何を入れても 0 を返す。$$Z(x)=0$$
- 後者関数：次の数を返す。$$S(x)=x+1$$
- 射影関数：入力の中から１つ取り出す。$$P_i^n(x_1,\cdots,x_n)=x_i$$
合成
合成とは、既に作った関数に別の関数の出力を代入する操作です。例えば、１を加える関数 $f$ は、以下のように２つの基本関数の合成で作ることができます。
$$f(x,y)=S\big(P_1^2(x,y)\big)=x+1$$
原始再帰
原始再帰とは、$k$ の値を $k+1$ の値から求めるという操作で、数学的帰納法と同じ形をもちます。初期値用の関数 $g$ とステップ用の関数 $h$ から、新しい関数 $f$ を以下のように作ります。
$$\left\{\begin{array}{ll}
f(0,x_1,\cdots,x_n)=g(x_1,\cdots,x_n) \\
f(k+1,x_1,\cdots,x_n)=h\big(k,f(k,x_1,\cdots,x_n),x_1,\cdots,x_n\big) \end{array} \right.$$
原始再帰関数の例
原始再帰関数の作成操作で、和、積、べき乗、階乗、多項式などの関数を作ることができます。以下にいくつかの例を示します。
和の関数
和の関数 $\mathrm{add}(x,y)=x+y$ は、以下のように、１づつ増やすの繰り返しで表すことができます。
$$\left\{\begin{array}{ll}
\mathrm{add}(0,y)=y \\
\mathrm{add}(x+1,y)=S\big(\mathrm{add}(x,y)\big) \end{array} \right.$$
積の関数
積の関数 $\mathrm{mul}(x,y)=x\cdot y$ は、以下のように、足し算の繰り返しで表すことができます。
$$\left\{\begin{array}{ll}
\mathrm{mul}(0,y)=0 \\
\mathrm{mul}(x+1,y)=\mathrm{add}\big(\mathrm{mul}(x,y),y\big) \end{array} \right.$$
階乗の関数
階乗の関数 $\mathrm{fact}(x)=x!$ は、以下のように、掛け算の繰り返しで表すことができます。
$$\left\{\begin{array}{ll}
\mathrm{fact}(0)=1 \\
\mathrm{fact}(x+1)=\mathrm{mul}\big(\mathrm{fact}(x),n+1\big) \end{array} \right.$$
原始再帰関数の特徴
メタ数学的な操作は、原始再帰という算術で表現することができます。メタ数学とは、数学そのものを研究対象とする学問で、例えば、ある体系は無矛盾か、この命題は証明可能かなど、数学についての論理的考察を行います。
１）原始再帰関数は体系内で表現可能
原始再帰関数の手続きは、形式体系（ペアノ算術）の中の数式（算術）として表現（形式化）できます。これにより、計算の話を数の性質の話に置き替えられるので、証明、代入、ゲーデル数化などを全て算術の中で扱えるようになります。
２）原始再帰述語は決定可能
原始再帰関数の定義より、原始再帰関数から作られる関係（述語）は決定可能（有限手順で判定可能）となります。そして 1) より、その手順は形式体系（ペアノ算術）の中で記述することができます。
３）構文操作は原始再帰関数で表現可能
論理式・証明列・代入・連結などの構文操作（文字列の操作）はすべて原始再帰関数で表現することができます。例えば、式 $a$ の $x$ に $y$ を代入する操作は、以下のように原始再帰関数で表される操作に分解することができます。
-
- 式 $a$ を素因数分解の列で表す
- 列の中から $x$ の部分を走査する
- $x$ を $y$ に置換する
- 新しい列をゲーデル数に戻す
このように、数式はゲーデル数により有限列の自然数で表され、代入という操作は「列の走査＋置換」という有限回の for ループ型処理（原始再帰）で記述することができます。
４）証明可能性は原始再帰で表現可能
例えば「$x$ は $y$ の証明のゲーデル数である」といった証明可能性は、原始再帰の述語として記述することができます。つまり、3) は論理式などの操作が原始再帰関数で作れることを示し、4) はその操作を使って証明可能性が原始再帰述語で記述できることを示します。
尚、「関数」は $x+y$ などのように自然数の入力から自然数の値を返す計算で、「述語」は $x\lt y$ などのように真偽を返す関係を表します。通常、述語は関数を用いて表され、関数が原始再帰なら述語も原始再帰になります。
$\mathrm{Proof}(x,y)$ は「数 $x$ は、式 $y$ の正しい証明である」という意味の原始再帰述語です。ここで、$x$ は証明全体のゲーデル数で、$y$ は証明したい論理式のゲーデル数です。例えば以下の証明の場合、
-
- $A\to B$ （公理）
- $A$ （仮定）
- $B$ （ 1 と 2 からの推論）
$x$ はこの証明全体のゲーデル数、$y$ は $B$ のゲーデル数です。従って、$\mathrm{Proof}(x,y)$ は「この３行は正しい証明」という意味になります。
