Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC