Meaningfulness and Genericity in a Subsuming Framework

TL;DR

This work proposes the dBang-calculus as a unifying framework that subsumes both call-by-name and call-by-value evaluation. It provides a precise notion of meaningfulness for dBang by characterizing terms via typability in a non-idempotent intersection type system and via inhabitation, and proves that the induced theory $\mathcal{H}_{\text{dBang}}$ is consistent with a unique maximal extension. The paper also establishes strong genericity results, showing that meaningless subterms are irrelevant to the meaning of meaningful terms, and demonstrates that the dCBN/dCBV notions of meaningfulness are subsumed by the dBang-based framework through embeddings that preserve reductions and typing. Finally, it connects these results to practical notions of inhabitation and typing-driven program synthesis, providing a cohesive, unified account of meaningfulness across evaluation paradigms with concrete translations between the calculi. The work thus advances a cohesive theory for normalization and resource-aware reasoning across CBN, CBV, and their Bang-based unification.

Abstract

This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCbN) and call-by-value (dCbV). We first characterize meaningfulness in dBang by means of typability and inhabitation in an associated non-idempotent intersection type system previously proposed in the literature. We validate the proposed notion of meaningfulness by showing two properties (1) consistency of the theory $\mathcal{H}$ equating meaningless terms and (2) genericity, stating that meaningless subterms have no bearing on the significance of meaningful terms. The theory $\mathcal{H}$ is also shown to have a unique consistent and maximal extension. Last but not least, we show that the notions of meaningfulness and genericity in the literature for dCbN and dCbV are subsumed by the respectively ones proposed here for the dBang-calculus.

Figures (5)

• Figure 1: Type System $\mathcal{B}$ for the dBang-calculus.
• Figure 2: A type derivation of $xx$ in system $\mathcal{B}$.
• Figure 3: Inhabitation of $\left[\alpha\right] \Rightarrow \left[\alpha\right]$ in system $\mathcal{B}$.
• Figure 4: Type System $\mathcal{N}$ for the dCBN-calculus.
• Figure 5: Type System $\mathcal{V}$ for the dCBV-calculus.

Theorems & Definitions (22)

• Theorem 1
• Lemma 2: BucciarelliKesnerRiosViso20
• Theorem 3: BucciarelliKesnerRiosViso20ArrialGuerrieriKesner23
• Definition 4
• Definition 5
• Lemma 5
• Theorem 6: Logical Characterization
• Proposition 6: Consistency of $\bangTheoryH$
• Lemma 6
• Theorem 7: Typed Genericity