(* Exercise 1 *) (* Look at the following type definition. *) type color = Red | Yellow | Blue | Green | Orange | Other of string type favorite = Color of color | Movie of string | Tvshow of string | Number of float | Letter of char (* We've defined some sample lists of favorite movies/colors/etc. * You can think of each of these lists as representing someone's * input describing their favorite things. * You may want to use these for testing your functions later.*) let a : favorite list = [Movie "Love Story"; Color Blue; Tvshow "The Simpsons"; Color Orange] let b : favorite list = [Number 1.0; Number 2.0; Number 5.0; Number 14.0; Number 42.0] let c : favorite list = [Movie "A Beautiful Mind"; Tvshow "House"; Letter 'P'; Color Orange] let d : favorite list = [Tvshow "Lost"; Number 3.14] let students = [a; b; c; d] (* 1a. Define a value of type favorite list for someone whose * favorite color is Aubergine and whose favorite number is 5. *) let prob1a : favorite list = [Color (Other "Aubergine"); Number 5.] (* 1b. Write a function that takes a value of type favorite list (like * those above) and returns the title of this person's favorite movie, * or None if a favorite movie isn't given. If multiple movies are * listed, return the first. What return type does this function have? *) let favmovie_type = "favorite list -> string option" let rec favmovie (lst: favorite list) : string option = match lst with | [] -> None | hd::tl -> match hd with | Movie m -> Some m | _ -> favmovie tl (* 1c. Write a function that takes a value of type favorite list and * returns true if and only if this person has listed Orange as a * favorite color. *) let princetonpride_type = "favorite list -> bool" let rec princetonpride (lst: favorite list) : bool = match lst with | [] -> false | (Color Orange)::_ -> true | _::tl -> princetonpride tl (* Exercise 2 *) (* 2a. Define an algebraic data type to represent either int or float *) type realnum = | Int of int | Float of float (* 2b. Define two functions to create realnums from an int and a float, respectively *) let real_of_int (i:int) : realnum = Int i let real_of_float (f:float) : realnum = Float f (* 2c. Define a function testing whether two realnums are equal. It shouldn't * matter whether they are ints or floats, e.g (realequal 4 4.0) => True. *) (* note: really shouldn't compare floats for equality, but done here for simplicity *) (* also: could separate int/int case, where comparison is "pure" *) let realequal (a: realnum) (b: realnum) : bool = let float_of_real (x: realnum) : float = match x with | Int y -> float_of_int y | Float y -> y in float_of_real a = float_of_real b (* Exercise 3: an expansion of last week's "form", as seen in precept *) type var = string type form = Var of var | And of forms | Or of forms and forms = form list type env = (var * bool) list (* We have defined a variable type 'var' and a boolean formula that is * made up of 'And's and 'Or's of variables. An environment is a mapping * from variables to boolean values. *) (* 3a. Write a function that given a boolean formula returns the list of all * unique variables that may be found in the bolean formula *) let fvars (f:form) : var list = let rec alreadySeen (v:var) (vl: var list) : bool = match vl with | [] -> false | hd::tl -> if hd=v then true else alreadySeen v tl in let rec aux_form (f:form) (vl: var list) : var list = match f with | Var v -> if not (alreadySeen v vl) then v::vl else vl | And x | Or x -> aux_forms x vl and aux_forms (f:forms) (vl: var list) : var list = match f with | [] -> vl | hd::tl -> aux_forms tl (aux_form hd vl) in aux_form f [] (* 3b. Write a function that takes a boolean formula and returns * Some e -- if there exists a satisfying environment for the formula * (and e is one such satisfying assignment) * None -- if there does not exist a satisfying assignment *) (* lookup, eval, and evals from precept *) let rec lookup (e: env) (x:var) : bool = match e with | [] -> failwith (x^" is not in e") | (hd_v, hd_b)::tl_e -> if x = hd_v then hd_b else lookup tl_e x let rec eval (e:env) (f:form) : bool = match f with | Var x -> lookup e x | Or fs -> evals e fs false (||) | And fs -> evals e fs true (&&) and evals (e:env) (fs:forms) (b:bool) (op:bool->bool->bool) : bool = match fs with | [] -> b | hd::tl -> op (evals e tl b op) (eval e hd) let is_Sat (f: form) : env option = let rec aux (f: form) (e:env) (vl: var list) : env option = match vl with | [] -> if eval e f then Some e else None | hd::tl -> match aux f ((hd,true)::e) tl with | Some re -> Some re | None -> match aux f ((hd,false)::e) tl with | Some re -> Some re | None -> None in aux f [] (fvars f) (* 3c. Reimplement the types and functions from the rest of part3 to * include a negation formula (Not of form'). For the autograder, add ' * to each type or function name (e.g. types var', form', forms', env' * and functions fvars' and is_Sat' *) type var' = string type form' = Var of var' | Not of form' | And of forms' | Or of forms' and forms' = form' list type env' = (var' * bool) list let fvars' (f:form') : var' list = let rec alreadySeen (v:var') (vl: var' list) : bool = match vl with | [] -> false | hd::tl -> if hd=v then true else alreadySeen v tl in let rec aux_form (f:form') (vl: var' list) : var' list = match f with | Var v -> if not (alreadySeen v vl) then v::vl else vl | And x | Or x -> aux_forms x vl | Not x -> aux_form x vl and aux_forms (f:forms') (vl: var' list) : var list = match f with | [] -> vl | hd::tl -> aux_forms tl (aux_form hd vl) in aux_form f [] let rec lookup' (e: env') (x:var') : bool = match e with | [] -> failwith (x^" is not in e") | (hd_v, hd_b)::tl_e -> if x = hd_v then hd_b else lookup' tl_e x let rec eval' (e:env') (f:form') : bool = match f with | Var x -> lookup' e x | Or fs -> evals' e fs false (||) | And fs -> evals' e fs true (&&) | Not f' -> not (eval' e f') and evals' (e:env') (fs:forms') (b:bool) (op:bool->bool->bool) : bool = match fs with | [] -> b | hd::tl -> op (evals' e tl b op) (eval' e hd) let is_Sat' (f: form') : env' option = let rec aux (f: form') (e:env') (vl: var' list) : env' option = match vl with | [] -> if eval' e f then Some e else None | hd::tl -> match aux f ((hd,true)::e) tl with | Some re -> Some re | None -> match aux f ((hd,false)::e) tl with | Some re -> Some re | None -> None in aux f [] (fvars' f) (* Exercise 4 *) (* 4a. Given the function below, give a short proof that * double N = 2*N *) let double (n: int) : int = n + n (* Theorem: double N = 2*N Lemma: + and * are total functions Proof by substitution. (1) double N left side of theorem (2) N + N eval double (3) N*(1 + 1) distributive property (4) 2*N math (addition and commutative property of * ) *) (* 4b. Given the function below, prove that for any natural number N: sum_sqrs N = (N * (N+1) * (2*N + 1))/6 You may assume that we have already proved this lemma: If N=k+1 and N is a natural number > 0, then k must also be a natural number *) let rec sum_sqrs (n: int) : int = if n <= 0 then 0 else (n*n) + sum_sqrs(n-1) (* Theorem: sum_sqrs N = (N * (N+1) * (2*N +1))/6 Lemma: N is a positive integer k+1, so k is a natural number Proof by induction over the natural numbers with two cases Case: N=0, by simple equational reasoning IMS : sum_sqrs 0 = (0 * (0+1) * (2*0 + 1))/6 (1) sum_sqrs 0 LHS (2) if 0 <= 0 then 0 eval sum_sqrs (3) 0 eval if (4) 0/6 math (5) (0*(0+1)*(2*0+1))/6 math Case: N=k+1 IMS : sum_sqrs (k+1) = ((k+1) * ((k+1)+1) * (2*(k+1)+1))/6 IH : sum_sqrs (k) = ((k) * ((k)+1) * (2*(k)+1))/6 (1) sum_sqrs (k+1) LHS (2) if ... else (k+1)*(k+1) + sum_sqrs ((k+1)-1) eval sum_sqrs (3) (k+1)*(k+1) + sum_sqrs k eval if, math (4) (k+1)*(k+1) + ((k) * ((k)+1) * (2*(k)+1))/6 IH (5) (k+1) * ((k+1) + ((k) * (2*k+1))/6) distributive property (6) (k+1) * ((6k+6) + (k) * (2*k+1))/6 math (7) (k+1) * (2k^2 + 7k + 6)/6 math (8) (k+1) * (k+2)*(2k+3)/6 math (9) (k+1) * ((k+1)+1) * (2*(k+1)+1) / 6 math *) (* 4c. Given the functions below, prove that for any list: behead ( prepend xs x) = xs *) let prepend (xs: 'a list) (x: 'a) : 'a list = x::xs let behead (xs: 'a list) = match xs with | [] -> [] | hd::tl -> tl (* Theorem: behead ( prepend xs x ) = xs Proof by simple equational reasoning. NB: this looks like a proof that will need two cases, but in fact it doesn't, because we never use any property of xs, thus it doesn't matter if xs is empty or not. (1) behead ( prepend xs x ) LHS (2) behead ( x::xs ) eval prepend (3) match (x::xs) with eval behead | hd::tl -> tl (4) xs eval match *) (* 4d. Given the function below, prove that for any list: noop xs = xs *) let rec noop (xs: 'a list) : 'a list = match xs with | [] -> [] | hd::tl -> hd :: noop tl (* Theorem: noop xs = xs Proof by induction over the structure of lists Case: xs=[], by simple equational reasoning IMS : noop [] = [] (1) noop [] LHS (2) match [] with eval noop | [] -> [] (3) [] eval match Case: xs=xh::xt IMS : noop (xh::xt) = xh::xt IH : noop xt = xt (1) noop (xh::xt) LHS (2) match (xh::xt) with eval noop | hd::tl -> hd :: noop tl (3) xh :: noop xt eval match (4) xh :: xt IH *)