原始再帰関数(Mathlib4版)
1変数関数$ f,g,h:\N \to \NはMathlib4の原始再帰関数であるとする 以下はMathlibの原始再帰関数である
1. ゼロ関数: $ \mathrm{zero}(n) = 0
2. 後続関数: $ \mathrm{succ}(n) = n+1
3. 合成: $ \mathrm{comp}(n) = f(g(n))
4. ペア: $ \mathrm{pair}(n) = \mathcal{P}\left( f(g), h(g) \right)
5. 左および右:
$ \mathrm{left}(n) = \mathcal{U}(n).1
$ \mathrm{right}(n) = \mathcal{U}(n).2
6. 原始再帰
関数$ \mathrm{prec}(n) = q \left( \mathcal{U(n).1}, \mathcal{U}(n).2 \right)
$ q: \N^2 \to \N
$ n: $ \N
$ q(z,n)は↓の関数とする
自然数$ \Nの帰納的定義に沿って
$ 0のとき$ f(\mathrm{0})
$ i+1のとき$ g\left( \mathcal{P}(z, \mathcal{P}(y,n)) \right)
ただし
2変数関数$ \mathcal{P}: \N^2 \to \NはCantorの対関数みたいなものを想定 $ \mathcal{U}(n) = (a,b)のとき↓の略記とする
$ \mathcal{U}(n).1 = a
$ \mathcal{U}(n).2 = b