CIS 500 — Software FoundationsFinal ExamDecember 14, 2005If taking the exam for WPE credit:WPE-I id:Otherwise:Name:EmailStatus registered for the coursenot registeredScore1234567891011121314TotalInstructions• This is a closed-book exam: you may not make use of any books or notes.• You have 120 minutes to answer all of the questions. The entire exam is worth 120 points.• Questions vary significantly in difficulty, and the point values of questions may not be exactly pro-portional to their difficulty. Do not spend too much time on any one question.• It is a good idea to read through the entire exa m before starting to work hard on individual problems.• Partial credit will be given wherever possible. All correct answers are short. The back side of eachpage may be used as a scratch pad.• Good luck!1True/False questionsFor each of the following stat ements, c ircle T if the sentence is true or F otherwise.1. (9 points)(a) T F The small-step evaluation relation of a language must be deterministic (i.e. for any termthere should be only way for it to take a step) for the preservation theorem to hold.(b) T F The uniqueness of types property (i.e. , in a given context Γ, a term t has at most onetype T. Furthermore, there is exactly one derivation of Γ ⊢ t : T.) must be true abouta language to prove the preservation theorem.(c) T F If the preservation theorem is true for a language, removing a typing rule may cause itto become untrue.(d) T F If the progress theorem is true for a language, removing a typing rule may cause it tobecome untrue.(e) T F In the pure untyped lambda calculus (without booleans, natural numbers, or anythingother than functions) all closed terms will either diverge or evaluate to a value. (Forreference, this language is shown on page 1 of the c ompanion handout.)(f) T F The algorithmic rules for the lambda calculus with subtyping has the uniqueness oftypes property. (For reference, this language is shown on page 4 of the companionhandout.)(g) T F The declarative rules for the lambda calculus with subtyping has the uniqueness oftypes property. (For reference, this language is shown on page 5 of the companionhandout.)(h) T F In Featherweight Java (FJ), all programs will either diverge or evaluate to a value. (Forreference, this language is shown on page 9 of the c ompanion handout.)(i) T F FJ is specified with a large-step operational semantics.2Inductive definitions2. (14 points) We can de fine a simple term language as follows:t ::= 2∗t ∧ tNow consider the following binary relation between these terms, specified by the following inferencerules:AX1∗ ∼ 2AX22 ∼ ∗t1∼ t4t2∼ t3AMP1(t1∧ t2) ∼ (t3∧ t4)(t2∧ t1) ∼ (t4∧ t3)AMP2(t1∧ t2) ∼ (t3∧ t4)(a) Draw a derivation for (∗ ∧ 2) ∼ (∗ ∧ 2)(b) As you may have noticed, this set of rules is not-syntax directed. Give a different derivation for(∗ ∧ 2) ∼ (∗ ∧ 2).3(c) Fortunately, we can remove e xactly one rule and produce a relation that (a) is syntax-directedand (b) equivalent to the previous relation. Which rule should we eliminate?(d) For any x does there exist at least one y such that x ∼ y? If yes, prove it. If no, show a counterex-ample. Be ex p licit in your answer, but to the point. Points may be deducted for any extraneousinformation (true or false).4Untyped lambda-calculusThe following questions refer to the untyped lambda- calculus. The syntax and evaluation rules for this systemare given on page 1 of the companion handout.3. (12 points) Circle the normal forms of the following lambda calculus terms, if one exists. If there isno normal form, circle NONE. (Recall that the normal form of t is a term u such that t −→∗u andu 6−→.)(a) (λy. (λz. x y)) (λx. z)i. (λy. (λz. x y)) (λx. z)ii. (λz. x (λx. z))iii. (λw. (λx.z) (λx.z))iv. (λw. x (λx.z))v. NONE(b) (λy. (λz. z z ) y)(λx. x)i. (λy. (λz. z z ) y)(λx. x)ii. (λz. z z)(λx.x)iii. (λx. x)iv. (λy. y y)(λz.z)v. NONE(c) (λx. x x x) (λx. x x x)i. (λx. x x x) (λx. x x x)ii. (λx. x x x)iii. (λx. x x x)(λx. x x x)(λx. x x x)iv. x x xv. NONE(d) (λx. (λy. y y)(λz. z z))i. (λx. (λy. y y)(λz. z z))ii. (λx. (λy. y y))iii. (λy. (λz. z z))iv. (λy. y y)(λz. z z)v. NONE5Recall the encoding of booleans and numbers in the untyped lambda calculus from Chapter 5 ofTAPL. The next two questions concern that encoding.tru = λt. λf. tfls = λt. λf. fc0= λs.λz.zscc = λn. λs. λz. s (n s z)4. (3 points) Which of these lambda calculus terms implements xor (the exclusive or function, whichreturns tru when exactly one of its arguments is tru.)(a) λx. λy. x (y fls tru) (y tru fls)(b) λx. λy. x y y(c) λx. λy. tru x y(d) λx. λy. x y fls5. (3 points) Which of these lambda calculus terms implements odd, a function that returns tru if itsargument (the encoding of a natural number) is odd and fls otherwise.(a) λm. m (λn. n fls tru) fls(b) λm. m fls (λn. tru fls)(c) λm. fls (λn. n m tru)(d) λm. m (λn. tru) fls6Implementing simple type systemsThe following questions refer to the Arith language, a typed calculus with booleans and natural numbers. Thesyntax, typing, and evaluation rules for this system are given on page 2 of the companion handout.6. (12 points) The eval1 function below implements the small-step evaluation relation almost correctly,but there are mistakes in the TmIf, TmSucc, TmPred and TmIsZero cases of the outer match. Showhow to change the c ode to repair at least one mistake in each branch. (For simplicity, file informationhas been omitted from the datatype.)type exp =TmZero | TmSucc of exp | TmPred of exp| TmIsZero of exp| TmTrue | TmFalse | TmIf of exp*exp*explet rec isnumericval t = ... (*returns true when t is a numeric value*)let rec isval t = ... (*returns true when t is a value.*)exception NoRuleApplieslet rec eval1 t = match t withv when isval v → raise NoRuleApplies| TmIf(t1,t2,t3) →(match t1 withTmTrue → t2| TmFalse → t3| _ → raise NoRuleApplies)| TmSucc(t1) → TmSucc(t1)| TmPred(t1) →(match t1 withTmZero → TmZero| TmSucc(nv1) → nv1| _ → TmPred(eval1 t1))| TmIsZero(t1) →(match t1 withTmZero → TmFalse| TmSucc(nv1) when isnumericval nv1 → TmFalse| _ → TmIsZero(eval1 t1))78Simply typed lambda-calculus with subtyping, records, and referencesThe following questions refer to the simply typ ed lambda-calculus with subtyping, records, and references. Thesyntax, typing, and evaluation rules for this system are given on page 5