How the Slowest Computer Programs Illuminate Math’s Fundamental Limits

Re:How the Slowest Computer Programs Illuminate Math’s Funda... by tromp on Friday December 11, 2020 @04:10AM (#25383793)

> 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

[ Parent | on HN ]

Re:How the Slowest Computer Programs Illuminate Math’s Funda... by bryan0 on Friday December 11, 2020 @12:28PM (#25388228)

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

[ Parent | on HN ]

Re:How the Slowest Computer Programs Illuminate Math’s Funda... by tromp on Friday December 11, 2020 @12:38PM (#25388344)

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...

[ Parent | on HN ]