A195691 -id:A195691 - cp's OEIS frontend

A114852 The number of closed lambda calculus terms of size n, where size(lambda x.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 (corresponding to a binary encoding).

0, 0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, 44, 101, 134, 298, 431, 883, 1361, 2736, 4405, 8574, 14334, 27465, 47146, 89270, 156360, 293840, 522913, 978447, 1761907, 3288605, 5977863, 11148652, 20414058, 38071898, 70125402, 130880047

Offset: 0

John Tromp, Feb 20 2006

nonn

			a(8) = 2 because lambda x.lambda y.lambda z.z and lambda x.(x x) are the only two closed lambda terms of size 8.

K. Grygiel and P. Lescanne, Counting terms in the binary lambda calculus, arXiv preprint arXiv:1401.0379 [cs.LO], 2014.
Katarzyna Grygiel and Pierre Lescanne, Counting and Generating Terms in the Binary Lambda Calculus (Extended version), HAL Id: ensl-01229794, 2015.
John Tromp, John's Lambda Calculus and Combinatory Logic Playground
John Tromp, Binary Lambda Calculus and Combinatory Logic
John Tromp, More efficient Haskell program

Cf. A114851, A195691.

a114852 = closed 0 where
  closed k n = if n<2 then 0 else
    (if n-2

A114852T := proc(k,n)
    option remember;
    local a;
    if n = 0 or n = 1 then
        0;
    else
        a := procname(k+1,n-2) ;
        if k > n-2 then
            a := a+1 ;
        fi ;
        a := a+add(procname(k,i)*procname(k,n-i-2),i=0..n-2) ;
    end if;
end proc:
A114852 := proc(n)
    A114852T(0,n) ;
end proc: # R. J. Mathar, Feb 28 2015

S[, 0] = 0; S[, 1] = 0; S[m_, n_] := S[m, n] = Boole[m >= n-1] + S[m+1, n-2] + Sum[S[m, k] S[m, n-k-2], {k, 0, n-2}];
a[n_] := S[0, n];
Table[a[n], {n, 0, 40}] (* Jean-François Alcover, May 23 2017 *)

a(n) = N(0,n) with
  N(k,0) = N(k,1) = 0
  N(k,n+2) = (if k>n then 1 else 0) +
             N(k+1,n) +
             Sum_{i=0..n} N(k,i) * N(k,n-i)

A114851 Number of lambda calculus terms of size n, where size(lambda x.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 (corresponding to a binary encoding).

Original entry on oeis.org

0, 0, 1, 1, 2, 2, 4, 5, 10, 14, 27, 41, 78, 126, 237, 399, 745, 1292, 2404, 4259, 7915, 14242, 26477, 48197, 89721, 164766, 307294, 568191, 1061969, 1974266, 3698247, 6905523, 12964449, 24295796, 45711211, 85926575, 161996298, 305314162, 576707409, 1089395667

Offset: 0

John Tromp, Feb 20 2006

nonn

Let r be the root of the polynomial P(x) = x^5 + 3x^4 - 2x^3 + 2 x^2 + x - 1 that is closest to the origin. r is about 0.5093081270242373 and 1/r is about 1.963447954075964. Let P' be the derivative of P. Let C = sqrt(P'(r)/(1-r)) / (2 sqrt(pi) r^(3/2)); then C is about 1.0218740729. Then a(n) ~ (C / n^(3/2)) * (1/r)^n. - Pierre Lescanne, May 29 2013

			a(4) = 2 because lambda x.x and var3 (bound by 3rd enclosing lambda) are the only two lambda terms of size 4.
G.f. = x^2 + x^3 + x^4 + x^5 + 2*x^6 + 3*x^7 + 6*x^8 + 9*x^9 + 17*x^10 + ...

Vincenzo Librandi, Table of n, a(n) for n = 0..1000
Maciej Bendkowski, K. Grygiel, and P. Tarau, Random generation of closed simply-typed lambda-terms: a synergy between logic programming and Boltzmann samplers, arXiv preprint arXiv:1612.07682 [cs.LO], 2016-2017.
K. Grygiel and P. Lescanne, Counting terms in the binary lambda calculus, arXiv preprint arXiv:1401.0379 [cs.LO], 2014.
Katarzyna Grygiel and Pierre Lescanne, Counting and Generating Terms in the Binary Lambda Calculus (Extended version), HAL Id: ensl-01229794, 2015.
Pierre Lescanne, An exercise on streams: convergence acceleration, arXiv preprint arXiv:1312.4917 [cs.NA], 2013.
P. Lescanne, Boltzmann samplers for random generation of lambda terms, arXiv preprint arXiv:1404.3875 [cs.DS], 2014.
Paul Tarau, A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms, arXiv preprint arXiv:1608.03912 [cs.PL], 2016.
John Tromp, John's Lambda Calculus and Combinatory Logic Playground
John Tromp, Binary Lambda Calculus and Combinatory Logic
John Tromp, More efficient Haskell program

Cf. A114852, A195691, A236393.

a114851 = open where
  open n = if n<2 then 0 else
           1 + open (n-2) + sum [open i * open (n-2-i) | i <- [0..n-2]]
-- See link for a more efficient version.

a[n_] := a[n] = 1 + a[n-2] + Sum[ a[i]*a[n-i-2], {i, 0, n-2}]; a[0] = a[1] = 0; Table[a[n], {n, 0, 32}] (* Jean-François Alcover, Dec 06 2011 *)
a[ n_] := SeriesCoefficient[ (1 - x - x^2 + x^3 - Sqrt[(1 + x - x^2 - x^3)^2 - 4 (x - 2 x^3 + x^4)]) / (2 (x^2 - x^3)), {x, 0, n}]; (* Michael Somos, Feb 25 2014 *)
CoefficientList[Series[(1 - x - x^2 + x^3 - Sqrt[(1 + x - x^2 - x^3)^2 -4 (x - 2 x^3 + x^4)])/(2 (x^2 - x^3)), {x, 0, 40}], x] (* _Vincenzo Librandi Mar 01 2014 *)

x='x+O('x^66); concat( [0,0], Vec( (1-x-x^2+x^3-sqrt((1+x-x^2-x^3)^2-4*(x-2*x^3+x^4)))/(2*(x^2-x^3)) ) ) \\ Joerg Arndt, Mar 01 2014

a(n+2) = 1 + a(n) + Sum_{i=0..n} a(i)*a(n-i), with a(0) = a(1) = 0.
G.f.: ( 1 - x - x^2 + x^3 - sqrt((1 + x - x^2 - x^3)^2 - 4*(x - 2*x^3 + x^4)) ) / (2*(x^2 - x^3)). - Michael Somos, Jan 28 2014
G.f.: A(x) =: y satisfies 0 = 1 / (1 - x) + (1 - 1/x^2) * y + y^2. - Michael Somos, Jan 28 2014
Conjecture: (n+2)*a(n) + 2*(-n-1)*a(n-1) + (-n+2)*a(n-2) + 4*(n-2)*a(n-3) + (-5*n+18)*a(n-4) + 2*(n-4)*a(n-5) + (n-6)*a(n-6) = 0. - R. J. Mathar, Mar 04 2015

More terms from Vincenzo Librandi, Mar 01 2014

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

A224345 Number of closed normal forms of size n in lambda calculus with size 0 for the variables.

Original entry on oeis.org

1, 3, 11, 53, 323, 2359, 19877, 188591, 1981963, 22795849, 284285351, 3815293199, 54762206985, 836280215979, 13527449608779, 230894574439485, 4144741143359355, 78017419806432567, 1535903379571939981, 31550210953904250759

Offset: 1

Pierre Lescanne, Apr 04 2013

nonn

Pierre Lescanne, Table of n, a(n) for n = 1..500
Maciej Bendkowski, K Grygiel, P Tarau, Random generation of closed simply-typed lambda-terms: a synergy between logic programming and Boltzmann samplers, arXiv preprint arXiv:1612.07682, 2016
K. Grygiel and P. Lescanne, Counting and generating lambda-terms, arXiv preprint arXiv:1210.2610 [cs.LO], 2012-2013.
Paul Tarau, On logic programming representations of lambda terms: de Bruijn indices, compression, type inference, combinatorial generation, normalization, 2015.
P. Tarau, A Logic Programming Playground for Lambda Terms, Combinators, Types and Tree-based Arithmetic Computations, arXiv preprint arXiv:1507.06944 [cs.LO], 2015.
Paul Tarau, A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms, arXiv preprint arXiv:1608.03912 [cs.PL], 2016.

Cf. A220894, A135501, A220895, A220896, A220897.

Cf. A195691 for another size of the terms.

gtab :: [[Integer]]
gtab = [0..] : [[s n m |  m <- [0..]] | n <- [1..]]
  where s n m  = let fi =  [ftab !! i !! m | i <- [0..(n-1)]]
                     gi =  [gtab !! i !! m | i <- [0..(n-1)]]
                 in foldl (+) 0 (map (uncurry (*)) (zip fi (reverse gi)))
ftab :: [[Integer]]
ftab = [0..] : [[ftab !! (n-1) !! (m+1) + gtab !! n !! m | m<-[0..]] | n<-[1..]]
f(n,m) = ftab !! n !! m

F[0, m_] := m; F[n_, m_] := F[n, m] = F[n-1, m+1] + G[n, m]; G[0, m_] := m; G[n_, m_] := G[n, m] = Sum[G[n-k-1, m]*F[k, m], {k, 0, n-1}]; a[n_] := F[n, 0]; Array[a, 20] (* Jean-François Alcover, May 23 2017 *)

a(n) = F(n,0) where F(0,m) = m, F(n+1,m) = F(n,m+1) + G(n+1,m), and G(0,m) = m, G(n+1,m) = sum(k=0..n, G(n-k,m)*F(k,m)*d(n,0) ) where d(0,i) = [i = 1], d(n+1,i) = sum(j=i..n+1, binomial(j,i)*d(n,j) + g(n+1,j) ) and g(0,i) = [i = 1], g(n+1,i) = sum(j=0..i, sum(k=0..n, g(k,j)*d(n-k,i-j) ) ).

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

cp's OEIS Frontend

A114852 The number of closed lambda calculus terms of size n, where size(lambda x.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 (corresponding to a binary encoding).

Views

Author

Keywords

Examples

Links

Crossrefs

Programs

Haskell

Maple

Mathematica

Formula

A114851 Number of lambda calculus terms of size n, where size(lambda x.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 (corresponding to a binary encoding).

Views

Author

Keywords

Comments

Examples

Links

Crossrefs

Programs

Haskell

Mathematica

PARI

Formula

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

A224345 Number of closed normal forms of size n in lambda calculus with size 0 for the variables.

Views

Author

Keywords

Links

Crossrefs

Programs

Haskell

Mathematica

Formula

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