I'm working on a proof-checker that can verify termination proofs. The fundamental method it provides for constructing such proofs is to translate the program into primitive recursion. Basically, I provide a combinator $\rho$ typed as:

$\rho: \forall A,B:(A\rightarrow Nat \rightarrow A)\rightarrow (A \rightarrow B)\rightarrow A\rightarrow Nat \rightarrow B$

which, in the notation defined here, constructs $h$ given $f$ and $g$.

Although the term language contains a fixed-point combinator and is therefore Turing-complete, terms that use it have a "tentative" flag in their type that indicate this. The $\rho$ combinator and the fixed-point combinator are the only two language primitives that allow for recursion or looping of any sort (i.e., without either of these two combinators, all you've got is a finite-state machine). Therefore, all terms that are well-typed and non-tentatively typed are primitive recursive.

What I'm wondering is if there are any interesting complexity classes that you can build by starting with primitive-recursive constructions, and adding a finite number of other functions $Nat \rightarrow Nat$, each of which is in R but not in PR, and allowing composition with these functions. It's easy to come up with *non*-interesting examples of such classes, e.g. "primitive recursion plus the Ackermann function", but I'm looking for any that have sufficiently interesting properties that it would be worth adding the functions which characterize them as admitted axioms in the proof system.

isTuring-complete, but expressions that invoke it have their types flagged to indicate that they do. But, every well-typed term that is not so-flagged is in PR, because $\rho$ is the only other combinator that provides recursion. $\endgroup$ – dfranke Aug 13 '10 at 12:50