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

Author

John Tromp, Feb 20 2006

Keywords

• nonn

Comments

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

Examples

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

Links

• 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

Crossrefs

Cf. A114852, A195691, A236393.

Programs

Haskell

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.

Mathematica

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

PARI

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

Formula

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

Extensions

More terms from Vincenzo Librandi, Mar 01 2014