<p>If I understand correctly, the primitive recursive functionals defined in the Wikipedia page linked in the question coincide with Gödel's system T, which is well-known to correspond to the class of functions whose totality may be proved in first-order Peano arithmetic.  I think that the <a href="https://www.wikiwand.com/en/Dialectica_interpretation" rel="noreferrer">Wikipedia page on Gödel's Dialectica interpretation</a> contains some relevant pointers, but I'll give a quick definition for the sake of self-containedness.</p>
<p>A function <span class="math-container">$\mathbb N^n\to\mathbb N$</span> is <em>provably total in <span class="math-container">$\mathsf{PA}_1$</span></em> (first-order Peano arithmetic) if its graph is of the form
<span class="math-container">$$\{(x_1,\ldots,x_n,y)\in\mathbb N^{n+1}\mathrel | \varphi(x_1,\ldots,x_n,y)\}$$</span>
where <span class="math-container">$\varphi$</span> is an arithmetic formula with <span class="math-container">$n+1$</span> free variables such that</p>
<ul>
<li><span class="math-container">$\mathsf{PA}_1\vdash\forall x_1\ldots\forall x_n\forall y.\forall y'.\varphi(x_1,\ldots,x_n,y)\land\varphi(x_1,\ldots,x_n,y')\Rightarrow y=y'$</span> (functionality);</li>
<li><span class="math-container">$\mathsf{PA_1}\vdash\forall x_1\ldots\forall x_n.\exists y.\varphi(x_1,\ldots,x_n,y)$</span> (totality).</li>
</ul>
<p>(The second part is the non-trivial one, that's why one just says &quot;provably total&quot;). Notice that, by standard proof-theoretic results (due to Gödel and Friedman), replacing <span class="math-container">$\mathsf{PA}_1$</span> with <span class="math-container">$\mathsf{HA}_1$</span> (Heyiting arithmetic, meaning <em>intuitionistic</em> Peano arithmetic) defines the same class. In other words, non-constructive reasoning does not add anything in terms of functions you may prove total in Peano arithmetic.  This is good to know in categorical contexts, where sometimes one may care about proofs being constructive.</p>
<p>I don't think this class has a standard name.  People usally just say &quot;functions definable in system T&quot;. &quot;Higher-order primitive recursive functions&quot; is another legitimate name.</p>
<p>It's a huge class: smaller than the class of total recursive functions, of course, but way bigger than primitive recursive.  It is not immediate to construct examples of total recursive functions which are not in this class (for example, the Ackermann function is easily seen to be in this class, see the last paragraph of <a href="https://www.wikiwand.com/en/Ackermann_function#/Definition_and_properties" rel="noreferrer">the section &quot;Definition and properties&quot; of the related Wikipedia article</a>).  Self-referential definitions work of course, such as the &quot;universal higher-order primitive recursive intepreter&quot;: the function <span class="math-container">$u(m,n)$</span> taking the code <span class="math-container">$m$</span> of a higher-order primitive recursive function of arity <span class="math-container">$1$</span> (a term <span class="math-container">$t_m:\mathsf{Nat}\to\mathsf{Nat}$</span> of system T) and an integer <span class="math-container">$n$</span> and returning <span class="math-container">$t_m(n)$</span>, is total recursive (just normalize the term in system T) but obviously not itself higher-order primitive recursive (for &quot;Gödelian&quot; reasons).  A non-self-referential example (not immediately, at least) is given by <a href="https://www.wikiwand.com/en/Goodstein%27s_theorem" rel="noreferrer">Goodstein's theorem</a>: the function <span class="math-container">$G(n)$</span> which returns the smallest <span class="math-container">$m$</span> such that the <span class="math-container">$m$</span>-th term of the <span class="math-container">$n$</span>-th Goodstein sequence is zero is total recursive but not higher-order primitive recursive.</p>

CC BY-SA 4.0
2021-08-21T14:18:00.690Z
I think that we're talking about the same thing, yes. Which complexity class is that? [WP](https://en.wikipedia.org/wiki/Dialectica_interpretation) doesn't list it.
Corbin
CC BY-SA 4.0
2021-08-22T08:44:10.850Z
I don't think there's a standard name.  I expanded my answer to include some more information, including an explicit definition.
Damiano Mazza
CC BY-SA 4.0
2021-08-22T08:53:52.933Z
A recursive function $\mathbb N^k\to\mathbb N$ is provably total in PA iff it is $\alpha$-recursive for some $\alpha<\varepsilon_0$; in other words (for $k=1$), iff it is bounded by a function $f_\alpha$ of the Wainer hierarchy for some $\alpha<\varepsilon_0$ (see https://en.wikipedia.org/wiki/Fast-growing_hierarchy).
Emil Jeřábek
CC BY-SA 4.0
2021-08-22T15:35:56.823Z
I appreciate the completeness of this answer. Thank you.
Corbin
CC BY-SA 4.0
2021-08-21T05:13:56.817Z
2021-08-22T12:30:35.110Z
2021-08-22T12:30:35.110Z
Damiano Mazza
<p>Short and sweet: The complexity class of primitive recursive functions (<a href="https://en.wikipedia.org/wiki/Primitive_recursive_function" rel="noreferrer">WP</a>) is <strong>PR</strong> (<a href="https://en.wikipedia.org/wiki/PR_(complexity)" rel="noreferrer">WP</a>, <a href="https://complexityzoo.net/Complexity_Zoo:P#pr" rel="noreferrer">Zoo</a>). What's the complexity class of higher-order primitive recursion (<a href="https://en.wikipedia.org/wiki/Primitive_recursive_functional" rel="noreferrer">WP</a>)?</p>
<p>The motivating context is simply that the primitive recursion provided by an NNO (<a href="https://en.wikipedia.org/wiki/Natural_numbers_object" rel="noreferrer">WP</a>, <a href="https://ncatlab.org/nlab/show/natural+numbers+object" rel="noreferrer">nLab</a>) is of the second, richer, &quot;functional&quot; kind. Further category-theoretic motivation comes from <a href="https://golem.ph.utexas.edu/category/2019/05/polyadic_boolean_algebras.html" rel="noreferrer">a n-café discussion on Boolean algebras</a>.</p>

CC BY-SA 4.0
2021-08-22T12:59:58.400Z
I just read the linked n-café discussion (sorry I answered before doing that!).  Everything I say in my answer is already mentioned in that thread (there's even Cody making exactly the same remark as Emil Jeřábek about the relationship with the fast-growing hierarchy!).  At this point, I don't know how useful my answer is and I'm afraid I don't understand anymore what it is that you would like to know exactly...
Damiano Mazza
CC BY-SA 4.0
2021-08-22T15:35:22.580Z
A concrete example: There are public lists of languages, each annotated with complexity classes which either they contain or contain them. When a language can express higher-order primitive recursion but isn't trivially Turing-complete, then it would be nice to know how to communicate its complexity classes to others.
Corbin
CC BY-SA 4.0
2021-08-23T14:51:03.057Z
I accepted the given answer as complete, but for posterity, the answer here in late 2021 is that this class is not yet identified or studied by computational complexity theorists. It sits somewhere between PR and R.
Corbin
<complexity-classes><computability>
What is the complexity class of higher-order primitive recursion?
Corbin
# What is the complexity class of higher-order primitive recursion?

(Asked by: username_0 on 2021-08-20)

Short and sweet: The complexity class of primitive recursive functions ([WP](https://en.wikipedia.org/wiki/Primitive_recursive_function)) is **PR** ([WP](https://en.wikipedia.org/wiki/PR_(complexity)), [Zoo](https://complexityzoo.net/Complexity_Zoo:P#pr)). What's the complexity class of higher-order primitive recursion ([WP](https://en.wikipedia.org/wiki/Primitive_recursive_functional))?

The motivating context is simply that the primitive recursion provided by an NNO ([WP](https://en.wikipedia.org/wiki/Natural_numbers_object), [nLab](https://ncatlab.org/nlab/show/natural+numbers+object)) is of the second, richer, "functional" kind. Further category-theoretic motivation comes from [a n-café discussion on Boolean algebras](https://golem.ph.utexas.edu/category/2019/05/polyadic_boolean_algebras.html).

**Tags:** complexity-classes, computability

> **Comments:**
> **username_1**: I just read the linked n-café discussion (sorry I answered before doing that!).  Everything I say in my answer is already mentioned in that thread (there's even Cody making exactly the same remark as username_2 about the relationship with the fast-growing hierarchy!).  At this point, I don't know how useful my answer is and I'm afraid I don't understand anymore what it is that you would like to know exactly...  
> **username_0**: A concrete example: There are public lists of languages, each annotated with complexity classes which either they contain or contain them. When a language can express higher-order primitive recursion but isn't trivially Turing-complete, then it would be nice to know how to communicate its complexity classes to others.  
> **username_0**: I accepted the given answer as complete, but for posterity, the answer here in late 2021 is that this class is not yet identified or studied by computational complexity theorists. It sits somewhere between PR and R.  

---

## 1 answers

### Answer by username_1 on 2021-08-21. Score: 9 | Accepted answer

If I understand correctly, the primitive recursive functionals defined in the Wikipedia page linked in the question coincide with Gödel's system T, which is well-known to correspond to the class of functions whose totality may be proved in first-order Peano arithmetic. I think that the [Wikipedia page on Gödel's Dialectica interpretation](https://www.wikiwand.com/en/Dialectica_interpretation) contains some relevant pointers, but I'll give a quick definition for the sake of self-containedness.

A function $\mathbb N^n\to\mathbb N$ is *provably total in $\mathsf{PA}\_1$* (first-order Peano arithmetic) if its graph is of the form
$$\{(x\_1,\ldots,x\_n,y)\in\mathbb N^{n+1}\mathrel | \varphi(x\_1,\ldots,x\_n,y)\}$$
where $\varphi$ is an arithmetic formula with $n+1$ free variables such that

* $\mathsf{PA}\_1\vdash\forall x\_1\ldots\forall x\_n\forall y.\forall y'.\varphi(x\_1,\ldots,x\_n,y)\land\varphi(x\_1,\ldots,x\_n,y')\Rightarrow y=y'$ (functionality);
* $\mathsf{PA\_1}\vdash\forall x\_1\ldots\forall x\_n.\exists y.\varphi(x\_1,\ldots,x\_n,y)$ (totality).

(The second part is the non-trivial one, that's why one just says "provably total"). Notice that, by standard proof-theoretic results (due to Gödel and Friedman), replacing $\mathsf{PA}\_1$ with $\mathsf{HA}\_1$ (Heyiting arithmetic, meaning *intuitionistic* Peano arithmetic) defines the same class. In other words, non-constructive reasoning does not add anything in terms of functions you may prove total in Peano arithmetic. This is good to know in categorical contexts, where sometimes one may care about proofs being constructive.

I don't think this class has a standard name. People usally just say "functions definable in system T". "Higher-order primitive recursive functions" is another legitimate name.

It's a huge class: smaller than the class of total recursive functions, of course, but way bigger than primitive recursive. It is not immediate to construct examples of total recursive functions which are not in this class (for example, the Ackermann function is easily seen to be in this class, see the last paragraph of [the section "Definition and properties" of the related Wikipedia article](https://www.wikiwand.com/en/Ackermann_function#/Definition_and_properties)). Self-referential definitions work of course, such as the "universal higher-order primitive recursive intepreter": the function $u(m,n)$ taking the code $m$ of a higher-order primitive recursive function of arity $1$ (a term $t\_m:\mathsf{Nat}\to\mathsf{Nat}$ of system T) and an integer $n$ and returning $t\_m(n)$, is total recursive (just normalize the term in system T) but obviously not itself higher-order primitive recursive (for "Gödelian" reasons). A non-self-referential example (not immediately, at least) is given by [Goodstein's theorem](https://www.wikiwand.com/en/Goodstein%27s_theorem): the function $G(n)$ which returns the smallest $m$ such that the $m$-th term of the $n$-th Goodstein sequence is zero is total recursive but not higher-order primitive recursive.

> **Comments:**
> **username_0**: I think that we're talking about the same thing, yes. Which complexity class is that? [WP](https://en.wikipedia.org/wiki/Dialectica_interpretation) doesn't list it.  
> **username_1**: I don't think there's a standard name.  I expanded my answer to include some more information, including an explicit definition.  
> **username_2**: A recursive function $\mathbb N^k\to\mathbb N$ is provably total in PA iff it is $\alpha$-recursive for some $\alpha<\varepsilon_0$; in other words (for $k=1$), iff it is bounded by a function $f_\alpha$ of the Wainer hierarchy for some $\alpha<\varepsilon_0$ (see https://en.wikipedia.org/wiki/Fast-growing_hierarchy).  
> **username_0**: I appreciate the completeness of this answer. Thank you.  

---

