A220894 -id:A220894 - cp's OEIS frontend

A135501 Number of closed lambda-terms of size n with size 1 for the variables.

0, 0, 1, 2, 4, 13, 42, 139, 506, 1915, 7558, 31092, 132170, 580466, 2624545, 12190623, 58083923, 283346273, 1413449148, 7200961616, 37425264180, 198239674888, 1069228024931, 5867587726222, 32736878114805, 185570805235978

Offset: 0

Christophe Raffalli (christophe.raffalli(AT)univ-savoie.fr), Feb 09 2008

nonn

A lambda-term is a term which is either a variable "x" (of size 1), an application of two lambda-terms (of size 1 + the sum of the sizes of the two subterms), or a lambda binding a new variable in a term (of size 1 + the size of the subterm).

The size of a lambda-term t can be equivalently defined as the number of ways of selecting a subterm of t (distinguishing between different occurrences of the same subterm). For example, the 2 closed terms with three subterms are \x.\y.x (subterms \x.\y.x, \y.x, and x) and \x.\y.y (subterms \x.\y.y, \y.y, and y), while the 4 with four subterms are \x.\y.\z.x, \x.\y.\z.y, \x.\y.\z.z, and \x.x(x) (subterms \x.x(x), x(x), x[1], and x[2], distinguishing between the two occurrences of the variable x). - Noam Zeilberger, Nov 10 2018

Noam Zeilberger, Table of n, a(n) for n = 0..300 (terms 2-63 from Christophe Raffalli)
Olivier Bodini, Danièle Gardy, Bernhard Gittenberger, Zbigniew Gołębiewski, On the number of unary-binary tree-like structures with restrictions on the unary height, arXiv:1510.01167 [math.CO], 2015, see p. 4.
Olivier Bodini, Paul Tarau, On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms, arXiv:1709.04302 [cs.PL], 2017.
Katarzyna Grygiel and Pierre Lescanne, Counting and generating lambda-terms, arXiv preprint arXiv:1210.2610 [cs.LO], 2012-2013.
Pierre Lescanne, On counting untyped lambda terms, arXiv:1107.1327 [cs.LO], 2011-2012.
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.
P. Tarau, A Logic Programming Playground for Lambda Terms, Combinators, Types and Tree-based Arithmetic Computations, arXiv preprint arXiv:1507.06944 [cs.LO], 2015.
Noam Zeilberger, Alain Giorgetti, A correspondence between rooted planar maps and normal planar lambda terms, arXiv:1408.5028 [cs.LO], 2014.

Cf. A220894, A062980.

T := proc(n, k) option remember; `if`(n <= 0, 0, `if`(n = 1, k,
T(n-1, k+1) + add(T(n-1-j, k)*T(j, k), j = 0..n-2))) end:
a := n -> T(n, 0): seq(a(n), n=0..25); # Peter Luschny, Nov 10 2018

T[0, ] = 0; T[1, m] := m;
T[n_, m_] := T[n, m] = T[n-1, m+1] + Sum[T[n-1-k, m] T[k, m], {k, 0, n-2}];
a[n_] := T[n, 0]; Table[a[n], {n, 0, 25}] (* Jean-François Alcover, Aug 06 2018, after Pierre Lescanne *)

f(n,0) where f(1,1) = 1; f(0,k) = 0; 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 1 for the variables) having exactly k free variables.
T(n,0) where T(0,m) = 0; T(1,m) = m; T(n+1,m) = T(n,m+1) + sum{k=0 to n-11} [T(n-k,m) T(k,m)].   T(n,m) is the number of lambda terms of size n (with size 1 for the variables) having at most m free variables. [Pierre Lescanne, Nov 18 2012]
The ordinary generating function l(z) can be computed using a catalytic variable as l(z) = L(z,0), where L(z,f) satisfies the functional equation L(z,f) = f*z + z*L(z,f)^2 + z*L(z,f+1). See equation (2) of [Bodini et al., 2015]. - Noam Zeilberger, Nov 10 2018

Two terms prepended by Noam Zeilberger, Nov 10 2018

A220471 Number of closed simply typable lambda-terms of size n with size 0 for the variables.

Original entry on oeis.org

1, 2, 9, 40, 238, 1564, 11807, 98529, 904318, 9006364, 96709332, 1110858977, 13581942434, 175844515544

Offset: 1

Pierre Lescanne, Apr 10 2013

Typable terms are terms that satisfy constraints which make them well formed.

The current computation requires one to generate all the plain lambda terms and to sieve out those that are typable. This is feasible for the 63782411 terms of size 10 but not for the 851368766 terms of size 11.

Alonzo Church, A Formulation of the Simple Theory of Types, J. Symb. Log. 5(2): 56-68 (1940).

Katarzyna Grygiel and Pierre Lescanne, Counting and generating lambda-terms, arXiv preprint arXiv:1210.2610, 2012
Paul Tarau, On a Uniform Representation for Combinators, Arithmetic, Lambda Terms and Types, preprint, 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.
P. Tarau, A Logic Programming Playground for Lambda Terms, Combinators, Types and Tree-based Arithmetic Computations, arXiv preprint arXiv:1507.06944, 2015
Paul Tarau, "Ranking/unranking of lambda terms with compressed de Bruijn indices, CICM 2015, Lect. Not. Comp. Sci. 9140, p. 118-133
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, 2016

Cf. A220894.

a(11) and a(12) added from Tarau (arXiv:1507.06944, 2015). - N. J. A. Sloane, Jan 30 2016

a(13) and a(14) added from Tarau (2016). - N. J. A. Sloane, Aug 04 2017

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

A259356 Triangle T(n,k) read by rows: T(n,k) is the number of closed lambda-terms of size n with size 0 for the variables and k abstractions.

Original entry on oeis.org

0, 0, 1, 0, 1, 2, 0, 2, 9, 3, 0, 5, 38, 35, 4, 0, 14, 181, 284, 95, 5, 0, 42, 938, 2225, 1320, 210, 6, 0, 132, 5210, 17816, 15810, 4596, 406, 7

Offset: 0

John Bodeen, Jun 24 2015

			In table format, the first few rows:
{0},
{0,1},
{0,1,2},
{0,2,9,3},
{0,5,38,35,4},
...
For n=3,k=2 we have the number of closed lambda terms of size three with exactly two abstractions, T(3,2,0) = 9:
\x.\y.x x
\x.\y.x y
\x.\y.y x
\x.\y.y y
(\x.x) (\y.y)
\x.(\y.y) x
\x.(\y.x) x
\x.x (\y.y)
\x.x (\y.x)

Cf. A220894 (row sums), A000108.

T(n,k) = T(n,k,0) where T(n,k,b) where n is size, k is number of abstractions, and b is number of free variables, T(0,0,b) = b, and T(n,k,b) = T(n-1,k-1,b+1) + Sum_{i=0..n-1} Sum_{j=0..k} T(i,j,b) * T(n-1-i,k-j,b).

T(n+1,1) = A000108(n).

cp's OEIS Frontend

A135501 Number of closed lambda-terms of size n with size 1 for the variables.

Views

Author

Keywords

Comments

Links

Crossrefs

Programs

Maple

Mathematica

Formula

Extensions

A220471 Number of closed simply typable lambda-terms of size n with size 0 for the variables.

Views

Author

Keywords

Comments

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

A259356 Triangle T(n,k) read by rows: T(n,k) is the number of closed lambda-terms of size n with size 0 for the variables and k abstractions.

Views

Author

Keywords

Examples

Crossrefs

Formula