Combinatorics of explicit substitutions

TL;DR

This paper explores the combinatorial and probabilistic properties of the extended lambda calculus with explicit substitutions, revealing connections to Catalan numbers and insights into the non-strict evaluation behavior of typical terms.

Contribution

It uncovers the combinatorial structure of lambda-v calculus, establishes sampling schemes for random terms, and analyzes the distribution of redexes and substitution primitives.

Findings

Counting sequence for lambda-v terms matches Catalan numbers.

Most substitutions in lambda-v are suspended and unevaluated.

Typical lambda-v terms correspond to non-strict computations.

Abstract

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