Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Qualitative Collapse of Concurrent Games

Pierre Clairambault

TL;DR

An interpretation-preserving functor is constructed from a category of concurrent games to the category of Scott domains and Scott-continuous functions, giving a concrete description of this functor, extending earlier results on the relational collapse of game semantics.

Abstract

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.

The Qualitative Collapse of Concurrent Games

TL;DR

An interpretation-preserving functor is constructed from a category of concurrent games to the category of Scott domains and Scott-continuous functions, giving a concrete description of this functor, extending earlier results on the relational collapse of game semantics.

Abstract

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.

Paper Structure

This paper contains 79 sections, 52 theorems, 176 equations, 14 figures.

Table of Contents

  1. Introduction
  2. The Qualitative and the Quantitative
  3. The Relational Model and Quantitative Semantics
  4. The relational model
  5. Non-idempotent intersection types
  6. Plays and refinement types.
  7. Rigidity and symmetries.
  8. The Qualitative
  9. Idempotent intersection types
  10. Cartesian maps
  11. Cartesian matching problems
  12. Outline.
  13. Thin Concurrent Games
  14. Basic Concurrent Games
  15. Event structures
  16. ...and 64 more sections

Key Result

Lemma 3.3

Consider a plain game $A$, and strategies $\sigma, \tau : A$. If $f : \mathscr{C}^+(\sigma) \cong \mathscr{C}^+(\tau)$ is an order-isomorphism such that $\partial_\tau \circ f = \partial_\sigma$, then there is a unique isomorphism of strategies $\hat{f} : \sigma \cong \tau$ such that for all $x \in

Figures (14)

  • Figure 1: Example of a play
  • Figure 2: Its position
  • Figure 3: Concrete configurations with copy indices
  • Figure 4: An example of matching but causally incompatible configurations, in the composition of $\sigma : \mathbb{U} \multimap \mathbb{U}$ and $\tau : \mathbb{U} \multimap \mathbb{U} \vdash \mathbb{N}$. The underlying games are left undefined, but can be recovered by removing the arrows $\rightarrowtriangle$. The configurations are matching on $\mathbb{U} \multimap \mathbb{U}$, but the arrows $\rightarrowtriangle$ impose incompatible orders (i.e. a cycle) between the two occurrences of $\checkmark$.
  • Figure 5: Payoff for $\otimes$ and $\parr$
  • ...and 9 more figures

Theorems & Definitions (111)

  • Definition 3.1
  • Definition 3.2
  • Lemma 3.3
  • proof
  • Proposition 3.4
  • proof
  • Proposition 3.5
  • proof
  • Theorem 3.6
  • Definition 3.7
  • ...and 101 more