

A361211


Busy Beaver for the Binary Lambda Calculus (BLC) language: the maximum output size of selfdelimiting 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

Selfdelimiting 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 prefixfree programming language, this busy beaver is optimal: for any other busy beaver BB based on selfdelimiting 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



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



KEYWORD

nonn,more


AUTHOR



STATUS

approved



