A recurring problem in game semantics is to enforce uniformity in strategies. Informally, a strategy is uniform when the Player's behaviour does not depend on the particular indexing of moves chosen by the Opponent. In game semantics, uniformity is used to define a resource modality !, that can be exploited for the semantics of programming languages. In this paper we give a new account of uniformity for strategies on event structures. This work is inspired by an older idea due to Melli\`es, that uniformity should be expressed as "bi-invariance" with respect to two interacting group actions. We explore the algebraic foundations of bi-invariance, adapt this idea to the language of event structures and define a general notion of uniform strategy in this context. Finally we revisit an existing approach to uniformity, and show how this arises as a special case of our constructions.
翻译:博弈语义中的一个反复出现的问题是强制策略的统一性。非形式地说,当玩家行为不依赖于对手选择的特定移动索引时,该策略是统一的。在博弈语义中,统一性用于定义资源模态!,该模态可用于编程语言的语义。本文给出了事件结构上策略统一性的新解释。这项工作受Melliès提出的一个较早想法的启发,即统一性应表示为关于两个相互作用的群作用的“双不变性”。我们探讨了双不变性的代数基础,将其思想适配到事件结构语言中,并在此背景下定义了统一策略的一般概念。最后,我们重新审视了一种现有的统一性方法,并展示了它如何作为我们构造的一个特例出现。