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

TL;DR

This paper analyzes the asymptotic count of lambda terms with prescribed size in their De Bruijn representation, disproving a previous conjecture and providing bounds for various classes of lambda terms.

Contribution

It generalizes the notion of size for lambda terms, derives asymptotic formulas, and disproves a conjecture about their enumeration.

Findings

Number of lambda terms of size n is Theta(n^{-3/2} rho^{-n}) for several classes.

Disproves Grygiel and Lescanne's conjecture on the asymptotic growth.

Provides bounds and numerical estimates for enumeration constants.

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} \tau^{-n})$ for $\tau \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 $\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.