Non-Cartesian Guarded Recursion with Daggers
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916641694023680 |
|---|---|
| author | Lemonnier, Louis |
| author_facet | Lemonnier, Louis |
| contents | Guarded recursion is a framework allowing for a formalisation of streams in classical programming languages. The latter take their semantics in cartesian closed categories. However, some programming paradigms do not take their semantics in a cartesian setting; this is the case for concurrency, reversible and quantum programming for example. In this paper, we focus on reversible programming through its categorical model in dagger categories, which are categories that contain an involutive operator on morphisms. After presenting classical guarded recursion, we show how to introduce this framework into dagger categories with sufficient structure for data types, also called dagger rig categories. First, given an arbitrary category, we build another category shown to be suitable for guarded recursion in multiple ways, via enrichment and fixed point theorems. We then study the interaction between this construction and the structure of dagger rig categories, aiming for reversible programming. Finally, we show that our construction is suitable as a model of higher-order reversible programming languages, such as symmetric pattern-matching. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_14591 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Non-Cartesian Guarded Recursion with Daggers Lemonnier, Louis Logic in Computer Science Programming Languages Category Theory Guarded recursion is a framework allowing for a formalisation of streams in classical programming languages. The latter take their semantics in cartesian closed categories. However, some programming paradigms do not take their semantics in a cartesian setting; this is the case for concurrency, reversible and quantum programming for example. In this paper, we focus on reversible programming through its categorical model in dagger categories, which are categories that contain an involutive operator on morphisms. After presenting classical guarded recursion, we show how to introduce this framework into dagger categories with sufficient structure for data types, also called dagger rig categories. First, given an arbitrary category, we build another category shown to be suitable for guarded recursion in multiple ways, via enrichment and fixed point theorems. We then study the interaction between this construction and the structure of dagger rig categories, aiming for reversible programming. Finally, we show that our construction is suitable as a model of higher-order reversible programming languages, such as symmetric pattern-matching. |
| title | Non-Cartesian Guarded Recursion with Daggers |
| topic | Logic in Computer Science Programming Languages Category Theory |
| url | https://arxiv.org/abs/2409.14591 |