The Benefits of Diligence
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914761991520256 |
|---|---|
| author | Arrial, Victor Guerrieri, Giulio Kesner, Delia |
| author_facet | Arrial, Victor Guerrieri, Giulio Kesner, Delia |
| contents | 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}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_12951 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Benefits of Diligence Arrial, Victor Guerrieri, Giulio Kesner, Delia Logic in Computer Science 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}. |
| title | The Benefits of Diligence |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2404.12951 |