Trouble with mutual recursion termination

Stream: new members

[Matti Åstrand]

Web editor link

I'm having trouble with proving mutual recursion to terminate. I believe it is the case since each time eval' calls exec it is with strictly smaller expressions. It might require some sort of custom well foundedness argument.

The code is inspired by section 8 of this tutorial

[Huỳnh Trần Khanh]

this isn't mutual recursion :joy: you can just define the two functions without the mutual keyword

[Huỳnh Trần Khanh]

haha what do you have to say now :joy: https://leanprover-community.github.io/lean-web-editor/#code=inductive%20aexpr%20%3A%20Type%0A%7C%20val%20%3A%20%E2%84%A4%20%E2%86%92%20aexpr%20%0A%7C%20add%20%3A%20aexpr%20%E2%86%92%20aexpr%20%E2%86%92%20aexpr%20%0A%0Aopen%20aexpr%20%0A%0Ainductive%20CStack%20%3A%20Type%0A%7C%20halt%20%3A%20CStack%0A%7C%20add%20%28n%20%3A%20%E2%84%A4%20%29%20%3A%20CStack%20%E2%86%92%20CStack%0A%7C%20eval%20%28y%20%3A%20aexpr%29%20%3A%20CStack%20%E2%86%92%20CStack%0A%0Adef%20eval'%20%3A%20aexpr%20%E2%86%92%20CStack%20%E2%86%92%20%E2%84%A4%0A%7C%20%28val%20n%29%20c%20%3A%3D%20n%0A%7C%20%28add%20x%20y%29%20c%20%3A%3D%20eval'%20x%20%28CStack.eval%20y%20c%29%0Adef%20exec%20%3A%20CStack%20%E2%86%92%20%E2%84%A4%20%E2%86%92%20%E2%84%A4%0A%7C%20CStack.halt%20n%20%3A%3D%20n%0A%7C%20%28CStack.eval%20y%20c%29%20n%20%3A%3D%20eval'%20y%20%28CStack.add%20n%20c%29%0A%7C%20%28CStack.add%20m%20c%29%20n%20%3A%3D%20exec%20c%20%28m%2Bn%29%0A

[Matti Åstrand]

Interesting! I tried it as well and looks like you are right code.

I'm confused how two functions calling each other isn't mutual recursion but it seems to work, thanks for help :)

[Matti Åstrand]

Ah, is it because eval' doesn't call exec? That seems to make sense now

[Matti Åstrand]

Sorry, there was a mistake in my original code, it should be this. I still have an issue with mutual recursion

[Patrick Johnson]

Try this:

def exec₁ : aexpr → ℤ
| (val a) := a
| (add a b) := exec₁ a + exec₁ b
def exec₂ : CStack → ℤ
| CStack.halt := 0
| (CStack.add a b) := a + exec₂ b
| (CStack.eval a b) := exec₁ a + exec₂ b
def eval' : aexpr → CStack → ℤ
| a b := exec₁ a + exec₂ b

[Matti Åstrand]

Sure, that works, but somewhat defeats the purpose. What you call exec₁ is called eval (without a tick) in the paper I linked above, and it is the "denotational semantics" of this tiny language.

The point is to define an "abstract machine" that uses a control stack but doesn't refer to the original evaluation function eval. One can then prove a connection between them, eval' e c = exec c (eval e)

Of course this is a toy language and the machine won't be very exciting, but I was curious of whether I can formalize it in Lean.

I'll play around trying to see if I can get the mutual recursion working, thanks for help anyhow!

[Patrick Johnson]

I'm not sure how to prove the mutual recursion terminates, but you can always prove it later (just put using_well_founded { dec_tac := [sorry] }` after the definition). For example:

def eval : aexpr → ℤ
| (val a) := a
| (add a b) := eval a + eval b

mutual def eval', exec
with eval': aexpr → CStack → ℤ
| (val n) c := exec c n
| (add x y) c := eval' x (CStack.eval y c)
with exec : CStack → ℤ → ℤ
| CStack.halt n := n
| (CStack.eval y c) n := eval' y (CStack.add n c)
| (CStack.add m c) n := exec c (m+n)
using_well_founded { dec_tac := `[sorry] }

lemma eval_eq_eval' {e : aexpr} : eval e = eval' e CStack.halt := begin
  ...
end

Now you can prove that eval is equal to eval', and later prove that the recursion terminates.

[Matti Åstrand]

Nice one, that's a good idea

[Huỳnh Trần Khanh]

@Matti Åstrand next time if you post a PDF link, make sure that the URL starts with https://. mobile browsers silently ignore HTTP PDF links :cry:

[Matti Åstrand]

Proof isn't too bad

theorem abstract_machine (x: aexpr) : ∀ c, eval' x c = exec c (eval x) :=
begin
  induction x with n x y hx hy,
  {
    intro c,
    rw [eval, eval'],
  },
  {
    intro c,
    rw [eval', hx, exec, hy, exec, eval],
  }
end

[Adam Topaz]

Hi @Matti Åstrand do we know eachother?

[Matti Åstrand]

Lol yes