The Benefits of Diligence

TL;DR

This paper introduces a unifying framework called the Bang Calculus ({ t dBANG}) to embed and analyze Call-by-Name ({ t dCBN}) and Call-by-Value ({ t dCBV}) evaluation strategies, enabling the transfer of static and dynamic properties between them.

Contribution

The paper develops novel embeddings of { t dCBN} and { t dCBV} into { t dBANG} and introduces a new concept of diligent reduction sequences to facilitate property transfer.

Findings

Dynamic properties like confluence are established for { t dCBN} and { t dCBV} via { t dBANG}.

Static properties are already known, but dynamic ones are now addressed.

The methodology simplifies proving properties for different evaluation strategies.

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 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}.