CS611 Homework 5 DUE: 26 November 2001What to turn inTurn in the written parts of the assignment during class on the due date. For the programming part, youshould mail your version of the file cpsTranslate.ml to [email protected] by 5pm on that day.1. Recursive types (20 pts.)Once we add recursive types to the simply-typed lambda calculus, we see that the untyped lambdacalculus is a subset of the simply-typed lambda calculus in which every variable is declared to havethe type Λ = µX.X → X. An arbitrary lambda calculus expression can be desugared to the typedlambda calculus with recursive types as follows:D[[x]] = xD[[λx . e]] = (foldΛ(λx : Λ. D[[e]]))D[[e0e1]] = ((unfold D[[e0]]) D[[e1]])In the untyped lambda calculus, a rec operator is not necessary because we can write a closed expressionY that has the same effect. Using the desugaring above, we can obtain a version of Y for the typedlambda calculus with recursive types. For this problem, we will assume that the language has lazy(normal order) evaluation, so either form of the Y operator that we saw earlier in lecture will work.However, the desugared Y operator is not generally useful in the typed lambda calculus because ittakes fixed points only for functions from µX.X → X to the same type. For a given type τ, we candefine an operator Yτthat takes fixed points over τ . Write the appropriate typed lambda expressionfor Yτ. Make sure that your expression can be proved to have the correct type using the typing rules.To make this straightforward, assume that the fold and unfold operators are annotated with the typeof the value that they produce, and have the following typing rules:Γ ` e : τ{µX.τ /X}Γ ` foldµX.τe : µX.τΓ ` e : µX.τΓ ` unfold e : τ {µX.τ/X}2. Type-safety of a stack language (40 pts.)In this problem, you will show that a simple stack language is type-safe by proving preservation andprogress lemmas. Consider the following simple stack language, Subscript, inspired by PostScript:p ::= c | c pc ::= skip | n | ⊕ | {p}σ| app | ifz |/x def | x | foldµX.τ| unfoldv ::= n | {p}σS ::= [ ] | v ::Sτ ::= int | σ1→ σ2| X | µX.τσ ::=  | τ ::σn ∈ Zx ∈ VarX ∈ TyVarA program p is a sequence of one or more commands made up of integer pushes, binary arithmeticoperations, command sequences, function pushes, function applications, variable definition and lookup,type folding and unfolding operations, and conditionals. The binary arithmetic operations pop twoargument integers from the stack and push the resulting integer onto the stack. Pushing a functiononto the stack requires both the commands to be executed on function application and an input stack1hn, Si 7−→ hskip, n::Si h⊕, n0::n1::Si 7−→ hskip, (n1⊕ n0):: Sih{p}σ, Si 7−→ hskip, {p}σ::Si happ, {p}σ::Si 7−→ hp, SihfoldµX.τ, v :: Si 7−→ hskip, v ::Si hunfold, v :: Si 7−→ hskip, v ::Sihifz, {p0}σ::{p1}σ::0 ::Si 7−→ hp1, Si hifz, {p0}σ::{p1}σ::n ::Si 7−→ hp0, Si(n 6= 0)h/x def, v ::Si 7−→ hskip, Si h/x def p, v ::Si 7−→ hp{v/x}, Sihskip p, Si 7−→ hp, Sihc, Si 7−→ hc0, S0ihc p, Si 7−→ hc0p, S0i(c 6= skip ∧ c 6= /x def)Figure 1: Operational Semanticstype (analogous to declaring the type of the argument to a function in the typed-lambda calculus).The type of a function is σ1→ σ2, where σ1and σ2correspond to the types of the input and outputstacks, respectively. Function application pops a function from the stack and executes the commandsof the function. The command /x def pops a value from the stack and inserts into the environmentthe binding of the value to the symbol x. Bindings are statically scoped; a binding is in scope untilthe end of the current function or until the end of the program. The command x pushes the valuebound to x in the current environment onto the stack. Folding and unfolding operations do not affectthe values on the stack but do affect the type of the top element of the stack. The command ifz popstwo functions {c2} and {c1} from the stack and then pops an integer. c1is executed if the integer is0; otherwise c2is executed. For example, here is a program which computes the factorial of 5, storingthe result as the only value on the stack:{ /f def /n defn{1}{n n 1 − f f unfold app ∗}ifz}(µX.X :: int :: →int :: ) :: int :: foldµX.X :: int :: →int :: /fact def5factfact unfold appNote how the recursive call to the factorial function is accomplished by passing a copy of the functionto itself as an argument on the stack. Recursive types are required in order to give a type to a functionwhich expects a function with the same type on its input stack.The operational semantics for Subscript are given in Figure 1. A configuration is a pair hp, Si consistingof a program and a stack. The initial configuration for a program p is given by hp, [ ]i. The finalconfigurations are of the form hskip, Si. Note that the rule for /x def p handle substituting the valueon the top of the stack for x in the remainder of the program p. The other rule for /x def only appliesfor programs which consist only of the definition. In Figure 2 we define the substitution rules.Figure 3 gives the typing rules for a subset of the commands. A judgment of the form Γ; σ ` p : σ0asserts that if the program p is executed with a typing context Γ and a stack of type σ, then, ifand when the program terminates, it will terminate with a stack of type σ0. In the rule for app,2x{v/x} = vy{v/x} = y x 6= y{p}σ{v/x} = {p{v/x}}σc{v/x} = c for all other commands c(/x def p){v/x} = /x def p(/y def p){v/x} = /y def p{v/x} x 6= y(c p){v/x} = (c{v/x} p{v/x}) (c 6= /x def)Figure 2: Substitution RulesΓ; σ ` skip : σ Γ; σ ` n : int :: σ Γ; σ ` x : Γ(x):: σΓ; (σ1→ σ2):: (σ1@ σ) ` app : (σ2@ σ)Γ; (τ {µX.τ/X})::σ ` foldµX.τ: (µX.τ ) ::σ Γ; (µX.τ ) ::σ ` unfold : (τ{µX.τ/X}) ::σΓ; (τ ::σ) ` /x def : σΓ; (τ ::σ) ` /x def : σ Γ[x 7→ τ]; σ ` p : σ0Γ; (τ ::σ) ` /x def p : σ0Γ; σ ` c : σ00Γ; σ00` p : σ0Γ; σ ` c p : σ0(c 6= /x def)Figure 3: Typing Rules for Commandsthe notation σa@ σbstands for the concatenation of the stack type σbto the stack type σa(e.g.,(τ1::· · ·::τa::) @ (τ01::· · ·::τ0b::) = τ1::· · ·::τa::τ01::· · ·::τ0b::).In order to prove the soundness of this type system, we need to relate typing judgments to configura-tions. Figure 4 gives the typing rules for stack