Paper detail

On the number of lambda terms with prescribed size of their De Bruijn representation

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.