Tetration of Church numerals?

Question

I haven't seen any examples of tetration of Church numerals, so I was trying to do it myself. Tetration is iterated exponention, for example: $2 \uparrow\uparrow 3={2^{2}}^{2}$. Unfortunately, I haven't been able to figure it out. Any suggestions or references are appreciated.

Answer 1

Usually, this would just follow a similar pattern to the slower growing functions. If we have typed Church numerals:

$$\mathsf{N} = ∀ r. r → (r → r) → r$$

Then successor can be defined as a base case as:

$$\mathsf{suc}\ n\ z\ s = s (n\ z\ s)$$

Addition is iterated successor:

$$m + n = n\ m\ \mathsf{suc}$$

Multiplication is iterated addition, and exponentiation is iterated multiplication:

$$m × n = n\ 0\ (λk. m + k)\\ m ^ n = n\ 1\ (λk. m × k)$$

And you can keep doing this:

$$m \uparrow\uparrow n = n\ 1\ (λ k . m ^ k) \\ m \uparrow\uparrow\uparrow n = n\ 1\ (λk. m \uparrow\uparrow k) \\ \vdots$$

One thing this relies on crucially, in a typed setting, is the ability to instantiate $r$ in the type of Church numerals with $\mathsf{N}$ itself (without types it's, of course, no problem either). If instead we are in a predicative setting, where quantifying over types can only be done by moving to a larger universe, then this process becomes more difficult, and which hyperoperations can be defined is related to how many universes there are. See here for some details.

Incidentally, in the first situation, it's possible to go beyond the hyperoperations and primitive recursion by instantiating $r$ to function types on $\mathsf{N}$. Essentially, we can iterate the process of iteration:

$$m \uparrow^k n = k\ (λ m\ n. m × n)\ (λ f\ m\ n. n\ 1\ (f\ m))$$

So, for $k = 0$ we get multiplication, for $k = 1$ we get exponentiation, for $k = 2$ we get tetration, and in general we get the $k$-th operation in Knuth's up-arrow notation.