How to prove the termination of Ackermann in Lean?

Question

I'm trying to write the Ackermann function and prove it terminates in Lean 4

def Ackermann : Nat → Nat → Nat :=
  fun x y => 
    if x == 0 then y + 1 else
    if y == 0 then Ackermann (x - 1) 1 else
    Ackermann (x - 1) (Ackermann x (y - 1))
  termination_by
    Ackermann x y => (x, y)

but it rejects the termination proof. I don't know how to write lexicographic tuples, and I haven't found in the documentation I looked for. Thanks for your help.

Answer 1

Usually x-1 is harder to work with (but not impossible). Pattern matching is much easier from a type theoretic perspective. So (this is actually one of the test cases of Lean):

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)
termination_by _ a b => (a, b)

Answer 2

With dependent types and the awesome prelude of Lean 4, one can define the Ackermann function in any equivalent way as long as the definition is constructive. However, the more closely the definition for the Ackermann follows the definitions of its associated types (in this case, pattern matching on Nat like @Trebor's answer), the easier it is to reason about termination, preconditions, postconditions, etc.

For your definition, the goal is to prove these 3 lexicographic orderings given your termination_by measure:

1. Prod.Lex (· < ·) (· < ·) (x - 1, 1) (x, y) which suffices to prove x - 1 < x.
2. Prod.Lex (· < ·) (· < ·) (x, y - 1) (x, y) which suffices to prove y - 1 < y.
3. Prod.Lex (· < ·) (· < ·) (x - 1, Ackermann x (y - 1)) (x, y) which suffices to prove x - 1 < x.

First of all, we can use this lemma to simplify things:

theorem pos_sub_one_lt_self {n: Nat} (h: n ≠ 0): n - 1 < n :=
  Nat.sub_lt (Nat.zero_lt_of_ne_zero h) .refl -- #check (Nat.le.refl: 0 < 1)

To package all the "decreasing" proofs in decreasing_by:

def Ackermann (x y: Nat): Nat :=
  if hx: x = 0 then
    y + 1
  else if hy: y = 0 then
    Ackermann (x - 1) 1
  else
    Ackermann (x - 1) (Ackermann x (y - 1))
termination_by _ => (x, y)
decreasing_by
  simp_wf
  try apply Prod.Lex.right
  try exact pos_sub_one_lt_self hy
  try apply Prod.Lex.left
  try exact pos_sub_one_lt_self hx

To place "decreasing" proofs directly next to their usage, and let the decreasing_by pick them up automatically:

def Ackermann (x y: Nat): Nat :=
  if hx: x = 0 then
    y + 1
  else if hy: y = 0 then
    have: Prod.Lex (· < ·) (· < ·) (x - 1, 1) (x, y) :=
      .left _ _ (pos_sub_one_lt_self hx)
    Ackermann (x - 1) 1
  else
    have: Prod.Lex (· < ·) (· < ·) (x, y - 1) (x, y) :=
      .right _ (pos_sub_one_lt_self hy)
    have: Prod.Lex (· < ·) (· < ·) (x - 1, Ackermann x (y - 1)) (x, y) :=
      .left _ _ (pos_sub_one_lt_self hx)
    Ackermann (x - 1) (Ackermann x (y - 1))
termination_by _ => (x, y)

On my machine with leanprover/lean4:nightly-2023-03-09, the following snippet didn't work originally, but after solving the two variants above, the definition below magically started to work even in another project and even after restarting VSCode. Why?

def Ackermann (x y: Nat): Nat :=
  if x = 0 then
    y + 1
  else if y = 0 then
    Ackermann (x - 1) 1
  else
    Ackermann (x - 1) (Ackermann x (y - 1))
termination_by _ => (x, y)

Documentation and tutorial for custom well-founded recursions in Lean 4 is lacking. The way I figured it out is by implementing mod and div for my own ℕ by reading Nat.mod, Nat.div, and WF.lean in the prelude.

Answer 3

Here's a variant that doesn't require termination_by:

def ackAux (f : Nat → Nat) : Nat → Nat
| 0 => f 1
| y + 1 => f (ackAux f y)

def ack : Nat → Nat → Nat
| 0   => Nat.succ
| x+1 => ackAux (ack x)

In a more condensed form:

def ack : Nat → Nat → Nat
| 0   => Nat.succ
| x+1 => 
  let f := ack x
  let rec g : Nat → Nat
  | 0 => f 1
  | y+1 => f (g y)
  g