CIS 500 — Software FoundationsMidterm IAnswer keyOctober 11, 2006Instructions• This is a closed-book exam: you may not use any books or notes.• You have 80 minutes to answer all of the questions. The entire exam is worth 80 points for studentsin section 002 and 90 points for students in section 001 (there is one PhD-section-only problem).• Questions vary significantly in difficulty, and the point value of a given question is not always exactlyproportional to its difficulty. Do not spend too much time on any one question.• Partial credit will be given. All correct answers are short. The back side of each page may be used asa scratch pad.• Good luck!1OCaml1. (5 points) The forall function takes a predicate p (a one-argument function returning a boolean)and a list l; it returns true if p returns true on every element of l and false otherwise.# forall (fun x -> x >= 3) [2;11;4];;- : bool = false# forall (fun x -> x >= 3) [3;4;5];;- : bool = true(a) What is the type of forall? Answer: (’a → bool) → ’a list → bool(b) Complete the following definition of forall as a recursive function: Answer:let rec forall p l =match l with| [] -> true| h::t -> (p h) && forall p tGrading scheme: (a) gets 0/2 for completely wrong type, 1/2 for small mistakes (e.g. not polymorphictype), 2/2 otherwise. (b) gets 0/3 for completely wrong functions, 1/3 if there is some pattern match-ing involved, 2/3 for simple mistakes such as base case error and 3/3 for various completely correctsolutions.2. (5 points) Recall the function fold discussed in class:# let rec fold f l acc =match l with[] -> acc| a::l -> f a (fold f l acc);;val fold : (’a -> ’b -> ’b) -> ’a list -> ’b -> ’bComplete the following definition of forall by supplying appropriate arguments to fold:Answer:let forall p l = fold (fun x acc → (p x) && acc) l trueGrading scheme: Roughly one point for right number/type of arguments, one point for the right initialaccumulator, three points for the function:0: Blank.1: Major omissions and errors: e.g., omitting f entirely, or wrong f and an integer as initial accu-mulator.2: Correct number and types of arguments, but f wrong. Most common:let forall p l = fold p l true3: f argument has right type, or right body, but two minor errors.4: One minor error.5: Perfect.2Untyped lambda-calculusThe following questions are about the untyped lambda calculus. For reference, the definition of thislanguage appears on page 13 at the end of the exam.Recall the definitions of the following lambda-terms from the book and/or lecture notes:/* A dummy "unit value", for forcing thunks */unit = λx. x;/* Standard definition of booleans */tru = λt. λf. t;fls = λt. λf. f;not = λb. b fls tru;test = λb. λt. λf. b t f unit;/* Standard definition of pairs */fst = λp. p tru;snd = λp. p fls;pair = λx. λy. λsel. sel x y;/* Standard call-by-value fixed point function. */fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y));/* Standard definitions of church numerals and arithmetic operations */c0 = λs. λz. z;c1 = λs. λz. s z;c2 = λs. λz. s (s z);c3 = λs. λz. s (s (s z));c4 = λs. λz. s (s (s (s z)));c5 = λs. λz. s (s (s (s (s z))));c6 = λs. λz. s (s (s (s (s (s z)))));scc = λn. λs. λz. s (n s z);iszro = λm. m (λdummy. fls) tru;zz = pair c0 c0;ss = λp. pair (snd p) (scc (snd p));prd = λm. fst (m ss zz);33. (6 points) Circle the term that each of the following lambda calculus terms steps to, using the single-step evaluation relation t −→ t0. If the term is a normal form, circle DOESN’T STEP.(a) (λx.x) (λx. x x) (λx. x x)i. (λx. x) (λx. x x) (λx. x x)ii. (λx. x x) (λx. x x)iii. (λx0. (λx. x x)) (λx. x x)iv. (λx. x) (λx. x x)v. DOESN’T STEPAnswer: (ii)(b) (λx. (λ x.x) (λx. x x))i. (λx. (λ x.x) (λx. x x))ii. (λx. (λx. x x))iii. (λx. (λx. x))iv. (λx. x) (λx. x x)v. DOESN’T STEPAnswer: (v)(c) (λx. (λz. λx. x z) x) (λx. x x)i. (λx. (λ z. λx. x z) x) (λx. x x)ii. (λz. λx0. (λx. x x) z) (λx. x x)iii. (λz. λ x. x z) (λx. x x)iv. (λx. x (λx. x x))v. DOESN’T STEPAnswer: (iii)Grading scheme: Two points for each.44. (10 points) Recall the definitions of observational and behavioral equivalence from the lecture notes:• Two terms s and t are observationally equivalent iff either both are normalizable (i.e., they reacha normal form after a finite number of evaluation steps) or both are divergent.• Terms s and t are behaviorally equivalent iff, for every finite sequence of values v1, v2, ..., vn(including the empty sequence), the applicationss v1v2... vnandt v1v2... vnare obser vationally equivalent.For each of the following pairs of terms, write Yes if the terms are behaviorally equivalent and No ifthey are not.(a) plus c2c1c3Answer: Yes(b) truλx. λy. (λz. z) xAnswer: Yes(c) λx. λy. x yλx. λy. x (λz. z) yAnswer: No(d) (λx. x x) (λx. x x)λx. (λx. x x) (λx. x x)Answer: No(e) λx. λy. x yλx. xAnswer: YesGrading scheme: Two points for each.55. (12 points) Complete the following definition of a lambda-term equal that implements a recursiveequality function on Church numerals. For example, equal c0 c0 and equal c2 c2 should be behav-iorally equivalent to tru, while equal c0 c1 and equal c5 c0 should be b ehaviorally equivalent tofls. You may freely use the lambda-terms defined on page 3.equal =fix (λe.λm. λn.test (iszro m)ANSWER:(λdummy. (iszro n))(λdummy.test (not (iszro n))(λdummy. e (prd m) (prd n))(λdummy. fls)))Grading scheme:• For getting the three main branches right:– 2pts for first branch, need to test (iszro n) and return fls– in second branch, need to test (iszro n) and return ( 2pts ) true or ( 2pts ) (e (prd n) (prd m).• 2pts for using test correctly (i.e., use of thunks)• 2pts for understanding how to right a recursive function with fix (i.e., use e, not equal)• 2pts for getting everything else right.6Simple types for numbers and booleans6. (18 points) Recall the following properties of the language of numbers and booleans:• Progress: If ` t : T, then either t is a value or else t −→ t0for some t0.• Preservation: If Γ ` t : T and t −→ t0, then Γ ` t0: T.• Uniqueness of types: Each term t has at most one type, and if t has a type, then there isexactly one derivation of that typing.Each part of this exercise suggests a different way of changing the language of typed arithmetic andboolean expressions (see page 11 for reference). Note that these changes are not cumulative: