<![CDATA[
# 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–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— that is, $O(\lg n)$—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—work on making your
projects awesome instead. :)
]]>