login
Busy Beaver for the Binary Lambda Calculus (BLC) language BBλ2: the maximum output size of self-delimiting BLC programs of size n, or 0 if no program of size n exists.
1

%I #70 May 09 2024 10:59:14

%S 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,

%T 42,52,44,64,223,160

%N Busy Beaver for the Binary Lambda Calculus (BLC) language BBλ2: the maximum output size of self-delimiting BLC programs of size n, or 0 if no program of size n exists.

%C 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.

%C 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).

%C 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).

%C 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.

%C 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

%H John Tromp, <a href="https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861">Binary Lambda Calculus</a>

%H John Tromp, <a href="https://github.com/tromp/AIT/blob/master/ait/BBU.lhs">Haskell program to compute initial terms</a>

%H John Tromp, <a href="https://github.com/tromp/AIT/blob/master/ait/Compressible.hs">program demonstrating BLC compressibility</a>

%e 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.

%e 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)).

%Y Cf. A333479.

%K nonn,more

%O 1,6

%A _John Tromp_, Apr 09 2023