11
$\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 * 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.

$\endgroup$
  • 1
    $\begingroup$ Are all those slashes supposed to represent lambda? $\endgroup$ – Wojowu Feb 25 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 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 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 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 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.