How to derive the Y combinator
Table of contents
Intro
In mathematics, there is a distinction between knowing how to prove something and knowing how to derive it. After all, proving an identity like
\[\sum_{i=0}^n i = \frac{n(n+1)}{2}\]requires nothing more than a straightforward proof by induction. However, to come up with that formula itself, to know how to find the right question to ask, one needs at least a little bit of ingenuity. By that same token, to prove that the Y combinator
\[\mathsf{Y} := \lambda f. (\lambda x. f(x x)) (\lambda x. f(x x))\]satisfies the fixed-point property $\mathsf Y f \leadsto_\beta f (\mathsf Y f)$, a couple of routine beta reductions will suffice. On the other hand, coming up with that expression from scratch is much more difficult.
When I first learned the lambda calculus, my initial impression was that it was too arcane, all these clever constructions and encodings that just magically seemed to work out in the end, no doubt devised by madmen with penchants for building Rube Goldberg machines. While I grew more comfortable with things like Church-encoded datatypes, the Y combinator remained mysterious. Eventually, I came upon a result known as Lawvere’s fixed-point theorem which I find quite helpful in explaining how one might come upon this expression. In this post I will explain Lawvere’s fixed-point theorem and how one might plausibly use it to derive the Y combinator.
Semantics for untyped lambda calculus
Suppose we are modelling the untyped lambda calculus using a set $X$. Given a term $T$ then, its denotation must lie in $X$: $[\![T]\!] \in X$. We also can think of $T$ as a function which acts on terms, so that $[\![T]\!] : X \rightarrow X$. This leads us to the conclusion that our $X$ must be such that $X \cong X^X$. Supposing we have a pair of functions $\mathsf{\Lambda} : X^X \rightarrow X$ and $\mathsf{\bullet} : X \rightarrow X^X$ that witness this isomorphism (for convenience’s sake let us also give $\mathsf{\bullet}$ binary infix notation), we see that we can translate lambda terms into this model by essentially mapping every lambda abstraction to $\mathsf{\Lambda}$ and every application to $\mathsf{\bullet}$. We will not go into the details here, but for instance, the lambda term
\[\lambda x. x (\lambda y. yx)\]is translated into $X$ as the element
\[\mathsf{\Lambda} (x \mapsto x \mathsf{\bullet} \mathsf{\Lambda}(y \mapsto y \mathsf{\bullet}x))\]Saying that $\mathsf{\bullet}$ is the left inverse of $\mathsf{\Lambda}$ gives us the equation
\[\mathsf{\Lambda}(f) \mathsf{\bullet} x = f(x).\]This is enough for us to prove that our semantics respects beta reduction (proof left as exercise for the reader) and will turn out to be all we need to apply Lawvere’s theorem in our context. The other equality (saying that $\mathsf{\Lambda}$ is the left inverse of $\mathsf{\bullet}$) gives us the equation
\[\mathsf{\Lambda} (y \mapsto x \mathsf{\bullet} y) = x\]which expresses the eta law and does not seem necessary for our purposes.
In classical mathematics (though not necessarily constructive mathematics) the only solutions to this set equation are singleton sets. For want of a more robust space of models, this led to the development of domain theory, essentially giving up on modelling using sets in favor of more exotic categories. Nonetheless, we will stick to our current set-based presentation for the sake of clarity.
Lawvere’s fixed-point theorem
Before we discuss Lawvere’s theorem, let us review Cantor’s:
Theorem: Let $X$ be a set. Then there is no surjection from $X$ onto $2^X$.
Proof: Suppose that $f : X \twoheadrightarrow 2^X$. Then we can construct $D : X \rightarrow 2$ by the rule $x \mapsto \neg f(x)(x)$. By surjectivity of $f$, there must be some $d \in X$ such that $f(d) = D$. However, this implies that
\[f(d)(d) = D(d) = \neg f(d)(d)\]a contradiction. $\blacksquare$
One can look at Lawvere’s result as an examination of the importance of the set $2$ in Cantor’s argument. After all, it is trivial to modify the proof to show that $X$ cannot surject onto things like $3^X$, $4^X$, $\omega^X$, and funnily enough even $0^X$. All we need to do is replace boolean negation ($\neg : 2 \rightarrow 2$) with a suitable function that has no fixed-points, and the final line above will yield a contradiction. To be precise: if $X$ surjects onto $A^X$, then it suffices to pick some $\varphi : A \rightarrow A$ without fixed-points and we are done. This is also why the argument won’t work for $1^X$: the only function from $1 \rightarrow 1$ is the identity, which of course has a fixed-point.
Lawvere’s theorem takes this insight and turns Cantor’s theorem on its head: instead of placing all of one’s attention on the paradoxical set $X$, we are invited to consider instead what such a surjection says about the set $A$. Let us see what it says:
Theorem: Let $A$ and $X$ be sets, and suppose that $X$ surjects onto $A^X$. Then for any function $\varphi : A \rightarrow A$, $\varphi$ has a fixed-point.
Proof: Suppose that $f : X \twoheadrightarrow A^X$, and suppose that $\varphi : A \rightarrow A$. We again construct the diagonal function $D : X \rightarrow A$ by $x \mapsto \varphi (f(x)(x))$. By surjectivity of $f$, there is some $d \in X$ such that $f(d) = D$. Hence,
\[f(d)(d) = D(d) = \varphi (f(d)(d))\]and therefore, $f(d)(d)$ is the desired fixed-point for $\varphi$. $\blacksquare$
Of course, the proof is exactly the same as Cantor’s, with minor modifications. The brilliance of this result lies not in the proof, but in how centering the result around $A$ instead of $X$ turns a non-existence statement into an existence statement. This sort of reframing is characteristic of how thinking constructively can yield positive results from negative ones.
Lawvere’s theorem gives us a fixed-point for any given $\varphi$, but we want a fixed-point functional; that is to say, a single object that tracks these fixed-points uniformly from the $\varphi$’s being input. Since we are thinking constructively, we will not deign to use choice here. After all, it is not too difficult to make Lawvere’s theorem uniform as long as we carefully consider our logical resources:
Theorem: Let $A$ and $X$ be sets, and suppose that $f : X \twoheadrightarrow A^X$ is a left inverse of $g : A^X \hookrightarrow X$. Then there is a functional $Y : A^A \rightarrow A$ such that for all $\varphi : A \rightarrow A$, $\varphi (Y (\varphi)) = Y(\varphi)$.
Proof: Again, construct the diagonal $D := x \mapsto \varphi (f (x)(x))$. Since $f$ is a left inverse of $g$, we have that $f(g(D)) = D$. Hence,
\[f(g(D))(g(D)) = D(g(D)) = \varphi (f (g(D)) (g(D)))\]and therefore
\[\varphi \mapsto f(g(D))(g(D)) = f(g(x \mapsto \varphi (f (x)(x))))(g(x \mapsto \varphi (f (x)(x))))\]is the desired functional. $\blacksquare$
The proof is the same as before; all we’ve done is uniformly selected the $d$ from the previous proof using the explicitly provided $g$ instead of using choice to implicitly create the necessary right inverse.
Bringing it all together
Recall that given $X$, a set model of untyped lambda calculus, we assume two functions, $\mathsf{\Lambda} : X^X \rightarrow X$ and $\mathsf{\bullet} : X \rightarrow X^X$, such that that $\mathsf{\bullet}$ is the left inverse of $\mathsf{\Lambda}$. Notice that this data perfectly fits the requirements for the uniform version of Lawvere’s theorem, with $\mathsf{\bullet}$ taking the role of $f$ and $\mathsf{\Lambda}$ taking the role of $g$. Therefore, this guarantees a fixed-point functional
\[\varphi \mapsto (\mathsf{\Lambda}(x \mapsto \varphi (x \mathsf{\bullet} x))) \mathsf{\bullet} (\mathsf{\Lambda}(x \mapsto \varphi (x \mathsf{\bullet} x))).\]The resemblance should be apparent by this point, though we still need to apply a few finishing touches. After all, we want an expression that takes an element and returns a fixed-point of it with respect to application, but our current expression takes a function. We can fix this by taking as input an element $f \in X$ in place of $\varphi$ and then coercing it to a function using $\mathsf{\bullet}$:
\[f \mapsto (f \mathsf{\bullet} -) \mapsto (\mathsf{\Lambda}(x \mapsto f \mathsf{\bullet} (x \mathsf{\bullet} x))) \mathsf{\bullet} (\mathsf{\Lambda}(x \mapsto f \mathsf{\bullet} (x \mathsf{\bullet} x))).\]Finally, to make this expression an element of $X$ itself instead of a function $X \rightarrow X$, we use $\mathsf{\Lambda}$ one last time:
\[\mathsf{\Lambda} (f \mapsto (\mathsf{\Lambda}(x \mapsto f \mathsf{\bullet} (x \mathsf{\bullet} x))) \mathsf{\bullet} (\mathsf{\Lambda}(x \mapsto f \mathsf{\bullet} (x \mathsf{\bullet} x)))).\]This corresponds precisely to the expression we needed, namely $\lambda f. (\lambda x. f(x x)) (\lambda x. f(x x))$.