|
|
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:
- Though I've used Haskell syntax, this is invalid Haskell because
the type system can't manage it.
- 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.
|
|
|