TPIL 7.10.3

Stream: new members

[Eduardo Cavazos]

From TPIL exercise 7.10.3:

Define an inductive data type consisting of terms built up from the following constructors:

• const n, a constant denoting the natural number n
• var n, a variable, numbered n
• plus s t, denoting the sum of s and t
• times s t, denoting the product of s and t

Recursively define a function that evaluates any such term with respect to an assignment of values to the variables.

Handling everything except for the var, here's what I have so far for the inductive data type:

inductive Expr
| const : ℕ → Expr
| plus  : Expr → Expr → Expr
| times : Expr → Expr → Expr

And the function that evaluates these terms:

def eval (e : Expr) : ℕ :=

    Expr.rec_on e

        (λ n, n)

        (λ a b c d, c + d)

        (λ a b c d, c * d)

This seems to work OK:

#reduce eval (plus (const 2) (const 3)) -- 5

#reduce eval (plus (plus (const 2) (const 3))   (const 4))  -- 9

#reduce eval (times (const 2) (const 3))    -- 6

#reduce eval (times   (plus (const 2) (const 3))   (plus (const 4) (const 5)))  -- 45

#reduce eval (plus   (times (const 2) (const 3))   (times (const 4) (const 5))) -- 26

It isn't clear what the exercise intends as far is support for var goes, however.

Can someone give an example of how var would be used as they're intending?

Thanks!

[Kenny Lau]

inductive Expr
| const : ℕ → Expr
| var : ℕ → Expr
| plus  : Expr → Expr → Expr
| times : Expr → Expr → Expr

def eval (e : Expr) (assignment : ℕ → ℕ) : ℕ := sorry

#reduce eval (Expr.var 2) (λ n, 3) -- 3

[Kenny Lau]

I think