Consider the following definition of the factorial function in a pseudo lambda calculus:
fac = λn. if n == 0 then 1 else n * fac (n - 1)
This definition makes use of recursion. But the lambda calculus doesn’t actually allow this. Partly because the lambda calculus does not have definitions using =. So this means that if we want to define this function in the lambda calculus, we’ll need to use some fancy lambda term that can get us something with the same effect as this. One such widget is the Y combinator, a mysterious thing that many people struggle with when they first see it. In explanations of the Y combinator, you’re usually presented with the definition of the combinator, and then some laborious attempt to make the definition intuitive, or just intuitive enough to make you stop puzzling over it.
What I’d like to do is instead try to show how to derive the definition of the Y combinator almost from first principles, so that the definition just falls out of the purpose of the Y combinator, as if for free. To do this, let’s just quickly remember what the definition of the lambda calculus is. We have terms, given by the following grammar, where x stands for any variable symbol:
T → x | T T | λx. T
And we have conversion/reduction rules (where M[y/x] means M, but with y replacing free occurences of x):
α: λx. M ⇝α λy. M[y/x] (if y is a new variable)
β: (λx. M) N ⇝β M[N/x]
η: λx. f x ⇝η f
Now let’s define the “problem” that we have. Essentially, we want to define something that behaves as if the following equation holds (this is a true equation, not a definition):
f = E (where E contains f)
Keep in mind, this is outside the lambda calculus, it’s just a meta-device for describing the issue. Also keep in mind, when I say that E contains f, you should interpret this to mean either that the whole of f appears within itself in an almost fractal way. This is ok to do because if we instead thought of E as containing the symbol f, we can always substitute the definition of f in for the symbol f and preserve equality, in some sense. Let’s treat this f as a lambda term (an infinitely long one or a self-referential one, however you want to think of it), and let’s perform a lambda abstraction on f:
g = (λrec. E[rec/f]) f
The choice of the name rec for the argument is because it represents the recursive occurance of f. Clearly, g reduces to f in one step using β reduction, so let’s identify f and g, because as before, they’re “the same” in some sense. Letting E′ = λrec. E[rec/f], we have
f = g = E′ f = E′ (E′ f) = … = E′ (E′ (…))
With E′s all the way down to infinity. So what we need is some sort of lambda term, let’s call it F (read “big f”), that will behave as if it’s E′ (E′ (…)). One way we could do this is if F were to β reduce directly into E′ F. We could keep on β reducing to get E′ (E′ F) then E′ (E′ (E′ F)) etc and if we kept β reducing forever, we’d get what we wanted. So that would be a perfectly good F. So we want something that behaves like this:
F ⇝β E′ F
Given the definition of β reduction from earlier, however, we know that F must be of the form M N. Or more precisely, it must be that M = λx. M′, for some M′. But let’s try to make our lives simpler, and assume that N = M, so that F = M M = (λx. M′) (λx. M′). What we’re saying now is that we have the following reduction:
M M = (λx. M′) M ⇝β E′ (M M)
because, as we said, F = M M = (λx. M′) M. Now, given the rules of β reduction, the reduction of (λx. M′) M must be M′[M/x]. But we also know that the reduction os E′ (M M), because that’s what we stipulated must be true. So M′[M/x] = E′ (M M). That leaves us with four choices for M′: either M′ = E′ (M M), in which case substitute M for x in M′[M/x] has no effect and produces what we want, or M′ = E′ (M x), in which case substitution produces E′ (M M) as we want, or M′ = E′ (x M) which also produces what we want, or M′ = E′ (x x) which again also produes what we want. Of these three choices, only the last one lets us choose M without running in the original problem of self-referentiality:
M = λx. E′ (x x)
F = M M = (λx. E′ (x x)) (λx. E′ (x x))
Now when we try out our little β reduction, as we wanted before, it works:
F = (λx. E′ (x x)) (λx. E′ (x x)) ⇝β E′ ((λx. E′ (x x)) (λx. E′ (x x)) = E′ F
And so we can keep β reducing F and get E′ (E′ (…)) all the way down. Ok, let’s remind ourselves why we want this, since we’ve gotten pretty far from that. We said f = E, but that we can also abstract over f, to get f = (λrec. E[rec/f]) f, and we said let E′ be λrec. E[rec/f], so that we get f = E′ (E′ (…)) equationally.
Now, using F, we have a lambda term that behaves just like f, because it reduces to E′ (E′ (…)) after an infinitely long time. Since our computations will last as long as we need them to, F behaves just like f. But F is a specially defined widget that only works for f because it’s build E′ into it. We can take F and abstract over E′, giving us a generic widget:
F = (λf. (λx. f (x x)) (λx. f (x x))) E′
This new abstracted term is precisely the Y combinator:
Y = λf. (λx. f (x x)) (λx. f (x x))
So we now have an effective way to get the behavior of f:
f = Y E′ = Y (λrec. E[rec/f])