Ackermann function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we define the two-argument Ackermann function
ack. Despite having a recursive
definition, we show that this isn't a primitive recursive function.
Main results #
exists_lt_ack_of_primrec: any primitive recursive function is pointwise bounded above by
ack mfor some
not_primrec₂_ack: the two-argument Ackermann function is not primitive recursive.
Proof approach #
We very broadly adapt the proof idea from
https://www.planetmath.org/ackermannfunctionisnotprimitiverecursive. Namely, we prove that for any
f : ℕ → ℕ, there exists
m such that
f n < ack m n for all
n. This then
λ n, ack n n can't be primitive recursive, and so neither can
ack. We aren't able
to use the same bounds as in that proof though, since our approach of using pairing functions
differs from their approach of using multivariate functions.
∀ n, nat.mkpair (f n) (g n) < ack (max a b + 3) n.
∀ n, g (f n) < ack (max a b + 2) n.
∀ n, nat.elim (f n.unpair.1) (λ (y IH : ℕ), g (nat.mkpair n.unpair.1 (nat.mkpair y IH))) n.unpair.2 < ack (max a b + 9) n.
The last one is evidently the hardest. Using
nat.unpair_add_le, we reduce it to the more
We then prove this by induction on
n. Our proof crucially depends on
ack_mkpair_lt, which is
applied twice, giving us a constant of
4 + 4. The rest of the proof consists of simpler bounds
which bump up our constant to
The two-argument Ackermann function, defined so that
This is of interest as both a fast-growing function, and as an example of a recursive function that isn't primitive recursive.