2 edited tags
1

# Between mu- and primitive recursion

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.