Busy Beaver for lambda calculus

Busy Beaver for lambda calculus (BBλ) is a variation of the Busy Beaver problem for lambda calculus invented by John Tromp. BBλ(n) = the maximum normal form size of any closed lambda term of size n. Like the traditional Busy Beaver functions, it is uncomputable (and in fact grows faster than any computable function). If you are not familiar with lambda calculus and beta-reduction, it is recommended to start with that article.

Size is measured in bits using Binary Lambda Calculus which is a binary prefix-free encoding for all closed lambda calculus terms.

Analogy to Turing machines

We evaluate terms by applying beta-reductions until they reach a normal form. As an analogy to Turing machines:

• Lambda terms are like TM configurations (tape + state + position).
• Applying beta-reduction to a term is like taking a TM step.
• A term is in normal form if no beta-reductions can be applied. This is like saying the term has halted.
• A term may or may not be reducible to a normal form. If it is, this is like saying the term halts.
• Determining whether a term is reducible to a normal form is an undecidable problem equivalent to the halting problem.

Note: That unlike for Turing machines, evaluating lambda terms is non-deterministic. Specifically, there may be multiple beta-reductions possible in a given term. However, if a term can be reduced to a normal form, that normal form is unique. It is not possible to reduce the original term to any different normal form. A term is strongly normalizing if any choice of beta-reductions will lead to this normal form and weakly normalizing if there exist divergent reduction paths which never reach the normal form.

Proof of Uncomputability

The proof that BBλ(n) is uncomputable is very similar to Radó's original proof that Σ(n) is uncomputable. Proof by contradiction:

Assume BBλ is computable and so there exists a term f which computes it on Church numerals. In other words: for all $n\in \mathbb {N}$: $(f\;C_{n})$ beta reduces to normal form $C_{BB\lambda (n)}$ (where $C_{n}$ denotes the Church numeral n). Denote the binary lambda encoded size of f as k. Consider the term $f\;(C_{2}\;C_{n})$ which has size $5n+k+26$ bits. This term reduces to $C_{BB\lambda (n^{2})}$ which has size $5\cdot BB\lambda (n^{2})+6$ bits. But for sufficiently large n, $n^{2}>5n+k+26$ and so $5\cdot BB\lambda (n^{2})+6>BB\lambda (5n+k+26)$. But this is a contradiction, we've found a $5n+k+26$ bit term which reduces to a normal form larger than $BB\lambda (5n+k+26)$.

Thus BBλ(n) is uncomputable. A variation of this argument shows that BBλ(n) eventually dominates all computable functions.

Binary Lambda Encoding

A lambda term using De Bruijn indexes is defined inductively as:

• Variables: For any $n\in \mathbb {Z} ^{+}$, Var(n) is a term. It represents a variable bound by the lambda expression n above this one (the De Bruijn index). It is typically written simply as n.
• Lambdas: For any term T, Lam(T) is a term. It represents a unary function with function body T. It is typically written $\lambda T$ or \T.
• Applications: For any terms T, U, App(T, U) is a term. It represents applying function T to argument U. It is typically written (T U).

We can think of this as a tree where each variable is a leaf, a lambda is a node with one child and applications are nodes with 2 children. A term is closed if every variable is bound. In other words, for every Var(n) leaf node, there exists n Lam() nodes above it in the tree of the term.

Encoding (blc()) is defined recursively:

$${\begin{array}{l}blc(Var(n))&=&1^{n}0\\blc(Lam(T))&=&00\;blc(T)\\blc(App(T,U))&=&01\;blc(T)\;blc(U)\\\end{array}}$$

For example, the Church numeral 2: $\lambda fx.(f\;(f\;x))$ = \\(2 (2 1)) = Lam(Lam(App(Var(2), App(Var(2), Var(1)))) is encoded as 00 00 01 110 01 110 10 or simply 0000011100111010 (spaces are not part of the encoding, only used for demonstration purposes) and thus has size 16 bits.

Text Encoding conventions

For human readability, a text encoding and set of conventions is used in this article. As described earlier we encode a lambda term as:

• Var(n) -> n
• Lam(T) -> (\T)
• App(T, U) -> (T U)

However, parentheses are also dropped in certain cases by convention:

• The outermost parentheses are dropped: Lam(1) -> \1 and App(1, 2) -> 1 2.
• Parentheses are dropped immediately inside a Lam: Lam(Lam(1)) -> \\1 and Lam(App(1, 1)) -> \1 1.
• Parentheses are dropped in nested Apps using left associativity: App(App(1, 2), 3) -> 1 2 3. (Note: parentheses are still required for App(1, App(2, 3)) -> 1 (2 3)).

This is the convention used in John Tromp's code and so is used here for consistency.

Champions

There are no closed lambda terms of size 0, 1, 2, 3 or 5 and so BBλ(n) is not defined for those values. The smallest closed lambda term is \1 which has size 4.

For the rest of n ≤ 20: BBλ(n) = n is trivial and can be achieved via picking any n bit term already in normal form. For example \\...\1 and \\...\2 with k lambdas has size 2k+2 and 2k+3 respectively (for k ≥ 1 and k ≥ 2 respectively).

n	BBλ(n)	Champion	# Beta reductions	Normal form	Discovered By
21	= 22	\(\1 1) (1 (\2))	1	\(1 (\2)) (1 (\2))	John Tromp & Bertram Felgenhauer
22	= 24	\(\1 1) (1 (\\1))\(\1 1 1) (1 1)	1 1	\(1 (\\1)) (1 (\\1)) \(1 1) (1 1) (1 1)	John Tromp & Bertram Felgenhauer
23	= 26	\(\1 1) (1 (\\2))	1	\(1 (\\2)) (1 (\\2))	John Tromp & Bertram Felgenhauer
24	= 30	\(\1 1 1) (1 (\1))	1	\(1 (\1)) (1 (\1)) (1 (\1))	John Tromp & Bertram Felgenhauer
25	= 42	\(\1 1) (\1 (2 1))	3	\1 (\1 (2 1)) (1 (1 (\1 (2 1))))	John Tromp & Bertram Felgenhauer
26	= 52	(\1 1) (\\2 (1 2))	3	\\2 (\\2 (1 2)) (1 (2 (\\2 (1 2))))	John Tromp & Bertram Felgenhauer
27	= 44	\\(\1 1) (\1 (2 1))	3	\\1 (\1 (2 1)) (1 (1 (\1 (2 1))))	John Tromp & Bertram Felgenhauer
28	= 58	\(\1 1) (\1 (2 (\2))))	3	\1 (\\1 (3 (\2))) (1 (\2 (\\1 (4 (\2)))))	John Tromp & Bertram Felgenhauer
29	= 223	\(\1 1) (\1 (1 (2 1)))	4	\B (B (1 B)) where: B = (A (A (1 A))) A = (1 (\1 (1 (2 1))))	John Tromp & Bertram Felgenhauer
30	= 160	(\1 1 1) (\\2 (1 2)) and (\1 (1 1)) (\\2 (1 2))	7 5	\\2 B A (1 (2 B A)) where: B = (\\2 A (1 (2 A))) A = (\\2 (1 2))	John Tromp & Bertram Felgenhauer
31	= 267	(\1 1) (\\2 (2 (1 2)))	6	\\2 A (2 A (C (2 A))) where: C = (2 A (2 A (1 B (2 A)))) B = (\3 A (3 A (1 (3 A)))) A = (\\2 (2 (1 2)))	John Tromp & Bertram Felgenhauer
32	= 298	\(\1 1) (\1 (1 (2 (\2))))			John Tromp & Bertram Felgenhauer
33	= 1812	\(\1 1) (\1 (1 (1 (2 1))))	5	\C (C (C (1 C))) where: C = (B (B (B (1 B))) B = (A (A (A (1 A))) A = (1 (\1 (1 (1 (2 1)))))	John Tromp & Bertram Felgenhauer
34	$=\ 5\left(2^{2^{2^{2}}}\right)+6=327\,686$	(\1 1 1 1) (\\2 (2 1)) and (\1 (1 1) 1) (\\2 (2 1))		$C(2^{2^{2^{2}}})$	John Tromp & Bertram Felgenhauer
35	$=5\left(3^{3^{3}}\right)+6>3.8\times 10^{13}$	(\1 1 1) (\\2 (2 (2 1)))		$C(3^{3^{3}})$	John Tromp & Bertram Felgenhauer
36	$=5\left(2^{2^{2^{3}}}\right)+6>5.7\times 10^{77}$	(\1 1) (\1 (1 (\\2 (2 1))))		$C(2^{2^{2^{3}}})$	John Tromp & Bertram Felgenhauer
37	$=BB\lambda (35)+2$	\(\1 1 1) (\\2 (2 (2 1)))		$\lambda x.C(3^{3^{3}})$	mxdys, tromp, dyuan, sligocki
38	$\geq 5\left(2^{2^{2^{2^{2}}}}\right)+6>10^{10^{4}}$	(\1 1 1 1 1) (\\2 (2 1)) and (\1 (1 1) 1 1) (\\2 (2 1))		$C(2^{2^{2^{2^{2}}}})$	John Tromp & Bertram Felgenhauer
39	$\geq 5\left(3^{3^{3^{3}}}\right)+6>10^{10^{12}}$	(\1 1 1 1) (\\2 (2 (2 1)))		$C(3^{3^{3^{3}}})$	John Tromp & Bertram Felgenhauer
40	$>(2\uparrow \uparrow )^{15}33>10\uparrow \uparrow \uparrow 16$	(\1 1 1) (\1 (\\2 (2 1)) 1)		$\lambda x.T(k)$ where $T(0)=x,\;T(n+1)=T(n)\;C(2)\;T(n)$ and $k>(2\uparrow \uparrow )^{15}33$	mxdys and racheline
41	$\geq 5\left(3^{3^{85}}\right)+6>10^{10^{40}}$	(\1 (\1 1) 1) (\\2 (2 (2 1)))		$C(3^{3^{85}})$	mxdys
42	$\geq BB\lambda (40)+2$	\(\1 1 1) (\1 (\\2 (2 1)) 1)
43	$>2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow 2\uparrow \uparrow 8$	(\1 1) (\1 (\1 (\\2 (2 1)) 2))		$\lambda x.T(k)$ where $T(0)=x,\;T(n+1)=T(n)\;(\lambda y.y\;C(2)\;T(n))$ and $k>2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow 2\uparrow \uparrow 8$	mxdys
44	$>10\uparrow \uparrow \uparrow 10\uparrow \uparrow \uparrow 16$	(\1 1 1 1) (\1 (\\2 (2 1)) 1)		$\lambda x.T(k)$ where $T(0)=x,\;T(n+1)=T(n)\;C(2)\;T(n)$ and $k>(2\uparrow \uparrow )^{(2\uparrow \uparrow )^{15}33-1}33$
45	$\geq BB\lambda (43)+2$	\(\1 1) (\1 (\1 (\\2 (2 1)) 2))
46	$\geq BB\lambda (44)+2$	\(\1 1 1 1) (\1 (\\2 (2 1)) 1)
47
48	$>10\uparrow \uparrow \uparrow 10\uparrow \uparrow \uparrow 10\uparrow \uparrow \uparrow 16$	(\1 1 1 1 1) (\1 (\\2 (2 1)) 1)		$\lambda x.T(k)$ where $T(0)=x,\;T(n+1)=T(n)\;C(2)\;T(n)$ and $k>(2\uparrow \uparrow )^{(2\uparrow \uparrow )^{(2\uparrow \uparrow )^{15}33-1}33-1}33$
49	$>f_{\omega +1}\left({\frac {2\uparrow \uparrow 6}{2}}\right)>{\text{Graham's number}}$	(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))		$C(N){\text{ for }}N\approx f_{\omega +1}\left({\frac {2\uparrow \uparrow 6}{2}}\right)$	Gustavo Melo
...
1850	> Loader's number	too large to show			John Tromp

Where $C(n)$ represents the Church numeral n ($\lambda fx.f^{n}(x)$) written as \\2 (2 ... (2 1)...) with n 2s in this text representation.

Oracle Busy Beaver

While BBλ grows uncomputably fast, one can define functions that grow much faster.

Let's define a higher order busy beaver function BBλ₁ by providing oracle access to BBλ.

This is done by enriching the set of terms and possible reduction steps considered in the BB definition.

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

Note that this is almost identical to the oracle steps in Barendregt and Klop's "Applications of infinitary lambda calculus", except that they require t itself to be church numeral s, while we prefer to make oracle steps as widely applicable as possible, while the domain of BBλ already consists of term sizes.

Now let BBλ₁ be 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. This appears as sequence A385712 in the OEIS.

The following table shows values of BBλ₁ up to 22 plus a lower bound for 28, with larger values expressed in terms of function $f(n)=6+5\times BB\lambda (n)$:

n	champion	BBλ1
1		0
2	1	1
3		0
4	\1	4
5	\2	5
6	\\1	6
7	\\2	7
8	1 (\1)	$f(4)=26$
9	\\2	9
10	1 (\\1)	$f(6)=36$
11	1 (\\2)	$f(7)=41$
12	1 (1 (\1))	$f^{2}(4)=266$
13	1 (\\2)	$f(9)=51$
14	1 (1 (\\1))	$f^{2}(6)=f(36)=25\times 2^{2^{2^{3}}}+36>2.85\times 10^{78}$
15	1 (1 (\\2))	$f^{2}(7)=f(41)\geq 25\times 3^{3^{85}}+36>10^{10^{40}}$
16	1 (1 (1 (\1)))	$f^{3}(4)=f(266)$
17	1 (1 (\\\2))	$f^{2}(9)=f(51)$
18	1 (\1) 1 (\1)	$f^{4}(4)$
19	1 (1 (1 (\\2)))	$f^{3}(7)$
20	1 (\\1) 1 (\1)	$f^{6}(4)$
21	1 (\\2) 1 (\1)	$f^{7}(4)$
22	1 (1 (\1)) 1 (\1)	$f^{52}(4)$
...
28	1 (\1) 1 (\1) 1 (\1)	$\geq f^{BB\lambda (f^{3}(4))}(4)$

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

See Also

• https://oeis.org/A333479
• The largest number representable in 64 bits. 24 Nov 2023. John Tromp.
• Binary Lambda Calculus. John Tromp.
• https://github.com/tromp/AIT/tree/master/BB