Zulip Chat Archive

Stream: new members

Topic: Recursion in expression definition in TPIL exercises


view this post on Zulip Yakov Pechersky (Jun 04 2020 at 19:12):

Thanks for everyone's help yesterday. I'm continuing with the TPIL inductive type exercises. Running into issues with well-founded recursion when trying to define an expression evaluator. I have some Haskell experience, so I think that might be hurting me here. How can I hint to the definition that working through the var path should decrease the complexity of the expression tree?

inductive expression {α : Type u}
| const : α -> expression
| var : α -> expression
| plus : expression -> expression -> expression
| times : expression -> expression -> expression

namespace expression

def eval (dict :  -> expression) : expression -> 
| (const n) := n
| (plus x y) := eval x + eval y
| (times x y) := eval x * eval y
| (var v) := eval (dict v)

--failed to prove recursive application is decreasing, well founded relation
--  @has_well_founded.r (@expression ℕ)
--    (@has_well_founded_of_has_sizeof (@expression ℕ) (@expression.has_sizeof_inst ℕ nat.has_sizeof))

end expression

view this post on Zulip David Wärn (Jun 04 2020 at 19:33):

I'm confused. How does the complexity decrease? Say dict 0 = var 0. Then eval dict (var 0) = eval dict (dict 0) = eval dict (var 0) = ..., no?

view this post on Zulip Yakov Pechersky (Jun 04 2020 at 19:43):

Ah, true.

view this post on Zulip Yakov Pechersky (Jun 04 2020 at 19:51):

Okay, then for the sake of the exercise, we can change it to

def eval (dict :  -> ) : expression -> 
| (const n) := n
| (plus x y) := eval x + eval y
| (times x y) := eval x * eval y
| (var v) := dict v

That works then, like with a eval nat.succ (plus (const 9) (times (const 3) (var 2))). Thanks!


Last updated: May 16 2021 at 05:21 UTC