Paper detail

Combinatorics of $λ$-terms: a natural approach

We consider combinatorial aspects of $λ$-terms in the model based on de Bruijn indices where each building constructor is of size one. Surprisingly, the counting sequence for $λ$-terms corresponds also to two families of binary trees, namely black-white trees and zigzag-free ones. We provide a constructive proof of this fact by exhibiting appropriate bijections. Moreover, we identify the sequence of Motzkin numbers with the counting sequence for neutral $λ$-terms, giving a bijection which, in consequence, results in an exact-size sampler for the latter based on the exact-size sampler for Motzkin trees of Bodini et alli. Using the powerful theory of analytic combinatorics, we state several results concerning the asymptotic growth rate of $λ$-terms in neutral, normal, and head normal forms. Finally, we investigate the asymptotic density of $λ$-terms containing arbitrary fixed subterms showing that, inter alia, strongly normalising or typeable terms are asymptotically negligible in the set of all $λ$-terms.