Lambda Calculus

Lambda calculus is a model of computation developed by Alonzo Church (of Church-Turing thesis fame) in 1932. If you are not familiar with lambda calculus and beta-reduction, it is recommended to start with this article.

BBλ is the Busy Beaver function for lambda calculus, where BBλ(n) is the maximum normal form size of any closed lambda term of size n (or 0 if no closed term of size n exists). Size is measured in bits using Binary Lambda Calculus, a binary prefix-free encoding for all closed lambda calculus terms. Pioneered by John Tromp, BBλ is uncomputable, and therefore grows faster than any computable function.

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 every beta-reduction sequence leads to this normal form and weakly normalizing if some sequence does (while others may diverge).

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) = 0 for those values.

$C(n)$ denotes Church numeral n = $\lambda f\lambda x.f^n(x)$.

In the last column, JT and BF abbreviate John Tromp and Bertram Felgenhauer.

We use the ordinal collapsing functions defined by Buchholz (1986). It is suspected (though not yet confirmed) that we used the fundamental sequences described by Maksudov (2017), or, in the case of lim(BMS), the sequence lim(BMS)[n] = BMS((0)(1,1,...,1)) w/n 1s.

The smallest Cryptid known currently is in 74 bits.

Small Champions

n	BBλ(n)	Champion	Normal form	Discovered By
4	= 4	$\lambda 1$		JT & BF
6	= 6	$\lambda \lambda 1$		JT & BF
7	= 7	$\lambda \lambda 2$		JT & BF
8	= 8	$\lambda \lambda \lambda 1$		JT & BF
9	= 9	$\lambda \lambda \lambda 2$		JT & BF
10	= 10	$\lambda \lambda \lambda \lambda 1$		JT & BF
11	= 11	$\lambda \lambda \lambda \lambda 2$		JT & BF
12	= 12	$\lambda \lambda \lambda \lambda \lambda 1$		JT & BF
13	= 13	$\lambda \lambda \lambda \lambda \lambda 2$		JT & BF
14	= 14	$\lambda \lambda \lambda \lambda \lambda \lambda 1$		JT & BF
15	= 15	$\lambda \lambda \lambda \lambda \lambda \lambda 2$		JT & BF
16	= 16	$\lambda \lambda \lambda \lambda \lambda \lambda \lambda 1$		JT & BF
17	= 17	$\lambda \lambda \lambda \lambda \lambda \lambda \lambda 2$		JT & BF
18	= 18	$\lambda \lambda \lambda \lambda \lambda \lambda \lambda \lambda 1$		JT & BF
19	= 19	$\lambda \lambda \lambda \lambda \lambda \lambda \lambda \lambda 2$		JT & BF
20	= 20	$\lambda \lambda \lambda \lambda \lambda \lambda \lambda \lambda \lambda 1$		JT & BF

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	$=5\cdot 2^{2^{2^{2^2}}}+6>10^{19,729}$	$(\lambda 11111)(\lambda \lambda 2(21))$	$C(2^{2^{2^{2^2}}})$	JT & BF & CppDS & mxdys & sligocki & dyuan & charles
39	$=5\cdot 3^{3^{3^3}}+6>10^{10^{12}}$	$(\lambda 1111)(\lambda \lambda 2(2(21)))$	$C(3^{3^{3^3}})$	JT & BF & CppDS & mxdys & sligocki & dyuan & charles & 2014MELO & mammilaria
40	$\approx 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	$=5\times 3^{3^{85}}+6>10^{1.7\times 10^{40}}\approx 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	$>f_{\omega }\left(f_5\left(2\right)\right)$	$(\lambda 111)(\lambda \lambda 1(12)(\lambda \lambda 2(21)))$		50_ft_lock
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(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(f_{{\omega }^{2\uparrow \uparrow 18-1}}\left(2\right))$	50_ft_lock
...
86	$>f_{{\omega }^{\omega 65536}}\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
201	> q(5)	too large to show	q is only proven to exceed all functions provably recursive in PA; the true value is likely much larger based on informal analysis	JT & BF & 50_ft_lock
331	> f3lim(BMS)(5)	too large to show		Patcail & JT & 50_ft_lock
1797	> D⁵(99) = Loader's number	too large to show		JT & BF & DropperAUGL

Optimal Busy Beaver

A closely related BBλ2 function, defined as OEIS sequence (A361211)[1], allows the lambda term access to (undelimited) raw binary data, which suffices to make it an optimal busy beaver function amongst all binary self-delimiting ones.

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	λ λ λ 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)=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^{26}(4)$
...
28	$1(\lambda 1)1(\lambda 1)1(\lambda 1)$	$\ge f^{BB\lambda (f^3(4))}(4)$
29	$1(\lambda 1)(\lambda 121)(\lambda 1)$	$\ge f^{BB\lambda (f^{BB\lambda (f^4(4))+4}(4))+BB\lambda (f^4(4))+5}(4)$

We can generalize BBλ₁ to BBλ_α for ordinals α by using oracle function BBλ_α-1 for successor ordinal α, 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

• SKI calculus
• De Bruijn index
• https://oeis.org/A333479
• The Largest Number Representable in 64 Bits. 26 Apr 2026. John Tromp.
• Binary Lambda Calculus. John Tromp.
• https://github.com/tromp/AIT/tree/master/BB
• https://github.com/ccz181078/BLC.git
• https://docs.google.com/spreadsheets/d/1jZ6TK9m3xmXUlC69727T-8WwvhALcsp8FrK6DzgThtw
• Buchholz, W. (1986). A new system of proof-theoretic ordinal functions. Annals of Pure and Applied Logic, 32, 195-207. https://doi.org/10.1016/0168-0072(86)90052-7
• Maksudov, D. (2017, April). Travelling To The Infinity - The extended Wilfried Buchholz's functions. Travelling To The Infinity. https://sites.google.com/site/travelingtotheinfinity/the-extension-of-buchholz-s-function