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](http://en.wikipedia.org/wiki/Primitive_recursion), 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.



Interesting complexity classes $PR \subsetneq c \subsetneq R$
First of all, it’s certainly possible to obtain *some* intermediate class by taking a language that only computes PR functions (say, an imperative programming language [using only `for` loops](http://en.wikipedia.org/wiki/BlooP_and_FlooP)) and adding any total computable but non PR function (e.g., Ackermann’s function). The resulting language *L* is non-universal, because it only computes total functions: you can still construct a computable but non-*L*-computable function by diagonalisation. However, *L* is clearly more powerful than the original language.


As for “interesting”, I guess it really depends on what you mean by that.


If “interesting” means “of practical use”, then one could answer that all computable functions of practical use are PR, since a non-PR function requires an amount of time to compute that is not, in turn, PR. Considering that time bounds such as 2*n*, 2*2**n*, 2*2**2*n**, …, are all PR, you see that there isn’t much hope to compute non-PR functions for large values of *n*.


If “interesting” means “logically interesting”, then I think the answer is “yes”. I’m somewhat familiar with Girard’s System F (also called “second order λ-calculus” or “polymorphic λ-calculus”), described for instance in Girard’s *Proofs and Types* (freely available [here](http://www.paultaylor.eu/stable/Proofs+Types.html)). The functions that can be computed in F are “*exactly* those which are provably total in [second order Peano arithmetic]” (page 123), and among these we have Ackermann’s function. There is an explicit λ-term for it on [these slides](http://www.pps.jussieu.fr/~miquel/enseignement/mpri/SystF.pdf) (page 20).


If I recall correctly, the standard calculus of constructions includes System F and only computes total functions, so it also provides an example.


