On 18/11/05, Paul Hudak <[EMAIL PROTECTED]> wrote:
> Cale Gibbard wrote:
> >>Y = (\f. (\x. f (x x)) (\x. f (x x)))
> >
> > In a sense, the real definition of Y is Y f = f (Y f), this lambda
> > term just happens to have that property, but such functions aren't
> > rare.
>
> Actually no, the "real"
Cale Gibbard wrote:
Y = (\f. (\x. f (x x)) (\x. f (x x)))
In a sense, the real definition of Y is Y f = f (Y f), this lambda
term just happens to have that property, but such functions aren't
rare.
Actually no, the "real" definition is the top one, because the other one
isn't even a valid la
On 18/11/05, Greg Woodhouse <[EMAIL PROTECTED]> wrote:
>
>
> --- Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> I guess I'm not doing a very good job of expressing myself. I see that
> if you define Y as you do, then the various functions you list have the
> property that Y f = f (Y f).
>
> I do
--- Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> It computes the fix point which you can also define as
> oo
> fix f = lub f^i(_|_)
> i=0
> where f^i is f iterated i times. Is that a definition
> of fixpoint that makes you happier?
Believe it or n
Greg Woodhouse wrote:
Perhaps the issue is that the manipulations below are purely syntactic,
But all the computation rules of the lambda calculus are "syntactic"
in that sense. When you can prove things by symbol pushing it's
the easiest way.
But as Paul Hudak mentioned, there definitions tha
--- Lennart Augustsson <[EMAIL PROTECTED]> wrote:
I guess I'm not doing a very good job of expressing myself. I see that
if you define Y as you do, then the various functions you list have the
property that Y f = f (Y f).
I don't want to draw out a boring discussion that is basically about my
o
