The Qualitative Collapse of Concurrent Games
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913547382947840 |
|---|---|
| author | Clairambault, Pierre |
| author_facet | Clairambault, Pierre |
| contents | In this paper, we construct an interpretation-preserving functor from a category of concurrent games to the category of Scott domains and Scott-continuous functions. We give a concrete description of this functor, extending earlier results on the relational collapse of game semantics. The crux is an intricate combinatorial lemma allowing us to synchronize states of strategies which reach the same resources, but with different multiplicity.
Putting this together with the previously established relational collapse, this provides a new proof of the qualitative-quantitative correspondence first established by Ehrhard in his celebrated extensional collapse theorem. Whereas Ehrhard's proof is indirect and rests on an abstract realizability construction, our result gives a concrete, combinatorial description of the extraction of quantitative information from a qualitative model. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_11389 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Qualitative Collapse of Concurrent Games Clairambault, Pierre Logic in Computer Science In this paper, we construct an interpretation-preserving functor from a category of concurrent games to the category of Scott domains and Scott-continuous functions. We give a concrete description of this functor, extending earlier results on the relational collapse of game semantics. The crux is an intricate combinatorial lemma allowing us to synchronize states of strategies which reach the same resources, but with different multiplicity. Putting this together with the previously established relational collapse, this provides a new proof of the qualitative-quantitative correspondence first established by Ehrhard in his celebrated extensional collapse theorem. Whereas Ehrhard's proof is indirect and rests on an abstract realizability construction, our result gives a concrete, combinatorial description of the extraction of quantitative information from a qualitative model. |
| title | The Qualitative Collapse of Concurrent Games |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2410.11389 |