Combinatorics of explicit substitutions

λν is an extension of the λ-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of λν focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for λν-terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random λν-terms. We show that typical λν-terms represent, in a strong sense, non-strict computations in the classic X-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e. unevaluated, under closures. Consequently, we argue that λν is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in λν and investigate the quantitative contribution of various substitution primitives