Deriving the Y-Combinator

Feb 28, 2026

Not that Y-combinator.

Haskell Curry’s “paradoxical” -combinator gives a fixed-point for every single term in the untyped -calculus. (Recall that in the untyped -calculus, as there is no notion of a term having type “function” or “variable,” every term may be regarded being allowed to have terms applied to it, which is in fact the crux of the derivation.)

Notions

For our purposes, our untyped -calculus will be a standard -theory, in the equational theoretic sense, in that it consists of the standard rules of the lambda calculus with the -conversion rule.

By the way

This tidbit is not really necessary or too interesting, but I thought I’d point it out. The -conversion rule is often called -reduction, but there’s a semantic distinction here. -conversion is defined by a binary relation called , which relates

Here, is not a distinct term in the lambda calculus but represents substituting all free occurrences of with in the term , while avoiding unintended capture of free variables via -conversion.

For any relation , we can define the compatible closure, an induced relation denoted . We call it the -reduction. It’s simply the relation itself, along with relating if (reduction on the left), a similar rule for reduction on the right, and reduction under abstraction.

When studying -calculi, we are usually interested in the -reduction.

A lambda abstraction is a term of the form . A combinator is a lambda abstraction with no free terms.

A fixed point of a term is simply any term such that . Additionally, if there exists a combinator such that for any terms and we have , i.e. is a fixed point of , then we say is a fixed-point combinator.

The Y

We proceed to derive the -combinator as the proof of this theorem.

Theorem

Every term in the simply untyped -calculus has a fixed point, moreover, we can find an explicit formula for such fixed points.

Let be any term. We basically are trying to solve for some term in the equation

Since appears in both sides, and it is not clear (nor true) that every term has the same fixed point, it’s pretty obvious our solution is going to contain the term itself . Therefore, we should search for a fixed-point combinator. We can first naively try the combinator that is the term itself. Let be arbitrary (free) and instead write

This doesn’t actually help us solve the problem at all, but it gives a hint, namely, we see . If only the left side was , then we would be done!

The key trick is to use self-reference. Write the combinator that gives

and see that . A fixed point! Now what could be? obviously works. Now just write out and bind and you recover the classical -combinator!

🎊 🎊 🎊