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!