On counting untyped lambda terms

Despite λ -calculus is now three quarters of a century old, no formula counting λ -terms has been proposed yet, and the combinatorics of λ -calculus is considered a hard problem. The difficulty lies in the fact that the recursive expression of the numbers of terms of size n with at most m free variables contains the number of terms of size n − 1 with at most m + 1 variables. This leads to complex recurrences that cannot be handled by classical analytic methods. Here based on de Bruijn indices (another presentation of λ -calculus) we propose several results on counting untyped lambda terms, i. e. , on telling how many terms belong to such or such class, according to the size of the terms and/or to the number of free variables. We extend the results to normal forms.

Authors

• Pierre Lescanne

Keywords

• Combinatorics
• Lambda calculus
• Functional programming
• Randomization
• Catalan numbers