John Tromp introduced the so-called 'binary lambda calculus' as a way to encode lambda terms in terms of 0-1-strings. Later, Grygiel and Lescanne conjectured that the number of binary lambda terms with m free indices and of size n (encoded as binary words of length n) is o(n^{-3/2} tau^{-n}) for tau ~ 1.963448... . We generalize the proposed notion of size and show that for several classes of lambda terms, including binary lambda terms with m free indices, the number of terms of size n is Theta(n^{-3/2} * rho^{-n}) with some class dependent constant rho, which in particular disproves the above mentioned conjecture. A way to obtain lower and upper bounds for the constant near the leading term is presented and numerical results for a few previously introduced classes of lambda terms are given.
@InProceedings{gittenberger_et_al:LIPIcs.STACS.2016.40, author = {Gittenberger, Bernhard and Golebiewski, Zbigniew}, title = {{On the Number of Lambda Terms With Prescribed Size of Their De Bruijn Representation}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {40:1--40:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.40}, URN = {urn:nbn:de:0030-drops-57411}, doi = {10.4230/LIPIcs.STACS.2016.40}, annote = {Keywords: lambda calculus, terms enumeration, analytic combinatorics} }
Feedback for Dagstuhl Publishing