John Tromp - cp's OEIS frontend

A385712 Busy Beaver BBlambda_1 for lambda calculus with a BB (A333479) oracle: 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.

0, 2, 0, 4, 5, 6, 7, 26, 9, 36, 41, 266, 51, 2894802230932904885589274625217197696331749616641014100986439600197828240998436

Offset: 1

John Tromp, Jul 07 2025

nonn

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).
The jump at a(14) is due to lambda term 1(1(\\1)). Subterm (1(\\1)) is an application of free variable f to a closed term of size 6 and thus oracle reduces to Church numeral BB(6) = C6. Next, (1 C6) is an application of free variable f to a closed term of size 36 and thus oracle reduces to Church numeral BB(36) = C(2^2^2^3) of size 6+5*2^2^2^3.
a(14) is also the last term that fits in this universe. Subsequent terms can be expressed in terms of function f(n) = 6+5*BB(n): a(15)=f(41) by 1(1(\\2)), a(16)=f(266) by 1(1(1(\1))), a(17)=f(51) by 1(1(\\\2)), a(18)=f^2(266) by 1(\1)1(\1), a(19)=f^2(41) by 1(1(1(\\2))), a(20)=f^4(266) by 1(\\1)1(\1), a(21)=f^5(266) by 1(\\2)1(\1), and a(22)=f^50(266) by 1(1(\1))1(\1).
a(28) >= f^BB(f^3(4))(4) by 1(\1)1(\1)1(\1).
a(29) >= f^{BB(f^{BB(f^4(4))+4}(4))+BB(f^4(4))+5}(4) by 1(\1)(\1 2 1)(\1).
This function is uncomputable even with access to a halting oracle.
We can generalize BB_1 to BB_a for ordinals a by using oracle function BB_{a-1} for successor ordinal a, and oracle function (\n -> BB_{a[n]}(n)) for limit ordinal a, assuming well-defined fundamental sequences up to a. Because of limited oracle inputs, all oracle busy beavers have identical values up to n=11.

			The only 1-closed term of size 2 is 1 (free variable f), which is in beta/oracle normal form, so a(2)=2.
The smallest example of an oracle reduction occurs in size 8 term 1 (\1). Since \1 has size 4, and BB(4)=4, reduction yields Church numeral C4 = \\2(2(2(2 1))) of maximal size a(8) = 26.

AIT repo on Github, BB1.lhs
John Tromp, Comment on "How does super BB work?", Googology Reddit, 2025.

Cf. A333479.

A368006 Rayo's function: smallest natural number larger than any number uniquely defined by an n-symbol formula in First Order Set Theory.

Original entry on oeis.org

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 2

Offset: 0

John Tromp, Dec 07 2023

The alphabet consists of the 7 symbols ∈, =, (, ), ~, ∧, ∃, plus infinitely many variables x_i, for i >= 0, each considered one symbol.
"x_i∈x_j" and "x_i=x_j" are atomic formulas.
If θ is a formula, then "(~θ)" is a formula (the negation of θ).
If θ and ξ are formulas, then "(θ∧ξ)" is a formula (the conjunction of θ and ξ).
If θ is a formula, then "∃x_i(θ)" is a formula (existential quantification).
A formula having x_0 as its only free variable defines a number m if it has a satisfying assignment, and all such assignments assign m to x_0.
Mexican philosophy professor Agustín Rayo defined a nondecreasing version of this function in a "big number duel" at MIT on 26 January 2007.
Its value at n=10^100 is known as Rayo's number.
This is a set theoretic analog of the busy beaver function, which it easily outgrows.

			a(30)=2, since the 30 symbol formula "(∃x_1(x_1∈x_0)∧(¬∃x_1(∃x_2((x_2∈x_1∧x_1∈x_0)))))" uniquely defines the number 1, while smaller formulae can only define the number 0, the smallest being the 10 symbol "(¬∃x_1(x_1∈x_0))".

Googology Fandom, Low-level Rayo bounds
Googology Fandom, Proof that Rayo(n) is 1 for n between 10 to 19
Wikipedia, Rayo's Number

Cf. A028444.

A367433 Number of successive Patcail predecessors of n-th binary tree.

Original entry on oeis.org

0, 1, 2, 5, 3, 6, 4

Offset: 0

John Tromp, Nov 18 2023

nonn

A binary tree is either 0 or a pair [s,t] of binary trees. Binary trees are counted by Catalan numbers A000108 and ordered by their binary code as given by A014486. Subtrees s and t correspond to A072771 and A072772.
Patcail defined the predecessor of [0,t] as t, and of [s,t], where s has predecessor s', as the result of replacing with [s',t] each occurrence of t within [s',t].
a(7), corresponding to [[0,[0,0]],0], is too large to show, exceeding an exponential tower of 2^63 2's. a(8), corresponding to [[[0,0],0],0], is much larger still, starting to approach Graham's Number. The next 3 terms are modest again, at a(9)=4, a(10)=7, a(11)=5.
The (A014138 indexed) subsequence for left skewed binary trees 0, [0,0], [[0,0],0], [[[0,0],0],0] ... forms an extremely fast growing sequence, at Buchholz's Ordinal in the Fast Growing Hierarchy.
Initial predecessors of these left skewed trees have sizes a(n) satisfying
a(n+1) = (a(n)+1)*(a(n)+3), which is A056207 counting the number of binary trees of height <= n.

			a(3)=5, since the 3rd binary tree is [[0,0],0] and its 5 successive Patcail predecessors are [[0,0],[0,0]], [0,[0,[0,0]]], [0,[0,0]], [0,0], and 0:
Index   n         3              6              4          2      1   0
A014486(n)       12             50             42         10      2   0
A063171(n)     1100         110010         101010       1010     10   0
Tree       [[0,0],0]  [[0,0],[0,0]]  [0,[0,[0,0]]]  [0,[0,0]]  [0,0]  0
A367433(n)        5              4              3          2      1   0

Code Golf, Patcail's winning answer to Code Golf challenge "Golf a number bigger than TREE(3)".

Cf. A000108, A014486, A014138, A056207.

data T = N | C T T deriving (Eq,Show)
a014486 = [0..] >>= at where
  at 0 = [N]
  at n = [C s t | (ns,s) <- to$n-1, t <- at$n-1-ns]
  to n = (0,N):[(1+ns+nt,C s t)|n>0,(ns,s)<-to$n-1,(nt,t)<-to$n-1-ns]
predT (C N t) = t
predT (C s t) = go u where
  u = [predT s) t
  go v = if v==t then u else case v of
    N     -> N
    C s t -> [go s) (go t)
a367433 = map nPred a014486 where
  nPred N = 0
  nPred t = 1 + nPred (predT t)

A361211 Busy Beaver for the Binary Lambda Calculus (BLC) language BBλ2: the maximum output size of self-delimiting BLC programs of size n, or 0 if no program of size n exists.

Original entry on oeis.org

0, 0, 0, 0, 0, 4, 0, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 24, 26, 30, 42, 52, 44, 64, 223, 160

Offset: 1

John Tromp, Apr 09 2023

Self-delimiting BLC programs are inputs p to the BLC universal machine U (defined in first link) that make U read all bits of p and none beyond. Formally, the only prefix p' of p for which U(p':Omega) has a normal form is p itself. The output of p is that normal form.
This Busy Beaver is directly related to Kolmogorov Complexity: a(n) = max {size(x)| KP(x) = n }, where KP is the prefix Kolmogorov complexity (defined in first link).
Because programs for U are at most a constant number of bits longer than programs for any prefix-free programming language, this busy beaver is optimal: for any other busy beaver BB based on self-delimiting programs, there is a constant c such that a(c+n) >= BB(n).
In particular, a(2+n) >= A333479(n), since for every closed term T, U(00 code(T) : Omega) = (lambda _. T) Omega = T. All entries above except for n=30 are of this form.
We can show that for some k, a(ceiling((113/114)*n) + k) > A333479(n), i.e., universality eventually pays off for BLC. See program link for the supporting computation. - Bertram Felgenhauer, Apr 10 2023

			The smallest closed lambda term is lambda x.x but its application to the unsolvable Omega lacks a normal form. The next smallest is lambda x.lambda y.y with encoding 000010 of size 6, which applied to Omega yields the normal form lambda x.x, giving a(6)=4.
a(30) = 64 because, with T=lambda x.lambda y.lambda z.x(z x), (lambda x.x x) T applied to Omega yields maximum size normal form lambda x.lambda y.lambda z.x T(z (x T)).

John Tromp, Binary Lambda Calculus
John Tromp, Haskell program to compute initial terms
John Tromp, program demonstrating BLC compressibility

Cf. A333479.

A333958 The number of closed lambda calculus terms of size n that have a normal form, where size(lambda M)=2+size(M), size(M N)=2+size(M)+size(N), and size(V)=1+i for a variable V bound by the i-th enclosing lambda.

Original entry on oeis.org

0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, 44, 101, 134, 297, 431, 882, 1361, 2729, 4405, 8549, 14311, 27400, 47101, 89022, 156080, 293014, 521730

Offset: 1

John Tromp, Apr 22 2020

This sequence is uncomputable, like the corresponding Busy Beaver sequence A333479, which takes the maximum normal form size of the a(n) terms that have one.

			This sequence first differs from A114852 at n=18 where it excludes the shortest term without a normal form (lambda x. x x)(lambda x. x x), hence a(18) = 298-1 = 297.

Computed by changing "maximum $ (n,0,P Bot) :" in the main function of this Haskell program for analyzing Busy Beaver numbers to "length".

Cf. A114852, A195691, A333479, A004147.

Terms > 2729 corrected by John Tromp, Mar 29 2025

A333479 Busy Beaver for lambda calculus BBλ: the maximum beta normal form size of any closed lambda term of size n, or 0 if no closed term of size n exists.

Original entry on oeis.org

0, 0, 0, 4, 0, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 24, 26, 30, 42, 52, 44, 58, 223, 160, 267, 298, 1812, 327686, 38127987424941, 578960446186580977117854925043439539266349923328202820197287920039565648199686

Offset: 1

John Tromp, Mar 23 2020

nonn

Sizes of terms are defined as in Binary Lambda Calculus (see Lambda encoding link) by size(lambda M)=2+size(M), size(M N)=2+size(M)+size(N), and size(V)=1+i for a variable V bound by the i-th enclosing lambda.
a(34), a(35) and a(36) correspond to Church numerals 2^2^2^2, 3^3^3, and 2^2^2^3, where numeral n has size 5*n+6.
a(38) > 10^19729, corresponding to Church numeral 2^2^2^2^2.
Only a finite number of entries can be known, as the function is uncomputable.
Quoting from Chaitin's paper below: "to information theorists it is clear that the correct measure is bits, not states [...] to deal with Sigma(number of bits) one would need a model of a binary computer as simple and compelling as the Turing machine model, and no obvious natural choice is at hand."
a(49) > Graham's number, as shown in program melo.lam in the links. - John Tromp, Dec 04 2023
a(111) > f_{ε_0+1}(4), as shown in program E00.lam in the links. - John Tromp, Aug 24 2024
a(404) > f_{PTO(Z_2)+1}(4), as shown in 1st Stackexchange link. - John Tromp, Dec 17 2024
a(1850) > Loader's number, as shown in 2nd Stackexchange link. - John Tromp, Dec 17 2024
A universal form of this Busy Beaver, using the binary input feature of Binary Lambda Calculus, is given in sequence A361211. - John Tromp, May 24 2023
An oracle form of this Busy Beaver is given in sequence A385712. - John Tromp, Jul 23 2025

			The smallest closed lambda term is lambda x.x with encoding 0010 of size 4, giving a(4)=4, as it is in normal form. There is no closed term of size 5, so a(5)=0. a(21)=22 because of term lambda x. (lambda y. y y) (x (lambda y. x)).

Gregory Chaitin, Computing the Busy Beaver Function, in T. M. Cover and B. Gopinath, Open Problems in Communication and Computation, Springer, 1987, pages 108-112.
John Tromp, Binary Lambda Calculus and Combinatory Logic, in Randomness And Complexity, from Leibniz To Chaitin, ed. Cristian S. Calude, World Scientific Publishing Company, October 2008, pages 237-260.

bbchallenge wiki, Busy Beaver for lambda calculus
AIT repo on Github, melo.lam.
Code Golf Stack Exchange, Comment on BMS[26] entry
Code Golf Stack Exchange, 1850 bit lambda term exceeding Loader's number
MathOverflow, What's the smallest lambda-calculus term not known to have a normal form?, 2020.
John Tromp, The largest number representable in 64 bits, John's Blog.
John Tromp, Lambda encoding
John Tromp, Haskell program for analyzing Busy Beaver numbers
John Tromp, program output analysis
John Tromp, Lambda term for 111 bit blc program computing 4 iterations of ε0 level growth
Index entries for sequences related to Busy Beaver problem

Cf. A028444, A114852, A195691, A333958, A361211, A385712.

a(33)-a(34) from John Tromp, Apr 10 2020
a(35) from John Tromp, Apr 18 2020
a(36) from John Tromp, Apr 19 2020

A269417 Number of Go games on n X n board with no repeating position and suicide allowed.

Original entry on oeis.org

1, 1, 386356909593

Offset: 0

John Tromp, Feb 25 2016

I only chose starting offset 0 because the number of 3 X 3 games is unknown (and over a thousand digits).
a(n) is also the number of simple paths in the Go game graph starting at the empty position.
a(n) is upper bounded by n^{2*3^{n^2}}, as shown in Theorem 7 from the linked paper.

			a(1) = 1 since the only legal Go game on a 1 X 1 board is Black pass, White pass.

J. Tromp and G. Farnebäck, Combinatorics of Go, Lecture Notes in Computer Science, 4630, 84-99, 2007.

Cf. A094777.

A268113 Number of legal positions in Go played on an n X n+1 grid (each group must have at least one liberty).

Original entry on oeis.org

5, 489, 321689, 1840058693, 93332304864173, 41945191530093646965, 166931297609667912727898521, 5882748866432370655674372752123193, 1835738613899845421140262364853644706891109, 5072588588647327658457862518216696854885169490987149

Offset: 1

John Tromp, Jan 26 2016

Upper bounded by 3^{n*(n+1)}.

			For n=1 the 5 legal 1x2 boards are .. X. O. .X .O

John Tromp, Table of n, a(n) for n = 1..19
John Tromp, Number of legal Go positions
J. Tromp and G. Farnebäck, Combinatorics of Go, Lecture Notes in Computer Science, 4630, 84-99, 2007.

Almost-square version of A094777.

A268125 Minimal order of recurrence for number of legal n X m Go positions, for fixed n.

Original entry on oeis.org

3, 7, 19, 57, 217, 791, 3107, 12110, 49361

Offset: 1

John Tromp, Jan 26 2016

			For n=1 the minimal recurrence is L(1,m) = 3*L(1,m-1)-L(1,m-2)+L(1,m-3).

J. Tromp and G. Farnebäck, Combinatorics of Go, Lecture Notes in Computer Science, 4630, 84-99, 2007.

Cf. A094777, A102620, A266278.

A256001 Minimum sum of a nonnegative integer triple that takes n moves to reach a 0 component, where a move picks two components, subtracts the smaller from the larger, and doubles the smaller.

Original entry on oeis.org

0, 3, 6, 11, 15, 23, 27, 45, 81, 105, 195, 329, 597, 885, 1425, 2793, 4725, 8025, 14265, 23205, 41685

Offset: 0

John Tromp, May 06 2015

a(21) > 65532. - Karl Desfontaines, Mar 02 2022

			The triple (1,2,3) is the triple with minimum sum that has no 0's or equal members and reaches a 0 after the 2 moves (1,2,3) -> (2,2,2) -> (4,0,2). Since the sum of this triple is 6, a(2) = 6.

IBM's Ponder This, 3 people betting game, May 2015, challenge essentially asks for (a witness for) a(12).
Fabian Frei, Peter Rossmanith, and David Wehner, An Open Pouring Problem, 10th International Conference on Fun with Algorithms (FUN 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 14:1-9.
John Tromp, C program computing diameter and witness for each sum.

Cf. A383586 (for 4-tuples), A383587 (for 5-tuples), A383588 (for 6-tuples).

// See link above for a C program from whose output the terms above were derived.

a(19)-a(20) from Karl Desfontaines, Mar 02 2022

cp's OEIS Frontend

User: John Tromp

A385712 Busy Beaver BBlambda_1 for lambda calculus with a BB (A333479) oracle: 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.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

A368006 Rayo's function: smallest natural number larger than any number uniquely defined by an n-symbol formula in First Order Set Theory.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

A367433 Number of successive Patcail predecessors of n-th binary tree.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

Programs

Haskell

A361211 Busy Beaver for the Binary Lambda Calculus (BLC) language BBλ2: the maximum output size of self-delimiting BLC programs of size n, or 0 if no program of size n exists.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

A333958 The number of closed lambda calculus terms of size n that have a normal form, where size(lambda M)=2+size(M), size(M N)=2+size(M)+size(N), and size(V)=1+i for a variable V bound by the i-th enclosing lambda.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

Extensions

A333479 Busy Beaver for lambda calculus BBλ: the maximum beta normal form size of any closed lambda term of size n, or 0 if no closed term of size n exists.

Views

Author

Keywords

Comments

Examples

References

Links

Crossrefs

Extensions

A269417 Number of Go games on n X n board with no repeating position and suicide allowed.

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

A268113 Number of legal positions in Go played on an n X n+1 grid (each group must have at least one liberty).

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

A268125 Minimal order of recurrence for number of legal n X m Go positions, for fixed n.

Views

Author

Keywords

Examples

Links

Crossrefs

A256001 Minimum sum of a nonnegative integer triple that takes n moves to reach a 0 component, where a move picks two components, subtracts the smaller from the larger, and doubles the smaller.

Views