On the Number of Lambda Terms With Prescribed Size of Their De Bruijn Representation

Authors Bernhard Gittenberger, Zbigniew Golebiewski

Thumbnail PDF


  • Filesize: 0.69 MB
  • 13 pages

Document Identifiers

Author Details

Bernhard Gittenberger
Zbigniew Golebiewski

Cite AsGet BibTex

Bernhard Gittenberger and Zbigniew Golebiewski. On the Number of Lambda Terms With Prescribed Size of Their De Bruijn Representation. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 40:1-40:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


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.
  • lambda calculus
  • terms enumeration
  • analytic combinatorics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc. A natural counting of lambda terms. CoRR, abs/1506.02367, 2015. URL: http://arxiv.org/abs/1506.02367.
  2. Olivier Bodini, Danièle Gardy, and Bernhard Gittenberger. Lambda-terms of bounded unary height. In Philippe Flajolet and Daniel Panario, editors, Proceedings of the Eighth Workshop on Analytic Algorithmics and Combinatorics, ANALCO 2011, San Francisco, California, USA, January 22, 2011, pages 23-32. SIAM, 2011. URL: http://dx.doi.org/10.1137/1.9781611973013.3.
  3. N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Nederl. Akad. Wetensch. Proc. Ser. A 75=Indag. Math., 34:381-392, 1972. Google Scholar
  4. Philippe Flajolet and Andrew M. Odlyzko. Singularity analysis of generating functions. SIAM J. Discrete Math., 3(2):216-240, 1990. URL: http://dx.doi.org/10.1137/0403019.
  5. Philippe Flajolet and Robert Sedgewick. Analytic Combinatorics. Cambridge University Press, New York, NY, USA, 1 edition, 2009. Google Scholar
  6. Katarzyna Grygiel and Pierre Lescanne. Counting and generating lambda terms. Journal of Functional Programming, 23:594-628, 2013. URL: http://dx.doi.org/10.1017/S0956796813000178.
  7. Katarzyna Grygiel and Pierre Lescanne. Counting terms in the binary lambda calculus. In DMTCS. 25th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms. Discrete Mathematics &Theoretical Computer Science, Jun 2014. Google Scholar
  8. John Tromp. Binary lambda calculus and combinatory logic. In Marcus Hutter, Wolfgang Merkle, and Paul M.B. Vitanyi, editors, Kolmogorov Complexity and Applications, number 06051 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany. URL: http://drops.dagstuhl.de/opus/volltexte/2006/628.