Between mu- and primitive recursion

I think it would also be reasonable to (explicitly) mention the functions definable by primitive recursion in higher types - instead of only defining functions $\mathbb{N}\to\mathbb{N}$ by primitive recursion, we may also define families of functions (i.e. functions $\mathbb{N}\to\mathbb{N^N}$) by primitive recursion (and, of course, even more complicated things).

As an example, let us first define an iteration function $g\colon\mathbb{N}\times\mathbb{N^N}\to\mathbb{N^N}$ by primitive recursion, by: \begin{array}{l} g(0,f) = i \qquad\qquad\text{(the identity function)}\\\\ g(n+1, f) = f\circ g(n, f) \end{array} We can then easily define a `curried' version of the Ackermann function as a function $A\colon\mathbb{N}\to\mathbb{N^N}$, by: \begin{array}{l} A(0) = S \quad\quad\text{(successor)}\\\\ A(n+1) = g(n, A(n)) \end{array}

This is quite popular with (some groups of) computer scientists, particularly those interested in functional programming, and some form of primitive recursion in higher types is behind the strength of the language Charity you mentioned (which also allows primitive recursion over other data structures than the natural numbers).

Robin Chapman's answer is very apropos. Here is a theoretical answer that points out a subtlety in the question.

First, recall that the primitive recursive functions are the smallest class of functions on $\mathbb{N}$ that:

• Includes the constant zero function, the successor function, and all projection functions;
• is closed under composition;
• and is closed under primitive recursion.

Let's call this class of functions $\operatorname{PR}(\emptyset)$. For any set $A$ of number theoretic functions, we can define a more general class $\operatorname{PR}(A)$ as the smallest class of functions that satisfies the above properties and also includes every function in $A$.

If every function in $A$ is computable, then every function in $\operatorname{PR}(A)$ is computable. Moreover, if every function in $A$ is total then every function in $\operatorname{PR}(A)$ is total.

It would be trivial, assuming $A$ is finite (or, more generally just explicitly enumerated), to create a programming language such that every program in the language computes a function in $\operatorname{PA}(A)$ and every such function has a program in the language. The language simply has primitives for all the functions in $A$ and for the basic primitive recursive functions, along with operators for composition and primitive recursion.

Therefore, one answer to "I'm curious about how "much" we can compute with a formalism that guarantees halting." is "For any total computable function there is such a formalism" and more generally this is true for any effective sequence of total computable functions.

The main thing that such a system cannot have is a universal function, provided the system has some basic closure properties.

Addendum

Since several people pointed out the same thing, I may as well add some value to the answer by including the standard proof of my remark about universal functions. A universal two-place function, for some system, is a function $g(i,k)$ such that for every one-place function $f(k)$ in the system there is some natural number $e$ with $\lambda k .f(k) = \lambda k. g(e,k)$. Suppose that $g$ is such a function; define a function $h$ as $h(k) = g(k,k) + 1$. Then $h$ has some index $e$. Thus $g(e,e) = h(e)$ by the definition of $g$ and $e$, and $h(e) = g(e,e) + 1$ by construction of $h$. This is impossible, so any system of total functions that allows me to form the functions like $h$ cannot have a universal function $g$.

In particular, for any class of functions $A$ and any function $g(j,i)$ in $\operatorname{PA}(A)$, the function $h(n) = g(n,n)+1$ is in $\operatorname{PR}(A)$. So this class will not have a universal function provided that every function in $A$ is total. Of course if you let $A$ be the set of all partial computable functions then $\operatorname{PR}(A)$ is also the set of all partial computable functions and so it does contain a universal function (which is not total).

From this point of view, the limitation is not on whether particular computable functions can be included; the limitation is on the internal structure of any particular effective class of functions.

You might look up fast-growing hierarchies.