|
| |
|
|
A333479
|
|
Busy Beaver for lambda calculus: the maximum normal form size of any closed lambda term of size n, or 0 if no closed term of size n exists.
|
|
2
|
|
|
|
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
(list;
graph;
refs;
listen;
history;
text;
internal format)
|
|
|
|
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 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
|
|
|
|
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. x x) (x (lambda y. x)).
|
|
|
CROSSREFS
|
|
|
|
KEYWORD
|
nonn
|
|
|
AUTHOR
|
|
|
|
EXTENSIONS
|
|
|
|
STATUS
|
approved
|
| |
|
|
