From Thin Concurrent Games to Generalized Species of Structures (Extended Version)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914119098040320 |
|---|---|
| author | Clairambault, Pierre Olimpieri, Federico Paquet, Hugo |
| author_facet | Clairambault, Pierre Olimpieri, Federico Paquet, Hugo |
| contents | Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically based on a category of relations. In this paper we introduce a formal bridge between a dynamic model and a static model: the model of thin concurrent games and strategies, based on event structures, and the model of generalized species of structures, based on distributors. A special focus of this paper is the two-dimensional nature of the dynamic-static relationship, which we formalize with double categories and bicategories.
In the first part of the paper, we construct a symmetric monoidal oplax functor from linear concurrent strategies to distributors. We highlight two fundamental differences between the two models: the composition mechanism, and the representation of resource symmetries. In the second part of the paper, we adapt established methods from game semantics (visible strategies, payoff structure) to enforce a tighter connection between the two models. We obtain a cartesian closed pseudofunctor, which we exploit to shed new light on recent results in the theory of the lambda-calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_01082 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | From Thin Concurrent Games to Generalized Species of Structures (Extended Version) Clairambault, Pierre Olimpieri, Federico Paquet, Hugo Logic in Computer Science Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically based on a category of relations. In this paper we introduce a formal bridge between a dynamic model and a static model: the model of thin concurrent games and strategies, based on event structures, and the model of generalized species of structures, based on distributors. A special focus of this paper is the two-dimensional nature of the dynamic-static relationship, which we formalize with double categories and bicategories. In the first part of the paper, we construct a symmetric monoidal oplax functor from linear concurrent strategies to distributors. We highlight two fundamental differences between the two models: the composition mechanism, and the representation of resource symmetries. In the second part of the paper, we adapt established methods from game semantics (visible strategies, payoff structure) to enforce a tighter connection between the two models. We obtain a cartesian closed pseudofunctor, which we exploit to shed new light on recent results in the theory of the lambda-calculus. |
| title | From Thin Concurrent Games to Generalized Species of Structures (Extended Version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2302.01082 |