-
The Benefits of Diligence
Authors:
Victor Arrial,
Giulio Guerrieri,
Delia Kesner
Abstract:
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embeddings enable establishing (static and dynamic) properties of {\tt dCBN} and {\tt dCBV} through their respective counterparts in {\tt dBANG}. While some specific static properties have been already successfully studied in…
▽ More
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embeddings enable establishing (static and dynamic) properties of {\tt dCBN} and {\tt dCBV} through their respective counterparts in {\tt dBANG}. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) {\tt dCBN} case, while a novel one must be introduced for the (difficult) {\tt dCBV} case. Moreover, a key point of our approach is the identification of {\tt dBANG} diligent reduction sequences, which eases the preservation of dynamic properties from {\tt dBANG} to {\tt dCBN}/{\tt dCBV}. We illustrate our methodology through two concrete applications: confluence/factorization for both {\tt dCBN} and {\tt dCBV} are respectively derived from confluence/factorization for {\tt dBANG}.
△ Less
Submitted 19 April, 2024;
originally announced April 2024.
-
Meaningfulness and Genericity in a Subsuming Framework
Authors:
Delia Kesner,
Victor Arrial,
Giulio Guerrieri
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 sho…
▽ More
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.
△ Less
Submitted 9 April, 2024;
originally announced April 2024.
-
Genericity Through Stratification
Authors:
Victor Arrial,
Giulio Guerrieri,
Delia Kesner
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 literat…
▽ More
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.
△ Less
Submitted 31 January, 2024; v1 submitted 22 January, 2024;
originally announced January 2024.
