# What's the smallest $\lambda$-calculus term not known to have a normal form?

For Turing Machines, the question of halting behavior of small TMs has been well studied in the context of the Busy Beaver function, which maps n to the longest output or running time of any halting n state TM. The smallest TM with unknown halting behavior has 5 states. It takes $$5\cdot2\cdot\log_2(5\cdot4 + 4)$$ or roughly 46 bits to describe, 50 bits if we assume a straightforward encoding.

In comparison, $$\lambda$$-calculus terms have a simple binary encoding: $$00$$ for lambda, $$01$$ for application, and $$1^n0$$ for variable with de Bruijn index $$n$$. It's natural to define a $$\lambda$$-calculus analog of the busy beaver function as the maximum normal form size of any size $$n$$ closed lambda term.

As the smallest closed lambda term is $$\lambda\,1$$, with encoding $$0010$$, we determine $$BB_{\lambda}(4) = 4$$ The next smallest ones, $$\lambda\,\lambda\,1$$ and $$\lambda\,\lambda\,2$$ are similarly already in normal form, and give $$BB_{\lambda}(6) = 6,\qquad BB_{\lambda}(7) = 7$$ $$BB_{\lambda}(n)$$ will have to remain undefined for $$n < 4$$ or $$n = 5$$.

The first enlarged normal form shows up at $$\lambda\,(\lambda\,1\,1)\,(1\,(\lambda\,2))$$ which gives $$BB_{\lambda}(21) = 22$$ $$BB_{\lambda}$$ starts to grow rapidly at $$n \geq 30$$, since tripling Church numeral two, $$(\lambda\,1\,1\,1)\,(\lambda\,\lambda\,2\,(2\,1))$$ with normal form Church numeral $$2^{2^2}= 16$$, gives $$BB_{\lambda}(30) \geq 5 \cdot 16 + 6 = 86$$ and quadrupling/quintupling give $$BB_{\lambda}(34) \geq 5 \cdot 2^{16} + 6$$ $$BB_{\lambda}(38) \geq 5 \cdot 2^{2^{16}} + 6$$ which exceed the TM Busy Beavers for 4 and 5 states.

An Ackermann-like function takes a mere 29 bits. A twisted application to Church numeral $$2$$ yields a $$BB_{\lambda}(51)$$ exceeding 2↑↑↑↑5.

Graham's number is exceeded in at most 63 bits, giving $$BB_{\lambda}(63) \geq 5 \cdot G + 6$$ (compared with a 16 state TM that needs over 192 bits to describe).

What's the smallest n for which $$BB_{\lambda}(n)$$ is unknown in ZFC?

One upper bound is 213 bits.

Let's try to narrow it down some more.

Function $$BB_{\lambda}$$ has been added to the Online Encyclopedia for Integer Sequences.

• Are all those slashes supposed to represent lambda? Feb 25, 2020 at 16:44
• Yes, they were. I replaced them by actual lambdas now. Feb 25, 2020 at 18:00
• Shouldn't $\lambda 1$ have encoding 00110 (of length five), or am I missing something in the notation here? Feb 25, 2020 at 23:26
• When i changed from 0-based to 1-based variables, I forgot to update the encoding. It's fixed now. Feb 25, 2020 at 23:41
• I also have an upper bound of 247 bits for finding an odd perfect number at github.com/tromp/AIT/blob/master/oddperfect.lam Mar 19, 2020 at 21:47