Lecture 14: Continuing with Recursive Data

1 Purpose

Complete arithmetic compiler example

2 Outline

We’re continuing with the ArithExpr definition from last time:

(define-struct divide-by-zero ())

(define-struct add (left right))

(define-struct mul (left right))

(define-struct div (num den))

(define-struct var ())

(define-contract ArithExpr (OneOf Real                                   (Add ArithExpr ArithExpr)                                   (Mul ArithExpr ArithExpr)                                   (Div ArithExpr ArithExpr)                                   (Var)))

(: eval (Function (arguments [_ Real] [_ ArithExpr]) (result Real) (raises divide-by-zero)))

(define (eval v a)   (cond [(number? a) a]         [(add? a) (+ (eval v (add-left a)) (eval v (add-right a)))]         [(mul? a) (* (eval v (mul-left a)) (eval v (mul-right a)))]         [(div? a) (let ([d (eval v (div-den a))])                     (if (zero? d)                         (raise (make-divide-by-zero))                         (/ (eval v (div-num a)) d)))]         [(var? a) v]))

If you recall, we showed a way to generate binary trees a few days ago:

(define (inttree-generate fuel)   (cond [(zero? fuel) (make-leaf (contract-generate Integer fuel))]         [else (if (< (random) 1/2)                   (make-leaf (contract-generate Integer fuel))                   (make-node (inttree-generate (sub1 fuel))                              (inttree-generate (sub1 fuel))))]))

We’d like to do a similar thing here, but rather than generating arbitrary ArithExprs (which contract-generate can do), we want to generate expressions without any Vars in them.

(define (var-less-expr fuel)   (cond [(zero? fuel) (contract-generate Real fuel)]         [else          (let ([choice (random 4)])            (cond [(equal? choice 0) (contract-generate Real fuel)]                  [(equal? choice 1) (make-add (var-less-expr (sub1 fuel))                                               (var-less-expr (sub1 fuel)))]                  [(equal? choice 2) (make-mul (var-less-expr (sub1 fuel))                                               (var-less-expr (sub1 fuel)))]                  [(equal? choice 3) (make-div (var-less-expr (sub1 fuel))                                               (var-less-expr (sub1 fuel)))]))]))

We can then show that the function eval will return the same thing for a given var-less ArithExpr, regardless of the value for the variable passed:

(define-contract VarLessExpr (Immediate (check (lambda (x) #t))                                         (generate var-less-expr)))   (: var-less-prop (Function (arguments [_ VarLessExpr]                                       [_ Real]                                       [_ Real])                            (result True)                            (raises divide-by-zero))) (define (var-less-prop e n1 n2)   (equal? (eval n1 e) (eval n2 e)))   (check-contract var-less-prop)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run

An alternate representation

Let’s now define an alternate arithmetic representation, which is only recursive on the right side of Add:

(define-contract RightExpr (OneOf Real                                   (Add (OneOf Real (Var)) ArithExpr)                                   (Mul ArithExpr ArithExpr)                                   (Div ArithExpr ArithExpr)                                   (Var)))

We can, similarly to above, define a reval that evaluates these to numbers, erroring on division by zero.

(: reval (-> Real RightExpr Real))

(define (reval v a)   (cond [(number? a) a]         [(add? a) (+ (if (var? (add-left a)) v (add-left a))                      (reval v (add-right a)))]         [(mul? a) (* (reval v (mul-left a)) (reval v (mul-right a)))]         [(div? a) (let ([d (reval v (div-den a))])                     (if (zero? d)                         (raise (make-divide-by-zero))                         (/ (reval v (div-num a)) d)))]         [(var? a) v]))

What’s more interesting is that we can convert from ArithExprs to RightExprs.

Initially, this might seem impossible: while ArithExprs like (make-add 2 (make-var)) are already RightExprs, others like (make-add (make-add (make-var) 2) 3) are not. And because of the (make-var)s, we can’t just evaluate all the left sides to numbers. So how do we do it?

Well, if we start by thinking about just expressions with Add, Real and Var, we figure out we can shuffle all the left side structure of the tree to the right, and end up with essentially a list. This is the core of the problem: we end up with an accumulator function that is collecting expressions we need to add somewhere in the tree, and then when we finally get to a leaf, we can start adding to the right.

Now if you then add back the other terms (Mul and Div), we can come up with a similar strategy: we have a bunch of terms to add, but to put them into either side of the Mul or Div, we end up having to transform them. For Mul, we have divide them all by the other side (as they’ll get multiplied when the expression is evaluated), and for Div, if we put them in the numerator, we have to multiply them all by the denominator.

(: translate (-> ArithExpr RightExpr))

(define (translate a)   (local [(define (translate/acc to-add a)             (cond [(or (number? a)                        (var? a))                    (if (empty? to-add)                        a                        (make-add a (translate/acc (rest to-add)                                                   (first to-add))))]                   [(add? a) (if (number? (add-left a))                                 (make-add (add-left a) (translate/acc to-add (add-right a)))                                 (make-add 0 (translate/acc (cons (add-left a) to-add)                                                            (add-right a))))]                   [(mul? a) (make-mul (translate/acc empty (mul-left a))                                       (translate/acc (map (lambda (e) (translate (make-div e (mul-left a))))                                                           to-add)                                                      (mul-right a)))]                   [(div? a) (make-div (translate/acc (map (lambda (e) (translate (make-mul e (div-den a))))                                                           to-add)                                                      (div-num a))                                       (translate/acc empty (div-den a)))]))]     (translate/acc '() a)))

Now, to be sure that we actually got this right, we want to write a specification that captures exactly this. This is a compiler correctness theorem (as our translation is a simple compiler) called "semantics preservation", as it should capture that the semantics (i.e., meaning: what the expression evaluates to) is preserved by the translation. Note that we say that this raises the exception, which, interestingly, is possible to be introduced by the transformation. Can you think why?

(: compiler-correctness (Function (arguments (x Real)                                              (y ArithExpr))                                   (result True)                                   (raises divide-by-zero)))

(define (compiler-correctness v a)   (< (abs (- (eval v a) (reval v (translate a))))      1e-5))