Genericity Through Stratification

TL;DR

This work addresses the problem of identifying meaningful terms in the λ-calculus, extending the classical CbN notion (solvability) to Call-by-Value (CbV) through scrutability and stratified genericity. It introduces meaningful approximants and a stratified reduction framework to capture qualitative and quantitative genericity for both CbN and CbV, culminating in direct operational proofs of consistency for the associated theories. The authors define the H and H* theories in CbV and show that H* coincides with observational equivalence, paralleling the CbN story and establishing a canonical semantic foundation for meaningfulness across evaluation strategies. The methodology relies on explicit substitutions and reduction at a distance, producing robust, modular results that open avenues toward broader unifying frameworks such as call-by-push-value and call-by-need."

Abstract

A fundamental issue in the $λ$-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name $λ$-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value $λ$-calculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literature as potential valuability, appropriately represents meaningfulness in 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 (which was an open problem), we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV, and in a quantitative way. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms. While the consistency result is not new, we provide the first direct operational proof of it. We also show that such a congruence has a unique consistent and maximal extension, which coincides with a well-known notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.

Theorems & Definitions (127)

• lemma 1: AP12
• lemma 2
• definition 1
• lemma 3: Meaningful Characterizations AP12AccattoliGuerrieri22bisBKRV20
• lemma 4: AccattoliGuerrieri22bis
• lemma 5: Typed Genericity
• theorem 1: Qualitative Surface Genericity
• proof
• lemma 6
• lemma 7: Approximant Genericity