A333479 Busy Beaver for lambda calculus BBλ: the maximum normal form size of any closed lambda term of size n, or 0 if no closed term of size n exists.

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

Offset

1,4

Comments

Sizes of terms are defined as in Binary Lambda Calculus (see Lambda encoding link) by size(lambda M)=2+size(M), size(M N)=2+size(M)+size(N), and size(V)=1+i for a variable V bound by the i-th enclosing lambda.

a(34), a(35) and a(36) correspond to Church numerals 2^2^2^2, 3^3^3, and 2^2^2^3, where numeral n has size 5*n+6.

a(38) > 10^19729, corresponding to Church numeral 2^2^2^2^2.

Only a finite number of entries can be known, as the function is uncomputable.

Quoting from Chaitin's paper below: "to information theorists it is clear that the correct measure is bits, not states [...] to deal with Sigma(number of bits) one would need a model of a binary computer as simple and compelling as the Turing machine model, and no obvious natural choice is at hand."

a(49) > Graham's number, as shown in program melo.lam in the links. - John Tromp, Dec 04 2023

a(111) > f_{ε_0+1}(4), as shown in program E00.lam in the links. - John Tromp, Aug 24 2024

a(415) > f_{PTO(Z_2)+1}(4), as shown in 1st Stackexchange link. - John Tromp, Aug 24 2024

a(1864) > Loader's number, as shown in 2nd Stackexchange link. John Tromp, Sep 21 2024

A universal form of this Busy Beaver, using the binary input feature of Binary Lambda Calculus, is given in sequence A361211. - John Tromp, May 24 2023

References

Gregory Chaitin, Computing the Busy Beaver Function, in T. M. Cover and B. Gopinath, Open Problems in Communication and Computation, Springer, 1987, pages 108-112.

John Tromp, Binary Lambda Calculus and Combinatory Logic, in Randomness And Complexity, from Leibniz To Chaitin, ed. Cristian S. Calude, World Scientific Publishing Company, October 2008, pages 237-260.

Links

Table of n, a(n) for n=1..36.

John's Blog, The largest number representable in 64 bits.

AIT repo on Github, melo.lam.

MathOverflow, What's the smallest lambda-calculus term not known to have a normal form?, 2020.

John Tromp, Lambda encoding

John Tromp, Haskell program for analyzing Busy Beaver numbers

John Tromp, program output analysis

John Tromp, Lambda term for 111 bit blc program computing 4 iterations of ε0 level growth

Code Golf Stack Exchange, Comment on BMS[26] entry

Code Golf Stack Exchange, 1864 bit lambda term exceeding Loader's number

Index entries for sequences related to Busy Beaver problem

Example

The smallest closed lambda term is lambda x.x with encoding 0010 of size 4, giving a(4)=4, as it is in normal form. There is no closed term of size 5, so a(5)=0. a(21)=22 because of term lambda x. (lambda y. y y) (x (lambda y. x)).

Crossrefs

Cf. A028444, A114852, A195691, A333958, A361211.

Sequence in context: A370743 A019833 A362219 * A361211 A155743 A361621

Adjacent sequences: A333476 A333477 A333478 * A333480 A333481 A333482

Keyword

nonn

Author

John Tromp, Mar 23 2020

Extensions

a(33)-a(34) from John Tromp, Apr 10 2020

a(35) from John Tromp, Apr 18 2020

a(36) from John Tromp, Apr 19 2020

Status

approved