Gödel defines in his System T primitive recursion over higher types. I found notes from Girard where he explains the implementation of System T on top of simply typed lambda calculus. On page 50 he mentions that once we use more types in the recursor we gain more expressive power with the system.

I don't understand how exactly this happens. Is it possible to come up with sort of Ackermann hierarchy with the higher order primitive recursion, i.e. a hierarchy of faster and faster growing functions where each function is expressible in System T but the diagonal is not? I guess so, but the construction does not seem evident to me and I would be interested seeing how one would construct it, or receive pointers to literature.

I'm after something concrete. I'm aware of the general diagonal argument that proves existence of a function not in T, but I would like to see how one would really "step up in the type hierarchy".

  • 2
    That's a nice question. I bet the hierarchy follows the rank of the type at which recursion happens. It's almost worth writing up. I'll come back here if I have the time to do it. – Andrej Bauer Jan 18 at 14:33
  • @AndrejBauer I have been thinking about this and I would guess that one could construct new iterators with higher levels on the type hierarchy and implement fast-growing hierarchy under $f_{\epsilon_0}$. Perhaps type levels correspond (with some offset) to tower height of exponents on $\omega^{\omega^{...}}$ on the hierarchy, but I have not been able to pull a proof off (..yet). – user27574 Jan 22 at 7:58
  • By the way, how do you envision the next level of recursion after the primitive recursion? If it is at a higher type, then would you alive general recursion (so that we get non-termination), or some sort of recursion that still keeps things terminating (in which case, what would it be)? – Andrej Bauer Jan 22 at 10:48
  • @AndrejBauer I believe this could be approached defining iterators. (I'm using number-theoretic functions instead of lambda-calculus.) For example $I(f,0)=f(1)$, $I(f,n+1)=f(I(f,n))$ and defining $g(0)=S$, $g(n)=I(g(n-1))$ (S is successor) where $g:\mathbb{N}\times \mathbb{N}^\mathbb{N}\to\mathbb{N}^\mathbb{N}$, $f:\mathbb{N}\to\mathbb{N}$. Now $h(n)=g(n)(n)$ should comparable to $f_\omega$. Getting to $f_{\omega^n}$ for $n\in\mathbb{N}$ seems doable, but $f_{\omega^\omega}$ seems challenging. After getting to $f_{\omega^\omega}$ I would expect things to clear up. – user27574 Jan 22 at 11:06
  • Your examples $I$ and $g$ are still in the System T fragment. – Andrej Bauer Jan 22 at 14:27

(This is a very partial answer, only addressing the first point, and not the main question about the hierarchy.)

I don't have a proof to point out to you, but the idea is that a single first-order recursor on naturals such as $$ \begin{array}{l} rec: (nat \to nat) \to nat \to nat \to nat \\ rec\ f\; z\; n = f(f(\ldots f(z))) \qquad \mbox{($n$ times $f$)} \end{array} $$

would be much less powerful than having the full (primitive) recursion scheme

$$ rec_U: (U \to U) \to U \to nat \to U $$

since the latter roughly resembles a polymorphic term in System F, which can be used at many types $U$.

Indeed, the basic $rec$ only gives us access to the first order primitive recursion scheme, as we can find in a computability / recursion theory book. With only that, we know functions like Ackermann's are not definable. (Well, this is not that obvious since here we also have higher-order lambdas, it's only recursion which is constrained. But the point should stand anyway, I think.)

With the $rec_U$ scheme, instead, we can choose $U = nat \to nat$, which allows us to define Ackermann's function, as Girard shows in the book mentioned by the OP. Hence, the scheme is strictly more powerful.

This is an interesting question, whose answer is absolutely not trivial.

I'll give the short answer first: There is a hierarchy of systems, call them $T_k$, where the only recursors allowed are $\mathrm{rec}_U$ with the order of $U\leq k$, where the order of a type is defined as:

$$ \mathrm{ord}(\mathrm{nat})=0$$ $$ \mathrm{ord}(U\rightarrow V)= \max(\mathrm{ord}(V),\mathrm{ord}(U)+1)$$

Then the theorem is:

Theorem: for every $k$, there is a term $t_k:\mathrm{nat}\rightarrow\mathrm{nat}$, such that

  • $T_{k}\vdash t_k:\mathrm{nat}\rightarrow\mathrm{nat}$

  • $T_{k-1}\not\vdash t_k:\mathrm{nat}\rightarrow\mathrm{nat}$

$t_k$ grows faster (as a function from $\mathbb{N}\rightarrow\mathbb{N}$) than any function definable in $T_l$, with $l<k$.

Note that $T=\bigcup_k T_k$.

As a first step, it's probably useful to note that the Ackermann function can be defined like this (as hinted by chi's answer): $$ \mathrm{ack}(n,m) = \mathrm{rec}_{\mathrm{nat}\rightarrow\mathrm{nat}}(\lambda f.\mathrm{rec}_{\mathrm{nat}}\ f\ 0\ m)\ (\lambda p.S\ p)\ n$$ modulo a mistake on my part.

This indeed suggests that $\mathrm{rec}_{\mathrm{nat}\rightarrow\mathrm{nat}}$ had additional "power".


But how do we go all the way up the tower to arbitrary $T_k$?

The trick is to consider a triple correspondence between:

1) Ordinals below $\varepsilon_0$

2) Fragments of $\mathrm{HA}_k$ of Heyting arithmetic where induction is restricted to statements with less than $k$ quantifier alternations.

3) Functions definable in $T_k$

For each ordinal $\lambda_k=\omega^{\omega^{{\dots}^\omega}}$ where the tower is of height $k$, it is possible to consider a proof in Heyting arithmetic that such an ordinal is well-founded, and to extract from it a term $t_k$ typeable in system $T_k$ which corresponds to the function $g_{\lambda_k}$ in the Grzegorczyk hierarchy.

Such a term cannot be well-typed in $T_{k-1}$ due to the correspondence outlined above, and the fact that $\mathrm{HA}_{k-1}$ does not prove the well-foundedness of $\lambda_k$.

Lies and references:

The correspondence between $T_k$, $\mathrm{HA_k}$ and $\lambda_k$ is not quite as clean as I suggested, there should actually be $k$, $k'$ and $k''$, each related by some concrete constant.

An explicit construction for the $t_k$ along the path outlined above is given by Ulrich Berger in Program Extraction from Gentzen’s Proof of Transfinite Induction up to $\varepsilon_0$

I'm afraid I don't have a reference for the triple correspondence better than Proofs and Types, though I would be very happy to hear of one.

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.