# Is there a name for the class of functions whose totality can be proved using “Ackermann-like” reasoning?

Primitive recursion is recursion where totality can be proved because there is a single natural number parameter that strictly decreases in every recursive call. Put another way, the recursion terminates because there is a parameter with order type $\omega$ that strictly decreases under the ordering in each call.

The Ackermann function is the standard example of a recursively-defined function that is not primitive recursive. Its totality can be proven by arguing as follows: at each recursive call, either the first parameter decreases, or the first parameter stays the same and the second parameter decreases. At the calls where the first parameter decreases, the value of the second parameter might blow up by a huge amount, but this is OK because the whole parameter tuple is still decreasing under the lexicographical order. Since the lexicographical order is a well-ordering, the recursion must terminate. We are effectively using the fact that the parameter tuple is ordered like the ordinal $\omega^2$ and arguing that the recursion terminates because that ordinal exists and is well-ordered.

We can consider the class of functions that is defined like the primitive recursive functions, but instead of being closed under primitive recursion, it is closed under this stronger form of recursion using lexicographical reasoning on parameter tuples (for any finite number of arguments—basically the ordinals less than $\omega^\omega$). This is a natural class of total recursive functions which includes all of the primitive recursive functions as well as the Ackermann function. Is there a standard name for this class of functions?

• In my limited experience, I have never met this class before. I think it should be a (proper, I guess) subclass of the functions definable through higher-order primitive recursion (e.g. those definable in Agda/Coq), which is a (proper) subclass of the total recursive functions. – chi Apr 4 '18 at 20:13
• @chi If my understanding is correct, the Agda/Coq functions are exactly the functions that are provably terminating if you pick a weak enough type theory as your background logic. So maybe this class is what you get if you pick one of the super-weak set theories from this list? Or a level of some fast-growing hierarchy? I'm not real familiar with this stuff so I'm going by what I can glean off the interwebs. – Aaron Rotenberg Apr 4 '18 at 23:27
• That might be the case, but I am not familiar either with these classes. – chi Apr 5 '18 at 8:45