Concurrent game strategies characterized as street fibrations with symmetry
Concurrent Strategies as Street Fibrations
Logic in Computer Science
Summary
This paper looks at how to handle symmetry in concurrent games, which are models for computers interacting with each other. The authors identify two kinds of strategies where combining actions behaves well, each with different levels of equivalence. They show that one of these kinds matches a mathematical concept called Street fibrations, which helps explain how strategies relate to the games they come from. They also connect this understanding to another framework involving profunctors, making the study of symmetry easier.
What this means in practice
- •For concurrent system designers: Use the characterization of strategies as Street fibrations to better model and verify concurrent interactions with symmetry.
- •For programming language theorists: Apply the connection to profunctors for developing semantics of languages with concurrency and symmetry.
A theory result. No direct application yet.
Authors
Hugo Paquet, Glynn Winskel
Abstract
Concurrent games and strategies based on event structures are an established and expressive model of interactive computation. In this paper we revisit the problem of equipping this model with symmetry. Symmetry is essential for many applications, but it is also a source of mathematical complexity, not least because strategies with symmetry can be compared up to several distinct notions of equivalence. Our first contribution is a complete characterization of two classes of strategies for which composition admits an identity. For these two classes the identity laws hold, respectively, up to a "weak" and a "strong" notion of equivalence. The main result is that the weak class of strategies corresponds precisely to those inducing Street fibrations over the game. We also show how the established "thin" approach to symmetry also fits in this general framework. A second contribution is a formal connection between games and setoid-valued profunctors. This follows a long tradition of relating games and relational models, but here additionally includes a very general model of symmetries. Our characterization of strategies as Street fibrations makes the connection to profunctors significantly easier to establish.