A385712 Busy Beaver BBlambda_1 for lambda calculus with a BB (A333479) oracle: the maximum beta/oracle normal form size of any 1-closed lambda term of size n, or 0 if no 1-closed term of size n exists.

0, 2, 0, 4, 5, 6, 7, 26, 9, 36, 41, 266, 51, 2894802230932904885589274625217197696331749616641014100986439600197828240998436

Offset: 1

Author

John Tromp, Jul 07 2025

Keywords

• nonn

Comments

A 1-closed term is a term in de Bruijn notation that is closed with 1 additional lambda in front. Any variable bound to that lambda is a free variable "f" in the term.

An oracle reduction step reduces f t, where t is a closed normal form of size s, to Church numeral BB(s).

The jump at a(14) is due to lambda term 1(1(\\1)). Subterm (1(\\1)) is an application of free variable f to a closed term of size 6 and thus oracle reduces to Church numeral BB(6) = C6. Next, (1 C6) is an application of free variable f to a closed term of size 36 and thus oracle reduces to Church numeral BB(36) = C(2^2^2^3) of size 6+5*2^2^2^3.

a(14) is also the last term that fits in this universe. Subsequent terms can be expressed in terms of function f(n) = 6+5*BB(n): a(15)=f(41) by 1(1(\\2)), a(16)=f(266) by 1(1(1(\1))), a(17)=f(51) by 1(1(\\\2)), a(18)=f^2(266) by 1(\1)1(\1), a(19)=f^2(41) by 1(1(1(\\2))), a(20)=f^4(266) by 1(\\1)1(\1), a(21)=f^5(266) by 1(\\2)1(\1), and a(22)=f^50(266) by 1(1(\1))1(\1).

a(28) >= f^BB(f^3(4))(4) by 1(\1)1(\1)1(\1).

a(29) >= f^{BB(f^{BB(f^4(4))+4}(4))+BB(f^4(4))+5}(4) by 1(\1)(\1 2 1)(\1).

This function is uncomputable even with access to a halting oracle.

We can generalize BB_1 to BB_a for ordinals a by using oracle function BB_{a-1} for successor ordinal a, and oracle function (\n -> BB_{a[n]}(n)) for limit ordinal a, assuming well-defined fundamental sequences up to a. Because of limited oracle inputs, all oracle busy beavers have identical values up to n=11.

Examples

			The only 1-closed term of size 2 is 1 (free variable f), which is in beta/oracle normal form, so a(2)=2.
The smallest example of an oracle reduction occurs in size 8 term 1 (\1). Since \1 has size 4, and BB(4)=4, reduction yields Church numeral C4 = \\2(2(2(2 1))) of maximal size a(8) = 26.
		

Links

• AIT repo on Github, BB1.lhs
• John Tromp, Comment on "How does super BB work?", Googology Reddit, 2025.

Crossrefs

Cf. A333479.