I'm trying to extend the class of primitive recursive functions by extending the recursion schema over higher types.

We usually define the class of primitive recursive functions by using zero function, successor function, projection function, composition and primitive recursion. Now, as I have learnt, we can define the same class replacing the primitive recursion with function iteration (this is in Odifreddi's classical recursion theory). Here the iteration is the operation that defines $h(n,x) = t^{(n)}(x)$ where $t$ is p.r. function and resulting $h$ is p.r.

I got a pointer to this work which defines an extension of primitive recursion and iteration over higher types in simply typed lambda calculus. This seems to follow Gödel's work on System T. In the paper (as I understand it), the iteration schema for type $\tau$ is defined as

$$ ITER_\tau(A,B,0) = A\\ ITER_\tau(A,B,n+1) = B(ITER_\tau(A,B,n)),\\ $$

where $A$ is of type $\tau$ and $B$ of type $\tau\to\tau$. If we study the case $\tau=\mathbb{N}$ we get the normal funtion iteration operation. For example the previous $h$ can be defined $$ h(n,x) = \begin{cases} ITER_\mathbb{N}(x,t,0) &= x\\ ITER_\mathbb{N}(x,t,n+1) &= t(ITER_\mathbb{N}(x,t,n)). \end{cases} $$

I tried to use the iteration $ITER_{\mathbb{N}\to\mathbb{N}}$ to define higher order functionals. I wanted to start with Ackermann function, that can be defined with higher types. First, we define the functional $g:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}^{\mathbb{N}}$ such that $g(f)(0) = f(1)$ and $g(f)(n+1)=f(g(f)(n))$, where $f\in\mathbb{N}^\mathbb{N}$, after which we can define $A(0) = S$ (successor) and $A(m+1)=g(A(m))$ where $A\in\mathbb{N}^\mathbb{N}$ (see this question).

Initial idea was to define $g$ and $A(m)$ with the iteration schema, but to be able to define them with the iteration I need to be able to define the parameter $B$, but it seems I need some "primitives" of higher type to be able to construct anything of type $\mathbb{N}^\mathbb{N}\to\mathbb{N}^\mathbb{N}$...

So the question is a bit wide; how should I proceed from here? Is there some standard set of "primitives" I should define for each $\tau$ and proceed with? Is there any prior work on applying the higher order schemas in defining pure number-theoretic functions or classes of them?

I'm targeting for a subrecursive hierarchy of number-theoretic functions below $f_{\epsilon_0}$.

[This goes cross some borders, thus tagging was difficult.]

  • 1
    $\begingroup$ This is a bit beyond my area of expertise. But it seems to me that you just need to take system $T$ as the language of description of higher-order functionals. There are at least two ways how one could define system $T$: 1. using $\lambda$-abstraction, 2. using combinators. From your question it seems to me that you want to have primitive functions (rather than $\lambda$-terms). Hence you should check the formulation of system $T$ with combinators. Unfortunately, I don't know what is a good reference about that. $\endgroup$ Commented Aug 2, 2022 at 14:50
  • $\begingroup$ @FedorPakhomov Yes, I'm targeting "pure number-theoretical" setup here, thus the lambda abstraction is somewhat out of scope. The core idea is to reach a hierarchy like that of Grzegorczyk's within the class PR, but within the class of functions provable total in PA. I remember reading about the combinators earlier, I need to revisit that. Thanks for the pointer. $\endgroup$
    – Jii
    Commented Aug 2, 2022 at 15:02
  • $\begingroup$ Of course, there are two well-known descriptions of $\mathsf{PA}$-provable total computable functions on naturals as 1. functions given by a system $T$ term of the type $\mathbb{N}\to\mathbb{N}$ and 2. functions that are elementary-recursive relative to some $F_\alpha$, where $\alpha<\varepsilon_0$. The combination of this two results immediately implies that each $F_\alpha$, $\alpha<\varepsilon_0$ could be written as a system $T$ term. I don't know whether this terms have been already explicitly by anyone before, although wouldn't be surprised if it would be the case. $\endgroup$ Commented Aug 2, 2022 at 15:23
  • $\begingroup$ However, the other direction, i.e. assignment of ordinals to $T$-terms was studied. See for example this paper by Andreas Weiermann cambridge.org/core/journals/journal-of-symbolic-logic/article/… $\endgroup$ Commented Aug 2, 2022 at 15:25
  • $\begingroup$ @FedorPakhomov Yep, the existence itself is clear. We could, for example, use the fast-growing hierarchy and define mentioned subrecursive hierarchy as closures over the PR and a chosen $f_\alpha$ for $\alpha<\epsilon_0$. However, I'm interested if we can define a hierarchy without any notion to ordinals, in (kind of) more "constructive" way just using the higher order recursion schema, but I have not been able to locate any references (only those around lambda calculus that employ different tools). $\endgroup$
    – Jii
    Commented Aug 2, 2022 at 17:41

1 Answer 1


a constructive (from intuitionistic point of view) of higher order calculus of functionals and relations is at


  • $\begingroup$ Very interesting pointer, thank you. It seems you have worked on the same core problem but at different tool set. I need to study this more deeply. $\endgroup$
    – Jii
    Commented Sep 25, 2023 at 10:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.