## Stream: new members

### Topic: TPIL 7.10.3

#### Eduardo Cavazos (Jan 05 2020 at 09:18):

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 (Jan 05 2020 at 09:26):

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 (Jan 05 2020 at 09:26):

I think

Last updated: May 18 2021 at 16:25 UTC