cp's OEIS Frontend

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.

%I A333479 #174 Jul 23 2025 09:06:29
%S A333479 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,
%T A333479 44,58,223,160,267,298,1812,327686,38127987424941,
%U A333479 578960446186580977117854925043439539266349923328202820197287920039565648199686
%N 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.
%C A333479 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.
%C A333479 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.
%C A333479 a(38) > 10^19729, corresponding to Church numeral 2^2^2^2^2.
%C A333479 Only a finite number of entries can be known, as the function is uncomputable.
%C A333479 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."
%C A333479 a(49) > Graham's number, as shown in program melo.lam in the links. - _John Tromp_, Dec 04 2023
%C A333479 a(111) > f_{ε_0+1}(4), as shown in program E00.lam in the links. - _John Tromp_, Aug 24 2024
%C A333479 a(404) > f_{PTO(Z_2)+1}(4), as shown in 1st Stackexchange link. - _John Tromp_, Dec 17 2024
%C A333479 a(1850) > Loader's number, as shown in 2nd Stackexchange link. - _John Tromp_, Dec 17 2024
%C A333479 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
%C A333479 An oracle form of this Busy Beaver is given in sequence A385712. - _John Tromp_, Jul 23 2025
%D A333479 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.
%D A333479 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.
%H A333479 bbchallenge wiki, <a href="https://wiki.bbchallenge.org/wiki/Busy_Beaver_for_lambda_calculus">Busy Beaver for lambda calculus</a>
%H A333479 AIT repo on Github, <a href="https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam">melo.lam</a>.
%H A333479 Code Golf Stack Exchange, <a href="https://codegolf.stackexchange.com/questions/18028/largest-number-printable/273656#273656">Comment on BMS[26] entry</a>
%H A333479 Code Golf Stack Exchange, <a href="https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634">1850 bit lambda term exceeding Loader's number</a>
%H A333479 MathOverflow, <a href="https://mathoverflow.net/questions/353514/whats-the-smallest-lambda-calculus-term-not-known-to-have-a-normal-form">What's the smallest lambda-calculus term not known to have a normal form?</a>, 2020.
%H A333479 John Tromp, <a href="https://tromp.github.io/blog/2023/11/24/largest-number">The largest number representable in 64 bits</a>, John's Blog.
%H A333479 John Tromp, <a href="https://tromp.github.io/cl/Binary_lambda_calculus.html#lambda_encoding">Lambda encoding</a>
%H A333479 John Tromp, <a href="https://github.com/tromp/AIT/blob/master/BB/BB.lhs">Haskell program for analyzing Busy Beaver numbers</a>
%H A333479 John Tromp, <a href="https://github.com/tromp/AIT/blob/master/BB/BB.txt">program output analysis</a>
%H A333479 John Tromp, <a href="https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/BBE0.lam">Lambda term for 111 bit blc program computing 4 iterations of ε0 level growth</a>
%H A333479 <a href="/index/Br#beaver">Index entries for sequences related to Busy Beaver problem</a>
%e A333479 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)).
%Y A333479 Cf. A028444, A114852, A195691, A333958, A361211, A385712.
%K A333479 nonn
%O A333479 1,4
%A A333479 _John Tromp_, Mar 23 2020
%E A333479 a(33)-a(34) from _John Tromp_, Apr 10 2020
%E A333479 a(35) from _John Tromp_, Apr 18 2020
%E A333479 a(36) from _John Tromp_, Apr 19 2020