Azerty: Created page with "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. {| class="wikitable" !BBλ_db(n)..."

2026-02-07T17:34:48Z

Created page with "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, <code>(\1 1) (\\2 (1 2))</code> 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. {| class="wikitable" !BBλ_db(n)..."

New page

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, <code>(\1 1) (\\2 (1 2))</code> 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.
{| class="wikitable"
!BBλ_db(n)
!Value
!Champion
!Discovered By
|-
|7
|7
|<code>\1 1 1 1 1 1</code>
|
|-
|8
|≥ 16
|<code>(\1 1) (\\2 (1 2))</code>
|[[User:Azerty|Azerty]] & John Tromp & Bertram Felgenhauer
|-
|9
|≥ 68
|<code>(\1 1) (\\2 (2 (1 2)))</code>
|John Tromp & Bertram Felgenhauer
|-
|10
|<math>\ge 3 \uparrow\uparrow 3 + 3 > 7.625 \times 10^{12}</math>
|<code>(\1 1 1) (\\2 (2 (2 1)))</code>
|
|-
|11
|<math>\ge 3 \uparrow\uparrow 4 + 3 > 10^{10^{12}}</math>
|<code>(\1 1 1 1) (\\2 (2 (2 1)))</code>
|
|-
|12
|<math>> 10 {\uparrow}^{3} 16</math>
|<code>(\1 1 1) (\1 (\\2 (2 1)) 1)</code>
|mxdys and racheline
|-
|13
|<math>> 10 {\uparrow}^{3} 10 {\uparrow}^{3} 10 {\uparrow}^{2} 6</math>
|<code>(\1 1) (\1 (\1 (\\2 (2 1)) 2))</code>
|mxdys
|-
|14
|<math>> 10 {\uparrow}^{3} 10 {\uparrow}^{3} 10 {\uparrow}^{3} 16</math>
|<code>(\1 1 1 1 1) (\1 (\\2 (2 1)) 1)</code>
|
|-
|15
|<math>> f_{\omega+1}(2 \uparrow\uparrow 6)</math>
|<code>(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))</code>
|[https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam Gustavo Melo]
|-
|18
|<math>> f_{\omega^\omega}(2 \uparrow\uparrow 18)</math>
|<code>(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))</code>
|[https://tromp.github.io/blog/2026/01/28/largest-number-revised 50_ft_lock]
|-
|22
|<math>> f_{\omega^{\omega+2}}(2)</math>
|<code>(\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|23
|<math>> f_{\zeta_0}(15)</math>
|<code>(\1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|24
|<math>> f_{\psi(\Omega_\omega)}(12)</math>
|<code>(\1 1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|25
|<math>> f_{\psi(\Omega_\omega)}(f_{\omega^{\omega+2}}(2))</math>
|<code>(\1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
|Patcail
|-
|26
|<math>> f_{\psi(\Omega_\omega+1)}(4)</math>
|<code>(\1 1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
|Patcail
|}
Most champions are currently taken from binary BBλ.

User:Azerty/Lambda Calculus Busy Beaver - Revision history