The Benefits of Diligence
Victor Arrial, Giulio Guerrieri, Delia Kesner
TL;DR
This work provides a unified framework for reasoning about Call-by-Name and Call-by-Value by embedding both into the Distant Bang Calculus $dBANG$, which is equipped with two modalities $\\oc$ and $\\mathsf{der}$ and supports reductions at a distance. A central novelty is the notion of diligent administration, which ensures administrative reductions are performed promptly, enabling robust simulation and reverse simulation between $dBANG$ and the adequate calculi $dCBN$ and $dCBV$. The authors introduce a refined $dCBV$ embedding that preserves reverse simulation and arrives at a three-for-one result: confluence/factorization properties of $dBANG$ immediately yield corresponding results for $dCBN$ and $dCBV$. They also prove a new factorization theorem for $dBANG$ and show how to project it to $dCBN$ and $dCBV$, dramatically simplifying dynamic property transfer across the unifying framework. Overall, the paper advances the methodology for deriving dynamic properties from a unifying calculus and broadens the toolkit for open-term computation models in typed and untyped settings.
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}.