16
$\begingroup$

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 35 bits. When applied to Church numeral $2$ it yields a $BB_{\lambda}(53)$ exceeding an exponential tower of 256 $2$s.

Graham's number is expressible in at most 114 bits, giving $$ BB_{\lambda}(114) \geq 5 \cdot 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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.