On counting untyped lambda terms. (English) Zbl 1259.68028

Lescanne, Pierre

Theor. Comput. Sci. 474, 80-97 (2013).

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.

MSC:

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

Keywords:

combinatorics; lambda calculus; functional programming; randomization; Catalan numbers