arXiv++ Combinatorics

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