JavaScript Y combinator and Z combinator

Note that this topic is a sub-set of lambda calculus.

First how to prove that Y combinator is a fixed-point combinator:

Y f = (lg. (lx. g (x x)) (lx. g (x x))) f
    = (lx. f (x x)) (lx. f (x x))
    = l(lx. f (x x)). f (x x)
    = f ((lx. f (x x)) (lx. f (x x)))
    = f (Y f)

So Y f = f (Y f) and this proves that it is a fixed-point combinator. Note that everything is made of unary functions.

We can use this fact to evaluate factorial'(2).

fact’(2) = (F(fact'))(2)
         = (n => n==0 ? 1 : n * fact'(n-1))(2)
         = 2==0 ? 1 : 2 * fact'(1)
         = 2 * fact'(1)

As you can see this gives the correct result: fact'(2) = 2 * fact'(1).