OFFSET
1,6
COMMENTS
Self-delimiting BLC programs are inputs p to the BLC universal machine U (defined in first 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.
This Busy Beaver is directly related to Kolmogorov Complexity: a(n) = max {size(x)| KP(x) = n }, where KP is the prefix Kolmogorov complexity (defined in first link).
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
John Tromp, Binary Lambda Calculus
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
KEYWORD
nonn,more
AUTHOR
John Tromp, Apr 09 2023
STATUS
approved