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.

`00110`

(of length five), or am I missing something in the notation here? $\endgroup$9more comments