

A333479


Busy Beaver for binary 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.


1



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 in binary lambda calculus are defined 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 ith enclosing lambda.
Note that there is also a universal form of binary lambda calculus in which encoded lambda terms are applied to pure binary data. This busy beaver uses the simpler nonuniversal form with lambda terms only.
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."


REFERENCES

Gregory Chaitin, Computing the Busy Beaver Function, in T. M. Cover and B. Gopinath, Open Problems in Communication and Computation, Springer, 1987, pages 108112.
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 237260.


LINKS

Table of n, a(n) for n=1..36.
MathOverflow, What's the smallest lambdacalculus term not known to have a normal form?, 2020.
John Tromp, Haskell program for analyzing Busy Beaver numbers
John Tromp, program output analysis
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. x x) (x (lambda y. x)).


CROSSREFS

Cf. A028444, A114852, A195691, A333958.
Sequence in context: A102393 A228131 A019833 * A155743 A262246 A194193
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



