zbMATH — the first resource for mathematics

On counting untyped lambda terms. (English) Zbl 1259.68028
Summary: Despite \(\lambda\)-calculus is now three quarters of a century old, no formula counting \(\lambda\)-terms has been proposed yet, and the combinatorics of \(\lambda\)-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 \(\lambda\)-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.

68N18 Functional programming and lambda calculus
68R05 Combinatorics in computer science
03B40 Combinatory logic and lambda calculus
Full Text: DOI