The Ackermann-Péter Function in Gödel's T

The Ackermann-Péter function is defined as:

A : ℕ × ℕ → ℕ
A(0, n)     = n+1 
A(m+1, 0)   = A(m, 1)
A(m+1, n+1) = A(m, A(m+1, n))

Famously, it is not expressible as a primitive recursive function. However, in lecture I showed my students that it is possible to define this function in Gödel's T. That is to say, the Ackermann-Péter function is nevertheless "higher-order primitive recursive". However, I didn't have time to really explain where the definition I supplied them with came from, an issue I wanted to rectify with this blog post.

The best way to explain it is to show how the definition in Gödel's T can be derived from the original definition. To do so, let's start by writing A in a curried style:

A : ℕ → ℕ → ℕ
A 0     n     = n+1 
A (m+1) 0     = A m 1
A (m+1) (n+1) = A m (A (m+1) n)

Note that the pair of clauses for A (m+1) look like a primitive recursive definition over the second argument. Following this idea, let's abuse notation and define a function B which is used instead of the direct call to A (m+1):

B : ℕ → ℕ → ℕ 
B m 0     = A m 1 
B m (n+1) = A m (B m n)

A : ℕ → ℕ → ℕ
A (0)   n     = n+1 
A (m+1) n     = B m n 

This looks a bit like we are going backwards: to define B, we needed to use mutual recursion. Unfortunately, this is not a feature of Gödel's T. However, note that our definition of B only uses its m argument to pass it to A. As a result, if we pass B the function A m as an argument, we can both remove the m argument and the mutual recursion with A:

B : (ℕ → ℕ) → ℕ → ℕ
B f 0     = f 1 
B f (n+1) = f (B f n)

A : ℕ → ℕ → ℕ
A (0)   n     = n+1 
A (m+1) n     = B (A m) n 

These are two independent, iterative functions now! We could stop right here, and turn them from functional equations into terms in Gödel's T, except that I find the first clause of B, that B f 0 = f 1 a bit inelegant. Let's define a new function, repeat:

repeat : (ℕ → ℕ) → ℕ → (ℕ → ℕ)
repeat f 0     = id
repeat f (n+1) = f ∘ (repeat f n)

The call repeat f n just defines the n-fold self-composition of the function f. I like this more than the raw definition of B, since it is a fairly mathematically natural notion. However, we can still use repeat to define B:

B : (ℕ → ℕ) → ℕ → ℕ
B f n     = repeat f n (f 1)

Putting this all together, we can define the whole Ackermann-Péter function as:

repeat : (ℕ → ℕ) → ℕ → (ℕ → ℕ)
repeat f 0 = id
repeat f (n+1) = f ∘ (repeat f n)

B : (ℕ → ℕ) → ℕ → ℕ
B f n = repeat f n (f 1)

A : ℕ → ℕ → ℕ
A (0)   n  = n+1 
A (m+1) n  = B (A m) n 

Since B is neither recursive, nor used more than once, it hardly makes sense as a separate definition. So we can inline it and get:

repeat : (ℕ → ℕ) → ℕ → (ℕ → ℕ)
repeat f 0     = id
repeat f (n+1) = f ∘ (repeat f n)

A : ℕ → ℕ → ℕ
A (0)   n = n+1 
A (m+1) n = repeat (A m) n ((A m) 1)

Note that the right-hand-side of the A (m+1) n clause only contains occurences of A m. Hence, we can write this whole thing as a primitive iteration.

repeat : (ℕ → ℕ) → ℕ → (ℕ → ℕ)
repeat = λf:ℕ → ℕ. λn:ℕ. iter(n, 0 → id,
                                 S(r) → f ∘ r)

A : ℕ → ℕ → ℕ
A = λm:ℕ. iter(m, 0 → (λn:ℕ. S(n)),
                  S(r) → (λn:ℕ. repeat r n (r 1)))

And this is just the definition I gave in lecture!