Enumerating Lambda Terms by Weighted Length of Their De Bruijn Representation

TL;DR

This paper analyzes the enumeration of lambda terms using weighted de Bruijn representations, disproves a previous conjecture on their asymptotic count, and introduces efficient random sampling methods for large lambda terms.

Contribution

It generalizes the notion of size for lambda terms, provides precise asymptotic counts, and develops an efficient uniform sampling algorithm for large lambda terms.

Findings

Disproves Grygiel and Lescanne's conjecture on lambda term enumeration.

Establishes asymptotic formulas for various classes of lambda terms.

Introduces a highly efficient method for uniform random sampling of large lambda terms.

Abstract

John Tromp introduced the so-called 'binary lambda calculus' as a way to encode lambda terms in terms of 0-1-strings using the de Bruijn representation along with a weighting scheme. 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$ and according to Tromp's weights) 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. The methodology used is setting up the generating functions for the classes of lambda terms. These are infinitely nested radicals which are investigated then by a singularity analysis. We show further how some properties of random lambda terms can be analyzed and present a way to sample lambda terms uniformly at random in a very efficient way. This allows to generate terms of size more than one million within a reasonable time, which is significantly better than the samplers presented in the literature so far.