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.]

2more comments