COP-5555 PROGRAMMING LANGUAGEPRINCIPLESNOTES ON RECURSION AND FIXED-POINT THEORY.Our purpose is to describe the meaning, or the semantics, of the keyword "rec" in RPAL. As is oftenthe case, an analogy is useful. The meaning of an RPAL program of the form "let x=P in Q", as we nowknow, isthe value of applicative expression "(λx.Q)P". In fact, "let x=P in Q" is not the only program withthat meaning (for example consider "Q where x=P"). Since all RPAL programs (except those containing"rec") can be similarly transformed toλ-expressions whose evaluation will yield the value of the program,we can say that RPAL programs are "syntactically sugared"λ-expressions, i.e. RPAL programs are simplyλ-expressions, presented in another form. Thus the question:What is the meaning of an RPAL program of the form "let rec f n = P in Q" ?can be re-phrased as:Whatλ-expression, if any, isthe "de-sugarized" version of "let rec f n = P in Q" ?To answer that question, we must first develop some intuition. Consider the most popular example ofrecursive computation: the factorial function:let rec f n = n eq 0 → 1|n*f(n-1) in f 3If we assume the "rec" keyword were not present, then the corresponding applicative expression would be(λf.f 3) [λn.n eq 0 → 1|n*f(n-1) ]It is easy to see that the last occurrence of "f" in this expression is free, and that the evaluation of theexpression would not succeed because of that "f" being undefined. Thus the purpose of the "rec" keywordis to "magically" makethat occurrence of "f" bound to the bracketed expression. With the "rec", somehow,(λf.f 3) [λn.n eq 0 → 1|n*f(n-1) ]= >β(λn.n eq 0 → 1|n*f(n-1)) 3= >β3eq0→1|3*f(3-1)= >δ3*f(2)= >magic3*(λn.n eq 0 → 1|n*f(n-1)) 2= >β3*(2 eq 0 → 1|2*f(2-1))= >δ3*2*f(1)= >magic3*2*(λn.n eq 0 → 1|n*f(n-1)) 1= >β3*2*(1 eq 0 → 1|1*f(1-1))= >δ3*2*1*f(0)= >magic3*2*1*(λn.n eq 0 → 1|n*f(n-1)) 0= >β3*2*1*(0 eq 0 → 1|0*f(0-1))= >δ3*2*1*1= >δ6To dispel the magic, we need some mathematics.PLP Notes Recursion-2-Definition:Let F be a function and w a value. w is called a fixed-point of F iffFw=w.Example 1:S=λx.x2-6 has twofixedpoints, 3 and -2, because(λx.x2-6)3 =>β32-6 =>δ3(λx.x2-6)-2 =>β(−2)2-6 =>δ-2There are no more fixed-points, because -2 and 3 are the only solutions to x2-x-6=0.Example 2:T=λf.λ().(f nil)2-6 has twofixedpoints,λ().3 andλ().-2, because(λf.λ().(f nil)2-6)λ().3 = >βλ().((λ().3) nil)2-6 =>βλ().32-6 =>δλ().3(λf.λ().(f nil)2-6)λ().-2 = >βλ().((λ().-2) nil)2-6 =>βλ().−22-6 =>δλ().-2Note that fixed points can be functions. In fact, the fixed points we are interested in can only be functions.Example 3:Consider U =λf.λn.n eq 0 → 1|n*f(n-1). The functionλx.x2is not afixedpoint of U, but the Factorialfunction is. Proof of this is left to the reader.Back to magic dispelling:let rec f n = P in Q= >let rec f =λn.P in Q (fcn_form)= >let rec f = (λf.λn.P)f in Q (abstraction)= >let rec f = F f in Qwhere F =λf.λn.P . Note that nowthere are no free occurrences of f in F,and there is only one free occur-rence of f in the entire expression. Further,inthis last expression (i.e. let rec f = F f in Q) the presence ofthe "rec" means that both f’s should be the same; without the "rec" theywould be different. With "rec", wewant f to be a fixed point of F !! Let us then re-phrase the expression aslet f = A_fixed_point_of F in Q.This operator,"A-fixed_point_of" is called a fixed point finder,and we will identify it from nowonas"Y". Hence our expression becomeslet f = Y F in Q= >(λf.Q) (Y F)= (λf.Q) (Y (λf.λn.P))Nowthere are no free occurrences of f !! In summary,the problem of explaining the purpose of "rec" isequivalent to finding a fixed point of F.Such a fixed point finder is called Y;wemust nowfind a suitable Y.Howdowefind a suitable Y ?WE DON’T NEED TO!! We only need to use some of its characteristics:PLP Notes Recursion-3-1) f =YF2) F f=fSubstituting 1) in 2), we obtainF(YF)=YFThis is called the fixed point identity,and it is all that is required to evaluateλexpressions that containY’s, which are "de-sugared" RPAL programs that contain rec’s. Let’sextend some earlier definitions:Definition. Axiomρ(rho): Y F = >ρF(YF).Definition. (Extension): An applicative expression M is not in normal form if it is of the form Y N.Definition. (Extension): A reduction sequence is in normal order iffatevery step we reduce the left-mostYorλ.We can nowreturn to the factorial function, and evaluate the applicative expression (again). This time,there is no magic.(λf.f 3) (Y F), where F =λf.λn.n eq 0 → 1|n*f(n-1)= >βYF3=>ρF(YF)3= (λf.λn.n eq 0 → 1|n*f(n-1)) (Y F) 3= >β(λn.n eq 0 → 1|n*YF(n-1)) 3= >β,δ3* Y F (2)= >ρ3* F (Y F) 2= 3* (λf.λn.n eq 0 → 1|n*f(n-1)) (Y F) 2= >β3* (λn.n eq 0 → 1|n*YF(n-1)) 2= >β,δ3*2* Y F (1)= >ρ3*2* F (Y F) 1= 3*2* (λf.λn.n eq 0 → 1|n*f(n-1)) (Y F) 1= >β3*2* (λn.n eq 0 → 1|n*YF(n-1)) 1= >β,δ3*2*1* Y F (0)= >ρ3*2*1* F (Y F) 0= 3*2*1* (λf.λn.n eq 0 → 1|n*f(n-1)) (Y F) 0= >β3*2*1* (λn.n eq 0 → 1|n*YF(n-1)) 0= >β,δ3*2*1*1= >δ6Notice that normal order is required to evaluate the expression; in programming language order the evalua-tion would not terminate.We hav e nowseen Y at work, but the question is, "Is YF really the factorial function ?" In other words, wehave seen that YF (for this particular F) can be used to compute factorial of three, but can it be used to com-pute factorial of k, for anyk?Let’stry it by induction.Base Case:YF0 =>ρF(YF)0= (λf.λn.n eq 0 → 1|n*f(n-1)) (Y F) 0PLP Notes Recursion-4-= >β(λn.n eq 0 → 1|n(YF)(n-1)) 0= >β,δ1Inductive step: for k > 0,YFk =>ρF(YF)k= (λf.λn.n eq 0 → 1| n*f(n-1)) (Y F) k= >β(λn.n eq 0 → 1| n*(Y F) (n-1)) k= >βkeq0→1|k*(YF)(k-1)= >δk*(YF)(k-1)Recursion via lambda-calculus.Recursion can be acheivedusing the fixed-point identity.The question nowiswhether it can also beacheivedusing lambda-calculus alone, i.e. does there exist a suitableλ-expression that can be used as thevalue of Y? After some trials and errors, someone came up with this:Y=λF.(λf.f f) (λg. F (g g))This satisfies the fixed-point identity:YF = (λF.(λf.f f) (λg. F(g g)) ) F= >β(λf.f f) (λg.F(g g))= >β(λg.F(g g)) (λg.F(g g))= >βF((λg.F(g g)) (λg.F(g g)) )< =βF((λf.f f) (λg.F(g g)) )< =βF((λF.(λf.f f) (λg.F(g g)) ) F )= F(YF)Notice again hownormal order of evaluation is required.Recursion in the CSE MachineWe finally come to what matters: getting