Deriving the Theta Combinator

• October 13, 2021
• (last revised on March 3, 2023)

This post is based on a lovely article on “Deriving the $Y$ Combinator”.

In a course on programming language fundamentals, our lecturer proved the Turing completeness of untyped $\lambda$ calculus by encoding Gödel’s recursive functions into the calculus. This proof included a translation of the primitive recursion operation into a parametrized extension of the much simpler function composition operation. Sadly, the rigid nature of this translation meant that he needed new ideas to encode the $\mu$-operator. These were precisely the $Y$ and $\mathrm{\Theta }$ combinators, two magical operators that exploit the structure of the reduction rules to simulate $\mu$.

In this entry, I’d like to illustrate a more natural way to represent recursion that leads quite neatly onto one (the other one) of these combinators. This way, I hope to de-mystify them a little.

Consider the following function. $$f(x)=\{\begin{array}{ll}1,& x=0\\ f(x-1)+1& \text{otherwise}\end{array}$$ It’s easy to see that $f$ is primitive recursive. Consider the following (incorrect) $\lambda$ translation: $$f\triangleq \lambda x.[\mathsf{if}\mathsf{\_}\mathsf{zero}]x[1]([\mathsf{sum}][1](f([\mathsf{pred}]x)))$$ Here, $[\mathsf{if}\mathsf{\_}\mathsf{zero}]$ is a $\lambda$ function of three variables that reduces to the second if the first is zero, and to the third otherwise. $[\mathsf{sum}]$ and $[\mathsf{pred}]$ can be similarly understood as translations of the addition and predecessor operations in $\lambda$ calculus.

The above translation is syntactically incorrect because $f$ is a free variable on the right hand side. It is, however, an almost mechanical translation of the function definition in $\lambda$-calculus. This makes it easy to generalize.

A natural fix for this syntactic error is to simply declare $f$ a parameter in the function definition. This gives $$M\triangleq \lambda fx.[\mathsf{if}\mathsf{\_}\mathsf{zero}]x[1]([\mathsf{sum}][1](f([\mathsf{pred}]x)))$$ One might hope that $MM$ computes $f$ correctly. Sadly, this won’t work because $f$ (in the body) is designed to take in a single parameter (whereas $M$ takes 2). A creative solution suggests $$M\triangleq \lambda fx.[\mathsf{if}\mathsf{\_}\mathsf{zero}]x[1]([\mathsf{sum}][1](ff([\mathsf{pred}]x))$$ $MM$ will now properly simulate $f$: $$MM{\to }_{\beta }\lambda x.[\mathsf{if}\mathsf{\_}\mathsf{zero}]x[1]([\mathsf{sum}][1](MM([\mathsf{pred}]x)))$$

Let’s take a step back and observe what we’ve accomplished. We began by realizing that to encode recursion, we needed to reference a function in its definition. While we weren’t able to do that directly, we were able to abstract that reference away as a variable that theoretically, any function could replace. But when we replaced that variable with the right function (which turned out to be the same function), we were left with an expression for the input (recursive) function.

(Notice the potential for an infinite sequence of $\beta$ reductions at $MM$, characteristic of Turing completeness!)

It turns out that this translation scheme is sufficient to encode all $\mu$-recursive functions. Recall that the objective was to produce $C$ such that $$Cx[n_1][n_2]\dots [n_k]{\stackrel{\ast }{\to }}_{\beta }[\mathsf{if}\mathsf{\_}\mathsf{then}\mathsf{\_}\mathsf{else}]([\mathsf{if}\mathsf{\_}\mathsf{zero}]gx[n_1]\dots [n_k])x(C([\mathsf{succ}]x)[n_1]\dots [n_k])$$ with $C(x)={\mu }_x(g(x,n_1,\dots n_k))$ (this is just the definition of the $\mu$-operator). Consider $$D\triangleq \lambda fx{n}_1{n}_2\dots n_k.[\mathsf{if}\mathsf{\_}\mathsf{then}\mathsf{\_}\mathsf{else}]([\mathsf{if}\mathsf{\_}\mathsf{zero}]gx{n}_1\dots n_k)x(ff([\mathsf{succ}]x)n_1\dots n_k)$$ Our discussion shows that taking $C=DD$ captures general recursion, proving the Turing completeness of untyped $\lambda$ calculus! Notice that $$DD{\to }_{\beta }\lambda x{n}_1\dots n_k.[\mathsf{if}\mathsf{\_}\mathsf{then}\mathsf{\_}\mathsf{else}]([\mathsf{if}\mathsf{\_}\mathsf{zero}]gx{n}_0\dots n_k]x(DD([\mathsf{succ}]x)n_1\dots n_k)$$

Deriving the $\mathrm{\Theta }$ Combinator

The first step in the translation scheme discussed so far is to regard the self-references as a parameter. In our toy example, this caused $f^{\prime }$: $$f^{\prime }(g,x)=\{\begin{array}{ll}1,& x=0\\ 1+g(x-1)& \text{otherwise}\end{array}$$ We can easily write this interim function in $\lambda$ calculus: $$\begin{array}{r}F\triangleq \lambda gx.[\mathsf{if}\mathsf{\_}\mathsf{zero}]x[1]([\mathsf{sum}][1](g([\mathsf{pred}]x)))\end{array}$$

Our goal now is to construct an expression $C$ that always reduces to $FC$. The usefulness of $C$ is captured by the following reduction sequence: $$\begin{array}{rl}FCx& {\to }_{\beta }[\mathsf{if}\mathsf{\_}\mathsf{zero}]x[1]([\mathsf{sum}][1](C([\mathsf{pred}]x)))\\ & {\to }_{\beta }C(\mathsf{[}\mathsf{pred}\mathsf{]}x)& & \mathit{\text{(assuming }}x>0\mathit{\text{)}}\\ & {\to }_{\beta }FC(\mathsf{[}\mathsf{pred}\mathsf{]}x)\end{array}$$ Using $C$, we can trick a reference to $F$ inside $F$. All that remains now is to solve for $C$.

Begin by observing that we want $$\begin{array}{r}C{\to }_{\beta }FC\end{array}$$ $C$ must thus be a reducible expression. For simplicity, suppose that $C=(\lambda x.A)B$ for some $A$ and $B$. This gives $$\begin{array}{r}A[x:=B]\equiv F(C)\end{array}$$ The simplest solution here is to set $A=x{C}^{\prime }$ and $B=F$ for some $C^{\prime }$. $$\begin{array}{r}\begin{array}{rl}F(C^{\prime }[x:=F])& =F(C)\\ ⟹C^{\prime }[x:=F]& =C=(\lambda x.x{C}^{\prime })F\end{array}\end{array}$$ Again, the simplest substitution is $C^{\prime }=Dx$. $$\begin{array}{rl}D[x:=F]F& =(\lambda x.x(Dx))F\\ ⟹D[x:=F]& =\lambda x.x(Dx))\\ ⟹D& =\lambda x.x(Dx)& & \mathit{\text{(replacing free variables has no effect)}}\end{array}$$ This is a recursive equation of the form we’ve solved in the earlier section! Hence, set $$\begin{array}{r}M\triangleq \lambda Dx.x(DDx)\end{array}$$ where $N=MM$ is the solution. Write this explicitly. $$\begin{array}{r}N=(\lambda Dx.x(DDx))(\lambda Dx.x(DDx))=\mathrm{\Theta }\end{array}$$ It appears that we’ve stumbled onto the $\mathrm{\Theta }$ Combinator!

To summarize, we have $$\begin{array}{r}C=(\lambda x.x(\mathrm{\Theta }x))F\end{array}$$ Such a $C$ can be written for any $F$, and is guaranteed to reduce to $F(CF)$: $$CF{\to }_{\beta }F(CF){\to }_{\beta }F(F(CF))$$ Expanding $$\begin{array}{rl}(\lambda x.x(\mathrm{\Theta }x))F& {\to }_{\beta }F(\mathrm{\Theta }F)\\ & {\to }_{\beta }F(F(\mathrm{\Theta }F))\end{array}$$ Indicating that $\mathrm{\Theta }F{\to }_{\beta }F(\mathrm{\Theta }F)$, which makes $C=\mathrm{\Theta }F$ an even simpler solution.