The Qualitative Collapse of Concurrent Games

TL;DR

This paper introduces a concrete, combinatorial functor linking concurrent games to Scott domains, providing a new proof of the qualitative-quantitative correspondence in game semantics.

Contribution

It constructs an interpretation-preserving functor from concurrent games to Scott domains, extending prior relational collapse results with a combinatorial approach.

Findings

Provides a concrete description of the functor

Extends earlier relational collapse results

Offers a new combinatorial proof of the extensional collapse theorem

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.