Primitive recursive function

Primitive recursive functions are generated by zero, successor, and projections under composition and primitive recursion.

For a decidable coding of finite construction trees, the codes of arity-$i$ primitive recursive functions in intension are decidable. Check initial-function tags, then verify the child arities at each composition and recursion node. This is a terminating finite syntax check, distinct from asking whether an arbitrary program's extension happens to be primitive recursive.

Enumerate all valid unary primitive recursive functions in intension by their decidable codes $p_n$, and interpret each extension $F_{p_n}$. The function $d(n)=F_{p_n}(n)+1$ is a total computable function, since each finite construction terminates. If it were primitive recursive, some $F_{p_j}$ would equal $d$, giving $d(j)=d(j)+1$. Repeated extensions in the syntax enumeration do not affect this argument.

A valid finite construction expression from the initial functions of recursion theory by function composition in recursion theory and primitive recursion. Its extension is a primitive recursive function. The construction grammar supplies both a decidable syntax and a total computable interpreter, but no uniformly primitive recursive interpreter for all valid codes.

For a fixed effective machine coding, the predicate that program $e$ on input $x$ halts within $t$ steps is primitive recursive. Code finite configurations, iterate a total single-step function by primitive recursion, and test for the halt state. This supplies a bounded simulation even though the unrestricted halting problem is undecidable.

Search over the finite interval $0\le y\le b$ for the least witness to a primitive recursive predicate, with an explicitly chosen default if there is none. The result is a primitive recursive function, by scanning this finite interval using primitive recursion. This differs from unbounded minimization, which may fail to terminate.

The predecessor function on the nonnegative integers is $\mathrm{pred}(0)=0$ and $\mathrm{pred}(n+1)=n$. This is a primitive recursive function by primitive recursion from the zero and projection functions.

The initial functions are the zero function, the successor function, and all coordinate projections.

The zero function has the constant valueDummy variables give a zero function of any finite arity.

The successor function is

The $i$th $k$-ary projection returns its $i$th input:

Given a $m$-ary function $g$ and $k$-ary functions $h_1,\dots ,h_m$, composition forms

From $g:{\mathbb{N}}^k\to \mathbb{N}$ and $h:{\mathbb{N}}^{k+2}\to \mathbb{N}$, primitive recursion defines

The functions generated from the initial functions using composition alone are exactlyfor a constant $c\in \mathbb{N}$. Structural induction proves necessity, and iterating the successor function on zero or a projection proves sufficiency.

To prove a property of every primitive recursive function, prove it for the zero, successor, and projection functions, then prove that it is preserved by composition and by primitive recursion. This is structural induction on the finite construction of the function.

The initial functions are total, composition preserves totality, and ordinary induction on the recursion argument shows that primitive recursion applied to total functions is total. Structural induction therefore proves that every primitive recursive function is total.

The graph of every primitive recursive $f:{\mathbb{N}}^k\to \mathbb{N}$ has a formulain the language of ordered rings, where every quantifier inside $\delta$ is bounded. Composition uses existentially quantified intermediate values, while primitive recursion uses a boundedly checked code for the finite sequence of intermediate values.

The Gödel beta function codes finite sequences by remainders:Choosing $c$ sufficiently large and divisible by the relevant small integers makes the moduli pairwise coprime, so the Chinese remainder theorem codes any prescribed finite sequence.

The graph of the factorial function has a fixed-length first-order formula in the language of ordered rings interpreted on the natural numbers. A remainder code records $a_0=1$, $a_n=y$, and $a_{i+1}=(i+1)a_i$ for every $i<n$. Uniqueness of remainders proves $y=n!$; sufficiently large pairwise-coprime moduli and the Chinese remainder theorem supply a code for every input. Formula length is independent of the input variable's value, although substituting a numeral adds its encoding length.

In a primitive recursion, an existential representation of the step function may need a different witness tuple at every time. Code each coordinate of the finite witness array by a separate beta-function code pair. All row witnesses then have bounded remainder quantifiers under the bounded time quantifier, while the finitely many code pairs remain in the outer unrestricted existential block.