OFFSET
0,5
COMMENTS
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.
LINKS
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
CROSSREFS
KEYWORD
nonn,more
AUTHOR
Pierre Lescanne, Jul 13 2016
STATUS
approved