login
The OEIS Foundation is supported by donations from users of the OEIS and by a grant from the Simons Foundation.

 

Logo


Hints
(Greetings from The On-Line Encyclopedia of Integer Sequences!)
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 i-th 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 non-universal 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 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.

MathOverflow, What's the smallest lambda-calculus 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

Lookup | Welcome | Wiki | Register | Music | Plot 2 | Demos | Index | Browse | More | WebCam
Contribute new seq. or comment | Format | Style Sheet | Transforms | Superseeker | Recent
The OEIS Community | Maintained by The OEIS Foundation Inc.

License Agreements, Terms of Use, Privacy Policy. .

Last modified July 6 06:05 EDT 2020. Contains 335476 sequences. (Running on oeis4.)