A114852 -id:A114852 - cp's OEIS frontend

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).

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

A195691 The number of closed normal form 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, 0, 0, 1, 0, 1, 1, 2, 1, 4, 4, 8, 7, 18, 23, 42, 50, 105, 153, 271, 385, 721, 1135, 1992, 3112, 5535, 9105, 15916, 26219, 45815, 77334, 135029, 229189, 399498, 685710, 1198828, 2070207, 3619677, 6286268, 11024475, 19241836, 33795365, 59197968, 104234931

Offset: 0

John Tromp, Sep 22 2011

nonn

			This sequence first differs from A114852 at n=10, where it excludes the two reducible terms (lambda x.x)(lambda x.x) and lambda x.(lambda x.x)x, so normal 10 = (closed 10)-2 = 6-2 = 4.

Wikipedia, Binary lambda calculus
John Tromp, A195691.hs

Cf. A114851, A114852.

Cf. A224345 for another way of counting normal forms in lambda-calculus.

a195691 = normal True 0 where
  normal qLam k n = if n<2 then 0 else
    (if n-2

A[, , 0] = A[, , 1] = 0; A[q_, k_, n_] := A[q, k, n] = Boole[k > n-2] + q*A[1, k+1, n-2] + Sum[A[0, k, i]*A[1, k, n-i-2], {i, 0, n-2}];
a[n_] := A[1, 0, n];
Table[a[n], {n, 0, 44}] (* Jean-François Alcover, May 23 2017 *)

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

A220894 Number of closed lambda-terms of size n with size 0 for the variables.

Original entry on oeis.org

0, 1, 3, 14, 82, 579, 4741, 43977, 454283, 5159441, 63782411, 851368766, 12188927818, 186132043831, 3017325884473, 51712139570022, 933654684562038, 17702959714232057, 351535449888420187, 7292626296788508624, 157698798590301690864, 3547597554377118966359

Offset: 0

N. J. A. Sloane, Dec 31 2012

nonn

Alois P. Heinz, Table of n, a(n) for n = 0..200
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.
Katarzyna Grygiel and Pierre Lescanne, Counting and generating lambda-terms, arXiv preprint arXiv:1210.2610 [cs.LO], 2012.
Katarzyna Grygiel and Pierre Lescanne, Counting and Generating Terms in the Binary Lambda Calculus (Extended version), HAL Id: ensl-01229794, 2015.
Paul Tarau, On Type-directed Generation of Lambda Terms, preprint, 2015.
Paul Tarau, On logic programming representations of lambda terms: de Bruijn indices, compression, type inference, combinatorial generation, normalization, 2015.
Paul 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. A135501, A114852.

Cf. A220895 (one free variable), A220896 (two free variables), A220897 (three free variables).

t :: Int -> Int -> Integer
t 0 m = (fromIntegral m)
t n m = t (n-1) (m+1) + foldl (+) 0 (let tt = [t i m | i<- [0..(n-1)]] in
                                      (map (uncurry (*)) (zip tt (reverse tt))))
-- Pierre Lescanne, Mar 18 2013

-- The following program is more efficient:
with memoization
ttab :: [[Integer]]
ttab = [0..] : [[ttab !! (n-1) !! (m+1) + s n m | m <- [0..]] | n <- [1..]]
  where s n m  = let ti = [ttab !! i !! m | i <- [0..(n-1)]] in foldl (+) 0 (map (uncurry (*)) (zip ti (reverse ti)))
t :: Int -> Int -> Integer
t n m = ttab !! n !! m
-- Pierre Lescanne, Mar 20 2013

a:= n-> T(n, 0):
T:= proc(n, m) option remember; `if`(n=0, m,
      T(n-1, m+1) +add(T(i, m)*T(n-1-i, m), i=0..n-1))
    end:
seq(a(n), n=0..30);  # Alois P. Heinz, Mar 20 2013

Clear[t]; t[0, m_] := m; t[n_, m_] := t[n, m] = t[n-1, m+1] + Sum[t[i, m]*t[n-1-i, m], {i, 0, n-1}]; a[n_] := t[n, 0]; Table[a[n], {n, 0, 21}] (* Jean-François Alcover, Apr 04 2013 *)

@CachedFunction
def T(n, m):
    if n == 0: return m
    return T(n-1, m+1) + sum(T(i, m) * T(n-1-i, m) for i in range(n))
def a(n):
    return T(n,0)
[a(n) for n in range(66)]
# Joerg Arndt, Jan 01 2013

T(n,0) where
    T(0,m) = m;
    T(n+1,m) = T(n,m+1) + sum_{i=0 to n} T(i,m) * T(n-i,m).
f(n,0) where f(0,1) = 1; f(0,k) = 0 if k!=1; f(n,k) = 0 if k>2n-1; f(n,k) = f(n-1,k) + f(n-1,k+1) + sum_{p=1 to n-2} sum_{c=0 to k} sum_{l=0 to k - c} [C^c_k C^l_(k-c) f(p,l+c) f(n-p-1,k-l)], where C^p_n are binomial coefficients (the last term is for the application where "c" is the number of common variables in both subterms). f(n,k) can be computed only using f(n',k') with n' < n and k' <= k + n - n'. f(n,k) is the number of lambda terms of size n (with size 0 for the variables) having exactly k free variables.
c(n,0) where
  c(0,1) = 1; c(0,i) if i!=1;
  c(n+1,i) sum{j=i to n+1} binomial(j,i) * c(n,j) + sum{j=0 to i} sum{k=0..n} c(k,j)* c(n-k,i-j).
G.f.: L(z,0) where L(z,u) = u + z*L(z,u+1) + z*L(z,u)^2. - Pierre Lescanne, Mar 14 2013

More terms from Joerg Arndt, Jan 01 2013

A236393 Number of typable lambda terms of size n with size 0 for the variables.

Original entry on oeis.org

0, 0, 1, 1, 2, 2, 3, 5, 8, 13, 22, 36, 58, 103, 177, 307, 535, 949, 1645, 2936, 5207, 9330, 16613, 29921, 53588, 96808, 174443, 316267, 572092, 1040596, 1888505, 3441755, 6268500, 11449522, 20902152, 38256759, 70004696, 128336318, 235302612, 432050796, 793513690, 1459062947, 2683714350

Offset: 0

N. J. A. Sloane, Jan 27 2014

nonn

For definition see Appendix A of Grygiel and Lescanne, arXiv 2014.

Katarzyna Grygiel, Pierre Lescanne. Counting and Generating Terms in the Binary Lambda Calculus (Extended version). 2015.

Katarzyna Grygiel, Pierre Lescanne, Counting and generating lambda terms, arXiv:1210.2610 [cs.LO], 2012.
Katarzyna Grygiel, Pierre Lescanne, Counting Terms in the Binary Lambda Calculus, arXiv:1401.0379 [cs.LO], 2014.
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.

Cf. A114851, A114852, A236405.

Name clarified by Pierre Lescanne, Jul 13 2016

A236405 Number of closed typable lambda terms of size n with size 0 for the variables.

Original entry on oeis.org

0, 0, 0, 0, 1, 0, 1, 1, 1, 1, 5, 4, 9, 13, 23, 29, 67, 94, 179, 285, 503, 795, 1503, 2469, 4457, 7624, 13475, 23027, 41437, 72165, 128905, 227510, 405301, 715078, 1280127, 2279393, 4086591, 7316698, 13139958, 23551957, 42383667, 76278547, 137609116, 248447221, 449201368, 812315229, 1470997501

Offset: 0

N. J. A. Sloane, Jan 31 2014

nonn

For definition see Appendix A of Grygiel and Lescanne, arXiv 2014.

Katarzyna Grygiel, Pierre Lescanne. Counting and Generating Terms in the Binary Lambda Calculus (Extended version). 2015.

K. Grygiel, P. Lescanne, Counting terms in the binary lambda calculus, arXiv preprint arXiv:1401.0379 [cs.LO], 2014.

Cf. A114851, A114852, A236393.

Name clarified by Pierre Lescanne, Jul 13 2016

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

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

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

A195691 The number of closed normal form 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

Mathematica

Formula

A220894 Number of closed lambda-terms of size n with size 0 for the variables.

Views

Author

Keywords

Links

Crossrefs

Programs

Haskell

Haskell

Maple

Mathematica

Sage

Formula

Extensions

A236393 Number of typable lambda terms of size n with size 0 for the variables.

Views

Author

Keywords

Comments

References

Links

Crossrefs

Extensions

A236405 Number of closed typable lambda terms of size n with size 0 for the variables.

Views

Author

Keywords

Comments

References

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

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