Adrian Neumann
Hello,
while studying for a exam I came across this little pearl:
Y = (L L L L L L L L L L L L L L L L L L L L L L L L L L L L) where L = λabcdefghijklmnopqstuvwxyzr. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))
posted by Cale Gibbard to this list. Now I'm wondering how exactly does one finde such awesome λ expressions?
In this particular case, once one has seen the Turing fixed point combinator, I think it's fairly obvious. The idea this is, we want a fixpoint combinator; let's assume we can make it by applying one thing to another. F G. We want (F G f) = f (F G f) so F has got to look something like \g f -> f (F g f). Oh, but where are we going to get another F without a fixpoint combinator? I know, how about passing it in as g? now F = (\g f -> f (g g f)), which works so long as the argument given for g is F. So Y = F F. Now, one can look at this as "F is half of a fixpoint combinator", so what about one third of a fixpoint combinator? ie T T T f = f (T T T f) Clearly T has to look like (\t2 t3 f -> f (T T T f)), and the same reasoning applies. Obviously it doesn't matter what you call the bound variables.
Is there some mathemagical background that lets one conjure such beasts?
If you play around with lambda expressions and combinators enough, they'll come to you in your dreams. To what extent this is a Good Thing is a matter of personal taste. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2008-04-26)