# A6: Prove it! **Soft deadline:** Thursday, 12/03/15, 11:59 pm **Hard deadline:** Saturday, 12/05/15, 11:59 pm * * * **Project component:** The implementation phase of your project is due at the same time as this assignment. See [Milestone 2 of the project description][ms2] for instructions. [ms2]: ../proj/proj.html#ms2 * * * *The rest of this writeup is an **individual** assignment. Sharing of solutions is not permitted, especially not between you and your project team.* ## Overview This assignment is a collection of written problems about correctness and efficiency. There are no programming problems on this assignment. Depending on the kind of problems you prefer, it might take you longer or shorter than a programming assignment. ## Objectives * Prove the correctness of functions. * Learn how to prove the correctness of data structure operations. * Practice proof by induction. * Write a monad and prove that it satisfies the monad laws. * Use amortized analysis to reason about the efficiency of a data structure. ## Recommended reading * [Lectures and recitations 19&ndash;23][web] [web]: http://www.cs.cornell.edu/Courses/cs3110/2015fa/ ## What we provide * A [template file `a6feedback.txt`][template] for submitting your written feedback. [template]: a6feedback.txt ## What to turn in Submit the following files on [CMS][cms]: * `a6solution.pdf` or `a6solution.txt`, containing your solution. You are welcome to use plain text, LaTeX, or any other word processing system to produce your solution. Please do not scan handwritten solutions. * `a6feedback.txt`, containing your written feedback. It contains some questions that you should answer individually on your project. [cms]: https://cms.csuglab.cornell.edu/ ## Grading issues * **Late submissions:** Carefully review the [course policies][syllabus] on submission and late assignments. Verify before the deadline on CMS that you have submitted the correct version. * **Clarify matters:** Your written solutions will be evaluated on clarity. A "correct" solution that a reader can't understand is incorrect. [style]: http://www.cs.cornell.edu/Courses/cs3110/2015fa/handouts/style.html [syllabus]: http://www.cs.cornell.edu/Courses/cs3110/2015fa/syllabus.php [vm]: http://www.cs.cornell.edu/Courses/cs3110/2015fa/vm.html ## Git As always, you should use git (or another version control system) to manage your files. We won't ask you to turn in a log for this assignment. But we also won't have sympathy for anyone who loses their solution because they weren't keeping it in version control. ## Problem 1: Correctness of data structures In this problem, we'll look at proving the correctness of entire data structures, not just individual functions. Consider data structures of the following form: ``` sig (* RI: Inv(v) must hold for v : t *) type t val value : t val constructor : 'a -> t val destructor : t -> 'b val transform : 'c -> t -> t end ``` A *value* of the data structure is a value of the representation type `t`. A *constructor* is an operation that can produce values of type `t` out of some type `'a`. (Note, this use of the word "constructor" is distinct from yet closely related to the use of that word with variant types in OCaml.) A *destructor* is an operation that can turn a value of type `t` into a value of some type `'b`. And a *transform* is an operation that, based on additional input of some type `'c`, transforms one value of the data structure into another. The `list` data structure can be understood in this way: * `[]` is a value. * `hd` and `length` are destructors. * `tl` and `rev` are transforms. * Although there is no function in the `List` module that behaves exactly like a constructor, we could think of the syntactic sugar `[ e ]` as being a kind of constructor. When proving the correctness of data structures, the *representation invariant* is important: * for any value `v` of type `t`, we prove `Inv(t)`. * for any constructor that takes input `x`, we add `Inv(constructor x)` to the postcondition of `constructor`. * for any destructor that takes value `v` as input, we add `Inv(v)` to the precondition of `destructor`. * for any transform that takes value `v1` as input and produces value `v2` as output, we add `Inv(v1)` to the precondition and `Inv(v2)` to the postcondition. Let's make that concrete by proving the correctness of sets represented as lists without duplicates: ``` module type SET = sig type 'a set val mem : 'a -> 'a set -> bool (* precondition: none * postcondition: for all x, mem x empty ~ false *) val empty : 'a set (* precondition: none * postcondition: mem x (add x s) ~ true *) val add : 'a -> 'a set -> 'a set (* precondition: none * postcondition: size empty ~ 0 && for all x, mem x s ~ true implies size (add x s) ~ size s && for all x, mem x s ~ false implies size (add x s) ~ 1 + size s *) val size : 'a set -> int val rem : 'a -> 'a set -> 'a set val union : 'a set -> 'a set -> 'a set val inter : 'a set -> 'a set -> 'a set end module ListSet : SET = struct (* RI: the list contains no duplicates *) type 'a set = 'a list let mem = List.mem let empty = [] let add x l = if mem x l then l else x::l let size l = List.length l let rem x l = List.filter ((<>) x) l let union l1 l2 = List.fold_left (fun a x -> if mem x l2 then a else x::a) l2 l1 let inter l1 l2 = List.filter (fun h -> mem h l2) l1 end ``` We can make the rep invariant precise by writing an OCaml function that checks it: ``` let rec inv = function | [] -> true | h::t -> not (mem h t) && inv t ``` *Hint: none of the proofs below needs induction.* ### Part A `empty` is a value of type `'a set`. We need to show that it satisfies its specification, including the rep invariant. When we add the rep invariant to the specification, we obtain ``` precondition: none postcondition: (for all x, mem x empty ~ false) && (inv empty ~ true) ``` So **prove two theorems:** ``` Theorem. for all x, mem x empty ~ false. Theorem. inv empty ~ true. ``` Use the following as the specification for `List.mem`: ``` (* precondition: none * postcondition: for all x, mem x [] ~ false && for all x and l, mem x (x::l) ~ true && for all x, h, and t, if x <> h then mem x (h::t) ~ mem t *) val mem : 'a -> 'a list -> bool ``` ### Part B `add` is a transform of type `'a -> 'a set -> 'a set`. We need to show that it satisfies its specification, including the rep invariant. When we add the rep invariant to the specification, we obtain ``` precondition: inv s ~ true postcondition: (mem x (add x s) ~ true) && (inv(add x s) ~ true) ``` So **prove two theorems:** ``` Theorem. for all x and s, (inv s ~ true) implies (mem x (add x s) ~ true). Theorem. for all x and s, (inv s ~ true) implies (inv(add x s) ~ true). ``` ### Part C `size` is a destructor of type `'a set -> int`. We need to show that it satisfies its specification, including the rep invariant. **State and prove a theorem (or theorems)** that do so. Use the following as the specification for `List.length`: ``` (* precondition: none * postcondition: length [] ~ 0 and length (h::t) ~ 1 + length t *) val length : 'a list -> int ``` ## Problem 2: Proof by induction Here is a type that represents a small language of integer expressions: ``` type expr = | Int of int (* integer constants *) | Neg of expr (* unary negation *) | Plus of expr * expr (* addition *) ``` ### Part A State the induction principle for `expr`. ### Part B Here is code that implements evaluation of expressions, as well as an *optimizer* that removes certain subexpressions that never need to be evaluated: ``` (* [eval e] is the integer to which [e] evaluates. *) let rec eval = function | Int n -> n | Neg e -> -(eval e) | Plus(e1,e2) -> (eval e1) + (eval e2) (* [opt e] is an expression that evaluates to the same value as [e], * but does not contain any subexpressions of the form 0+e'. *) let rec opt = function | Int n -> Int n | Neg e -> Neg (opt e) | Plus(e1,e2) -> let e1' = opt e1 in if e1'=Int 0 then opt e2 else Plus(e1',opt e2) ``` **Formally restate** the informal specification given above for `opt` and **prove the correctness** of the function. *Hint 1: define a function `no_zero_plus` that formalizes what it means to "not contain any subexpressions of the form `0+e'`". Use that function in your formal specification, much like we used `mem` and `inv` in Problem 1.* *Hint 2: you will likely need to nest a proof by case analysis inside a proof by induction.* ## Problem 3: Monads In lecture, we studied a monad for debuggable functions, which had the *effect* of producing a debug string in addition to computing a value. That monad made it easy for us to pipeline debuggable functions. Suppose that instead of producing a single string, we wanted debuggable functions to produce a list of strings. Think of that list as being like a log: as the computation of the function proceeds, it appends entries to the end of the log. ### Part A **Implement the `Logger` module** by completing the structure below. Your implementation should be linear time or better. ``` module type Monad = sig type 'a t val (>>=) : 'a t -> ('a -> 'b t) -> 'b t val return : 'a -> 'a t end module type LogMonad = sig include Monad val log : string list -> unit t end module Logger : (LogMonad with type 'a t = 'a * string list) = struct (* TODO *) end ``` Your implementation should be compatible with the following code, which logs the computation of a greatest common divisor function: ``` open Logger let rec gcdlog a b = let str = string_of_int in if b = 0 then log ["gcd is " ^ str a] >>= fun () -> return a else let s = str a ^ " mod " ^ str b ^ " = " ^ str (a mod b) in log [s] >>= fun () -> gcdlog b (a mod b) ``` Sample usage: ``` # gcdlog 31 10;; - : int t = (* : int * bytes list is also okay *) (1, ["31 mod 10 = 1"; "10 mod 1 = 0"; "gcd is 1"]) # gcdlog 20 15;; - : int t = (* : int * bytes list is also okay *) (5, ["20 mod 15 = 5"; "15 mod 5 = 0"; "gcd is 5"]) ``` ### Part B **Prove that the monad laws hold** for your implementation of `Logger`. You may use without proof any theorems and lemmas about `@` that we have stated in recitation or on exams. ``` LAW 1: return x >>= f ~ f x LAW 2: m >>= return ~ m LAW 3: (m >>= f) >>= g ~ m >>= (fun x -> f x >>= g) ``` *Hint: these proofs should be relatively simple calculations; no induction is needed.* ## Problem 4: Efficiency In Problem 1, we considered a data structure for immutable sets. Now let's consider mutable sets: ``` module type MUTABLE_SET = sig type 'a set val mem : 'a -> 'a set -> bool val empty : unit -> 'a set val add : 'a -> 'a set -> unit end ``` What should we choose as the representation type? An array is an appealing choice, especially if we stipulate as the representation invariant that the array is in sorted order. Then `mem` could be implemented with binary search and run in $O(\lg n)$ time, which is competitive with balanced binary trees. Unfortunately, `add` is not so easy to implement efficiently. A naive implementation would copy the array with each `add`, making it run in $O(n)$ time. A 3110 student has a better idea: when elements are first added to the set, temporarily store them in a list of recently added elements; and when that list gets too long, move elements from it into the array. This representation type is what the student has in mind: ``` type 'a set = { mutable sorted: 'a array; mutable recent: 'a list; mutable recent_length : int (* RI: recent_length = List.length recent *) } ``` Since cons-ing onto a list takes constant time, `add` will usually be an efficient operation. And `mem` will first search `recent` then `sorted` for the element; as long as the length of `recent` is kept small, this will be only a little slower than the naive implementation. But when elements need to be moved from `recent` to `sorted`, the `add` operation might take more than constant time. To decide when to move elements, the 3110 student assumes the existence of some function $f$; the move will occur when $m = f(n)$, where $n$ is the size of `sorted`, and $m$ is the number of elements in `recent` after adding the newest element. At that time, `recent` is sorted using mergesort, then those sorted elements and the $n$ elements from `sorted` are merged into a new array. The student is assuming that $f(n) \leq n$ for all $n$, but so far hasn't specified exactly what $f$ is. ### Part A 1. What is the running time of `mem`, expressed using $O(\cdot)$, $f$, and $n$? 2. To ensure that `mem` has a running time that is competitive with a balanced search tree&mdash; that is, $O(\lg n)$&mdash;what function should the student choose for $f$? 3. Suppose that a set currently has $n$ elements in `sorted` and that `recent` is empty. As a function of $f$ and $n$, what is the running time of $f(n)$ applications of `add`? *Hint: This should cause exactly one sort and merge*. ### Part B For certain choices of $f$, it is possible to show that `mem` and `add` both have an amortized running time of $O(\sqrt n)$, which might be better or worse than the bounds you achieved in Part A. Your task is to prove the $O(\sqrt n)$ bound using the potential method. You are free to choose a different $f$ in this part of the problem than you did in Part A. * Define a potential function $U$. * Choose a function $f$. * Show that the amortized running time of a single `mem` operation is $O(\sqrt n)$, and likewise for `add`. *Hint: Start by leaving $U$ and $f$ undetermined. Try to prove the bound for `mem`. This will help you choose $f$. Then try to prove the bound for `add`. This will help you choose $U$. You want $U$ to be 0 right after a sort and merge, and maximal just as you start a sort and merge; and you want to split whatever cost you incur in the sort and merge over all the adds that have occurred since the last sort and merge.* ## Karma There's no karma on this assignment&mdash;work on making your projects awesome instead. :)