# 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 * 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$$

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.

• Are all those slashes supposed to represent lambda? – Wojowu Feb 25 at 16:44
• Shouldn't $\lambda 1$ have encoding 00110 (of length five), or am I missing something in the notation here? – Steven Stadnicki Feb 25 at 23:26
• When i changed from 0-based to 1-based variables, I forgot to update the encoding. It's fixed now. – John Tromp Feb 25 at 23:41
• For an upper bound, do you know what a lambda calculus formulation of twin primes / Goldbach / similar number-theoretic statements might look like? – Will Sawin Feb 27 at 0:17
• I also have an upper bound of 247 bits for finding an odd perfect number at github.com/tromp/AIT/blob/master/oddperfect.lam – John Tromp Mar 19 at 21:47