|
%I #123 Dec 17 2023 11:21:17
%S 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 44,58,223,160,267,298,1812,327686,38127987424941,
%U 578960446186580977117854925043439539266349923328202820197287920039565648199686
%N Busy Beaver for 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.
%C 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 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 a(38) > 10^19729, corresponding to Church numeral 2^2^2^2^2.
%C Only a finite number of entries can be known, as the function is uncomputable.
%C 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 a(49) > Graham's number, as shown in program melo.lam in the links. _John Tromp_, Dec 04 2023
%C 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
%D 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 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 John's Blog, <a href="https://tromp.github.io/blog/2023/11/24/largest-number">The largest number representable in 64 bits</a>.
%H AIT repo on Github, <a href="https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam">melo.lam</a>.
%H 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 John Tromp, <a href="https://tromp.github.io/cl/Binary_lambda_calculus.html#Lambda_encoding">Lambda encoding</a>
%H John Tromp, <a href="https://github.com/tromp/AIT/blob/master/ait/BB.lhs">Haskell program for analyzing Busy Beaver numbers</a>
%H John Tromp, <a href="https://github.com/tromp/AIT/blob/master/ait/BB.txt">program output analysis</a>
%H <a href="/index/Br#beaver">Index entries for sequences related to Busy Beaver problem</a>
%e 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)).
%Y Cf. A028444, A114852, A195691, A333958, A361211.
%K nonn
%O 1,4
%A _John Tromp_, Mar 23 2020
%E a(33)-a(34) from _John Tromp_, Apr 10 2020
%E a(35) from _John Tromp_, Apr 18 2020
%E a(36) from _John Tromp_, Apr 19 2020
|
