Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as:

FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. x~x~y))$

I understand its purpose and I can trace the execution of its application perfectly fine; I would like to understand how to derive FIX from first principles.

Here is as far as I get when I try to derive it myself:

  1. FIX is a function: FIX $\triangleq \lambda_\ldots$
  2. FIX takes another function, $f$, to make it recursive: FIX $\triangleq \lambda f._\ldots$
  3. The first argument of the function $f$ is the "name" of the function, used where a recursive application is intended. Therefore, all appearances of the first argument to $f$ should be replaced by a function, and this function should expect the rest of the arguments of $f$ (let's just assume $f$ takes one argument): FIX $\triangleq \lambda f._\ldots f~(\lambda y. _\ldots y)$

This is where I do not know how to "take a step" in my reasoning. The small ellipses indicate where my FIX is missing something (although I am only able to know that by comparing it to the "real" FIX).

I already have read Types and Programming Languages, which does not attempt to derive it directly, and instead refers the reader to The Little Schemer for a derivation. I have read that, too, and its "derivation" was not so helpful. Moreover, it is less of a direct derivation and more of a use of a very specific example and an ad-hoc attempt to write a suitable recursive function in $\lambda$.

share|improve this question
1  
This post might be helpful. In general, I think just going through and computing several iterations of the combinator is helpful in figuring out why it works. –  Xodarap Feb 8 '13 at 15:14
2  
There are several different fixed point combinators. Perhaps people just played with combinators until they stumbled upon them. –  Yuval Filmus Feb 9 '13 at 5:55
    
@YuvalFilmus, that's what my research and the response to this question are beginning to make me think. But I still think it would be instructive to "see" how the combinator(s) are formed logically, a skill that would be especially helpful when, e.g., trying to construct a new combinator. –  BlueBomber Feb 9 '13 at 16:49
add comment

2 Answers

up vote 8 down vote accepted

I haven't read this anywhere, but this is how I believe $Y$ could have been derived:

Let's have a recursive function $f$, perhaps a factorial or anything else like that. Informally, we define $f$ as pseudo-lambda term where $f$ occurs in its own definition:

$$f = \ldots f \ldots f \ldots $$

First, we realize that the recursive call can be factored out as a parameter:

$$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} f$$

Now we could define $f$ if we only had a way how to pass it as an argument to itself. This is not possible, of course, because we don't have $f$ at hand. What we have at hand is $M$. Since $M$ contains everything we need to define $f$, we can try to pass $M$ as the argument instead of $f$ and try to reconstruct $f$ from it later inside. Our first attempt looks like this:

$$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}$$

However, this is not completely correct. Before, $f$ got substituted for $r$ inside $M$. But now we pass $M$ instead. We have to somehow fix all places where we use $r$ so that they reconstruct $f$ from $M$. Actually, this not difficult at all: Now that we know that $f = M M$, everywhere we use $r$ we simply replace it by $(r r)$.

$$f = \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'} \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'}$$

This solution is good, but we had to alter $M$ inside. This is not very convenient. We can do this more elegantly without having to modify $M$ by introducing another $\lambda$ that sends to $M$ its argument applied to itself: By expressing $M'$ as $\lambda x.M(xx)$ we get

$$f = (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx)) (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx))$$

This way, when $M$ is substituted for $x$, $MM$ is substituted for $r$, which is by the definition equal to $f$. This gives us a non-recursive definition of $f$, expressed as a valid lambda term!

The transition to $Y$ is now easy. We can take an arbitrary lambda term instead of $M$ and perform this procedure on it. So we can factor $M$ out and define

$$Y = \lambda m . (\lambda x. m(xx)) (\lambda x.m(xx))$$

Indeed, $Y M$ reduces to $f$ as we defined it.


Note: I've derived $Y$ as it is defined in literature. The combinator you've described is a variant of $Y$ for call-by-value languages, sometimes also called $Z$. See this Wikipedia article.

share|improve this answer
    
The missing-but-seemingly-obvious intuition that your excellent response gave me is that a recursive function needs itself as an argument, so we start off with an assumption that the function will have the form $f = X (X) $ for some $X$. Then, as we construct $X$, we make use of that assertion that $f$ is defined as the application of something to itself internally in $X$, e.g., applying $x$ to $x$ in your answer, which is by definition equal to $f$. Fascinating! –  BlueBomber Feb 11 '13 at 6:34
add comment

As Yuval has pointed out there is not just one fixed-point operator. There are many of them. In other words, the equation for fixed-point theorem do not have a single answer. So you can't derive the operator from them.

It is like asking how people derive $(x,y)=(0,0)$ as a solution for $x=y$. They don't! The equation doesn't have a unique solution.

Just in case that what you want to know is how the first fixed-point theorem was discovered. Let me say that I also wondered about how they came up with the fixed-point/recursion theorems when I first saw them. It seems so ingenious. Particularly in the computability theory form. Unlike what Yuval says it is not the case that people played around till they found something. Here is what I have found:

As far as I remember, the theorem is originally due to S.C. Kleene. Kleene came up with the original fixed-point theorem by salvaging the proof of inconsistency of Church's original lambda calculus. Church's original lambda calculus suffered from a Russel type paradox. The modified lambda calculus avoided the problem. Kleene studied the proof of inconsistency probably to see how if the modified lambda calculus would suffer from a similar problem and turned the proof of inconsistency into a useful theorem in of the modified lambda calculus. Through his work regarding equivalence of lambada calculus with other models of computation (Turing machines, recursive functions, etc.) he transferred it to other models of computation.

share|improve this answer
    
Thank you for your insight and historical context. –  BlueBomber Feb 11 '13 at 6:06
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.