Fixed Point Combinator

[Arjan van IJzendoorn]

Hello Nick,

>Y f= f (Y f)
>
>And the factorial is defined as,
>
>Y (\ loop n m -> (if (n<1) m (loop (n-1) (n*m) )))

Here's a somewhat simpler definition of factorial using Y:

fac = Y ( \loop n -> if (n == 1) n (n * loop (n - 1)) )

If we substitute Y by its definition, we get:

fac = ( \loop n -> if (n == 1) n (n * loop (n - 1)) )
   (Y ( \loop n -> if (n == 1) n (n * loop (n - 1)) ) )

Now we use beta-reduction and obtain the following:

fac = \n -> if (n == 1) n (n * LOOP (n - 1))
  where
    LOOP = Y ( \loop n -> if (n == 1) n (n * loop (n - 1)) )

Tadaa! Here we are: LOOP is equal to fac, so we can replace
equals by equals and get:

fac = \n -> if (n == 1) n (n * fac (n - 1))

The loop argument is essential and essentially the factorial
function itself. The Y combinator feeds the function repeatedly
to itself and creates recursion in this way:

Y f = f (f (f (f .....

The if-expression takes care of termination.

Greetings,
 Arjan