ackermann

Stream: lean4

[Ciprian Teodorov]

Hi,

Is it possible to write the termination proof for ackermann in lean4. I think we should be able to use the lexicographic order, but I cannot find any documentation on how that might work.

def ackm : Nat × Nat → Nat
| (0, y)         => y+1
| ((x+1), 0)     => ackm (x, 1)
| ((x+1), (y+1)) => ackm (x, (ackm ((x+1), y)))
termination_by Prod.lex (Nat.lt_wfRel) (Nat.lt_wfRel)
decreasing_by exact (by {sorry})

cheers,
ciprian

[Chris B]

You can fulfill the base obligation like this:

def ackm : Nat × Nat → Nat
| (0, y)         => y+1
| ((x+1), 0)     => ackm (x, 1)
| ((x+1), (y+1)) => ackm (x, (ackm ((x+1), y)))
termination_by Prod.lex (Nat.lt_wfRel) (Nat.lt_wfRel)
decreasing_by
  simp [Prod.lex, Prod.Lex]
  exact Prod.Lex.left _ _ (Nat.lt.base _)

But it doesn't seem to like the presence of the outer call. If you change it to

def ackm : Nat × Nat → Nat
| (0, y)         => y+1
| ((x+1), 0)     => ackm (x, 1)
| ((x+1), (y+1)) =>
  let inner := (ackm ((x+1), y))
  ackm (x, inner)

Then it shows two goals, but it complains if you give either one saying it wants the other one. I'm not sure how you're supposed to discharge these.

[David Renshaw]

Here's another way to define it:

def iterate {α : Sort _} (op : α → α) : Nat → α → α
 | 0,          a  => a
 | Nat.succ k, a => iterate op k (op a)

def ackermann : Nat → Nat → Nat
 | 0 => Nat.succ
 | Nat.succ p => λ n => iterate (ackermann p) n (ackermann p 1)

[David Renshaw]

(from Bob Harper's _Practical Foundations for Programming Languages_ http://www.cs.cmu.edu/~rwh/pfpl/ )

[David Renshaw]

no extra termination proof needed with this formulation

[Mario Carneiro]

I believe this proof works, but I get unknown constant 'ackm' on the definition and I'm not sure what to make of that.

def ackm : Nat × Nat → Nat
| (0, y)     => y+1
| (x+1, 0)   => ackm (x, 1)
| (x+1, y+1) => ackm (x, ackm (x+1, y))
termination_by Prod.lex Nat.lt_wfRel Nat.lt_wfRel
decreasing_by
  first | apply Prod.Lex.right | apply Prod.Lex.left
  apply Nat.lt.base

[David Renshaw]

Did y'all see this: https://github.com/leanprover/lean4/commit/068cc700d8540728558556bf6f86ff6988478d91 ?

[Mario Carneiro]

the syntax for termination_by recently changed, this is for the old version

[Leonardo de Moura]

https://github.com/leanprover/lean4/blob/master/tests/lean/run/ack.lean