# 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.

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