On: How the Slowest Computer Programs Illuminate Math’...

[tromp]

> The busy beaver game is all about the behavior of Turing machines

A busy beaver for lambda calculus is even easier to define:

the maximum normal form size of any closed lambda term of size n (or 0 if none exists).

The series [1] starts as 0, 0, 0, 4, 0, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 24, 26, 30, 42, 52, 44, 58, 223, 160, 267, 298, 1812, 327686, 38127987424941,

578960446186580977117854925043439539266349923328202820197287920039565648199686

Results are more fine grained than for TMs because these sizes are in units of bits (lambda and application measuring as 2 bits, and a variable bound by n'th enclosing lambda as n+1 bits).

Graham's number is surpassed within 114 bits, while the smallest known TM for surpassing it takes 225 bits to describe.

[1] https://oeis.org/A333479

[bryan0 → tromp]

Cool. What are the first few lambda terms in the sequence?

[tromp → bryan0]

Here's the initial output of a Haskell program used to find them (courtesy of Bertram Felgenhauer):

    4:  \1
    6:  \\1
    7:  \\2
    8:  \\\1
    9:  \\\2
    10: \\\\1
    11: \\\\2
    12: \\\\\1
    13: \\\\\2
    14: \\\\\\1
    15: \\\\\\2
    16: \\\\\\\1
    17: \\\\\\\2
    18: \\\\\\\\1
    19: \\\\\\\\2
    20: \\\\\\\\\1
    21: \(\1 1) (1 (\2))

A few more are given in [1].

[1] https://mathoverflow.net/questions/353514/whats-the-smallest...