Recursion in expression definition in TPIL exercises

Stream: new members

[Yakov Pechersky]

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

[David Wärn]

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?

[Yakov Pechersky]

Ah, true.

[Yakov Pechersky]

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!