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 * 2 * log$_2$ (5*4 + 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$^n$0 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, 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 * 16 +6 = 86$

and quadrupling/quintupling give

BB$_{\lambda}(34) \geq 5 * 2^{16} + 6$

BB$_{\lambda}(38) \geq 5 * 2^{2^{16}} + 6$

which exceed the TM Busy Beavers for 4 and 5 states.

An Ackermann-like function takes a mere 35 bits. When applied to Church numeral 2 it yields a BB$_{\lambda}$(53) exceeding an exponential tower of 256 2s.

Graham's number is expressible in at most 116 bits, giving

BB$_{\lambda}(116) \geq 5 * G + 6$

(compared with an 18 state TM that needs 225 bits to describe).

What's the smallest n for which BB$_{\lambda}$(n) is unknown?

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$ – Steven Stadnicki Feb 25 at 23:26