Deriving the Y Combinator

Deriving the Y Combinator.md

Recall that the definition of the Y combinator is

    x   = f x       -- fixed-point
    Y f = f (Y f)

The simplest recursion is

    x = x   -- [error: cannot reference a symbol before it is defined]

Create a function repeat that takes a function that calls itself.

    repeat x = x x
    repeat repeat = repeat repeat       -- infinite recursion

This is pretty useless, we need a way to transport f around. Replace repeat with loop f

    (loop f) (loop f) = f (loop f) (loop f)     -- loop f = repeat
    
    -- But... replacing (loop f) (loop f) with Y gives
    Y = f Y

Congratulations, we have the Y combinator!!

Cleaning up the definitions, we have:

    repeat x = x x
    loop f x = f (x x)
    Y f = loop f (loop f)

    Y f = repeat (loop f)           -- simplifying even further
    Y = repeat . loop               -- or, even simpler!

Summarizing the steps, we have:

    Y = f Y                                         -- 1) define the fixed-point equation
    x x = f (x x)                                   -- 2) redefine y as recursive function x
    (L f) (L f) = f ((L f) (L f))                   -- 3) inject f
    Y = (L f) (L f) where L f x = f (x x)           -- Y combinator

Turing's Y-combinator

Slightly modifying the steps we derive Turing's version, which personally I find more intuitive.

    x x = f (x x)
    
    -- notice how we inject the f differently
    x x f = f (x x f)
    U U f = f (U U f)
    Y f = U U f where U x f = f(x x f)
    Y = U U