(* Precept 5: Proofs about Fuctional Programs *) (* This precept will help familiarize you with material on proving * things about programs. As part of your homework this week, you must * read the online notes about proving things about programs. *) (* Refer to these notes to help you through this week's precept * materials: * http://www.cs.princeton.edu/~cos326/notes/reasoning.php * http://www.cs.princeton.edu/~cos326/notes/reasoning-data.php *) (* * 1. Consider the function tail, below. * * Is tail a total function? * * Is tail [] a valuable expression? * * Is tail [3] a valuable expression? *) let tail (xs: 'a list) : 'a list = match xs with hd :: tail -> tail (* * 2. Consider the function safediv, below. * * Is safediv a total function? * * Is safediv (1, 0) valuable? *) let safediv (nums : int * int) : int option = let (x,y) = nums in if y == 0 then None else Some (x/y) (* * 3. Consider the following type and function declarations * * Is free_var total? * * Is free_vars total? *) type form = Var of string | And of form list let rec free_var (f : form) = match f with Var s -> [s] | And fs -> free_vars fs and free_vars (fs: form list) = match fs with [] -> [] | f :: rest -> free_var f @ free_vars rest (* * 4. Consider the mutually recursive functions f and g: * * Is f total? * * Is g total? *) let rec f (x:int) = if x > 50 then 1 + f (x-1) else g x and g (y: int) = if y > 0 then 1 else f (y-1) (* * 5. Consider f', a function used by g', and the definition of g' * * What do we need to know about f' to know that g' is total? *) let f' x = (* some definition *) let g' x = if f' x then 1 else 0 (* 6. Given the definition of inc, give justifications for each of the * equations below using the equational rules given in the online * notes. Whenever you need to use reflexivity, transitivity, * symmetry, congruence, etc., say so. *) (* inc 3 == 4 * inc 4 == 5 * inc (inc 3) == 5 * fun x -> x + 1 == inc * for all values v, v + 1 == inc v * for all valuable expressions e, e + 1 == inc e *) let inc x = x + 1 (* 7. Consider the function multo, below: *) let multo (x:int option) (y:int option) = match (x,y) with (Some m, Some n) -> Some ((m + m)*n) | (_, _) -> None (* Prove the following equation holds, step by step, * for all o : int option. * Note: You can start top down, or you can start bottom up, * or go from both ends to meet in the middle. *) multo o o == (match o with Some i -> Some (2*(i*i)) | None -> None) (* Proof: *) (* 8. Consider the function compose, below: *) let compose (f:'a -> 'b) (g:'b -> 'c) (x:'a) = g (f x) in (* Prove the following equation holds, step by step, for all n : int *) compose (fun x -> x * 2) (fun y -> y * 8) n == compose (fun z -> z * 4) (fun w -> w * 4) n (* Proof: *) (* 9. Consider the functions double and half, below: *) let rec double (xs: int list) : int list = match xs with [] -> [] | hd :: rest -> hd::hd::double rest let rec half (xs: int list) : int list = match xs with [] -> [] | [x] -> [] | x::y::rest -> y::half rest (* Disprove this conjecture: for all l, double(half l) == l. * Rhetorical question: How does one disprove such a conjecture? *) (* Proof: *) (* Prove that for all integer lists l. half (double l) == l. * Structure your proof as an inductive proof in two cases * on the structure of the list l. *) (* Proof: *) (* 10. Recall the familiar map and function composition operators, below. * Note that (%%) is the same as the function compose from problem 8, * but defined using an infix operator instead, just for fun. *) let rec map (f: 'a -> 'b) (xs : 'a list) : 'b list = match xs with [] -> [] | hd::tail -> f hd :: map f tail let (%%) (g:'b -> 'c) (f:'a -> 'b) (x:'a) : 'c = g (f x) (* A common program optimization is to take a series of several map * operations and compress them in to a single map operation. Instead * of traversing a list multiple times (once for each application of * the map operation), one only traverses the list once. More * specifically, the following property of map is true (for any total * functions f and g with the correct types): *) map (g %% f) == (map g) %% (map f) (* We are going to prove this fact with the aid of the following * lemma: * For all types 'a, 'b and values f : 'a -> 'b, if f is total then map f is valuable and total. * * Now the theorem. We will provide each step in the proof of the * theorem. It is up to you to provide the correct justification. * However, you can omit mentioning reflexivity, transitivity, * symmetry or congruence explicitly (just use these laws wherever * you see fit from now on without mentioning them). * * * For all types 'a, 'b, 'c and for all values f : 'a ->'b and g : 'b -> 'c and l : 'a list, * if f and g are total then ((map g) %% (map f)) l == map (g %% f) l *) (* * Facts we know, observations, and justifications: * * 1. f is total Given * 2. g is total Given * * 3. map f is valuable and total * 4. map g is valuable and total * 5. g %% f is valuable * 6. g %% f is total * 7. map (g %% f) is valuable and total * * 8. ((map g) %% (map f)) l == (fun x -> map g (map f y)) l * 9. == map g (map f l) * * 10. thus, by transitivity of equality, we only have to prove that: * map g (map f l) == map (g %% f) l * * Structure your proof as an inductive proof in two cases * on the structure of the list l. * * Proof: *)