Zulip Chat Archive

Stream: new members

Topic: Trouble with mutual recursion termination

Matti Åstrand (Dec 12 2021 at 09:06):

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 (Dec 12 2021 at 09:51):

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

Huỳnh Trần Khanh (Dec 12 2021 at 09:54):

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 (Dec 12 2021 at 09:58):

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 (Dec 12 2021 at 09:59):

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

Matti Åstrand (Dec 12 2021 at 10:10):

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

Patrick Johnson (Dec 12 2021 at 11:34):

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 (Dec 12 2021 at 12:43):

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 (Dec 12 2021 at 13:03):

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

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

Matti Åstrand (Dec 12 2021 at 13:19):

Nice one, that's a good idea

Huỳnh Trần Khanh (Dec 12 2021 at 13:23):

@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 (Dec 12 2021 at 13:43):

Proof isn't too bad

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

Adam Topaz (Dec 12 2021 at 13:47):

Hi @Matti Åstrand do we know eachother?

Matti Åstrand (Dec 12 2021 at 13:50):

Lol yes

Last updated: Dec 20 2023 at 11:08 UTC