arXiv · 1509.06139
On the number of lambda terms with prescribed size of their De Bruijn representation
Abstract
John Tromp introduced the so-called 'binary lambda calculus' as a way to encode lambda terms in terms of binary words. 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} τ^{-n})$ for $τ\approx 1.963448\ldots$. 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 $Θ(n^{-3/2} ρ^{-n})$ with some class dependent constant $ρ$, 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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Bernhard Gittenberger, Zbigniew Gołębiewski. 2015-09-21. On the number of lambda terms with prescribed size of their De Bruijn representation. https://arxiv.org/abs/1509.06139
Cite the original work for its findings. Save a collection to share your selection of sources.