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



(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)



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."


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.


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


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)).


Cf. A028444, A114852, A195691, A333958.

Sequence in context: A102393 A228131 A019833 * A155743 A262246 A194193

Adjacent sequences:  A333476 A333477 A333478 * A333480 A333481 A333482




John Tromp, Mar 23 2020


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



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.)