arrows pointing right and left

Deriving the Y Combinator


email Scott Turner
home
programming

The Y combinator makes a non-recursive function into a recursive one. The resulting function is called the fixed point of the input function.

There are many other derivations of Y ... I produced this one in order to refresh my intuition.


The function which determines the recursive result, i.e. that we want the fixed point of, is something like
  f = \g->\x-> ... x ... g ...
Now, we find it difficult to put the fixed point into closed form and apply f to it. So we modify f into a function that can accept itself as an argument.
  f' = \g'->\x-> ... x ... (g' g') ...
If we pass f' to itself (f' f'), we get the desired fixed point of f.

But we can write f' in terms of f!
  f' = \g'->\x-> (f (g' g')) x
or just
  f' = \g'-> f (g' g')
To represent the fixed point of f we come up with (\g'-> f (g' g'))(\g'-> f (g' g'))
and the combinator is
  y = \f->(\g'-> f (g' g'))(\g'-> f (g' g'))


Notes:

  1. Though I've used Haskell syntax, this is invalid Haskell because the type system can't manage it.
  2. A while back, I persuaded myself that "Recursion requires laziness." Then I lost track of the reasoning. Now I see that there is a version of Y which works in Scheme, or in the applicative-order lambda calculus.
    What I had in mind was that recursion requires that evaluation be non-eager, i.e. that you don't willy-nilly reduce an arbitrary redex just because it's available. Applicative order doesn't wait until the last possible moment, but it is restrained enough to work with a version of Y. This is a point against strict evaluation, that the normal-order choice of redex is the most straightforward one for termination and recusion.

Support open standards!  
Valid XHTML 1.0!