PaperlayerView exact revision on arXiv

Source-linked AI summary

Concurrent Strategies as Street Fibrations

Hugo Paquet, Glynn Winskel

arXiv:2609.37815v1cs.LOmath.CT

TL;DR

Symmetry is important for applications of concurrent games but complicates their mathematical theory. The paper develops a model of games with symmetry, characterizes weak strategies as Street fibrations, and connects the model to setoid-valued profunctors.

  • Problem

    Adding symmetry to concurrent games is important for applications such as programming-language semantics, but it complicates the mathematical theory of strategies.

    Source: §1 · p. 1

  • Method

    The paper constructs a general model of games and strategies with symmetry and relates strategies to Street fibrations and setoid-valued pseudo-profunctors.

    Source: §1 · p. 2

  • Results

    Weak strategies are characterized as Street fibrations over a category induced by the game, and the paper establishes a formal connection to pseudo-profunctors.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The Street-fibration characterization gives weak strategies canonical status and makes their connection to setoid-valued profunctors mathematically straightforward.

    Source: §9 · p. 17

    A similar characterization of strong strategies remains open without restricting the symmetry on strategies.

    Source: §9 · p. 17

Abstract

from arXiv · show

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.

1 Introduction

Event structures support concurrent games, but adding symmetry complicates strategy composition and equivalence. The paper characterizes weak and strong strategies and connects games with symmetry to setoid-valued profunctors.

1 Introduction

  • Concurrent games model program interaction as strategies over event structures, while symmetry is needed for applications such as programming-language semantics but complicates the theory.With symmetry, composition and identities require new operations and equivalences weaker than isomorphism.Source: §1 · pp. 1–2

1.1 The problem of characterizing strategies

  • The paper gives a complete characterization of strong strategies and characterizes weak strategies as Street fibrations over a category induced by the game.Strong equivalence implies weak equivalence, so weak strategies include strong strategies.Source: §1.1 · p. 2

1.2 Strategies and profunctors

  • An oplax functor connects games and strategies with symmetry to setoid-valued pseudo-profunctors, abstracting interaction while retaining a description of symmetries.The Street-fibration characterization makes this connection especially easy to describe.Source: §1.2 · p. 2

1.3 Summary of contributions and outline of the paper

  • The paper’s stated contributions are the characterizations of weak and strong strategies and the connection to profunctors; its outline also includes a connection to thin concurrent games.The proof development covers event structures with symmetry, polarity and the Scott category, fibrations, and games and strategies.Source: §1.3 · pp. 2–3

2 Symmetry in event structures and the role of setoids

The section develops event structures with symmetry and setoid-valued homotopies, then uses them to describe synchronization and hiding. Its constructions preserve symmetry equivalences as a core part of the model.

2 Symmetry in event structures and the role of setoids

  • An event structure with symmetry equips configurations with bijections closed under identities, composition, inverses, and restriction, alongside a bisimulation condition.Maps preserve these symmetries, and homotopies between maps are unique when they exist, making each hom-category a setoid.Source: §2 · pp. 3–4
  • The configuration category uses inclusions and symmetry bijections, with each morphism factoring uniquely as a symmetry followed by an inclusion.The resulting hom-categories are groupoids with at most one morphism between any pair of maps.Source: §2 · p. 4

2.1 Synchronization via pseudo-pullbacks

  • Pseudo-pullbacks synchronize configurations through a symmetry bijection, and their partial orders must avoid deadlocks or causal loops.The 2-category of event structures with symmetry has all pseudo-pullbacks.Source: §2.1 · p. 4

2.2 Hiding

  • Hiding restricts an event structure to a subset of events; when that subset is closed under symmetry, the restriction inherits symmetry.The inherited symmetry is characterized by extending the restricted bijection to one between completed configurations.Source: §2.2 · p. 5

3 Polarity and the Scott category of configurations

Polarity distinguishes Player moves from Opponent moves, and the Scott category organizes configurations using polarity-sensitive morphisms. Its induced functor captures homotopies exactly through natural transformations.

3 Polarity and the Scott category of configurations

  • Polarity labels events as positive for Player moves or negative for Opponent moves, and the Scott category is generated by positive inclusions and negative reverse inclusions.Its morphisms are partial functions between configurations.Source: §3 · p. 5
  • The Scott category itself is not new; this paper’s novelty is using it to characterize strategies, simplifying and generalizing earlier results.The functorial construction extends to maps and homotopies of event structures with symmetry and polarity.Source: §3 · p. 6
  • The Scott-category construction is locally full and faithful: a natural transformation C(f) ⇒ C(g) exists exactly when f and g are homotopic.When it exists, there is exactly one such natural transformation.Source: §3 · p. 6

4 Fibrations, Street fibrations, and Setoid-valued profunctors

The section relates maps of event structures to fibrations and setoid-valued profunctors. For induced Scott-category functors, fibres are setoids, and essentially unique lifts characterize fibrations with setoid fibres.

4 Fibrations, Street fibrations, and Setoid-valued profunctors

  • A map of event structures with symmetry and polarity induces a Scott-category functor whose fibres and essential fibres are setoids.The section’s goal is to study such maps through the fibrational properties of those induced functors.Source: §4 · p. 6

4.1 Rudiments of fibrations and setoids

  • Essentially unique lifts characterize fibrations whose fibres are setoids; the pseudo-lift version characterizes Street fibrations with setoid essential fibres.The result is stated as an equivalence in Lemma 4.5.Source: §4.1 · p. 7

4.2 A 3-dimensional profunctor model

  • Setoid-valued pseudo-profunctors retain the equivalence information needed to model event-structure symmetries, within a 3-dimensional structure whose 3-cells encode equivalence between 2-cells.The profunctor tricategory’s 3-dimensional structure is simple enough that no three-dimensional coherence axioms need verification.Source: §4.2 · p. 8

5 Games and strategies with symmetry

The section develops games and strategies with symmetry, including weak strategies whose composition laws hold up to weak equivalence. It defines composition and copycat identities, then organizes the strategies into a tricategory.

5 Games and strategies with symmetry

  • The model extends with weak strategies, whose composition laws hold only up to weak equivalence.The section defines composition and identity strategies for games and strategies as event structures with symmetry.Source: §5 · p. 9

5.1 Games and pre-strategies

  • A pre-strategy maps an event structure with symmetry and polarity to a game; weak equivalence allows non-strict maps, unlike strong equivalence.In the example, (b) and (d) are strongly equivalent to each other and weakly equivalent to (c).Source: §5.1 · p. 9

5.2 The composition of pre-strategies

  • Composition forms an interaction by homotopy pullback, then hides the shared game’s events; it is associative up to equivalence and preserves weak and strong equivalences.The shared events are those of B in a composition from A to B and B to C.Source: §5.2 · p. 10

5.3 Copycat

  • Copycat supplies the identity: its configurations correspond to the twisted arrow category of a game’s configuration category, and composition with it admits natural strict maps from each pre-strategy.The copycat map corresponds to the canonical projection from the twisted arrow category to the product of the opposite and original configuration categories.Source: §5.3 · p. 10

5.4 Strategies

  • A weak strategy is a pre-strategy whose canonical maps to and from copycat composites are weak equivalences; strong strategies require strong equivalences.Strategies are defined as the pre-strategies for which composition works well, and are organized into a tricategory where copycat is an identity up to equivalence; the strong submodel is the ∼-bicategory of.Source: §5.4 · pp. 10–11

6 Characterizations of weak strategies and strong strategies

This section characterizes strong and weak strategies using lifting properties and a collapse construction. Its central result identifies weak strategies with Street fibrations.

6.1 Lifting properties for pre-strategies

  • Innocence lifts positive inclusions uniquely, receptivity lifts negative inclusions uniquely, while pseudo-receptivity allows essentially unique pseudo-lifts.Source: §6.1 · p. 11
  • Saturation freely adds symmetry lifts, and every pre-strategy is weakly equivalent to its saturation; an isofibration alone does not ensure saturation.Source: §6.1 · p. 12
  • Saturated, innocent, strongly receptive pre-strategies suffice for strong strategies, but these conditions are not necessary.Source: §6.1 · p. 13

6.2 The collapse of a pre-strategy

  • For innocent, pseudo-receptive pre-strategies, collapse yields a strongly equivalent pre-strategy with unique negative-inclusion lifts; with receptivity existence, the result is receptive.Source: §6.2 · p. 13

6.3 A characterization of strong strategies

  • A pre-strategy is a strong strategy if and only if it is saturated, innocent, and pseudo-receptive.Source: §6.3 · p. 14

6.4 A characterization of weak strategies

  • Weak strategies are exactly innocent, pseudo-receptive pre-strategies, equivalently those whose induced configuration-category map is a Street fibration.Source: §6.4 · p. 14

7 Strategies as Setoid-profunctors

The paper maps strategies to setoid-valued profunctors through their Street-fibration structure. This yields an oplax functor because the profunctor view forgets causal structure relevant to composition.

7 Strategies as Setoid-profunctors

  • Each strategy becomes a setoid-valued profunctor by assigning configurations the essential fibre over their combined configuration.The object assignment sends a game A to its Scott category C(A).Source: §7 · p. 15
  • The construction gives an oplax functor from Strat to Setoid-Prof, with a non-invertible comparison from the profunctor of a composite to the composite of profunctors.The comparison is non-invertible because viewing strategies as profunctors forgets causal structure that affects composition.Source: §7 · p. 15
  • Copycat configurations correspond to the identity profunctor, while composite-strategy configurations project to matching configurations of the component strategies.These facts provide the identity and composition comparisons for the oplax functor.Source: §7 · p. 16

8 Thin games

Thin concurrent games and strategies embed into the broader Strat model, linking the thin and saturated approaches to symmetry. Their stronger axioms simplify identities and composition, while thin-game structure is essentially unique over a fixed underlying event structure.

8 Thin games

  • The pseudo-functor J embeds the bicategory Thin into Strat, placing thin games and strategies within the broader model of symmetry.The embedding challenges treating thin and saturated approaches as separate; the paper presents them as coexisting in a general framework.Source: §8 · pp. 16–17
  • A thin game equips an event structure with positive and negative symmetry subfamilies that satisfy separate closure conditions and intersect only in identity bijections.Source: §8 · p. 16
  • Thin strategies are innocent and strongly receptive, and positive-symmetry moves must be identities.Source: §8 · p. 16
  • Stronger thin-game axioms allow simpler identities and composition, with associativity and unit laws holding up to isomorphism; thin composition uses ordinary pullbacks.Thin copycat is equivalent to the general copycat, but is not defined for arbitrary games; ordinary-pullback composition is likewise not defined for arbitrary non-thin strategies.Source: §8 · p. 16
  • Thin games with the same underlying event structure, symmetry, and polarity are internally equivalent in Thin, so the positive and negative subfamilies are essentially unique up to that equivalence.The thin copycat can serve as strategies in both directions between the games.Source: §8 · p. 17
  • J is identity on morphisms and higher cells, but its status as a higher-categorical embedding remains informal because reflection of equivalences is unclear.Source: §8 · p. 17

9 Conclusion

The conclusion presents a general model of concurrent games with symmetry and characterizes weak strategies as Street fibrations. It identifies strong-strategy characterization as an open problem.

9 Conclusion

  • The model brings together existing approaches to symmetry and characterizes weak strategies as Street fibrations, supporting a straightforward connection with setoid-valued profunctors.Source: §9 · p. 17
  • A similar characterization for strong strategies remains open without restricting strategy symmetries, since Grothendieck fibration structure is not sufficient.All strong strategies define Grothendieck fibrations, but the converse fails.Source: §9 · p. 17
  • The authors identify formalizing concurrent games in a type theory or proof assistant that supports reasoning up to homotopy as future work.Source: §9 · p. 17

A Stable families, event structures, and symmetry

The appendix recalls stable families as a foundation for event structures and symmetry, then uses them to describe an adjunction and an alternative span-based presentation of symmetry.

A Stable families, event structures, and symmetry

B.1 Preliminary terminology and notation

This section states a condition on negative events and introduces notation for polarity-restricted configurations and event down-closures.

B.1 Preliminary terminology and notation

  • A pre-strategy is ⊟-innocent when it preserves the causal order of negative events in the game.Pseudo-receptivity implies ⊟-innocence, though the results below typically rely only on innocence.Source: §B.1 · p. 21
  • For a configuration, x⊞ and x⊟ denote its positive and negative events; symmetry bijections are restricted correspondingly.These restricted bijections preserve polarity.Source: §B.1 · p. 21
  • The down-closure [e] is the smallest configuration containing event e, and [Z] is the configuration generated by a consistent subset Z.Source: §B.1 · p. 21

B.2 The collapse construction

The collapse construction turns a strategy into a collapsed pre-strategy by forming configurations from positive events and their mapped negative events. Under pseudo-receptivity, the resulting strategy is strongly equivalent to the original.

B.2 The collapse construction

  • For a ⊟-innocent pre-strategy, the sets x⊞ ∪ σx⊟ form a stable family and determine the event structure collapse(S).The construction requires only ⊟-innocence for this stable-family property.Source: §B.2 · pp. 21, 23
  • The map g sends s to the prime configuration [s]⊞ ∪ σ[s]⊟, while collapse(σ) sends that prime to σ(s).Their composite is σ.Source: §B.2 · pp. 22, 25
  • Under ⊟-innocence, a compatible subconfiguration in the game has a unique configuration preimage contained in the given strategy configuration.The proof uses innocence to show the selected events are down-closed.Source: §B.2 · p. 22
  • With pseudo-receptivity, the induced symmetry family is an isomorphism family, and the collapse's prime configurations are exactly those generated by events of S.The lemma also establishes the stated map properties of collapse(σ) and g.Source: §B.2 · p. 22
  • The collapse map distinguishes compatible configurations, while equal images under g imply that the original configurations are symmetric.Source: §B.2 · p. 22
  • For any pseudo-receptive pre-strategy, the map g gives a strong equivalence between the strategy and its collapse.The collapse map composed with g recovers the original strategy.Source: §B.2 · pp. 22, 25

B.3 Universality of the collapse

The collapse construction has a universal mapping property: maps into collapsed pre-strategies factor uniquely through it. Consequently, collapse is left adjoint to inclusion of collapsed pre-strategies.

B.3 Universality of the collapse

  • For a map from an innocent, pseudo-receptive pre-strategy to a collapsed one, there is a unique map from its collapse that factors the original map.Source: §B.3 · pp. 26–27
  • Among innocent, pseudo-receptive pre-strategies, collapse is left adjoint to inclusion of the collapsed pre-strategies.Source: §B.3 · p. 27
  • Finite configurations of the induced symmetry structure correspond order-isomorphically to the isomorphism family of S.The correspondence sends z to the bijection from l_S z to r_S z.Source: §B.3 · p. 27
Loading 2609.37815v1…