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. If you are not familiar with lambda calculus and beta-reduction, I recommend starting 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.

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	Normal form	Discovered By
21	= 22	`(\1 1) (1 (\2))`	`(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)`	John Tromp & Bertram Felgenhauer
23	= 26	`(\1 1) (1 (\\2))`	`(1 (\\2)) (1 (\\2))`	John Tromp & Bertram Felgenhauer
24	= 30	`(\1 1 1) (1 (\1))`	`(1 (\1)) (1 (\1)) (1 (\1))`	John Tromp & Bertram Felgenhauer
25	= 42	`\(\1 1) (\1 (2 1))`	`\1 (\1 (2 1)) (1 (1 (\1 (2 1))))`	John Tromp & Bertram Felgenhauer
26	= 52	`(\1 1) (\\2 (1 2))`	`\\2 (\\2 (1 2)) (1 (2 (\\2 (1 2))))`	John Tromp & Bertram Felgenhauer
27	= 44	`\\(\1 1) (\1 (2 1))`	`\\1 (\1 (2 1)) (1 (1 (\1 (2 1))))`	John Tromp & Bertram Felgenhauer
28	= 58	`\(\1 1) (\1 (2 (\2))))`		John Tromp & Bertram Felgenhauer
29	= 223	`\(\1 1) (\1 (1 (2 1)))`		John Tromp & Bertram Felgenhauer
30	= 160	`(\1 1 1) (\\2 (1 2))`		John Tromp & Bertram Felgenhauer
31	≥ 267	`(\1 1) (\\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))))`		John Tromp & Bertram Felgenhauer
34	$\geq 5\left(2^{2^{2^{2}}}\right)+6=327\,686$	`(\1 1 1 1) (\\2 (2 1))`	$C(2^{2^{2^{2}}})$	John Tromp & Bertram Felgenhauer
35	$\geq 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	$\geq 5\left(2^{2^{2^{3}}}\right)+6>5.7\times 10^{77}$	`(\1 1 1 1) (\\2 (2 1))`	$C(2^{2^{2^{2}}})$	John Tromp & Bertram Felgenhauer
37
38	$\geq 5\left(2^{2^{2^{2^{2}}}}\right)+6>10^{10^{4}}$	`(\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	$>5\left(2^{2^{2059}}\right)+6>10^{10^{619}}$	`(\1 1 (\1 1) 1) (\\2 (2 1))`	$C(2^{2^{2059}})$
41
42	$\geq 5\left(2\uparrow \uparrow 6\right)+6>10^{10^{10^{4}}}$	`(\1 1 1 1 1 1) (\\2 (2 1))`	$C(2\uparrow \uparrow 6)$
43	$\geq 5\left(3\uparrow \uparrow 5\right)+6>10^{10^{10^{12}}}$	`(\1 1 1 1 1) (\\2 (2 (2 1)))`	$C(3\uparrow \uparrow 5)$
44	$>(2\uparrow )^{14}2059>10\uparrow \uparrow 15$	`(\1 1 1 (\1 1) 1) (\\2 (2 1))`	$C((\lambda x.x^{x})^{16}(2))$
45	$>3\uparrow \uparrow 28>10\uparrow \uparrow 27$	`(\1 1 (\1 1) 1) (\\2 (2 (2 1)))`	$C((\lambda x.x^{x})^{27}(3))$
46	$>256\uparrow \uparrow 257>10\uparrow \uparrow 257$	`(\1 (\1 (\1 1) 1) 1) (\\2 (2 1))`	$C((\lambda x.x^{x})^{256}(256))$
47
48	$>(2\uparrow )^{65534}2059>10\uparrow \uparrow 65535$	`(\1 1 1 1 (\1 1) 1) (\\2 (2 1))`	$C((\lambda x.x^{x})^{65536}(2))$
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)))))`		Gustavo Melo
...
1850	> Loader's number	`too large to show`		John Tromp