7
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jan 18 '18 at 14:33
  • $\begingroup$ @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). $\endgroup$ – user27574 Jan 22 '18 at 7:58
  • $\begingroup$ 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)? $\endgroup$ – Andrej Bauer Jan 22 '18 at 10:48
  • $\begingroup$ @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. $\endgroup$ – user27574 Jan 22 '18 at 11:06
  • $\begingroup$ Your examples $I$ and $g$ are still in the System T fragment. $\endgroup$ – Andrej Bauer Jan 22 '18 at 14:27
1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy