Primitive recursion with varying parameters

Question

Suppose $g\colon \mathbb{N}^k \to \mathbb{N}$, $v_1,\ldots,v_r\colon \mathbb{N}^k \to \mathbb{N}^k$ and $h\colon \mathbb{N}^{k+r+1} \to \mathbb{N}$ are all primitive recursive, and define $f\colon \mathbb{N}^{k+1} \to \mathbb{N}$ by $$ \begin{aligned} f(0,\underline{x}) &= g(\underline{x}) \cr f(n+1,\underline{x}) &= h(n, \underline{x}, f(n,v_1(\underline{x})),\ldots, f(n,v_r(\underline{x}))) \end{aligned} $$ (note that for $r=1$ and $v_1$ the identity function, this is precisely a definition by primitive recursion).

If I am not mistaken, $f$ is then primitive recursive as well¹.

Questions:

• Does this form of recursion have a name²? (Or if not exactly this, then a more general form which includes the one above and which is satisfied by p.r. functions.)

• Is there some standard reference for this fact?

• Is there a proof that isn't horribly tedious (contra the one sketched in footnote 1 below), based on the standard textbook definition of p.r. functions (e.g., as found in Wikipedia)?

1. Sketch of proof: from $n$ and $x$ we can primitive recursively construct some encoding of the full $r$-ary tree of depth $n$ of values $v_{i_1}(v_{i_2}(\cdots(v_{i_s}(\underline{x}))\cdots))$, since this is requires at most exponentially many computations, and then evaluate $f(i,\underline{y})$ on each node $\underline{y}$ at depth $n-i$ in this tree.

2. Note: I thought it was “course-of-values” recursion, but “course-of-values” actually refers to the so-to-speak dual case when $f(n,\underline{x})$ refers to $f(i,\underline{x})$ for several different $i<n$ but for the same $\underline{x}$ rather than, as is the case here, $f(n-1,\underline{v})$ for several different $\underline{v}$.

Edit+comment: answering a comment by Saroupille, the $v_i$ take values in $\mathbb{N}^k$ (rather than, as I had initially written, in $\mathbb{N}$). Maybe I should also have allowed $v_i$ bo take $n$ as input in the second formula, but I guess that would be easy to fix anyway. Probably more subtle, and maybe also desirable, is the case where we allow $v_i$ to take expressions in $f(n,\ldots)$ as input — but let me refrain from editing the question any further.

Answer 1

I would call the scheme you have written unnested type-1 primitive recursion.

First, type-1 primitive recursion allows us to abstract number arguments to define a type-1 function by induction on the (0,succ)-representation of numbers. Referring to your example above we may define $f(n): \mathbb N^k \to \mathbb N$ (think of this as $\lambda \underline x . f(n,\underline x)$) by:

• $f(0) = g$
• $f(n+1) = \lambda \underline x . h(n,\underline x, f(n)(\underline{v}_1(\underline x)),\dots,f(n)(\underline {v}_r(\underline x))$.

Higher-type primitive recursion is standard terminology in higher-order computability and proof theory (see e.g. Avigad-Feferman chapter on Dialectica). A priori, type-1 primitive recursion is strictly more powerful than usual (type-0) primitive recursion, as it allows for the definition of the Ackermann-Péter function. However in your scheme, you have no applications of the recursive call to terms including itself. In spirit this is what underlies Kleene's predicative higher primitive recursion (outlined in Section 5.1 of Avigad-Feferman), however you are also allowing multiple instances of the recursive call with compositions during recursion (terminology e.g. from Section 3.4.3 Bellantoni's thesis). I have seen this called unnested recursion (as opposed to nested recursion such as the definition of Ackermann-Péter function). I am not sure how standard this is but, for instance, I have used the terminology in my own papers (e.g. Section 4 of this), and it has seemed non-controversial when communicating about the scheme. With this terminology, by the way, there is no reason not to allow $n$ as a further argument to each $v_i$.

I do not know a proof that primitive recursive functions (PRF) are closed under your scheme other than the one you describe, which seems standard. Note that some simplification could be made by simply prescribing a monotone bounding function (mbf) that is in PRF, as PRF is closed under bounded search. E.g., now assuming $k=1$ for simplicity as Emil suggests, if $b_g,b_h,b_{v_i}$ are mbfs for $g,h,v_i$ respectively, then $b_v = \max (b_{v_1}, \dots, b_{v_r})$ is a mbf for all $v_i$. Now the function you defined is bounded by the mbf $b_f$ given by:

• $b_f(0 , \underline x) = b_g (\underline x)$
• $b_f(n+1,\underline x) = b_h (n,\underline x , b_f (n, b_v (\underline x)), \dots, b_f (n,b_v (\underline x)))$

This is an instance of primitive recursion with (single) composition during recursion (cf. Bellantoni). Closure of PRF under this scheme is well-known. E.g. a similar argument is used for Lemma 2.4.4 of Avigad-Feferman, where the function $e$ carries out the sort of 'pre-computation' you describe in your proof sketch.