The OEIS is supported by the many generous donors to the OEIS Foundation.

 Hints (Greetings from The On-Line Encyclopedia of Integer Sequences!)
 A361211 Busy Beaver for the Binary Lambda Calculus (BLC) language: the maximum output size of self-delimiting BLC programs of size n, or 0 if no program of size n exists. 1
 0, 0, 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, 64, 223, 160 (list; graph; refs; listen; history; text; internal format)
 OFFSET 1,6 COMMENTS Self-delimiting BLC programs are inputs p to the BLC universal machine U (see link) that make U read all bits of p and none beyond. Formally, the only prefix p' of p for which U(p':Omega) has a normal form is p itself. The output of p is that normal form. Because programs for U are at most a constant number of bits longer than programs for any prefix-free programming language, this busy beaver is optimal: for any other busy beaver BB based on self-delimiting programs, there is a constant c such that a(c+n) >= BB(n). In particular, a(2+n) >= A333479(n), since for every closed term T, U(00 code(T) : Omega) = (lambda _. T) Omega = T. All entries above except for n=30 are of this form. We can show that for some k, a(ceiling((113/114)*n) + k) > A333479(n), i.e., universality eventually pays off for BLC. See program link for the supporting computation. - Bertram Felgenhauer, Apr 10 2023 LINKS Table of n, a(n) for n=1..32. John Tromp, Universal machine U John Tromp, Haskell program to compute initial terms John Tromp, program demonstrating BLC compressibility EXAMPLE The smallest closed lambda term is lambda x.x but its application to the unsolvable Omega lacks a normal form. The next smallest is lambda x.lambda y.y with encoding 000010 of size 6, which applied to Omega yields the normal form lambda x.x, giving a(6)=4. a(30) = 64 because, with T=lambda x.lambda y.lambda z.x(z x), (lambda x.x x) T applied to Omega yields maximum size normal form lambda x.lambda y.lambda z.x T(z (x T)). CROSSREFS Cf. A333479. Sequence in context: A019833 A362219 A333479 * A155743 A361621 A354491 Adjacent sequences: A361208 A361209 A361210 * A361212 A361213 A361214 KEYWORD nonn,more AUTHOR John Tromp, Apr 09 2023 STATUS approved

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

Last modified April 23 19:56 EDT 2024. Contains 371916 sequences. (Running on oeis4.)