Implementing the Y-Combinator

Curry defines the $Y$ -combinator as:

$\begin{eqnarray*} Y &=& \lambda f .(\lambda x.f(xx))(\lambda x.f(xx)) \end{eqnarray*}$

which, when applied to a lambda term $g$ , $\beta$ -reduces in two steps to:

$\begin{eqnarray*} Y g &=& g (Y g) \end{eqnarray*}$

An equivalent $Y$ -combinator definition is the following:

$\begin{eqnarray*} Y &=& \lambda f.(\lambda x.xx)(\lambda x.f(xx)) \end{eqnarray*}$

which consists of part of the $\Omega$ combinator $\Omega = (\lambda x.xx)(\lambda x.xx)$ named $\omega = \lambda x.xx$ and the term $\lambda x.f(xx)$ .

If we $\beta$ -reduce the equivalent form once:

$\begin{eqnarray*} Y &=& \lambda f.(\lambda x.xx)(\lambda x.f(xx)) \end{eqnarray*}$

we would obtain Curry's form of the $Y$ -combinator.

Whilst the Curry form should work perfectly fine in Scheme and untyped lambda calculus, a statically typed language will not accept a function application such as $x x$ since the type system will forbid it. In order to do that, we start by applying an additional $\eta$ -abstraction to obtain the form:

$\begin{eqnarray*} Y &=& \lambda f.(\lambda x.xx)(\lambda x.(f (\lambda y.((x x) y)))) \end{eqnarray*}$

which can be re-written as:

$\begin{eqnarray*} Y &=& \lambda f.(\lambda x.xx)(f (\lambda y.((\lambda x.xx) y))) \end{eqnarray*}$

We notice that the $\omega$ combinator ( $\lambda x.xx$ ) appears twice in the resulting $Y$ -combinator which lets us express the $Y$ -combinator using the $\omega$ combinator:

$\begin{eqnarray*} \omega &=& \lambda x.xx \\ Y' &=& \lambda f.\omega(f (\lambda y.\omega y)) \end{eqnarray*}$

where $Y'$ and $Y$ are $\beta$ -equivalent.

Expressing the $Y$ combinator in terms of $\omega$ allows us to implement the $Y$ combinator in statically typed programming languages.

Implementations

Python
PHP

Exponentiation with Church Numerals

You may have seen the definition of exponentiation as the combinator $\mathbbold{EXP}$ (or $\mathbbold{POW}$ ) given by the lambda abstraction:

$\begin{eqnarray*} \mathbbold{EXP} &\equiv& \lambda m.\lambda n.mn \end{eqnarray*}$

where $n$ and $m$ are both Church numerals. $\mathbbold{EXP}$ will perform the mathematical equivalent of $m^{n}$ using Church numerals.

Therefore the application of a Church numeral $n$ to another Church numeral $\mathbbold{m}$ will yield the Church numeral equivalent to $m^n$ . For instance, applying the Church numeral $\mathbbold{1}$ to Church numeral $\mathbbold{2}$ should yield $m^{n} = 2^{1} \equiv \mathbbold{2}$ . While all the numerals work out, the application of the Church numeral zero to any other Church numeral $\beta$ -reduces to the identity function $\mathbbold{I}$ . For instance, applying the Church numeral $\mathbbold{0}$ to $\mathbbold{2}$ we have:

$\begin{eqnarray*} \mathbbold{0}(\mathbbold{2}) &\equiv& (\lambda f.\lambda x.x)(\lambda f.\lambda x.f(f(x))) \\ &\xrightarrow{\beta-reduce: \lambda f}& \lambda x.x \\ &\equiv& \mathbbold{I} \end{eqnarray*}$

Since the identity function $\mathbbold{I}$ is not a Church numeral, it would seem that the application is not defined. However, by the rules of exponentiation, any number to the power zero should yield one; in other words: $2^{0} = 1$ .

The trick here is that the identity function $\mathbbold{I}$ is equivalent with the Church numeral $\mathbbold{I}$ under the $\eta$ -expansion.

The $\eta$ -expansion is given by:

$\begin{eqnarray*} f &\xrightarrow{\eta-expand: f}& \lambda x.f(x) \end{eqnarray*}$

so we can re-work the application of the Church numeral zero to the Church numeral two:

$\begin{eqnarray*} \mathbbold{0}(\mathbbold{2}) &\equiv& (\lambda f.\lambda x.x)(\lambda f.\lambda x.f(f(x))) \\ &\xrightarrow{\beta-reduce: \lambda f}& \lambda x.x \\ &\xrightarrow{\alpha-convert: x \mapsto f}& \lambda f.f \\ &\xrightarrow{\eta-expand: f \mapsto \lambda x.f(x)}& \lambda f.\lambda x.f(x) \\ &\equiv& \mathbbold{1} \end{eqnarray*}$