CIS 500 — Software FoundationsFinal ExamDecember 20, 2006Name or WPE-I Id:Score1234567891011TotalInstructions• This is a closed-book exam.• 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 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 and the companionhandout may be used as scratch paper.• Good luck!1Inductively Defined RelationsDefine the syntactic categories of blobs (written x) and counts (written y) as follows:x ::= ♯♭♮x · xy ::= 0+y−yThat is, a blob is a tree whose leaves are labeled ♯, ♮, or ♭; a count is a sequence of +s and −s ending in 0.Now define the relation “accumulating x onto y yields y′,” written x y y ⊲ y′, as the least three-placerelation closed under the following rules:♯ y y ⊲ +y(Sharp)♭ y y ⊲ −y(Flat)♮ y y ⊲ y(Natural)x1y y ⊲ y′′x2y y′′⊲ y′x1· x2y y ⊲ y′(Dot)x2· x1y y ⊲ y′x1· x2y y ⊲ y′(Swap)Notice that the result of accumulating x onto y always has y itself as a suffix, and that it additionally includesone + for every ♯ in x and one − for every ♭ in x. The middle component of the relation, y, is analogous tothe “accumulator parameter” sometimes used by tail-recursive OCaml functions. The Swap rule introducessome flexibility in the order of +s and −s in y′, relative to the positions of ♯s and ♭s in x.21. (6 points) Are the following statements derivable? (Write YES or NO for each.)(a) ♯ · (♮ · ♮) y 0 ⊲ +0(b) ♯ · (♯ · ♭) y 0 ⊲ + − +0(c) (♯ · ♮) · (♭ · ♮) y +0 ⊲ + + −032. (20 p oints) Write a careful inductive proof of the following fact. Make sure to explictly mention everystep in the proof (use of an assumption, use of the induction hypothesis, use of one of the inferencerules, etc.).Fact: For every x there is some y′such that x y 0 ⊲ y′4Untyped Lambda-CalculusThe following problem concerns the untyped lambda-calculus. This system is summarized on page 1of the companion handout.3. (6 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 observationally equivalent.For each of the following pairs of terms, write YES if the terms are behaviorally equivalent and NO ifthey are not.(a) (λx. λy. x (λz. z) y)and (λx. λy. (λz. z) x y)(b) (λs. λz. s (s z))and (λn. λs. λz. s (n s z)) (λs. λz. s z)(c) (λx. x x) (λx. x x)and Z (λg. λh. h) (λz. z)where Z = (λf. λy. (λx. f (λy. x x y)) (λx. f (λy. x x y)) y), as in lecture notes5SubtypingThe following problems concern the simply typed lambda-calculus with subtyping (and records, vari-ants, and references). This system is summarized on page 2 of the companion handout.4. (10 points) Circle T or F for each of the following statements.(a) There is an infinite descending chain of distinct types in the subtype relation—that is, an infinitesequence of types S0, S1, etc., such that all the Si’s are different and each Si+1is a subtype of Si.T F(b) There is an infinite ascending chain of distinct types in the subtype relation—that is, an infinitesequence of types S0, S1, etc., such that all the Si’s are different and each Si+1is a supertype ofSi.T F(c) There exists a type that is a subtype of every other type.T F(d) There exists a record type that is a subtype of every other record type.T F(e) There exists a variant type that is a subtype of every other variant type.T F65. (15 points) The standard subtyping rule for references is:T1<: S1S1<: T1Ref S1<: Ref T1(S-Ref)Suppose we drop the first premise so that Ref becomes a covariant type constructor:S1<: T1Ref S1<: Ref T1(S-Ref-New)Indicate whether each of the following properties remains true (write “TRUE”) or becomes false (write“FALSE”), and briefly explain why.(a) Progress: Suppose t is a closed, well-typed term (that is, ∅|Σ ⊢ t : T for some T and Σ). Theneither t is a value or else, for any store µ such that ∅|Σ ⊢ µ, there is some term t′and store µ′with t|µ −→ t′|µ′.(b) Preservation: IfΓ|Σ ⊢ t : TΓ|Σ ⊢ µt|µ −→ t′|µ′then, for some Σ′⊇ Σ,Γ|Σ′⊢ t′: TΓ|Σ′⊢ µ′.(c) Existence of joins: For every pair of types S and T there is some type J such that S and T areboth subtypes of J and such that, for any other type U, if S and T are both subtypes of U, then Jis a subtype of U.7Object Encodings in Lambda-CalculusThe questions in this section are based the following small class hierarchy encoded in lambda-calculus.(Note that this encoding is in the simpler style of section 18.11 of TAPL; it does not incorporate therefinements for improved efficiency discussed at the very end of the chapter, in 18.12.)/* A couple of miscellaneous helper functions -- "not" on booleans... */not = λb:Bool. if b then false else true;/* and a comparison function for numbers: */leq =fix (λf:Nat→Nat→Bool.λm:Nat. λn:Nat.if iszero m then trueelse if iszero n then falseelse f (pred m) (pred n));/* The interface type of "pair objects": */Pair = {set1:Nat→Unit, set2:Nat→Unit, lessoreq:Unit→Bool, greater:Unit→Bool};/* The internal representation of "pair objects": */PairRep = {x1: Ref Nat, x2:Ref Nat};/* A class of "abstract pair objects." Note that the lessoreq andgreater methods call each other recursively. */absPairClass =λr:PairRep.λself: Unit→Pair.λ_:Unit.{set1 = λi:Nat. r.x1:=i,set2 = λi:Nat. r.x2:=i,lessoreq = λ_:Unit. not ((self unit).greater unit),greater = λ_:Unit. not ((self unit).lessoreq unit)};/* A function that creates a new abstract pair object: */newAbsPair =λ_:Unit. let r = {x1=ref 0, x2=ref 0} infix (absPairClass r) unit;/* A subclass that overrides the lessoreq method: */pairClass =λr:PairRep.λself: Unit→Pair.λ_:Unit.let super = absPairClass r self unit in{set1 = super.set1,set2 = super.set2,lessoreq = λ_:Unit. leq (!(r.x1)) (!(r.x2)),greater =