The Quantitative Collapse of Concurrent Games with Symmetry

TL;DR

This paper establishes a formal connection between thin concurrent games and weighted relational models of linear logic, introducing a collapse functor that counts witnesses while respecting symmetries, and extends to probabilistic and other semiring weights.

Contribution

It defines a novel interpretation-preserving collapse functor from concurrent games to relational models, handling symmetries and witnesses, and generalizes to arbitrary continuous semirings.

Findings

The collapse functor accurately translates strategies into weighted relational models.

Witness counting requires factoring out symmetries, a key technical contribution.

The framework extends to probabilistic and other weighted models using continuous semirings.

Abstract

We explore links between the thin concurrent games of Castellan, Clairambault and Winskel, and the weighted relational models of linear logic studied by Laird, Manzonetto, McCusker and Pagani. More precisely, we show that there is an interpretationpreserving "collapse" functor from the former to the latter. On objects, the functor defines for each game a set of possible execution states. Defining the action on morphisms is more subtle, and this is the main contribution of the paper. Given a strategy and an execution state, our functor needs to count the witnesses for this state within the strategy. Strategies in thin concurrent games describe non-linear behaviour explicitly, so in general each witness exists in countably many symmetric copies. The challenge is to define the right notion of witnesses, factoring out this infinity while matching the weighted relational model. Understanding how witnesses compose is particularly subtle and requires a delve into the combinatorics of witnesses and their symmetries. In its basic form, this functor connects thin concurrent games and a relational model weighted by N $\cup$ {+$\infty$}. We will additionally consider a generalised setting where both models are weighted by elements of an arbitrary continuous semiring; this covers the probabilistic case, among others. Witnesses now additionally carry a value from the semiring, and our interpretation-preserving collapse functor extends to this setting.