The Y Combinator (Slight Return)

[mvanier]

or:

How to Succeed at Recursion Without Really Recursing

Tiger got to hunt,
Bird got to fly;
Lisper got to sit and wonder, (Y (Y Y))?

Tiger got to sleep,
Bird got to land;
Lisper got to tell himself he understand.

- Kurt Vonnegut, modified by Darius Bacon Introduction

I recently wrote a blog post about the Y

Comments

[rus_kz]

could you insert lj cut please? :)

[mvanier]

What's LJ cut?

[rus_kz]

http://www.livejournal.com/support/faqbrowse.bml?faqid=75

it allows to hide most of the message under "read more...". Otherwise friendlist is completely occupied by your long post...

[mvanier]

Done. Thanks! I didn't know about that feature.

Yawn

[anonymous]

Why waste your time blogging when you should be coding?

The joy of parens

[anonymous]

I'm not at the repl at the moment, but shouldn't that be

(define Y
(lambda (f)
((lambda (x) (f (lambda (y) ((x x) y))))
(lambda (x) (f (lambda (y) ((x x) y)))))))
^ ^

Re: The joy of parens

[mvanier]

Right you are -- fixed. Thanks for catching this.

Excellent article.

[ext_117279]

I stopped at the part "I realize that the preceding discussion and derivation is nontrivial, so don't be discouraged if you don't get it right away. Just sleep on it, play with it in your mind and with your trusty DrScheme interpreter, and you'll eventually get it."

I'm going to sleep on what I've read so far. I'll continue reading once I feel comfortable with what you presented up to that point. Thank you for writing about the Y combinator.

You explain abstract topics in a way that is easy to understand. When are you going to write a post explaining Monads?

Re: Excellent article.

[ext_117279]

I reckon you have.

Re: Excellent article.

[mvanier]

Thanks for the compliment! I still have to finish the state monad article. My new policy is to not post until I have the article finished, but I _will_ finish that article, promise!

I also have a nearly-finished article on lambda calculus, and I'd love to write something on continuations and continuation-passing style.

Re: Excellent article.

[mvanier]

One thing you might try is to manually evaluate (factorial 3) using the definition that uses the strict version of Y. That will be very illuminating if you can tough it out.

Y doesn't have a straightforward static type?

[ryani]

y :: forall a. (a -> a) -> a
y f = let x = f x in x

Now, it's true that you cannot define "y" without the use of recursion in many statically typed languages; this is a property of System F and most other typed lambda-calculus... it follows directly from the fact that these systems are strongly normalizing. That is to say, there are no infinite loops in typed lambda-calculi like System F; any program will always complete successfully. On the other hand, System F + Y-combinator is Turing complete; just one single recursive let in the definition of "y" is all that is needed.

Re: Y doesn't have a straightforward static type?

[mvanier]

Good point -- I didn't know about this definition of Y. I tried it in Haskell, and it works fine. However, note that Haskell's let is what is known as letrec in Scheme (a let where all the bindings are in the scope of all the other ones), so there is explicit recursion built in to this definition even though it's not obvious. If this was a Scheme-equivalent let then this definition would be equivalent to:

(define Y
(lambda (f)
(let ((x (f x)))
x)))

which by the let/lambda equivalence rule would be the same as:

(define Y
(lambda (f)
((lambda (x) x)
(f x))))

which is meaningless since the x in (f x) is unbound. What it really is is this:

(define Y
(lambda (f)
(letrec ((x (f x)))
x)))

which works in lazy Scheme but not in strict (standard) Scheme.

I definitely need to learn more about System F.