Lecture 13: More Recursive Data

1 Purpose

More recursive data

2 Outline

(define-struct leaf [value])

(define-struct node [left right])

(define-contract (Tree X) (OneOf (Leaf X) (Node (Tree X) (Tree X))))

Let’s write another function:

(: max-tree (-> (Tree Natural) Natural))

(define (max-tree t)   (cond [(leaf? t) (leaf-value t)]         [(node? t) (max (max-tree (node-left t)) (max-tree (node-right t)))]))

Again, we’d like to think about how to write a theorem that ensures that our function behaves as expected. We want to think about what it means to be a maximum of a tree. One way of doing this is to say that if a tree has a given maximum, if we put a node that has that tree as one subtree, and a leaf with a larger value on the other side, the max of the resulting tree should be the larger value.

(: max-tree-prop (-> (Tree Natural) True)) (define (max-tree-prop t)   (let ([m (max-tree t)])     (and (equal? (max-tree (make-node t (make-leaf (add1 m))))                  (add1 m))          (equal? (max-tree (make-node (make-leaf (add1 m)) t))                  (add1 m))))) (check-contract max-tree-prop)

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

We could also check that if two trees are combined, the maximum of the two is what results:

(: max-tree-prop2 (-> (Tree Natural) (Tree Natural) True)) (define (max-tree-prop2 t1 t2)   (let ([m1 (max-tree t1)]         [m2 (max-tree t2)])     (and (equal? (max-tree (make-node t1 t2))                  (max m1 m2))          (equal? (max-tree (make-node t2 t1))                  (max m1 m2))))) (check-contract max-tree-prop2)

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

As another example of recursive data, let’s define data for an arithmetic expression with addition, multiplication, and division. We’ll also include a single variable, to make it so that expressions cannot be simplified to just numbers.

(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)))

Let’s start by defining a function eval that takes a value for the variable and an ArithExpr and either returns a Real or raises a error if there is a division by 0. How do we handle errors? LSL has slightly more support for exceptions than ISL+: in particular, rather than using error (with arbitrary values), we call raise with some struct you have defined. These still cannot be caught (so these are not exceptions like you know from Java, etc), so should only be used for unrecoverable failure, but they communicate more information than unstructured data.

The exceptions that a function may raise should also be communicated via the function signature. In order to do this, we use a third argument to the dependent version of function signatures (review Dependent Functions) to list the structs that may be raised. Note that since this function is not dependent, we use underscores for the names of the arguments within the function contract.

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

(: 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]))

(check-expect (eval 10 (make-var)) 10) (check-expect (eval 0 (make-add 1 2)) 3) (check-expect (eval 10 (make-add 1 (make-var))) 11) (check-expect (eval 3 (make-add (make-mul 2 (make-var)) 2)) 8) (check-raises (eval 0 (make-div 10 (make-var)))) (check-raises (eval 0 (make-div 10 (make-var))) divide-by-zero)

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