Recursive Functions (Cont.)

Using this observation: 
     Y = λG.(λg.G(g g))(λg.G(g g)),   and
     Y F = F( Y F )
It is possible to evaluate factorial(3) as follows: 
     let  F = λf.λn. if n=0 then 1 else n*f(n-1)  in  Y F 3
    Y F 3
 =  Y (λf.λn. if n=0 then 1 else n*f(n-1))  3
 =  F( Y F ) 3
 =  (λf.λn. if n=0 then 1 else n*f(n-1)) (Y F)  3
 ⇒β (λn. if n=0 then 1 else n*(Y F)(n-1)) 3
 ⇒β if 3=0 then 1 else 3*((Y F 2))
 =  3 * ( Y F 2 )
     …
 =  6
The existence of Y means that recursive declarations can be introduced for free. Any such declaration can be converted to a non-recursive one by the use of Y and can then be removed as before. The grammar is extended to 
    <expr> ::= ... as before ...
             | let [rec] <decs> in <expr>
For one declaration, 
    let rec  x=e  in f
 ⇒ let  x=Y(λx.e)  in f
For more declarations, 
    let rec  x=e, y=f  in g
 ⇒ let rec  xy= let x=hd xy, y=tl xy
                 in  e::f
    in let x=hd xy, y=tl xy
       in  g

Demonstration