2023-07-28

- Knowledge of lambda calculus and combinatory logic
- Zero-based De Bruijn indices instead of named variables
- $\langle n\rangle$ encodes $n\in\mathbb{N}$ as a lambda calculus term

While analyzing various rapidly growing sequences in pure lambda calculus due to procrastination, I stumbled upon $(n\omega)$ and $(\omega n)$. I found the behavior of these very similar, yet very different sequences interesting, so maybe someone else will, too.

The $\omega$ combinator is defined by $\lambda(0 0)$. It therefore duplicates every term that’s applied. $(\omega \omega)$ will result in an infinite loop.

For this sequence to work, a number $n$ encoded in lambda calculus uses the Church encoding. Church numerals are defined by an $n$-fold composition of the outermost abstraction: $\langle 2\rangle\equiv\lambda\lambda(1 (1 0))$ Similar to $\omega$, these terms will also duplicate their first argument – this time $n$ times.

In this reduction $\omega$ gets cloned $n$ times. After that, $\omega$ duplicates itself repeatedly.

$\begin{align*} (\langle2\rangle\omega)\equiv&\ (\lambda\lambda(1 (1 0))\ \lambda(0 0))\\ \leadsto&\ \lambda(\lambda(0 0)\ (\lambda(0 0)\ 0))\\ \leadsto&\ \lambda(\lambda(0 0)\ (0 0))\\ \leadsto&\ \lambda((0 0) (0 0)) \end{align*}$

As $\omega$ duplicates itself $n-1$ times, the growth of $(n\omega)$ is in $\mathcal{O}(2^n)$.

For higher $n$, the reduced term will look like this: $\lambda\underbrace{(((0 0)^2)^2...)^2}_{n-1\ \mathrm{times}}$

*Fun fact*: The exact bit count of its binary lambda calculus
encoding is
$2^{n+2}$.

This term is just the inverted application of $(n\omega)$. Therefore, $n$ first gets duplicated by $\omega$ and then $n$ clones itself $n$ times:

$\begin{align*} (\omega\langle2\rangle)\equiv&\ (\lambda(0 0)\ \lambda\lambda(1 (1 0)))\\ \leadsto&\ (\lambda\lambda(1 (1 0))\ \lambda\lambda(1 (1 0)))\\ \leadsto&\ \lambda(\lambda\lambda(1 (1 0))\ (\lambda\lambda(1 (1 0))\ 0))\\ \leadsto&\ \lambda(\lambda\lambda(1 (1 0))\ \lambda(1 (1 0)))\\ \leadsto&\ \lambda\lambda(\lambda(2 (2 0))\ (\lambda(2 (2 0))\ 0))\\ \leadsto&\ \lambda\lambda(\lambda(2 (2 0))\ (1 (1 0)))\\ \leadsto&\ \lambda\lambda(1 (1 (1 (1 0))))\\ \equiv&\ \langle4\rangle \end{align*}$

Due to its repeated internal application, $\omega n$ turns out to represent $n^n$: $\lambda\lambda\underbrace{1\circ...\circ1}_{n^n-1\ \mathrm{times}}\circ(10)$

*Fun fact*: The exact bit count of its binary lambda calculus
encoding is
$5\cdot n^n + 6$.
The factor
$5$
is the result of encoding repeated applications of
$1$s.

Adding more applications to the $\omega$ combinator will result in a higher power tower. Using $(\omega_3 n)$ with $\omega_3=\lambda((0 0) 0)$, for example, will reduce to $n^{n^n}$. $(\omega_3\langle 3\rangle)$ already can’t easily be solved by most traditional reducers.

*Detour*: After getting caught in the depths of Googology, I
now know that these power towers have quite interesting notations. Using
Knuth’s up-arrow notation,
$3^{3^3}$
can be written as
$n\uparrow\uparrow3$.
One can escalate this even further:
$n\uparrow\uparrow\uparrow3$
would equal
$n\uparrow\uparrow (n\uparrow\uparrow(n\uparrow\uparrow n))$.
Graham’s
number abuses this notation to create an unimaginably huge number.
Yet, to come back to lambda calculus, numbers **even
bigger** than Graham’s number can be represented in just
**8 bytes** of binary encoded lambda calculus! See this Googology
entry and this codegolf
post.

*However*, these numbers are still basically zero compared to
the growth of busy
beavers. One of my next posts will discuss some interesting aspects
of the busy beaver of lambda calculus,
$\mathrm{BB}_\lambda$.

$❦$

Thanks for reading. Suggest improvements or fixes via email. Support on Ko-fi.

Methods used in this article include bruijn’s

`:time`

and`:length`

commands.