原始再帰関数及び原始再帰関係の一覧

イントロ

あると便利だから，

あるいは毎回毎回ちゃんと確認するのも面倒だから

原始再帰の定義

自然数$ \N上の関数のうち，原始再帰的関数と呼ばれる次の関数がある．

1: $ n項定数関数

$ n項変数関数$ \mathrm{const}^n_c(\vec{x}): \N^n \to \N=cは原始再帰関数とする．

すなわち，変数を受け取るが全部捨てて$ cを返す定数関数は原始再帰関数とする．

2: 後者関数

$ \mathrm{succ}(x): \N^1 \to \N = x + 1は，原始再帰関数とする．

3: 射影関数

$ \mathrm{proj}^n_i(x_1,\dots,x_n) : \N^n \to \N = x_iは，原始再帰関数とする．

4: 合成

原始再帰関数$ f:\N^n \mapsto \N及び$ g_1,\dots,g_n:\N^m \to \Nについて，

関数$ h(\vec{x}) : \N^n \to \N = f(g_1(\vec{x}),\dots,g_n(\vec{x}))は原始再帰関数である．

ただし，$ \vec{x}とは$ x_1,\dots,x_mとする．

5: 原始再帰

原始再帰関数$ f:\N^n\to\N及び$ g:\N^{n+2}\to\Nに対して，

次のように定める関数$ h(\vec{x},y):\N^{n+1}は原始再帰関数である．

$ h(\vec{x},0) = f(\vec{x})

$ h(\vec{x},\mathrm{succ}(n)) = g(\vec{x},n,h(\vec{x},n))

6: これ以外に原始再帰関数であるものは存在しない．

以下では証明と書いたものは基本的には原始再帰関数の定義に沿って関数を定義して示す．

$ n変数ゼロ関数: $ \mathrm{zero}^n(\vec{x})

引数を$ n個取るがそれらを全て捨てて定数0を返す関数$ \mathrm{zero}^n(\vec{x}):\N^n \to \Nは原始再帰関数である

証明

$ \mathrm{zero}^n \coloneqq \mathrm{const}^n_0とする．

加算:$ \mathrm{add}(x,y)/$ x+y

加算$ \mathrm{add}(x,y): \N^2 \to \Nは原始再帰関数である．

証明

$ \mathrm{add}(x,0) = \mathrm{zero}^2(x,0) = 0

$ \mathrm{add}(x, \mathrm{suc}(y)) = \mathrm{succ}(\mathrm{proj}^3_3(x,y,\mathrm{add}(x,y))) = \mathrm{succ}(\mathrm{add}(x,y))

注意

長すぎるので，$ \mathrm{add}(x,y)を省略して$ x+yと書く

乗算:$ \mathrm{mult}(x,y)/$ x \times y

乗算$ \mathrm{mult}(x,y): \N^2 \to \Nは原始再帰関数である．

証明

$ \mathrm{mult}(x,0) = \mathrm{zero}^2(x,0) = 0

$ \mathrm{mult}(x, \mathrm{suc}(y)) = \mathrm{proj}^3_3(x,y,\mathrm{mult}(x,y)) + \mathrm{proj}^3_1(x,y,\mathrm{mult}(x,y)) = \mathrm{mult}(x, y) + x

注意

長すぎるので，$ \mathrm{mult}(x,y)を省略して$ x \times yと書く

冪乗:$ \exp(x,y)/$ x^y

冪乗$ \exp(x,y): \N^2 \to \Nは原始再帰関数である．

証明

$ \exp(x,0) = \mathrm{zero}^2(x,0) = 0

$ \exp(x, \mathrm{suc}(y)) = \mathrm{proj}^3_3(x,y,\mathrm{mult}(x,y)) + \mathrm{proj}^3_1(x,y,\mathrm{mult}(x,y)) = \mathrm{mult}(x, y) + x

注意

長すぎるので，$ \exp(x,y)を省略して$ x^yと書く

前者関数:$ \mathrm{pred}(x,y)

一つ前の自然数を返す関数$ \mathrm{succ}(x): \N \to \Nは原始再帰関数である．

証明

$ \mathrm{pred}(0) = \mathrm{zero}^1(0) = 0

$ \mathrm{pred}(\mathrm{succ}(x)) = \mathrm{proj}^2_1(x,\mathrm{pred}(x)) = x

補正付き減算: $ \mathrm{msub}(x,y)/ $ x \ominus y

補正付き減算$ \mathrm{msub}(x,y): \N^2 \to \Nは原始再帰関数である．

なお補正付き減算とは次のようなものである

$ x \ge yならば$ x \ominus y = x - y

$ x < yならば$ x \ominus y = 0

証明

$ \mathrm{msub}(x,0) = \mathrm{zero}^2(x,0) = 0

$ \mathrm{msub}(x,\mathrm{succ}(y)) = \mathrm{pred}(\mathrm{proj}^3_3(x,y,\mathrm{msub}(x,y))) = \mathrm{pred}(x,y,\mathrm{msub}(x,y))

注意

長すぎるので，$ \mathrm{msub}(x,y)を省略して$ x \ominus yと書く

最大値: $ \max(\vec{x})

$ 1 \leq n個以上$ \vec{x}の最大値を求める関数$ \max(\vec{x}):\N^n \to \Nは原始再帰関数である．

最小値: $ \min(\vec{x})

$ 1 \leq n個以上$ \vec{x}の最小値を求める関数$ \min(\vec{x}):\N^n \to \Nは原始再帰関数である．