Double recursion

In recursive function theory, double recursion is an extension of primitive recursion which allows the definition of non-primitive recursive functions like the Ackermann function.

Raphael M. Robinson called functions of two natural number variables G(n, x) double recursive with respect to given functions, if

• G(0, x) is a given function of x.
• G(n + 1, 0) is obtained by substitution from the function G(n, ·) and given functions.
• G(n + 1, x + 1) is obtained by substitution from G(n + 1, x), the function G(n, ·) and given functions.<ref>{{cite journal | author=Raphael M. Robinson | title=Recursion and Double Recursion | journal=Bulletin of the American Mathematical Society | year=1948 | volume=54 | pages=987–93 | url=http://pro