CS 8, Fall 2009

Short Assignment 7: Inductive Proofs of Program Equivalence

Instructions

You should write up or print out your solutions to this assignment, and either turn them in at lecture, or leave them in the TA's mailbox at Sudikoff by class time on Wed. Oct. 21, 2009.

Hand-written solutions are perfectly acceptable, as long as they are neat. Please make sure your name is clearly marked on all pages, and if your solution takes more than one page, please staple the pages together. As with all other work for this class, no late assignments will be accepted.

You must work alone on this short assignment.

Assignment

Problem 1. Show the following properties of lists from pp. 138-139 of SOE.

1. map (f.g) = map f . map g
2. map f (xs ++ ys) = map f xs ++ map f ys
3. Extra Credit: head (reverse xs) = last xs
4. Extra Credit: foldr op e xs = foldl (flip op) e (reverse xs)

Problem 2. In BSTMap.hs we defined toList as follows:

toList :: Map a b -> [(a,b)]
toList tree = toListHelper tree []
  where toListHelper :: Map a b -> [(a,b)] -> [(a,b)]
        toListHelper Leaf acc = acc
        toListHelper (Branch k v l r) acc = 
          toListHelper l ((k,v) : toListHelper r acc)

A more natural way of doing this would have been the way that fringe was defined in the book:

fringe :: Map a b -> [(a,b)]
fringe Leaf = []
fringe (Branch k v l r) = 
  fringe l ++ ((k, v) : fringe r)

Show that toList = fringe. You may use any of the properties on pp. 138-139 of SOE or other things proved in the text as lemmas in your proof.

Hint: first use induction to prove the lemma: toListHelper t1 acc = (fringe t1) ++ acc. Then figure out what toList tree = toListHelper tree [] evaluates to (no induction needed).

Hand in

Hand in your proofs of the properties. Make sure that you justify each step.