mathlib3 documentation

computability.ackermann

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 m for some m.
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 primitive recursive f : ℕ → ℕ, there exists m such that f n < ack m n for all n. This then implies that λ 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.

The important bounds we show during the main inductive proof (exists_lt_ack_of_primrec) are the following. Assuming ∀ n, f n < ack a n and ∀ n, g n < ack b n, we have:

∀ 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 manageable

∀ m n, elim (f m) (λ (y IH : ℕ), g (nat.mkpair m (nat.mkpair y IH))) n < ack (max a b + 9) (m + n).

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 9.

def ack :

ℕ → ℕ → ℕ

The two-argument Ackermann function, defined so that

ack 0 n = n + 1
ack (m + 1) 0 = ack m 1
ack (m + 1) (n + 1) = ack m (ack (m + 1) n).

This is of interest as both a fast-growing function, and as an example of a recursive function that isn't primitive recursive.

Equations

ack (m + 1) (n + 1) = ack m (ack (m + 1) n)
ack (m + 1) 0 = ack m 1
ack 0 n = n + 1

@[simp]

theorem ack_zero (n : ℕ) :

ack 0 n = n + 1

@[simp]

theorem ack_succ_zero (m : ℕ) :

ack (m + 1) 0 = ack m 1

@[simp]

theorem ack_succ_succ (m n : ℕ) :

ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

@[simp]

theorem ack_one (n : ℕ) :

ack 1 n = n + 2

@[simp]

theorem ack_two (n : ℕ) :

ack 2 n = 2 * n + 3

@[simp]

theorem ack_three (n : ℕ) :

ack 3 n = 2 ^ (n + 3) - 3

theorem ack_pos (m n : ℕ) :

0 < ack m n

theorem one_lt_ack_succ_left (m n : ℕ) :

1 < ack (m + 1) n

theorem one_lt_ack_succ_right (m n : ℕ) :

1 < ack m (n + 1)

theorem ack_strict_mono_right (m : ℕ) :

strict_mono (ack m)

theorem ack_mono_right (m : ℕ) :

monotone (ack m)

theorem ack_injective_right (m : ℕ) :

function.injective (ack m)

@[simp]

theorem ack_lt_iff_right {m n₁ n₂ : ℕ} :

ack m n₁ < ack m n₂ ↔ n₁ < n₂

@[simp]

theorem ack_le_iff_right {m n₁ n₂ : ℕ} :

ack m n₁ ≤ ack m n₂ ↔ n₁ ≤ n₂

@[simp]

theorem ack_inj_right {m n₁ n₂ : ℕ} :

ack m n₁ = ack m n₂ ↔ n₁ = n₂

theorem max_ack_right (m n₁ n₂ : ℕ) :

ack m (linear_order.max n₁ n₂) = linear_order.max (ack m n₁) (ack m n₂)

theorem add_lt_ack (m n : ℕ) :

m + n < ack m n

theorem add_add_one_le_ack (m n : ℕ) :

m + n + 1 ≤ ack m n

theorem lt_ack_left (m n : ℕ) :

m < ack m n

theorem lt_ack_right (m n : ℕ) :

n < ack m n

theorem ack_strict_mono_left (n : ℕ) :

strict_mono (λ (m : ℕ), ack m n)

theorem ack_mono_left (n : ℕ) :

monotone (λ (m : ℕ), ack m n)

theorem ack_injective_left (n : ℕ) :

function.injective (λ (m : ℕ), ack m n)

@[simp]

theorem ack_lt_iff_left {m₁ m₂ n : ℕ} :

ack m₁ n < ack m₂ n ↔ m₁ < m₂

@[simp]

theorem ack_le_iff_left {m₁ m₂ n : ℕ} :

ack m₁ n ≤ ack m₂ n ↔ m₁ ≤ m₂

@[simp]

theorem ack_inj_left {m₁ m₂ n : ℕ} :

ack m₁ n = ack m₂ n ↔ m₁ = m₂

theorem max_ack_left (m₁ m₂ n : ℕ) :

ack (linear_order.max m₁ m₂) n = linear_order.max (ack m₁ n) (ack m₂ n)

theorem ack_le_ack {m₁ m₂ n₁ n₂ : ℕ} (hm : m₁ ≤ m₂) (hn : n₁ ≤ n₂) :

ack m₁ n₁ ≤ ack m₂ n₂

theorem ack_succ_right_le_ack_succ_left (m n : ℕ) :

ack m (n + 1) ≤ ack (m + 1) n

theorem ack_add_one_sq_lt_ack_add_three (m n : ℕ) :

(ack m n + 1) ^ 2 ≤ ack (m + 3) n

theorem ack_ack_lt_ack_max_add_two (m n k : ℕ) :

ack m (ack n k) < ack (linear_order.max m n + 2) k

theorem ack_add_one_sq_lt_ack_add_four (m n : ℕ) :

ack m ((n + 1) ^ 2) < ack (m + 4) n

theorem ack_mkpair_lt (m n k : ℕ) :

ack m (nat.mkpair n k) < ack (m + 4) (linear_order.max n k)

theorem exists_lt_ack_of_nat_primrec {f : ℕ → ℕ} (hf : nat.primrec f) :

∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n

If f is primitive recursive, there exists m such that f n < ack m n for all n.

theorem not_nat_primrec_ack_self :

¬nat.primrec (λ (n : ℕ), ack n n)

theorem not_primrec_ack_self :

¬primrec (λ (n : ℕ), ack n n)

theorem not_primrec₂_ack :

¬primrec₂ ack

The Ackermann function is not primitive recursive.