It is well known that primitive recursion is not powerful enough
to express all functions, Ackermann function being probably the best
known example.
Now, in the logic courses (that I have had look at) one always proceeded from primitive recursion to mu-recursion. In computer science terms this basicly means we are jumping from a formalism where programs are quaranteed to halt to a Turing-complete formalism where halting is a non-computable property i.e. we can't say for every program if it will eventually halt.
I got curious if there is any hierarchy between primitive recursion and
mu-recursion. After a while I found a programming language called Charity. In Charity (according to Wikipedia)
all programs are quaranteed to stop, thus its not Turing-complete, but,
on the other hand, it is expressive enough to implement Ackermann function.
This suggests there is at least one level between mu-recursion and primitive recursion.
My question is: does there exists any other halt-for-sure formalisms that are more expressive than primitive recursion? Or, even better, does there exist some known hierarchies between mu-recursive and primitive recursive functions? I'm curious about how "much" we can compute with a formalism that guarantees halting.
Best Answer
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).