A333479 Busy Beaver for lambda calculus BBλ: the maximum beta normal form size of any closed lambda term of size n, or 0 if no closed term of size n exists.

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

Offset: 1

Author

John Tromp, Mar 23 2020

Keywords

• nonn

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(404) > f_{PTO(Z_2)+1}(4), as shown in 1st Stackexchange link. - John Tromp, Dec 17 2024

a(1850) > Loader's number, as shown in 2nd Stackexchange link. - John Tromp, Dec 17 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

An oracle form of this Busy Beaver is given in sequence A385712. - John Tromp, Jul 23 2025

Examples

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

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

• bbchallenge wiki, Busy Beaver for lambda calculus
• AIT repo on Github, melo.lam.
• Code Golf Stack Exchange, Comment on BMS[26] entry
• Code Golf Stack Exchange, 1850 bit lambda term exceeding Loader's number
• MathOverflow, What's the smallest lambda-calculus term not known to have a normal form?, 2020.
• John Tromp, The largest number representable in 64 bits, John's Blog.
• John Tromp, Lambda encoding
• John Tromp, Haskell program for analyzing Busy Beaver numbers
• John Tromp, program output analysis
• John Tromp, Lambda term for 111 bit blc program computing 4 iterations of ε0 level growth
• Index entries for sequences related to Busy Beaver problem

Crossrefs

Cf. A028444, A114852, A195691, A333958, A361211, A385712.

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