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
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, program output analysis
Code Golf Stack Exchange, Comment on BMS[26] entry
Code Golf Stack Exchange, 1864 bit lambda term exceeding Loader's number
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
KEYWORD
nonn,changed
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