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 \)

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 \)

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} $$