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