24
$\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 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 49 bits, giving $$ BB_{\lambda}(49) \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.

$\endgroup$
14
  • 1
    $\begingroup$ Are all those slashes supposed to represent lambda? $\endgroup$
    – Wojowu
    Commented Feb 25, 2020 at 16:44
  • 1
    $\begingroup$ Yes, they were. I replaced them by actual lambdas now. $\endgroup$
    – John Tromp
    Commented Feb 25, 2020 at 18:00
  • 1
    $\begingroup$ Shouldn't $\lambda 1$ have encoding 00110 (of length five), or am I missing something in the notation here? $\endgroup$ Commented Feb 25, 2020 at 23:26
  • 2
    $\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
    Commented Feb 27, 2020 at 0:17
  • 3
    $\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
    Commented Mar 19, 2020 at 21:47

0

You must log in to answer this question.

Browse other questions tagged .