(* COMP 302 Winter 2013 HOMEWORK 2 Instructors: Francisco Ferreira, Andrew Cave Due 1st February 2013, at the BEGINNING OF CLASS (2:35pm) *) (* Question 1 code for reference *) infix 3 \/ fun m \/ n = Int.max (m,n) datatype mobile = Object of int | Wire of mobile * mobile fun mobile_max (Object n) = n | mobile_max (Wire (l,r)) = (mobile_max l) \/ (mobile_max r) fun mobile_max_acc (Object n) m = n \/ m | mobile_max_acc (Wire (l,r)) m = mobile_max_acc l (mobile_max_acc r m) exception NotImplemented (* Question 1.1: Theorem: for any M : mobile, reflect (reflect M) => M Proof: By structural induction on M. Case: M = Object n reflect (reflect (Object n)) => reflect (Object n) (by program reflect) => Object n (by program reflect) Case: M = Wire (l,r) We are granted the I.H: reflect (reflect l) => l and reflect (reflect r) => r reflect (reflect (Wire (l,r)) => reflect (Wire (reflect r, reflect l)) (by program reflect) => Wire (reflect (reflect l), reflect (reflect r)) (by program reflect) => Wire (l,r) (by I.H.) *) (* Question 1.2 We must generalize the statement to: Lemma: for any M:mobile and x:int, mobile_max_acc M x = (mobile_max M) \/ x Proof: By structural induction on M. Case: M = Object n mobile_max_acc (Object n) x => n \/ x (by program mobile_max_acc) On the other side, (mobile_max (Object n)) \/ x => n \/ x (by program mobile_max) As required. Case: M = Wire (l, r) We are granted the I.H: for any y, mobile_max_acc l y = (mobile_max l) \/ y and for any y, mobile_max_acc r y = (mobile_max r) \/ y mobile_max_acc (Wire (l,r)) x => mobile_max_acc l (mobile_max_acc r x) (by program mobile_max_acc) = mobile_max_acc l ((mobile_max r) \/ x) (by I.H. 2 with y = x) = (mobile_max l) \/ ((mobile_max r) \/ x) (by I.H. 1 with y = (mobile_max r) \/ x) = (mobile_max l \/ mobile_max r) \/ x (by associativity of \/) <= (mobile_max (Wire (l,r)) \/ x (by program mobile_max) As required. Theorem: for any M with positive weights, mobile_max_acc M 0 = mobile_max M Proof: Using the lemma with x = 0, we obtain: mobile_max_acc M 0 = (mobile_max M) \/ 0 And (mobile_max M) \/ 0 = mobile_max M (property of \/, since mobile_max M is positive) So we are done. *) (* Question 2: Associative lists *) (* Question 2.1 *) fun zipWith f xs ys = ListPair.foldr (fn (x,y,z) => (f (x,y))::z) [] (xs,ys) (* Question 2.2 *) fun ziprev xs ys = zipWith (fn (x,y) => (x,y)) xs (List.rev ys) (* Question 2.3 *) fun lookup k [] = NONE | lookup k ((k',v)::xs) = if k = k' then SOME v else lookup k xs (* Question 2.4 *) type dict = string -> int option val empty : dict = fn key => NONE fun insert (k,v) d = fn key => if k = key then SOME v else d key fun lookup2 k d = d k (* Question 3 preamble *) (* Suspended computation : we can suspend computation by wrapping it in a closure. *) datatype 'a susp = Susp of (unit -> 'a) (* delay: *) fun delay (f ) = Susp(f) (* force: *) fun force (Susp(f)) = f () (* ---------------------------------------------------- *) (* Define an infinite stream *) datatype 'a stream' = Cons of 'a * 'a stream withtype 'a stream = ('a stream') susp (* ---------------------------------------------------- *) (* Inspect a stream up to n elements take : int -> 'a stream' susp -> 'a list take': int -> 'a stream' -> 'a list *) fun take 0 s = [] | take n (s) = take' n (force s) and take' 0 s = [] | take' n (Cons(x,xs)) = x::(take (n-1) xs) (* Question 3.1 *) fun hailstones n = Susp(fn () => Cons(n, hailstones (if n mod 2 = 0 then n div 2 else 3*n + 1))) (* Examples: - take 20 (hailstones 13); val it = [13,40,20,10,5,16,8,4,2,1,4,2,...] : int list - take 20 (hailstones 8); val it = [8,4,2,1,4,2,1,4,2,1,4,2,...] : int list *) (* Question 3.2 *) fun unfold f x = Susp(fn () => Cons(x, unfold f (f x))) fun deriv f x = let val h = 0.0000001 in (f (x + h) - f x) / h end fun newton f guess = unfold (fn c => c - (f c) / (deriv f c)) guess (* Example: - take 10 (newton (fn x => x*x - 2.0) 7.0) val it = [7.0,3.64285718209,2.09593841013,1.52508247335,1.41824348423,1.41421928801, 1.41421356238,1.41421356237,1.41421356237,1.41421356237] : real list *)