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{\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 $2+k+2+(5\times 2+6)+(5n+6)=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{\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}{lll}blc(Var(n))& =& 1^{n}0\\ blc(Lam(T))& =& 00blc(T)\\ blc(App(T,U))& =& 01blc(T)blc(U)\\ \end{array}$$

For example, the Church numeral 2: $\lambda fx.(f(fx))$ = \\(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). In the last column, JT and BF abbreviate John Tromp and Bertram Felgenhauer.

n	BBλ(n)	Champion	Normal form	Discovered By
21	= 22	$\lambda (\lambda 11)(1(\lambda 2))$	$\lambda (1(\lambda 2))(1(\lambda 2))$	JT & BF
22	= 24	$\lambda (\lambda 111)(11)$	$\lambda (11)(11)(11)$	JT & BF
23	= 26	$\lambda (\lambda 11)(1(\lambda \lambda 2))$	$\lambda (1(\lambda \lambda 2))(1(\lambda \lambda 2))$	JT & BF
24	= 30	$\lambda (\lambda 111)(1(\lambda 1))$	$\lambda (1(\lambda 1))(1(\lambda 1))(1(\lambda 1))$	JT & BF
25	= 42	$\lambda (\lambda 11)(\lambda 1(21))$	$\lambda 1(\lambda 1(21))(1(1(\lambda 1(21))))$	JT & BF
26	= 52	$(\lambda 11)(\lambda \lambda 2(12))$	$\lambda \lambda 2(\lambda \lambda 2(12))(1(2(\lambda \lambda 2(12))))$	JT & BF
27	= 44	$\lambda \lambda (\lambda 11)(\lambda 1(21))$	$\lambda \lambda 1(\lambda 1(21))(1(1(\lambda 1(21))))$	JT & BF
28	= 58	$\lambda (\lambda 11)(\lambda 1(2(\lambda 2))))$	$\lambda 1(\lambda \lambda 1(3(\lambda 2)))(1(\lambda 2(\lambda \lambda 1(4(\lambda 2)))))$	JT & BF
29	= 223	$\lambda (\lambda 11)(\lambda 1(1(21)))$	$\lambda B(B(1B))\text{ where}$ $B=(A(A(1A)))$, $A=(1(\lambda 1(1(21))))$	JT & BF
30	= 160	$(\lambda 111)(\lambda \lambda 2(12))$	$\lambda \lambda 2BA(1(2BA))\text{ where}$ $B=(\lambda \lambda 2A(1(2A)))$, $A=(\lambda \lambda 2(12))$	JT & BF
31	= 267	$(\lambda 11)(\lambda \lambda 2(2(12)))$	$\lambda \lambda 2A(2A(C(2A)))\text{ where}$ $C=(2A(2A(1B(2A))))$, $B=(\lambda 3A(3A(1(3A))))$, $A=(\lambda \lambda 2(2(12)))$	JT & BF
32	= 298	$\lambda (\lambda 11)(\lambda 1(1(2(\lambda 2))))$		JT & BF
33	= 1812	$\lambda (\lambda 11)(\lambda 1(1(1(21))))$	$\lambda C(C(C(1C)))\text{ where}$ $C=(B(B(B(1B)))$, $B=(A(A(A(1A)))$, $A=(1(\lambda 1(1(1(21)))))$	JT & BF
34	$=327686$	$(\lambda 1111)(\lambda \lambda 2(21))$	$C(2^{2^{2^2}})$	JT & BF
35	$=5\cdot 3^{3^3}+6$ $>3.8\times 10^{13}$	$(\lambda 111)(\lambda \lambda 2(2(21)))$	$C(3^{3^3})$	JT & BF
36	$=5\cdot 2^{2^{2^3}}+6$ $>5.7\times 10^{77}$	$(\lambda 11)(\lambda 1(1(\lambda \lambda 2(21))))$	$C(2^{2^{2^3}})$	JT & BF
37	$=2+BB\lambda (35)$	$\lambda (\lambda 111)(\lambda \lambda 2(2(21)))$	$\lambda x.C(3^{3^3})$	mxdys & JT & dyuan & sligocki
38	$\ge 10^{10^4}$	$(\lambda 11111)(\lambda \lambda 2(21))$	$C(2^{2^{2^{2^2}}})$	JT & BF
39	$\ge 10^{10^{12}}$	$(\lambda 1111)(\lambda \lambda 2(2(21)))$	$C(3^{3^{3^3}})$	JT & BF
40	$>10\uparrow \uparrow \uparrow 16$	$(\lambda 111)(\lambda 1(\lambda \lambda 2(21))1)$	$\lambda x.T(k)\text{ where}$ $T(0)=x$, $T(n+1)=T(n)C(2)T(n)$, $k>(2\uparrow \uparrow {)}^{15}33$	mxdys & racheline
41	$\ge 10^{10^{40}}$	$(\lambda 1(\lambda 11)1)(\lambda \lambda 2(2(21)))$	$C(3^{3^{85}})$	mxdys
42	$\ge 2+BB\lambda (40)$	$\lambda (\lambda 111)(\lambda 1(\lambda \lambda 2(21))1)$
43	$>2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow 2\uparrow \uparrow 8$	$(\lambda 11)(\lambda 1(\lambda 1(\lambda \lambda 2(21))2))$	$\lambda x.T(k)\text{ where}$ $T(0)=x$, $T(n+1)=T(n)(\lambda y.yC(2)T(n))$, $k>2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow 2\uparrow \uparrow 8$	mxdys
44	$>10\uparrow \uparrow \uparrow 10\uparrow \uparrow \uparrow 16$	$(\lambda 1111)(\lambda 1(\lambda \lambda 2(21))1)$	$\lambda x.T(k)\text{ where}$ $T(0)=x$, $T(n+1)=T(n)C(2)T(n)$, $k>(2\uparrow \uparrow {)}^{(2\uparrow \uparrow {)}^{15}33-1}33$||
45	$\ge 2+BB\lambda (43)$	$\lambda (\lambda 11)(\lambda 1(\lambda 1(\lambda \lambda 2(21))2))$
46	$\ge 2+BB\lambda (44)$	$\lambda (\lambda 1111)(\lambda 1(\lambda \lambda 2(21))1)$
47
48	$>10\uparrow \uparrow \uparrow \uparrow 4$	$(\lambda 11111)(\lambda 1(\lambda \lambda 2(21))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)$ > Graham's number	$(\lambda 11)(\lambda 1(1(\lambda \lambda 12(\lambda \lambda 2(21)))))$	$C(N)\text{ for }N\approx f_{\omega +1}\left(\frac{2\uparrow \uparrow 6}{2}\right)$	Gustavo Melo
...
61	$>f_{{\omega }^{2\uparrow \uparrow 18-1}}\left(2\right)$	$(\lambda 111)(\lambda 1(1(\lambda \lambda \lambda 132(\lambda \lambda 2(21)))))$	$C(N)\text{ for }N\approx f_{{\omega }^{2\uparrow \uparrow 18-1}}\left(2\right)$	50_ft_lock
...
86	$>f_{{\omega }^{{\omega }^2}}\left(2\right)$	$(\lambda 1(\lambda \lambda \lambda \lambda 1444321)1111)(\lambda \lambda 2(21))$		Patcail
...
90	$>f_{{\zeta }_0}\left(15\right)$	$(\lambda 11(\lambda \lambda \lambda \lambda 1444321)1111)(\lambda \lambda 2(21))$		Patcail
...
94	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}\left(12\right)$ > TREE(G64)	$(\lambda 111(\lambda \lambda \lambda \lambda 1444321)1111)(\lambda \lambda 2(21))$		Patcail
95	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}\left(23\right)$	$(\lambda 11(\lambda \lambda \lambda \lambda 1444321)1111)(\lambda \lambda 2(2(21)))$		Patcail
96	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}\left(f_{{\omega }^{{\omega }^2}}\left(2\right)\right)$	$(\lambda 1(\lambda 1(\lambda \lambda \lambda \lambda 1444321)1111)1)(\lambda \lambda 2(21))$		Patcail
100	$>f_{\psi ({\mathrm{\Omega }}_{\omega })+1}\left(4\right)$	$(\lambda 11(\lambda 1(\lambda \lambda \lambda \lambda 1444321)1111)1)(\lambda \lambda 2(21))$		Patcail
331	lim(BMS)	too large to show		Patcail & JT & 50_ft_lock
1850	> Loader's number	too large to show		JT

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 a church numeral. Allowing arbitrary closed t makes oracle steps more widely applicable while aligning with BBλ's focus on 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	$\lambda 1$	4
5	$\lambda 2$	5
6	$\lambda \lambda 1$	6
7	$\lambda \lambda 2$	7
8	$1(\lambda 1)$	$f(4)=26$
9	$\lambda \lambda 2$	9
10	$1(\lambda \lambda 1)$	$f(6)=36$
11	$1(\lambda \lambda 2)$	$f(7)=41$
12	$1(1(\lambda 1))$	$f^2(4)=266$
13	$1(\lambda \lambda 2)$	$f(9)=51$
14	$1(1(\lambda \lambda 1))$	$f^2(6)=f(36)=25\times 2^{2^{2^3}}+36>2.85\times 10^{78}$
15	$1(1(\lambda \lambda 2))$	$f^2(7)=f(41)\ge 25\times 3^{3^{85}}+36>10^{10^{40}}$
16	$1(1(1(\lambda 1)))$	$f^3(4)=f(266)$
17	$1(1(\lambda \lambda \lambda 2))$	$f^2(9)=f(51)$
18	$1(\lambda 1)1(\lambda 1)$	$f^4(4)$
19	$1(1(1(\lambda \lambda 2)))$	$f^3(7)$
20	$1(\lambda \lambda 1)1(\lambda 1)$	$f^6(4)$
21	$1(\lambda \lambda 2)1(\lambda 1)$	$f^7(4)$
22	$1(1(\lambda 1))1(\lambda 1)$	$f^{52}(4)$
...
28	$1(\lambda 1)1(\lambda 1)1(\lambda 1)$	$\ge 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.

De Bruijn

We can use De Bruijn index instead of binary to evaluate lambda calculus size. To get the size of an expression, convert it into De Bruijn index then count the number of lambdas / backslashes and numbers. By example, (\1 1) (\\2 (1 2)) is size 8 because it has 3 backslashes and 5 numbers.

For n < 7, BBλ_db(n) = n is trivial and can be achieved via picking any size n term already in normal form, like BBλ(m) for m ≤ 20.

BBλ_db(n)	Value	Champion	Discovered By
7	≥ 7	\1 1 1 1 1 1
8	≥ 16	(\1 1) (\\2 (1 2))	Azerty & John Tromp & Bertram Felgenhauer
9	≥ 68	(\1 1) (\\2 (2 (1 2)))	John Tromp & Bertram Felgenhauer
10	$\ge 3\uparrow \uparrow 3+3>7.625\times 10^{12}$	(\1 1 1) (\\2 (2 (2 1)))
11	$\ge 3\uparrow \uparrow 4+3>10^{10^{12}}$	(\1 1 1 1) (\\2 (2 (2 1)))
12	$>10{\uparrow }^{3}16$	(\1 1 1) (\1 (\\2 (2 1)) 1)	mxdys and racheline
13	$>10{\uparrow }^{3}10{\uparrow }^{3}10{\uparrow }^{2}6$	(\1 1) (\1 (\1 (\\2 (2 1)) 2))	mxdys
14	$>10{\uparrow }^{3}10{\uparrow }^{3}10{\uparrow }^{3}16$	(\1 1 1 1 1) (\1 (\\2 (2 1)) 1)
15	$>f_{\omega +1}(2\uparrow \uparrow 6)$	(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))	Gustavo Melo
18	$>f_{{\omega }^{\omega }}(2\uparrow \uparrow 18)$	(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))	50_ft_lock
22	$>f_{{\omega }^{\omega +2}}(2)$	(\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))	Patcail
23	$>f_{{\zeta }_0}(15)$	(\1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))	Patcail
24	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}(12)$	(\1 1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))	Patcail
25	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}(f_{{\omega }^{\omega +2}}(2))$	(\1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))	Patcail
26	$>f_{\psi ({\mathrm{\Omega }}_{\omega }+1)}(4)$	(\1 1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))	Patcail

See Also

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