What is the complexity class of higher-order primitive recursion?

Short and sweet: The complexity class of primitive recursive functions (WP) is PR (WP, Zoo). What's the complexity class of higher-order primitive recursion (WP)?

The motivating context is simply that the primitive recursion provided by an NNO (WP, nLab) is of the second, richer, "functional" kind. Further category-theoretic motivation comes from a n-café discussion on Boolean algebras.

• 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... Aug 22 at 12:59
• 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. Aug 22 at 15:35
• 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. Aug 23 at 14:51

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 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). 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: 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.

• I think that we're talking about the same thing, yes. Which complexity class is that? WP doesn't list it. Aug 21 at 14:18
• I don't think there's a standard name. I expanded my answer to include some more information, including an explicit definition. Aug 22 at 8:44
• 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 en.wikipedia.org/wiki/Fast-growing_hierarchy). Aug 22 at 8:53
• I appreciate the completeness of this answer. Thank you. Aug 22 at 15:35