Bounded Summation of Integers is Primitive Recursive
Jump to navigation
Jump to search
Theorem
Let the function $f : \N^{k + 1} \to \N$ be primitive recursive.
Let the function $g : \N^{k + 1} \to \N$ be defined as:
- $\map g {n_1, \dotsc, n_k, z} = \paren {\sum_{y = 0}^{z - 1} \ell_y}_\Z$
where $\map f {n_1, \dotsc, n_k, y}$ codes the integer $\ell_y$.
Then, $g$ is primitive recursive.
Proof
We can equivalently write $g$ as:
- $\map g {n_1, \dotsc, n_k, z} = \begin{cases} 0 & : z = 0 \\ \map g {n_1, \dotsc, n_k, z - 1} +_\Z \map f {n_1, \dotsc, n_k, z - 1} & : z > 0 \end{cases}$
which is clearly obtained by primitive recursion from:
$\blacksquare$.