Replacing ordinal recursion with primitive recursion

Ordinal numbers are used to order things, no surprise there. What can be surprising for some is that logicians consider ordinals that go beyond the daily 1st, 2nd,... The ordinal $\omega$ denotes the position right after all "normal" positions 1st, 2nd, 3rd,... And then we can continue with $\omega + 1, \omega + 2,...$ For instance, suppose we order the natural numbers in such a way that we first enumerate all odd numbers 1, 3, 5,... and then after all these the even numbers 2, 4, 6,... We see that the number two is in the position $\omega$ and number 4 is in position $\omega + 1$, and so on. Now, what is called $\alpha$-recursion, for an ordinal number $\alpha$ is the ability to define a function by course-of-values recursion on the ordinal $\alpha$. So $\omega$-recursion is the good old primitive recursion. Formally, given a primitive recursive ordering $\prec$ of type $\alpha$ -- meaning the you will need the ordinal $\alpha$ in order to count 1st, 2nd, 3rd,... -- an $\alpha$-recursive function $f \colon \mathbb{N} \rightarrow \mathbb{N}$ is one defined as $$f(n) = F(n)(\lambda i \prec n . f (i))$$ So, in order to define $f(n)$ we are allowed to use any "previously calculated" value of f, where "previous" is formalised with the ordering $\prec$.

Now, there is an interesting relation between primitive recursion over an ordering of type $\alpha < \varepsilon_0$ and the primitive recursive functionals of finite type. Here, $\varepsilon_0$ is the fist $\varepsilon$ ordinal, and primitive recursive functionals of finite type are Goedel's extension of Kleene's primitive recursion, where one allows the input and return type of a function to be another function (quite common nowadays in functional programming languages such as Haskell, Python and Scala). It is well-known that a function is $\alpha$-recursive, for $\alpha < \varepsilon_0$, if and only if it is definable as a primitive recursive functional.

In this post we will look at part of one direction: how to replace $\alpha$-recursion by higher-type primitive recursion. In particular, we will look at the construction given in Tait's paper "Constructive Reasoning" from 1968, where he shows how to replace a $2^\alpha$-recursion, by an $\alpha$-recursion together with one application of higher-type primitive recursion. We will be following this proof quite closely.

So let $\prec$ be a primitive recursive ordering of type $\alpha$. Assume also that we have a standard primitive recursive one-to-one correspondence between natural numbers and finite sequences of natural numbers $$a \quad \leftrightarrow \langle a_0, \ldots, a_{|a| - 1} \rangle$$ such that $a_0 > a_1 > \ldots > a_{|a| - 1}$.

Define $a \subset b$ if and only if either

• $|a| < |b|$ and $a_i = b_i$ for all $i < |a|$, or
• there is a $k < \min\{|a|, |b|\}$ with $a_i \prec b_k$

Ie. $a \subset b$ is nothing more than the lexicographical ordering on words given the pointwise ordering $\prec$ on letters.

Then, note that if each $a_i$ is in position $\alpha_i$ in the ordering $\prec$, then $a$ is in position $2^{\alpha_0} + 2^{\alpha_1} + \ldots + 2^{\alpha_{|a| - 1}}$ in the lexicographical ordering $\subset$. Hence the ordering $\subset$ has type $2^\alpha$.

Assume now $\phi \colon \mathbb{N} \rightarrow (\mathbb{N} \rightarrow \mathbb{N})$ is defined by $2^\alpha$-recursion $$\phi(n) = \lambda i \subset n . F(i, \phi i)$$ We will give a definition of $\phi$ only using $\alpha$-recursion plus some extra primitive recursion of higher-type.

Given $a = \langle a_0, \ldots, a_{|a| - 1} \rangle$, let us define $a^k = \langle a_0, \ldots, a_{k - 1} \rangle$, i.e. the chopping of the sequence $a$ after $k$ elements.

The idea of the construction is quite simple. We just need to notice that for $k < |n|$ we have that $i \subset n^{k+1}$ if and only if either

• $i \subseteq n^k$, or
• $|n| > k \wedge i^k \equiv n^k \wedge i_k \prec n_k$

In other words, the sequence $i$ is strictly smaller than the first $k + 1$ bits of $n$ if either $i$ is already smaller or equal than the first $k$ bits of $n$, or if $i$ is equal to $n$ up to point $k - 1$ but strictly smaller at point $k$.

So we are essentially done. In the first case we compute by primitive recursion, whereas in the second case we compute by $\alpha$-recursion!

Formally, define a more general functional $\Psi(k)(v)(n)(i)$ by primitive recursion on $k$ (on a higher-type) $$\Psi(k) = {\huge\{} \begin{array}{ll} \lambda v \lambda n \lambda i . 0 & k = 0 \\ \chi(k, \Psi(k-1)) & k > 0 \end{array}$$ where $\chi(k, f)(v)$ is defined by $\alpha$-recursion on $v$ as $$\chi(k, f)(v) = \lambda n \lambda i . {\huge\{} \begin{array}{ll} f(v)(n)(i) & i \subseteq n^k \\ F(i, \chi(k, f)(i_k)(i)) & i^k \equiv n^k \wedge i_k \prec v \end{array}$$ with $\chi(k, f)(v) = \lambda n \lambda i . 0$ if $i \not\subset n^{k+1}$ or $k \geq |n|$. By induction on $k$ and $\alpha$-induction on $v$ we can see that if $k \leq |n|$ and $k > 0 \rightarrow v = n_{k-1}$ then $$\Psi(k)(v)(n) = \lambda i \subset n^k . F(i, \phi i)$$ Hence, we can define $$\phi(n) = {\huge\{} \begin{array}{ll} \Psi(|n|)(n_{|n| - 1})(n) & n > 0 \\ \lambda i . 0 & n = 0 \end{array}$$