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!