CS611 Homework 2 DUE: 10/01/01What to turn inTurn in the assignment during class on the due date.1. Proo fs by induction (25 pts.)Consider a version of IMP that has for loops instead of while loops. We redefine commands c asfollows:c ::= skip | x := a | if b then c0else c1| c0; c1| for x = a0to a1do cLet us suppose that the large-step semantics are unchanged except that we substitute the followingfor rules for the while rules:a0,σ ⇓n0a1,σ ⇓n1for x = a0to a1do c, σ ⇓σwhere n0>n1a0,σ ⇓n0a1,σ ⇓n1for x = n0to n1do c, σ ⇓σfor x = a0to a1do c, σ ⇓σwhere n0≤ n1c; for x = n0to n1do c, σ[x → n0] ⇓σfor x = n0to n1do c, σ ⇓σwhere n0≤ n1∧ n0= n0+1Informally, the bounds of the loop are computed once, at the beginning of the loop, and although theloop index variable can be assigned within the loop, these assignments do not affect the value of thevariable at the beginning of the next loop iteration.(a) Write a program in this language that, given an input number in the variable n, outputs the nthprime number in the variable x.(b) Define a series of programs P1,P2,P3,... such that the length of program Pnis polynomial in nbut the running times of the programs grow faster than any exponential in n.(c) Despite the fact that we can write many useful programs in this language—it can compute theprimitive recursive functions—the language is not universal. Show that it is not universal bydemonstrating that all programs terminate. (Hint: Use well-founded induction, but make sureyou show your well-founded relation is indeed well-founded!)2. Free and bound variables (10 pts.)Identify the free and bound variables in each of the following expressions:(a) (λ(xyz) zxy)(b) (λ(xy)(λz (zy)) (λx (zx)))(c) ((λ(xy) y) x)We defined substitution into a lambda term using the following three rules:(λx e0){e1/x} =(λx e0)(λy e0){e1/x} =(λy e0{e1/x})(wherey = x ∧ y ∈ FV[[ e1]] )(λy e0){e1/x} =(λye0{y/y}{e1/x})(wherey= x ∧ y∈ FV[[ e0]] ∧ y∈ FV[[ e1]] )(d) In these rules, we note a number of conjuncts in the side-conditions whose purpose is perhaps notimmediately apparent. Show by counterexample that each of the conjuncts above is independentlynecessary.13. Fixed Point Combinator (10 pts.)In class we have seen a fixed point operator Y, which has the property Yf = f (Yf). This is not theonly fixed point operator. Prove that the combinator B defined as the following is also a fixed pointeroperator.A ≡ λ(abcdefghijklmnopqstuvwxyzr) r(thisisafixedpointcombinator)B ≡ AAAAAAAAAAAAAAAAAAAAAAAAAA4. Enco dings (25 pts.)We have seen in class one way to represent natural numbers in the λ-calculus. However, there aremany other ways to encode numbers in λ-calculus. Consider the following definitions:TRUE ≡ λ(xy) xFALSE ≡ λ(xy) y0 ≡ λxxn +1≡ λx (xFALSE) n(a) Show how to write the DEC (decrement by one) operation for this number representation. Reduce(DEC (DEC 2)) to its βη normal form, which should be the representation of 0, above.(b) Show how to write a λ-term ZERO? that determines whether a number is zero or not. It shouldreturn TRUE when the number is zero, and FALSE otherwise. Use the definitions of TRUE andFALSE given above.(c) Show how to write the ADD and MULT operations for this number representation.5. The S and K Combinators (30 pts.)Consider the following definitions of the S and K combinators:S ≡ λ(xyz)((xz)(yz))K ≡ λ(xy) xAny λ-calculus expression without free variables can be written using only applications of the S andK combinators; thus, the λ-calculus can be universal with only three distinct identifier names, sinceboth combinators use no more than three identifiers.(a) Show that the S and K combinators can be used to construct an expression with the same normalform as the identity expression I ≡ λxx.(b) Now, we will construct a translation from λ-calculus expressions to expressions containing onlyapplications of the S and K combinators. This translation will be defined in terms of two functions:C[[ e]], which converts an expression e into this form, and a function A[[ x, e]] , w h i c h abstracts thevariable x from the expression e. removing all uses of x within e.The idea is that A[[ x, e]] = λx e, in the sense that the two expressions have the same effect whenapplied to any argument (they are extensionally equal). Using the function A, the function C canbe defined simply by structural induction:C[[ x]] = xC[[ e0e1]] = ( C[[ e0]] C[[ e1]] )C[[ λx e]] = A[[ x, C[[ e]] ]]Because A is only applied to expressions produced by C, it needs to be defined only for expressionsthat are identifiers and applications. For example, consider A[[ x, x]] w h e r e x= x.Werequire(A[[ x, x]] e)=(λx x)e for any e, so we obtain the right effect with the following definition:A[[ x, x]] = ( K x)(wherex = x)Define the remainder of the translation to the S and K combinators. Does this translation resultin the most compact equivalent expression using these combinators? Justify your