Knowledge of lambda calculus and combinatory logic
Zero-based De Bruijn indices instead of named variables
⟨n⟩
encodes
n∈N
as a lambda calculus term
While analyzing various rapidly growing sequences in pure lambda
calculus due to procrastination, I stumbled upon
(nω)
and
(ωn).
I found the behavior of these very similar, yet very different sequences
interesting, so maybe someone else will, too.
n,
ω?!
The
ω
combinator is defined by
λ(00).
It therefore duplicates every term that’s applied.
(ωω)
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:
⟨2⟩≡λλ(1(10))
Similar to
ω,
these terms will also duplicate their first argument – this time
n
times.
(nω)
In this reduction
ω
gets cloned
n
times. After that,
ω
duplicates itself repeatedly.
Due to its repeated internal application,
ωn
turns out to represent
nn:
λλnn−1times1∘...∘1∘(10)
Fun fact: The exact bit count of its binary lambda calculus
encoding is
5⋅nn+6.
The factor
5
is the result of encoding repeated applications of
1s.
(ωin)
and beyond
Adding more applications to the
ω
combinator will result in a higher power tower. Using
(ω3n)
with
ω3=λ((00)0),
for example, will reduce to
nnn.
(ω3⟨3⟩)
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,
333
can be written as
n↑↑3.
One can escalate this even further:
n↑↑↑3
would equal
n↑↑(n↑↑(n↑↑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,
BBλ.
❦
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.