Ackermann function

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_nat_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 fun 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_nat_primrec) are the following. Assuming ∀ n, f n < ack a n and ∀ n, g n < ack b n, we have:

• ∀ n, pair (f n) (g n) < ack (max a b + 3) n.
• ∀ n, g (f n) < ack (max a b + 2) n.
• ∀ n, Nat.rec (f n.unpair.1) (fun (y IH : ℕ) => g (pair n.unpair.1 (pair y IH))) n.unpair.2 < ack (max a b + 9) n.

The last one is evidently the hardest. Using unpair_add_le, we reduce it to the more manageable

• ∀ m n, rec (f m) (fun (y IH : ℕ) => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n).

We then prove this by induction on n. Our proof crucially depends on ack_pair_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.

@[irreducible]

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 0 x = x + 1
• ack m.succ 0 = ack m 1
• ack m.succ n.succ = ack m (ack (m + 1) n)

@[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)

@[irreducible]

theorem ack_strictMono_right (m : ℕ) : StrictMono (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 (max n₁ n₂) = max (ack m n₁) (ack m n₂)

@[irreducible]

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_strictMono_left (n : ℕ) : StrictMono fun (m : ℕ) => ack m n

theorem ack_mono_left (n : ℕ) : Monotone fun (m : ℕ) => ack m n

theorem ack_injective_left (n : ℕ) : Function.Injective fun (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 (max m₁ m₂) n = 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 (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_pair_lt (m : ℕ) (n : ℕ) (k : ℕ) : ack m (Nat.pair n k) < ack (m + 4) (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 fun (n : ℕ) => ack n n

theorem not_primrec_ack_self : ¬Primrec fun (n : ℕ) => ack n n

theorem not_primrec₂_ack : ¬Primrec₂ ack

The Ackermann function is not primitive recursive.