Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929380517740544 |
|---|---|
| author | Paquet, Hugo Saville, Philip |
| author_facet | Paquet, Hugo Saville, Philip |
| contents | We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games.
We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics.
In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2304_11014 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads Paquet, Hugo Saville, Philip Logic in Computer Science Category Theory We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games. We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics. In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results. |
| title | Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2304.11014 |