<p>I would call the scheme you have written <strong>unnested type-1 primitive recursion</strong>.</p>
<p>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 <span class="math-container">$f(n): \mathbb N^k \to \mathbb N$</span> (think of this as <span class="math-container">$\lambda \underline x . f(n,\underline x)$</span>) by:</p>
<ul>
<li><span class="math-container">$f(0) = g$</span></li>
<li><span class="math-container">$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))$</span>.</li>
</ul>
<p>Higher-type primitive recursion is standard terminology in higher-order computability and proof theory (see e.g. <a href="https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf" rel="nofollow noreferrer">Avigad-Feferman chapter on Dialectica</a>). A priori, type-1 primitive recursion is strictly more powerful than usual (type-0) primitive recursion, as it allows for the definition of the <a href="https://en.m.wikipedia.org/wiki/Ackermann_function" rel="nofollow noreferrer">Ackermann-Péter function</a>. However in your scheme, you have no applications of the recursive call to terms including itself. In spirit this is what underlies Kleene's <em>predicative</em> higher primitive recursion (outlined in Section 5.1 of <a href="https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf" rel="nofollow noreferrer">Avigad-Feferman</a>), however you are also allowing multiple instances of the recursive call with <em>compositions during recursion</em> (terminology e.g. from Section 3.4.3 <a href="https://citeseerx.ist.psu.edu/document?repid=rep1&amp;type=pdf&amp;doi=fca3985d1321ab7bb851fdae658a92508feaa500" rel="nofollow noreferrer">Bellantoni's thesis</a>). I have seen this called <strong>unnested recursion</strong> (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 <a href="https://arxiv.org/abs/2110.01114" rel="nofollow noreferrer">this</a>), and it has seemed non-controversial when communicating about the scheme. With this terminology, by the way, there is no reason not to allow <span class="math-container">$n$</span> as a further argument to each <span class="math-container">$v_i$</span>.</p>
<p>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 <span class="math-container">$k=1$</span> for simplicity as Emil suggests, if <span class="math-container">$b_g,b_h,b_{v_i}$</span> are mbfs for <span class="math-container">$g,h,v_i$</span> respectively, then <span class="math-container">$b_v = \max (b_{v_1}, \dots, b_{v_r})$</span> is a mbf for all <span class="math-container">$v_i$</span>. Now the function you defined is bounded by the mbf <span class="math-container">$b_f$</span> given by:</p>
<ul>
<li><span class="math-container">$b_f(0 , \underline x) = b_g (\underline x)$</span></li>
<li><span class="math-container">$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)))$</span></li>
</ul>
<p>This is an instance of primitive recursion with (single) composition during recursion (cf. <a href="https://citeseerx.ist.psu.edu/document?repid=rep1&amp;type=pdf&amp;doi=fca3985d1321ab7bb851fdae658a92508feaa500" rel="nofollow noreferrer">Bellantoni</a>). Closure of PRF under this scheme is well-known. E.g. a similar argument is used for Lemma 2.4.4 of <a href="https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf" rel="nofollow noreferrer">Avigad-Feferman</a>, where the function <span class="math-container">$e$</span> carries out the sort of 'pre-computation' you describe in your proof sketch.</p>

CC BY-SA 4.0
2023-10-18T12:56:51.483Z
2023-10-18T12:56:51.483Z
Anupam Das
<p>Suppose <span class="math-container">$g\colon \mathbb{N}^k \to \mathbb{N}$</span>, <span class="math-container">$v_1,\ldots,v_r\colon \mathbb{N}^k \to \mathbb{N}^k$</span> and <span class="math-container">$h\colon \mathbb{N}^{k+r+1} \to \mathbb{N}$</span> are all primitive recursive, and define <span class="math-container">$f\colon \mathbb{N}^{k+1} \to \mathbb{N}$</span> by
<span class="math-container">$$
\begin{aligned}
f(0,\underline{x}) &amp;= g(\underline{x}) \cr
f(n+1,\underline{x}) &amp;= h(n, \underline{x}, f(n,v_1(\underline{x})),\ldots, f(n,v_r(\underline{x})))
\end{aligned}
$$</span>
(note that for <span class="math-container">$r=1$</span> and <span class="math-container">$v_1$</span> the identity function, this is precisely a definition by primitive recursion).</p>
<p>If I am not mistaken, <span class="math-container">$f$</span> is then primitive recursive as well¹.</p>
<p><strong>Questions:</strong></p>
<ul>
<li><p>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.)</p>
</li>
<li><p>Is there some standard reference for this fact?</p>
</li>
<li><p>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 <a href="https://en.wikipedia.org/wiki/Primitive_recursive_function" rel="nofollow noreferrer">found in Wikipedia</a>)?</p>
</li>
</ul>
<ol>
<li><p>Sketch of proof: from <span class="math-container">$n$</span> and <span class="math-container">$x$</span> we can primitive recursively construct some encoding of the full <span class="math-container">$r$</span>-ary tree of depth <span class="math-container">$n$</span> of values <span class="math-container">$v_{i_1}(v_{i_2}(\cdots(v_{i_s}(\underline{x}))\cdots))$</span>, since this is requires at most exponentially many computations, and then evaluate <span class="math-container">$f(i,\underline{y})$</span> on each node <span class="math-container">$\underline{y}$</span> at depth <span class="math-container">$n-i$</span> in this tree.</p>
</li>
<li><p>Note: I thought it was “course-of-values” recursion, but “course-of-values” actually refers to the so-to-speak dual case when <span class="math-container">$f(n,\underline{x})$</span> refers to <span class="math-container">$f(i,\underline{x})$</span> for several different <span class="math-container">$i&lt;n$</span> but for the same <span class="math-container">$\underline{x}$</span> rather than, as is the case here, <span class="math-container">$f(n-1,\underline{v})$</span> for several different <span class="math-container">$\underline{v}$</span>.</p>
</li>
</ol>
<p><strong>Edit+comment:</strong> answering a comment by Saroupille, the <span class="math-container">$v_i$</span> take values in <span class="math-container">$\mathbb{N}^k$</span> (rather than, as I had initially written, in <span class="math-container">$\mathbb{N}$</span>).  Maybe I should also have allowed <span class="math-container">$v_i$</span> bo take <span class="math-container">$n$</span> 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 <span class="math-container">$v_i$</span> to take expressions in <span class="math-container">$f(n,\ldots)$</span> as input — but let me refrain from editing the question any further.</p>

CC BY-SA 4.0
2023-10-18T06:43:42.247Z
Is your formula well-typed? Since $f(n,v_1(x))$ is not a natural number but a partial application (except if $k=1$, but I guess this is not the intent).
Saroupille
CC BY-SA 4.0
2023-10-18T07:23:19.393Z
@Saroupille Fixed (I want $v_i$ to take values in $\mathbb{N}^k$).
Gro-Tsen
CC BY-SA 4.0
2023-10-18T11:29:19.877Z
You could underline each $v_i$ to emphasise that it is a tuple of functions.
Anupam Das
CC BY-SA 4.0
2023-10-18T11:40:52.537Z
Using a pairing function, you can just assume $k=1$ without loss of generality.
Emil Jeřábek
CC BY-SA 4.0
2023-10-18T12:03:12.207Z
@EmilJeřábek Agreed, $k$ is very much a red herring here. On the other hand, $r$ is not.
Gro-Tsen
CC BY-SA 4.0
2023-10-18T12:45:34.013Z
Is there a reason you do not allow $n$ to occur as an argument of each $v_i$?
Anupam Das
CC BY-SA 4.0
2023-10-18T18:13:04.560Z
@AnupamDas No, this was merely an oversight. I just happened not to need them in the case where this came up, but I have no good reason not to have an $n$ here.
Gro-Tsen
<computability>
Primitive recursion with varying parameters
Gro-Tsen
# Primitive recursion with varying parameters

(Asked by: username_0 on 2023-10-17)

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](https://en.wikipedia.org/wiki/Primitive_recursive_function))?

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 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 username_1, 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.

**Tags:** computability

> **Comments:**
> **username_1**: Is your formula well-typed? Since $f(n,v_1(x))$ is not a natural number but a partial application (except if $k=1$, but I guess this is not the intent).  
> **username_0**: @username_1 Fixed (I want $v_i$ to take values in $\mathbb{N}^k$).  
> **username_2**: You could underline each $v_i$ to emphasise that it is a tuple of functions.  
> **username_3**: Using a pairing function, you can just assume $k=1$ without loss of generality.  
> **username_0**: @EmilJeřábek Agreed, $k$ is very much a red herring here. On the other hand, $r$ is not.  
> **username_2**: Is there a reason you do not allow $n$ to occur as an argument of each $v_i$?  
> **username_0**: @AnupamDas No, this was merely an oversight. I just happened not to need them in the case where this came up, but I have no good reason not to have an $n$ here.  

---

## 1 answers

### Answer by username_2 on 2023-10-18. Score: 4

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](https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf)). 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](https://en.m.wikipedia.org/wiki/Ackermann_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](https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf)), 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](https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=fca3985d1321ab7bb851fdae658a92508feaa500)). 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](https://arxiv.org/abs/2110.01114)), 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](https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=fca3985d1321ab7bb851fdae658a92508feaa500)). Closure of PRF under this scheme is well-known. E.g. a similar argument is used for Lemma 2.4.4 of [Avigad-Feferman](https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf), where the function $e$ carries out the sort of 'pre-computation' you describe in your proof sketch.


---

