Genericity Through Stratification

A fundamental issue in the λ-calculus is to find appropriate notions for meaningfulness. Inspired by well-known results for the call-by-name λ-calculus (CbN), where meaningful terms are identified to the solvable ones, this paper validates the challenging claim that the notion of potential valuability (aka scrutability), previously introduced in the literature, adequately represents meaningfulness in the call-by-value λ-calculus (CbV). Akin to CbN, this claim is corroborated by proving two essential properties. The first one is genericity, stating that meaningless subterms have no bearing on evaluating normalizing terms. To prove this, we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms (without equating all terms). We also show that such a congruence has a unique consistent and maximal extension, which coincides with a natural notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.