The Benefits of Diligence

This paper studies the strength of embedding Call-by-Name (dCBN) and Call-by-Value (dCBV) into a unifying framework called the Bang Calculus (dBANG). These embeddings enable establishing (static and dynamic) properties of dCBN and dCBV through their respective counterparts in \(\texttt {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) dCBN case, while a novel one must be introduced for the (difficult) dCBV case. Moreover, a key point of our approach is the identification of dBANG diligent reduction sequences, which eases the preservation of dynamic properties from \(\texttt {dBANG} \) to \(\texttt {dCBN}/\texttt {dCBV} \) . We illustrate our methodology through two concrete applications: confluence/factorization for both dCBN and dCBV are respectively derived from confluence/factorization for dBANG .