The Benefits of Diligence

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