Re: Y combinator derivation

[Brad Pierce <lanai!pierce@locus.ucla.edu>]

In article <16800018@uicsrd.csrd.uiuc.edu> jozwiak@uicsrd.csrd.uiuc.edu writes:
>
>You may want to consult:
> "Denotational Semantics-A Methodology for Language Development"
>by David A. Schmidt, ISBN 0-697-06849-8.
> I think that the Y combinator is:
>
> Y = lambda h.(lambda x. h(x x))
>              (lambda x. h(x x)) .
>
> I think that this does what it should is pretty patent from it, but
>as for deriving it, this involves insight that I don't yet have.
>
>  john

I think the previous poster was asking for a derivation of the
*applicative-order* Y combinator, not the normal-order as given
here. ``The Little Lisper'' (as someone else mentioned) has a
good presentation, but its complexity points out the price pays
for using an applicative-order language.

In normal-order languages, like standard lambda calculus, the
derivation is straightforward. The motivation for the Y-combinator
in lambda calculus is to allow the use of recursive definitions.
Recall that there is no such thing as assignment in lambda calculus, 
but that this elegant and mathematically tractable model of 
computation is rich enough to support recursion anyway.

The standard example goes as follows:

Define the factorial function FACT(n) = n! as

     FACT (n) = lambda n. if (n == 0) 1 else n*FACT(n-1)

Then abstracting out the FACT, define:

     H = lambda fact. lambda n. if (n == 0) 1 else n*fact(n-1)

Then we have the equation:

     FACT = H(FACT)

We want to solve for FACT. Since the only other factor is the
function H, we look for a function that will take H as input
and return the solution FACT. Said another way, we're looking 
for a function, F, that satisfies the following equation:

     FH = H(FH)

If combinator theory is defined in terms of the lambda calculus,
then we can define combinators as lambda expressions without
free variables. For obvious reasons, a combinator with the kind
of property described above is called a fixed-point combinator.
It is possible to define an infinite number of different fixed-
point combinators in the lambda calculus, but the simplest
is the so-called Y-combinator given above. It is easy to verify
the definition, as long as you remember that it is to be
evaluated in normal-order. Finding a fixed-point combinator
is not so easy when using applicative-order evaluation. Please see 
the ``Little Lisper''. 

Maybe it's time to start thinking seriously about whether the
current performance benefits of applicative-order evaluation
is worth the theoretical and human factors price tag.

-- Brad