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 double recursive with respect to given functions, ifG is a given function of x.G is obtained by substitution from the function G and given functions.G is obtained by substitution from G, the function G and given functions.
Robinson goes on to provide a specific double recursive function G = x + 1G = GG = G
where the given functions are primitive recursive, but G is not primitive recursive. In fact, this is precisely the function now known as the Ackermann function.