I have a question for those who are familiar with recursion theory. According to Wikipedia (https://en.wikipedia.org/wiki/Double_recursion),
Raphael M. Robinson called functions of two natural number variables $G(n, x)$ double recursive with respect to the 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 the given functions.
This definition is only for $2$ variables but I think there can be double recursive functions with more variables. So I made my own definition of a multivariable double recursive function using the formula, and I would like to know if I am expressing the wikipedia text properly, if there is a better definition, and the fundamental point of what makes a double recursive function "double" (for the sake of defining higher-order recursive functions in the future).
Here is the definition I have made.
(1) Constant functions are double recursive functions.
(2) The latter function is a double recursive function.
(3) Projective functions are double recursive functions.
(4) For a $k$-variable double recursive function $f$ and $m$-variable double recursive functions $g_1$,..., $g_k$, a $m$-variable function $h$ defined by
$h(x_1, ..., ... , x_m) = f(g_1(x_1, ... , x_m), ... , g_k(x_1, ... , x_m))$
is a double recursive function.
(5) For a $k$-variable double recursive function $f$ and a $(k + 2)$-variable double recursive function $g$, a $(k+1)$-variable function $h$ defined by
$h(0, x_1, ..., x_k) = f(x_1, ..., x_k)$ and
$h(n+1, x_1, ..., x_k) = g(h(n, x_1, ..., x_k), n, x_1, ..., x_k)$
is a double recursive function.
(6) For $(k+1)$-variable double recursive functions $f$ and $h$, a $(k+2)$-variable function $g$, and a $(k+3)$-variable double recursive function $α$, a $(k+2)$-variavle function $j$ defined by
$j(0, m, x_1, ..., x_k)=f(m, x_1, ..., x_k)$,
$j(n+1, 0, x_1, ..., x_k)=g(j(n, h(n, x_1, ..., x_k), x_1, ..., x_k), n, x_1, ..., x_k)$, and
$j(n+1, m+1, x_1, ..., x_k)=α(j(n, j(n+1, m, x_1, ..., x_k), x_1, ..., x_k), n, m, x_1, ..., x_k)$
is a double recursive function.
(7) Only those determined by (1) — (6) are double recursive functions.