Pierre Lescanne - cp's OEIS frontend

A287141 Numbers of closed affine (a.k.a. BCK) lambda terms of natural size n.

0, 0, 1, 1, 2, 5, 12, 25, 64, 166, 405, 1050, 2763, 7239, 19190, 51457, 138538, 374972, 1020943, 2792183, 7666358, 21126905, 58422650, 162052566, 450742451, 1256974690, 3513731861, 9843728012, 27633400879, 77721141911, 218984204904, 618021576627, 1746906189740, 4945026080426, 14017220713131

Offset: 0

Pierre Lescanne, May 20 2017

nonn

Pierre Lescanne, Table of n, a(n) for n = 0..100
Pierre Lescanne, Quantitative aspects of linear and affine closed lambda term, arXiv:1702.03085 [cs.DM], 2017.

Cf. A281270, A275057.

A275057 Numbers of closed lambda terms of natural size n.

Original entry on oeis.org

0, 0, 1, 1, 3, 6, 17, 41, 116, 313, 895, 2550, 7450, 21881, 65168, 195370, 591007, 1798718, 5510023, 16966529, 52506837, 163200904, 509323732, 1595311747, 5013746254, 15805787496, 49969942138, 158396065350, 503317495573, 1602973785463, 5116010587910, 16360492172347

Offset: 0

Pierre Lescanne, Jul 14 2016

nonn

Natural size measure lambda terms as follows: all symbols are assigned size 1, namely applications, abstractions, successor symbols in de Bruijn indices and 0 symbol in de Bruijn indices (i.e., a de Bruijn index n is assigned size n+1).

Here we count the closed terms of natural size n, where "closed" means that there is no free index (no free bound variable).

Pierre Lescanne, Table of n, a(n) for n = 0..299
Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, Marek Zaionc, A Natural Counting of Lambda Terms, SOFSEM 2016: 183-194.
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 [cs.LO], 2016-2017.

Cf. A105633, A272794.

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

L(0,m) = 0.

L(n+1,m) = (Sum_{k=0..n} L(k,m)*L(n-k,m)) + L(n,m+1) + [m >= n+1], where [p(n,m)] = 1 if p(n,m) is true and [p(n,m)] = 0 if p(n,m) is false then one considers the sequence (L(n,0)).

A272794 The numbers of closed simply typable lambda terms of natural size n.

Original entry on oeis.org

0, 0, 1, 1, 2, 5, 13, 27, 74, 198, 508, 1371, 3809, 10477, 29116, 82419, 233748, 666201, 1914668, 5528622, 16019330, 46642245, 136326126, 399652720, 1175422931, 3467251920, 10258152021

Offset: 0

Pierre Lescanne, Jul 13 2016

Natural size measure lambda terms as follows: all symbols are assigned size 1, namely applications, abstractions, successor symbols in de Bruijn indices and 0 symbol in de Bruijn indices (i.e., a de Bruijn index n is assigned size n+1).
Here we count the closed simply typable terms of natural size n. "Closed" means that there is no free index (no free bound variable). "Simply typable" means that lambda terms have a simple type.
The numbers are computed as follows: all the closed terms are generated and then filtered using a type reconstruction algorithm. The values given above are the only known values of the sequence.

Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, Marek Zaionc, A natural counting of Lambda terms, arXiv:1506.02367 [cs.LO], 2015.
Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, Marek Zaionc, A Natural Counting of Lambda Terms, SOFSEM 2016: 183-194
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

Cf. A105633, A220471, A236393, A236405.

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

cp's OEIS Frontend

User: Pierre Lescanne

A287141 Numbers of closed affine (a.k.a. BCK) lambda terms of natural size n.

Views

Author

Keywords

Links

Crossrefs

A275057 Numbers of closed lambda terms of natural size n.

Views

Author

Keywords

Comments

Links

Crossrefs

Programs

Mathematica

Formula

A272794 The numbers of closed simply typable lambda terms of natural size n.

Views

Author

Keywords

Comments

Links

Crossrefs

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