36
$\begingroup$

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$.

$\endgroup$
6
  • 1
    $\begingroup$ 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. $\endgroup$
    – Xodarap
    Feb 8, 2013 at 15:14
  • 2
    $\begingroup$ There are several different fixed point combinators. Perhaps people just played with combinators until they stumbled upon them. $\endgroup$ Feb 9, 2013 at 5:55
  • $\begingroup$ @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. $\endgroup$
    – BlueBomber
    Feb 9, 2013 at 16:49
  • $\begingroup$ Read chapter 9 in "The Little Lisper", by Daniel P. Friedman (or "The Little Schemer"). $\endgroup$
    – user18199
    Jun 6, 2014 at 17:10
  • 2
    $\begingroup$ The OP seems to indicate that they have already read that. $\endgroup$
    – Raphael
    Jun 6, 2014 at 17:49

7 Answers 7

37
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ 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! $\endgroup$
    – BlueBomber
    Feb 11, 2013 at 6:34
11
$\begingroup$

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.


How to derive the operator you might ask? Here is how I keep it in mind. Fixed-point theorem is about removing self-reference.

Everyone knows the liar paradox:

I am a lair.

Or in the more linguistic form:

This sentence is false.

Now most people think the problem with this sentence is with the self-reference. It is not! The self-reference can be eliminated (the problem is with truth, a language cannot speak about the truth of its own sentences in general, see Tarski's undefinability of truth theorem). The form where the self-reference is removed is as follows:

If you write the following quote twice, the second time inside quotes, the resulting sentence is false: "If you write the following quote twice, the second time inside quotes, the resulting sentence is false:"

No self-reference, we have instructions about how to construct a sentence and then do something with it. And the sentence that gets constructed is equal to the instructions. Note that in $\lambda$-calculus we don't need quotes because there is no distinction between data and instructions.

Now if we analyse this we have $MM$ where $Mx$ is the instructions to construct $xx$ and do something to it.

$Mx = f(xx)$

So $M$ is $\lambda x. f(xx)$ and we have

$MM = (\lambda x. f(xx))(\lambda x. f(xx))$

This is for a fixed $f$. If you want to make it an operator we just add $\lambda f$ and we get $Y$:

$Y = \lambda f. (MM) = \lambda f.((\lambda x. f(xx))(\lambda x. f(xx)))$

So I just keep in mind the paradox without self-reference and that helps me understand what $Y$ is about.

$\endgroup$
0
3
$\begingroup$

So you need to define a fixed point combinator

fix f = f (fix f)
      = f (f (fix f))
      = f (f (f ... ))

but without explicit recursion. Let's start with the simplest irreducible combinator

omega = (\x. x x) (\x. x x)
      = (\x. x x) (\x. x x)
      = ...

The x in the first lambda is repeatedly substituted by the second lambda. Simple alpha-conversion makes this process clearer:

omega =  (\x. x x) (\x. x x)
      =α (\x. x x) (\y. y y)
      =β (\y. y y) (\y. y y)
      =α (\y. y y) (\z. z z)
      =β (\z. z z) (\z. z z)

I.e. the variable in the first lambda always disappears. So if we add an f to the first lambda

(\x. f (x x)) (\y. y y)

the f will bob up

f ((\y. y y) (\y. y y))

We have got our omega back. It should be clear now, that if we add an f to the second lambda, then the f will appear in the first lambda and then it will bob up:

Y f = (\x. x x)     (\x. f (x x))
      (\x. f (x x)) (\x. f (x x)) -- the classical definition of Y

Since

(\x. s t) z = s ((\x. t) z), if `x' doesn't occur free in `s'

we can rewrite the expression as

f ((\x. x x) (\x. f (x x))

which is just

f (Y f)

and we have got our equation Y f = f (Y f). So the Y combinator is essentially

  1. double the f
  2. make the first f bobbed up
  3. repeat
$\endgroup$
8
  • $\begingroup$ "it should be clear now" = "let me give you a solution here out of the blue". :) $\endgroup$
    – Will Ness
    Jun 29, 2023 at 18:21
  • $\begingroup$ Well, I tried! Nice to see you're still active on SO legend. $\endgroup$ Jun 30, 2023 at 19:58
  • $\begingroup$ Hope I haven't caused any offense. :) I'm just trying to understand this stuff fully myself. I think I found a good way, and it's the same as the accepted answer except the wording there is unsatisfactory: "We can do this more elegantly" is just as arbitrary as what I commented on, above. Instead, the way to find this directly and mechanistically, is to abstract away the self-application (U x = x x) on the inside, (contd.) $\endgroup$
    – Will Ness
    Jul 1, 2023 at 11:46
  • $\begingroup$ as U (^r. ...(r r)...) = U (^r. (^x. ...x...) (r r)). this is self-evident and simple abstraction step. the transformation in that answer is not at all clear to me, although it happens to produce alpha-equivalent lambda-term. So overall, I find the following really clear: U (^f. ...(f f)...) = U (^f. (^r. ...r...) (f f)) = (^g. U (^f. g (f f))) (^r. ...r...) -- the last step again by simple, self-evident abstraction. et-voila, Y. -- say, what you mean by "legend"? :) :) $\endgroup$
    – Will Ness
    Jul 1, 2023 at 11:46
  • $\begingroup$ ... and then having found this Y, we discover that (with Hgf = g(f f)) Yg = U(Hg) = g(U(Hg)) = g(Yg), i.e. it is a fixed point combinator, and g reveals its meaning as a "functional" (as they called it in old times LISP literature) expressing one computational step of a recursive function, expecting its first argument to be that recursive function, so it can call it if needed. -- using self-application (U) for passing along self copy for the next invocation is the real insight here. maybe it's also simple in some very-high-level math, who knows. $\endgroup$
    – Will Ness
    Jul 1, 2023 at 13:46
3
$\begingroup$

You may have seen the classic example of an equation without a normal form:

$$(\lambda x.xx)(\lambda x.xx) \triangleright (\lambda x.xx)(\lambda x.xx)$$

A similar equation is suggested by that for general recursion:

$$\begin{array} {rr} & (\lambda x.R(xx))(\lambda x.R(xx)) ~\\ \triangleright & R(~ (\lambda x.R(xx))(\lambda x.R(xx))~) \\ \triangleright & R(R(~ (\lambda x.R(xx))(\lambda x.R(xx))~)) \\ \triangleright & \dots \end{array} \tag{A}$$

(A) is a way to write general recursive equations in lambda calculus (beyond primitive recursive). So how you solve the equation $Yf = f(Yf)$ ? Plug $f$ in for $R$ in the above equation to get:

$$Yf = (\lambda x.f(xx))(\lambda x.f(xx))$$ $$Y = \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$

$\endgroup$
2
$\begingroup$

Instead of starting with the properties of $\mathrm{Y}$, start with a term that explicitly refers to itself:

$$\textbf{letrec }f = \ldots f \ldots f \ldots \textbf{ in } f$$

and consider how it could be expressed without $\textbf{letrec}$.

You can get an equivalent term by passing $f$ as an argument to itself at each call site:

$$\textbf{let }f f' = \ldots f' f' \ldots f' f' \ldots \textbf{ in } f f$$

As this point, we have already accomplished the interesting part of this construction: effective self reference in a language that lacks explicit self reference. This is enough to show that the language is inconsistent as a logic, or to simulate a Turing machine in it. You don't need a $\mathrm{Y}$ combinator as such – that is, self-referencing expressions needn't contain any subexpression with the properties of $\mathrm{Y}$.


If you want to define $\mathrm{Y}$ anyway, that's easy too: it takes a function of the form $(λg'.\ \ldots g' \ldots g' \ldots)$ and returns an expression equivalent to the above. Therefore, you can take*

$$\mathrm{Y}\,g = \textbf{let }f f' = g (f' f') \textbf{ in } f f$$

To convert this to a term in the pure lambda calculus, replace the function arguments with lambdas:

$$\mathrm{Y} = λg. \textbf{let }f = λf'. g (f' f') \textbf{ in } f f$$

and then replace $\textbf{let }x = e' \textbf{ in } e$ with either $e[e'/x]$ or $(λx.e)e'$, whichever is your preferred interpretation of $\textbf{let}$. This gets you either

$$\mathrm{Y} = λg. (λf'. g (f' f')) (λf'. g (f' f'))$$

or

$$\mathrm{Y} = λg. (λf. f f) (λf'. g (f' f'))$$

I find both of those forms far more confusing than the $\textbf{let}$ form, which is why I used $\textbf{let}$ throughout this answer. You can use $\textbf{let}$ without sullying the purity of the calculus if you interpret it as a meta-notation like $e[e'/x]$ rather than an expression form.


* In an eagerly evaluated programming language, this is not equivalent because it evaluates $(f' f')$ too early. You can fix that by replacing $(f' f')$ with $(λx. f' f' x)$. With the substitution interpretation of $\textbf{let}$ and renaming of variables, that yields the FIX from the question.

$\endgroup$
0
$\begingroup$

M a = a a is the self-applicator combinator that receives a function and applies it to itself. The trick of passing itself as an argument is essential. Now,

y = f x   // function    
y = f y   // fixed-point function

The problem is y is referring to itself before being assigned; so we use the trick above.

y = (x x)
x x = f (x x)    // x is the name of the function which is ALSO the first argument

The problem is where does f come from?

There are a couple of ways to pass f in x x = f (x x).

#1:
    x = (L f)     // introduce a new function L
    (L f) (L f) = f ((L f) (L f))

#2:
    x x f = f (x x f)    // pass directly

NOTE: in both cases the pattern Y = f(Y)

The first method gives us Curry's Y-combinator. The second gives us Turing's!

We could end here, but for completeness we convert to the typical lambda notation you find in literature.

Curry's

(L f) (L f) = f ((L f) (L f)) where L a b = a (b b)
L = λf.λx. f (x x)
Y = λf. (L f) (L f)
Y = λf. (λx.f(x x)) (λx.f(x x))

Turing's

x x f = f (x x f)
U U f = f (U U f) where U a b = b(a a b)
Y = U U
Y = λf.((λx.λy.y(x x y)) (λx.λy.y(x x y)))
$\endgroup$
0
$\begingroup$

Having a one-step functional $G := (\lambda r.\lambda x.\ \dots r\dots)$ where $r$ is used for a "recursive" call (or calls), the corresponding recursive function denoted by the $\lambda$-term $R$ must fulfill

$$R = G\ R = G(GR) = \dots $$

precisely because $r$ is used for the recursive call(s).

Lambda terms have no names, but they can be passed as arguments to other terms, which will thus be able to refer to them. Thus we seek lambda terms $M$, $N$ such that

$$MN = G\ (NN) = G(G(NN)) = \dots $$

but we must have $R = GR$, thus $MN = NN$ i.e. $M = N$:

$$MM = G\ (MM) = G(G(MM)) = \dots $$

The term $M$ must depend on $G$ to be able to recreate it that way; thus we seek

$$ M = HG \\ HG(HG) = G(HG(HG))$$

i.e., with the combinators $C$, $B$ and $Ux = x\ x$, $H$ is a plain combinator defined as

$$ Hgz = g(z\ z ) = g(Uz) = CBUgz $$

which, when self-applied with any given appropriate $G$ term as seen above, will achieve what we want. Thus,

$$Yg = Hg(Hg) = U(Hg) = BU(CBU)g$$

or in lambda notation,

$$ H = \lambda g. \lambda z. g(z\ z) \\ Y = \lambda g. (\lambda z. g(z\ z))\ (\lambda z. g(z\ z)) $$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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