CS611 Homework 6 DUE: December 7, 2001What to turn inTurn in the assignment during class on the due date.1. Strong normalization (25 pts.)(a) (20 pts.) Show that all expressions in the language λ→×+are strongly normalizing by extendingthe proof of strong normalization for λ→.(b) (5 pts.) Where does the proof fail if we add recursive types to the language?2. Object encodings (35 pts.)In this problem we will examine two ways to encode object types. These formulations give some insightinto sound subtyping rules for object types in object-oriented languages. Let us consider the typedlambda calculus extended with pairs, records, recursive types, existential types, and subtyping:e ::= b | x | λx : τ.e | e0e1| he0, e1i | left e | right e | {l1= e1, . . . , ln= en} | e.l |pack [X = τ, e] | unpack e as [X, x] in e0| foldµX.τe | unfold eτ ::= B | X | τ → τ0| τ ∗ τ0| {l1: τ1, . . . , ln: τn} | µX.τ | ∃X.τWe define a context ∆ to contain the type variables in scope:∆ ::= ∅ | ∆, Xand augment this definition with the usual rules about the irrelevance of ordering type variables in ∆.A judgment of the form ∆ ` τ asserts that τ is well-formed in ∆. Thus, we have:∆ ` B ∆, X ` X∆ ` τ ∆ ` τ0∆ ` τ → τ0∆ ` τ ∆ ` τ0∆ ` τ ∗ τ0∆ ` τ∀i∈{1,...,n}i∆ ` {l1: τ1, . . . , ln: τn}∆, X ` τ∆ ` µX.τ∆, X ` τ∆ ` ∃X.τEncoding as recursive recordsOne way to model objects is as recursive record types of the form µX.{l1: τ1, . . . , ln: τn}. For instance:point = µP.{x : real, y : real}mvpoint = µQ.{x : real, y : real, move : real → real → Q}To construct a point object we might write the function:make point = λa : real. λb : real. foldpoint{x = a, y = b}The rules for subtyping in this language can be obtained by modifying the rules given in class for typeequivalence in the typed lambda calculus extended with recursive types. As with type equivalence, wedefine a context E containing a set of assumed subtype relations τ1≤ τ2, and use the following rule toterminate the unfolding of recursive types:∆; E, τ1≤ τ2` τ1≤ τ21Recall the subtyping rules for function types, pairs, and records:∆; E ` τ01≤ τ1∆; E ` τ2≤ τ02∆; E ` τ1→ τ2≤ τ01→ τ02∆; E ` τ1≤ τ01∆; E ` τ2≤ τ02∆; E ` τ1∗ τ2≤ τ01∗ τ02∆; E ` τi≤ τ0i∀i∈{1,...,n}∆; E ` {l1: τ1, . . . , lm: τm} ≤ {l1: τ01, . . . , ln: τ0n}where m ≥ n(a) (5 pts.) Give the inference rules defining the subtype judgments ∆; E ` µX.τ ≤ τ0and ∆; E `τ0≤ µX.τ , where τ0does not have the form µY.τ00.(b) (5 pts.) Give the inference rule defining the subtype judgment ∆; E ` µX.τ ≤ µY.τ0.(c) (5 pts.) According to the rules you have given, we should have mvpoint ≤ point. Say whethereach of the following putative subtype relationships also holds. If the relationship holds, give asubtype derivation (proof tree). If it does not hold, give a counter-example: code demonstratingthat the subtype relationship would be unsafe.i. µP.{x : P } ≤ µQ.{x : Q}ii. µP.{mv : int → P, y : int} ≤ µQ.{mv : int → Q}iii. µP.{eq : P → bool, y : int} ≤ µQ.{eq : Q → bool}iv. µP.{a : ref P, y : int} ≤ µQ.{a : ref Q} (Note that ref τ ≤ ref τ0iff τ∼=τ0).v. µP.{l : P, r : P, v : int} ≤ µQ.{l : Q, r : Q}Encoding as recursive records with existentialsOne problem with the recursive record encoding is that an object’s implementation is visible to itsclients. In languages such as Smalltalk, Java, or C++, the implementation may be hidden by declaringsome fields of the object private; in fact, in Smalltalk, all class members are private and clients canaccess the object only through its method interface.To model this property, we hide the implementation of an object using existential types. We treatobjects as a pair of a state, represented by the type variable X, and a record of methods, each of whichtakes an argument of type X. This argument can be considered analogous to this in Java or C++ orself in Smalltalk. As an example, we might encode the point type above aspoint = µP. ∃X.X ∗ {x : X → real, y : X → real}Note that we are no longer constrained to implement a point as a record of two reals with named x andy. For instance, we might implement a point as a pair using polar coordinates and define the followingfunction to create a new point from its Cartesian coordinates:make point = λa : real. λb : real.letrec m : {x : (real ∗ real) → real, y : (real ∗ real) → real} = {x = λs : (real ∗ real). (left s) ∗ cos(right s),y = λs : (real ∗ real). (left s) ∗ sin(right s)} inlet r = sqrt(a ∗ a + b ∗ b) inlet θ = arcsin(b/r) infoldpoint(pack [X = real ∗ real, hhr, θi, mi])Now, to call the method x on a point p, we do:unpack (unfold p) as [X, o] inlet s : X = (left o) inlet m : {x : X → real, y : X → real} = (right o) in(m.x s)Observe that the caller does not know the implementation of the state X.2(d) (3 pts.) Using this encoding, what is the type encoding of mvpoint?(e) (5 pts.) Define a function make mvpoint which, given two reals, returns a new mvpoint representingthat point. The move method should take two real numbers dx and dy and return a new mvpointwhere the x and y coordinates of the original point are offset by dx and dy, respectively. You arefree to implement an mvpoint’s state in any way you choose.(f) (10 pts.) Give the inference rule defining the subtype judgment ∆; E ` ∃X.τ ≤ ∃X0.τ0. The ruleshould not require that the types be equivalent; however, if the subtype relation holds in bothdirections, the rule should enforce equivalence of the two types.(g) (2 pts.) Show that ∅; ∅ ` mvpoint ≤ point.3. Encoding sum and product types in the polymorphic lambda calculus (40 pts.)Sum types and product types, as seen in λ→×+, are important features in programming languages.In this problem, we will show that by using some insights from the Curry-Howard isomorphism, sumtypes in λ→×+can be encoded using product types and universal types in the polymorphic lambdacalculus. Similarly, we can encode product types as sum types.Our source language will consist of the simply typed language extended with sum and product types.τ ::= B | τ1→ τ2| τ1+ τ2| τ1∗ τ2e ::= b | x | λx:τ. e | e1e2| inlτ1+τ2e | inrτ1+τ2e | case e0of e1|e2| he1, e2i | left e | right eThe typing rules for this language are the same as defined in lecture