Coalgebraic Multigames

Abstract

Coalgebraic games have been recently introduced as a generalization of Conway games and other notions of games arising in different contexts. Using coalgebraic methods, games can be viewed as elements of a final coalgebra for a suitable functor, and operations on games can be analyzed in terms of (generalized) coiteration schemata. Coalgebraic games are sequential in nature, i.e. at each step either the Left (L) or the Right (R) player moves (global polarization), moreover only a single move can be performed at each step. Recently, in the context of Game Semantics, concurrent games have been introduced, where global polarization is abandoned, and multiple moves are allowed. In this paper, we introduce coalgebraic multigames, which are situated half-way between traditional sequential games and concurrent games: global polarization is still present, however multiple moves are possible at each step, i.e. a team of L/R players moves in parallel. Coalgebraic operations, such as sum and negation, can be naturally defined on multigames. Interestingly, sum on coalgebraic multigames turns out to be related to Conway’s selective sum on games, rather than the usual (sequential) disjoint sum. Selective sum has a parallel nature, in that at each step the current player performs a move in at least one component of the sum game, while on disjoint sum the current player performs a move in exactly one component at each step. A monoidal closed category of coalgebraic multigames in the vein of a Joyal category of Conway games is then built. The relationship between coalgebraic multigames and games is then formalized via an equivalence of the multigame category and a monoidal closed category of coalgebraic games where tensor is selective sum.

Work supported by MIUR PRIN Project CINA 2010LHT4KM.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In [14], coalgebraic games have been introduced as a generalization of Conway games [11] to possibly non-terminating games. Coalgebras offer an elementary but sufficiently abstract framework, where games are represented as elements of a final coalgebra for a suitable functor, by abstracting away superficial features of positions, and operations are smoothly defined as final morphisms via (generalized) coiteration schemata. Coalgebraic games have been further studied and generalized in [15–18]. In particular, in [17], coalgebraic games have been shown to subsume also games arising in the context of Game Semantics. In [3] a similar notion of coalgebraic game has been used to model games arising in Economics (see also [23, 24]).

Coalgebraic games are 2-player games of perfect information, the two players being Left (L) and Right (R). A game is identified with its initial position. At any position, there are moves for L and R taking to new positions of the game. Contrary to other approaches in the literature, where games are defined as graphs, we view possibly non-wellfounded games as points of a final coalgebra of graphs, i.e. minimal graphs w.r.t. bisimilarity. This coalgebraic representation is more in the spirit of Conway’s original presentation, and it is motivated by the fact that the existence of winning/non-losing strategies is invariant w.r.t. graph bisimilarity.

Coalgebraic games are sequential in nature, i.e. at each step either L or R moves (global polarization), moreover only a single move can be performed at each step. Recently, in the context of Game Semantics, concurrent games have been introduced [2, 10, 13, 30], where global polarization is abandoned, and multiple moves are allowed.

In this paper, we introduce coalgebraic multigames, which are situated half-way between traditional sequential games and concurrent games: global polarization is still present, however multiple moves are possible at each step, i.e. a team of L/R players moves in parallel. Coalgebraic operations, such as sum and negation, can be naturally defined on multigames via (generalized) coiteration schemata.

The notion of coalgebraic multigame introduced in the present paper is inspired by that of multigame recently defined by the same authors in [19], in the context of Game Semantics. The approach in [19] is slightly different, in that (multi)games are defined via trees of positions, rather than coalgebraically as sets/minimal graphs.

The main difference between coalgebraic multigames and games lies in the fact that in the sum of games, at each step, the current player can move in exactly one component, while in the multigame sum, by exploiting the parallel nature of multigames, the current player can perform a multimove consisting of atomic moves on both components. Sum on games amounts to Conway’s disjoint sum, which corresponds to interleaving semantics and standard tensor product in Game Semantics (see e.g. [1, 20]), while multigame sum is related to Conway’s selective sum, a form of parallel sum on games, where the current player can possibly move in both components.

We formalize the relationship between coalgebraic games and multigames in categorical terms. In particular, inspired by Joyal’s categorical construction of Conway games [22], we build a symmetric monoidal closed category of coalgebraic multigames, where tensor is multigame sum. Namely, in [22], Joyal showed how to endow (well-founded) Conway games and winning strategies with a structure of compact closed category. This construction is based on the disjunctive sum of games, which induces a tensor product, and, in combination with negation, yields linear implication. Recently, the above categorical construction has been generalized to non-wellfounded games with disjoint or selective sum [16–18], while, in the context of Linear Logic and Semantics, various categories of possibly non-wellfounded Conway games have been introduced and studied in [19, 25, 26, 28].

In the present paper, we build a category of coalgebraic multigames and strategies in the line of the above constructions. Moreover, we show that this is equivalent to a category of coalgebraic games with a parallel tensor product inspired by Conway’ s selective sum. In particular, we carry out these categorical constructions in the context of polarized (multi)games, i.e. (multi)games where each position is marked as L or R, that is only L or R can move from that position, R starts, and L/R positions strictly alternate. Polarized games typically arise in Game Semantics, see e.g. [1, 19, 20].

Technically, the main difficulty in defining the above categories of (multi)games with parallel tensor product lies in the definition of strategy composition, which is not a straightforward adaptation of usual composition, but it requires a non-standard parallel application of strategies.

Our categorical constructions are related in particular to those carried out in [19] in the context of Game Semantics. In [19], the usefulness of multigames for modeling parallel languages is shown by providing a (universal) model of a simple parallel language, i.e. unary PCF with parallel or.

The interest of coalgebraic (multi)games is manifold. Multigames help in clarifying/factorizing the steps taking from sequential games (with global polarization and single moves) to concurrent games (no global polarization, multiple moves), offering a model of parallelism with a low level of complexity but still of a set-theoretic nature, compared to more complex concurrent games. Notably, the coalgebraic approach, both in the game and multigame version, appears significantly simpler than the traditional Game Semantics approach, where definitions of games and strategies require complex additional structures, such as equivalences on plays and strategies in the style of [1], or pointers in the arena style [20]. Such extra structure is not needed in the coalgebraic framework.

Related Work. Coalgebraic methods for modeling games have been used also in [5], where the notion of membership game has been introduced. This corresponds to a subclass of our coalgebraic games, where at any position L and R have the same moves, and all infinite plays are deemed winning for player II (the player who does not start). However, no operations on games are considered in that setting. In the literature, various notions of bisimilarity equivalences have been considered on games, see e.g. [6, 29]. But, contrary to our approach, such games are defined as graphs of positions, and equivalences on graphs, such as trace equivalences or various bisimilarities are considered. By defining games as the elements of a final coalgebra, we directly work up to bisimilarity of game graphs.

Summary. In Sect. 2, we introduce the notions of coalgebraic multigame, play and strategy. In Sect. 3, we define operations on the final coalgebra of multigames via suitable (generalized) coiteration schemata. In Sect. 4, we build a monoidal closed category of polarized coalgebraic multigames and strategies, where tensor is sum. In Sect. 5, the relationship between coalgebraic multigames and games is expressed in categorical terms via an equivalence between the category of multigames and a monoidal closed category of coalgebraic games where tensor is selective sum. Conclusions and directions for future work appear in Sect. 6.

We assume the reader familiar with basic notions of coalgebras, see [21], and basic categorical definitions.

2 Coalgebraic Multigames and Strategies

In this section, we introduce the definitions of coalgebraic multigame, play, and strategy.

We consider a general notion of 2-player multigame of perfect information, where the two players are called Left (L) and Right (R). On a multigame, at each step, players can perform a multimove, i.e. a non-empty finite set of atomic moves. A multigame $X$ is identified with its initial position; at any position, there are (multi)moves for L and R, taking to new positions of the game. By abstracting superficial features of positions, multigames can be viewed as elements of the final coalgebra for the functor $F_{\mathcal{M }_\mathcal{A}}(A) = {\mathcal P}_{<\kappa }(\mathcal{M}_\mathcal{A} \times A)$, where $\mathcal{A}$ is a set of atomic moves, each atomic move is marked with the name of the player who performs the move, ${\mathcal M}_{\mathcal A}$ is the set of multimoves, i.e. the finite powerset of atomic moves with the same polarity, and ${\mathcal P}_{<\kappa }$ is the set of all subsets of cardinality $<\kappa$, where $\kappa$ can be $\omega$ if only games with finitely many moves are considered, or it can be an inaccessible cardinal if we are interested in more general games. The coalgebra structure captures, for any position, the moves of the players and the corresponding next positions.

We work in the category $Set ^*$ of sets belonging to a universe satisfying the Antifoundation Axiom, see [4, 12], where the objects are the sets with hereditary cardinal less than $\kappa$, and whose morphisms are the functions with hereditary cardinal less than $\kappa$ ¹. Of course, we could work in the category $Set$ of well-founded sets, but we prefer to use $Set ^*$ so as to be able to use identities, i.e. extentional equalities in formal set theory, rather than isomorphisms in some naive set theory. Formally, we define:

Definition 1

(Coalgebraic Multigames)  

• Let $\mathcal{A}$ be a set of atoms with functions:

  (i) $\mu : \mathcal{A} \rightarrow \mathcal{N}$ yielding the name of the move (for a set $\mathcal{N}$ of names),

  (ii) $\lambda :\mathcal{A} \rightarrow \{ L,R\}$ yielding the player who has moved.

  We assume that $\mathcal{A}$ is closed under complementation, i.e. $a\in \mathcal{A}\ \Rightarrow \ \overline{a}\in \mathcal{A}$, where $\mu \overline{a} = \mu a$ and $\lambda \overline{a} =\overline{\lambda a}$, with $\overline{R}=L$ and $\overline{L}=R$.

• Let $\mathcal{M}_\mathcal{A}$ be the powerset of all finite sets of atomic moves with the same polarity, i.e.

  $$\begin{aligned} \mathcal{M}_\mathcal{A}= \{ \alpha \in \mathcal{P}_f ({\mathcal A}) \ | \ \forall a,a' \in \alpha .\ \lambda a = \lambda a'\} \ . \end{aligned}$$

• Let $F_{\mathcal{M}_\mathcal{A} }: \text{ Set }^* \rightarrow \text{ Set }^*$ be the functor defined by

  $$\begin{aligned} F_{\mathcal{M}_\mathcal{A} } (A) = {\mathcal P}_{<\kappa }(\mathcal{M}_\mathcal{A} \times A) \end{aligned}$$

  with the usual definition on morphisms, and let $(\mathbf{M}_\mathcal{A} , id )$ be the final $F_{\mathcal{M}_\mathcal{A} }$-coalgebra².

A coalgebraic multigame is an element $X$ of the carrier $\mathbf{M}_\mathcal{A}$ of the final coalgebra.

The elements of the final coalgebra $\mathbf{M}_\mathcal{A}$ are the minimal graphs up to bisimilarity.

Clearly, every multigame can be viewed as a game whose moves are the multimoves. However, as we will see, multigame sum (as well as other constructions) is not preserved under this mapping.

We call player I the player who starts the multigame (who can be L or R in general), and player II the other. Once a player has moved on a multigame $X$, this leads to a new multigame/position $X'$. We define the plays on $X$ as the sequences of pairs move-position from $X$; moves in a play are alternating:

Definition 2

(Plays). A play on a coalgebraic game $X_0$ is a possibly empty finite or infinite sequence of pairs in $\mathcal{M}_\mathcal{A} \times \mathbf{M}_ \mathcal{A}$, $s= \langle \alpha _1, X_1\rangle \ldots$ such that

$$ \forall n> 0.\ (\langle \alpha _{n}, X_{n}\rangle \in X_{n-1} \ \& \ \lambda \alpha _{n+1} = \overline{\lambda \alpha _{n}} ) \ .$$

We denote by $Play _X$ the set of plays on $X$ and by $FPlay _X$ the set of finite plays.

Here we focus on a general notion of (deterministic) partial strategy. Formally, strategies in our framework are partial functions on finite plays ending with a position where the player is next to move, and yielding (if any) a pair in $\mathcal{M}_\mathcal{A} \times \mathbf{M}_\mathcal{A}$, consisting of “a move of the given player together with a next position” on the game $X$. In what follows, we denote by

• $FPlay ^{LI}_X$ ($FPlay ^{RI}_X$) the set of possibly empty finite plays on the game $X$ on which L (R) acts as player I, and ending with a position where the turn is L (R), i.e. $s= \epsilon$ or $s= \langle \alpha _1, X_1 \rangle \ldots \langle \alpha _n, X_n\rangle$, where $\lambda \alpha _1= L$ ($\lambda \alpha _1= R$) and $\lambda \alpha _n= R$ ($\lambda \alpha _n =L$).

• $FPlay ^{LII}_X$ ($FPlay ^{RII}_X$) the set of finite plays on the game $X$ on which L (R) acts as player II, and ending with a position where R (L) was last to move, i.e. $s= \langle \alpha _1, X_1 \rangle \ldots \langle \alpha _n, X_n\rangle$, where $\lambda \alpha _1 =R$ ($\lambda \alpha _1 =L$) and $\lambda \alpha _n =R$ ($\lambda \alpha _n =L$).

Formally, we define:

Definition 3

(Strategies). Let $X$ be a coalgebraic multigame. A strategy $\sigma$ for LI (i.e. L acting as player I) is a partial function $\sigma : FPlay ^{LI}_X \rightarrow \mathcal{M}_\mathcal{A} \times \mathbf{M}_\mathcal{A}$ such that, for any $s\in FPlay ^{LI}_X$,

$$ \begin{aligned} \sigma (s)= \langle \alpha , X' \rangle \ \Longrightarrow \ \lambda \alpha =L \ \& \ s\langle \alpha , X'\rangle \in FPlay _X \ . \end{aligned}$$

Similarly, one can define strategies for players LII, RI, RII.

For any player LI, LII, RI, RII, we define the opponent player as RII, RI, LII, LI, respectively.

A counterstrategy of a strategy for a player in $\{$LI,LII,RI,RII$\}$ is a strategy for the opponent player.

We are interested in studying the interactions of a strategy for a given player with the (counter)strategies of the opponent player. When a player plays on a game according to a strategy $\sigma$, against an opponent player who follows a (counter)strategy $\sigma '$, a play arises. Formally, we define:

Definition 4

(Product of Strategies). Let $X$ be a coalgebraic multigame.

(i) Let $s$ be a play on $X$, and $\sigma$ a strategy for a player in $\{$LI,LII,RI,RII$\}$. Then $s$ is coherent with $\sigma$ if, for any proper prefix $s'$ of $s$, ending with a position where the player is next to move, $\sigma (s') = \langle \alpha , X'\rangle \ \Longrightarrow \ s'\langle \alpha , X'\rangle \text{ is } \text{ a } \text{ prefix } \text{ of } s.$

(ii) Given a strategy $\sigma$ on $X$ and a counterstrategy $\sigma '$, we define the product of $\sigma$ and $\sigma '$, $\sigma *\sigma '$, as the unique play coherent with both $\sigma$ and $\sigma '$.

Notice that a play arising from the product of strategies is alternating.

We call well-founded multigames those multigames which correspond to well-founded sets as elements of the final coalgebra $\mathbf{M}_\mathcal{A}$, and non-wellfounded multigames the non-wellfounded sets in $\mathbf{M}_\mathcal{A}$. Clearly, strategies on well-founded multigames generate only finite plays, while strategies on non-wellfounded multigames can generate infinite plays.

A special subclass of multigames on which we focus on in the sequel is that of polarized multigames. Such multigames have the following special structure: R starts, at any non-ending position only moves either for R or for L are available and along any path in the game graph R/L moves strictly alternate. Polarized multigames play a central rôle in the construction of our categories of multigames. Such games arise in traditional Game Semantics of Linear Logic and Programming Languages, see e.g. [1, 20].

3 Multigame Operations

In this section, we show how to define various operations on multigames, including sum, negation, linear implication, and infinite sum. The crucial operation on multigames is sum, which, as we will see, is related to Conway’s selective sum on traditional games, and it will give rise to a tensor product on the category of multigames defined in Sect. 4 below. In our coalgebraic framework, operations can be conveniently defined via final morphisms, using (some generalizations of) the standard coiteration schema. Before defining multigame operations, we start by recalling a useful generalized coiteration schema introduced in [9].

3.1 Guarded Coiteration Schema

Here we recall a generalized coiteration schema based on $\lambda$-bialgebras, for $\lambda$ a distributive law, which will be used in the sequel for defining multigame operations.

Definition 5

(Guarded Coiteration). Let $(\varOmega , \alpha _{\varOmega })$ be a final coalgebra for a functor $F: Set ^* \rightarrow Set ^*$, and let $A$ be a set. A guarded specification for a morphism $h: A \rightarrow \varOmega$ is of the form:

$$\begin{aligned} \alpha _{\varOmega } \circ h = F( g \circ G(h)) \circ \delta _A \ , \end{aligned}$$

(1)

where $\delta _A : A \rightarrow F(G A)$ and $g: G(\varOmega ) \rightarrow \varOmega$ are given, $g$ is the guard.

I.e. $h$ makes the following diagram commutes:

Under suitable conditions, the above schema admits a unique solution, see [9] for more details. In particular, a functor $G: Set ^* \rightarrow Set ^*$ is required and a generalized distributive law $\lambda : GF \mathop {\rightarrow }\limits ^{\cdot } FG$ for which $(\varOmega , g, \alpha _{\varOmega })$ is a $\lambda$-bialgebra.

3.2 Operations on Multigames

Sum. In the context of multigames, the following notion of sum arises naturally. On the sum multigame, at each step, the next player selects either one (non-ended) or both component multigames, and makes a legal move in each of the selected components, while the component which has not been chosen (if any) remains unchanged.

Definition 6

(Sum). The sum of two multigames $\triangledown : \mathbf{M}_{\mathcal A} \times \mathbf{M}_{\mathcal A} \longrightarrow \mathbf{M}_{\mathcal A}$ is defined by:

$$ \begin{aligned} X\triangledown Y = \{ \langle \alpha ', X' \triangledown Y\rangle \ | \ \langle \alpha , X'&\rangle \in X\}\ \cup \ \{ \langle \beta ', X\triangledown Y'\rangle \ |\ \langle \beta ,Y'\rangle \in Y \}\ \cup \ \\&\{ \langle \alpha + \beta , X' \triangledown Y'\rangle \ | \ \langle \alpha ,X'\rangle \in X\ \& \ \langle \beta ,Y'\rangle \in Y \}\ , \end{aligned}$$

where $\alpha ', \beta '$ are the sets obtained from $\alpha , \beta$ by adding tags to atomic moves.

The above definition corresponds to a standard coiteration schema, namely the function $\triangledown$ is the final morphism from the coalgebra $(\mathbf{M}_{\mathcal A} \times \mathbf{M}_{\mathcal A}, f_{\triangledown })$ to the final coalgebra $(\mathbf{M}_{\mathcal A}, \text{ id })$, where the coalgebra morphism $f_{\triangledown }: \mathbf{M}_{\mathcal A} \times \mathbf{M}_{\mathcal A} \longrightarrow F_{\mathcal{M}_\mathcal{A}} (\mathbf{M}_{\mathcal A} \times \mathbf{M}_{\mathcal A})$ is defined by:

$$ \begin{aligned} f_{\triangledown } (X,Y)= \{ \langle \alpha ',\langle X' , Y\rangle \rangle&\ | \ \langle \alpha ,X'\rangle \in X\}\ \cup \ \{\langle \beta ',\langle X,Y'\rangle \rangle \ |\ \langle \beta ,Y'\rangle \in Y\}\ \cup \ \\&\{ \langle \alpha + \beta ,\langle X',Y'\rangle \rangle \ |\ \langle \alpha ,X'\rangle \in X \ \& \ \langle \beta ,Y'\rangle \in Y\} \end{aligned}$$

Remark. Notice that, in composing multigames via the sum, we keep track of the moves coming from the two different components by using tags. This definition is different from original Conway’s sum on games, which is a purely set-theoretic extensional operation, possibly allowing for identifications between the two components. Our sum definition, where we keep track of the component in which each move has been performed, is necessary e.g. for extending sum to a bifunctor in categories of multigames and strategies such as that defined in Sect.  4 below, or even to define strategy composition in this category. Nonetheless, notice that, from a determinacy point of view, this sum and Conway’s original one behave in the same way, i.e. they are equivalent w.r.t. the existence of (winning) strategies.

Negation. The negation is a unary multigame operation, which allows us to build a new game, where the rôles of L and R are exchanged. For $\alpha \in \mathcal{M}_\mathcal{A}$, we define

$$\begin{aligned} \overline{\alpha } = \{ \overline{a}\ |\ a \in \alpha \} \ . \end{aligned}$$

The definition of multigame negation is as follows:

Definition 7

(Negation). The negation ${\ }^{-}: \mathbf{M}_{\mathcal A} \longrightarrow \mathbf{M}_{\mathcal A}$ is defined by:

$$\begin{aligned} \overline{X} = \{ \langle \overline{\alpha }, \overline{X'}\rangle \ | \ \langle \alpha ,X'\rangle \in X \} \ . \end{aligned}$$

Also negation is an instance of the coiteration schema. It is the final morphism from the coalgebra $(\mathbf{M}_{\mathcal A} , f_{-})$ to the final coalgebra $(\mathbf{M}_{\mathcal A}, \text{ id })$, where the coalgebra morphism $f_{-}: \mathbf{M}_{\mathcal A} \longrightarrow F_{\mathcal{M}_\mathcal{A} }(\mathbf{M}_{\mathcal A})$ is defined by:

$$\begin{aligned} f_{-} (X)= \{ \langle \overline{\alpha },X'\rangle \ | \ \langle \alpha ,X'\rangle \in X\} \ . \end{aligned}$$

Linear Implication. Using the above notions of sum and negation, we can now define the following linear implication, which corresponds to the notion of linear implication in Linear Logic:

Definition 8

(Linear Implication). The linear implication of the multigames $X,Y$, $X\multimap Y$, is defined by

$$ X\multimap Y = \overline{X} \triangledown Y\ .$$

Infinite Sum. We can enrich multigames with a further interesting unary coalgebraic operation, $\triangledown ^{\infty }$, an infinite sum: on the game $\triangledown ^{\infty } x$, at each step, the current player can perform a move in finitely many of the infinite components of $X$. Our infinite sum is related to the exponential modality defined on a category of games in [28], and it will induce a comonad on the categories of multigames that we will consider in Sect. 4.

Definition 9

(Infinite Sum). We define the infinite sum $\triangledown ^{\infty }: \mathbf{M}_\mathcal{A} \longrightarrow \mathbf{M}_\mathcal{A}$ by:

$$ \begin{aligned} \triangledown ^{\infty } X=\{ \langle \alpha _1 + \ldots + \alpha _n, X'_{1} \triangledown&\ldots \triangledown X'_{n} \triangledown (\triangledown ^{\infty } X)\rangle \ | \ n\ge 1\ \& \ \\&\langle \alpha _1, X'_{1}\rangle , \ldots , \langle \alpha _n, X'_{n}\rangle \in X \ \& \ \lambda \alpha _1 = \ldots =\lambda \alpha _n \} \ . \end{aligned}$$

The above specification defines a unique function $\triangledown ^{\infty }$, since it is an instance of the guarded coiteration of Definition 5 above, where

• the functor $G: Set ^* \rightarrow Set ^*$ is defined by

  $$\begin{aligned} G(A) = \coprod _{n\ge 1} (\mathbf{M}_\mathcal{A}^n \times A) \end{aligned}$$

• the guard $g: G(\mathbf{M}_\mathcal{A})\longrightarrow \mathbf{M}_\mathcal{A}$ is defined by

  $$\begin{aligned} g(X_1, \ldots , X_{n+1}) = X_1 \triangledown \ldots \triangledown X_{n+1} \end{aligned}$$

• the function $\delta _{\mathbf{M}_\mathcal{A}}: \mathbf{M}_\mathcal{A} \rightarrow \mathcal{P}_{<\kappa } (\mathcal{M}_\mathcal{A} \times \coprod _{n\ge 1} (\mathbf{M}_\mathcal{A}^n \times \mathbf{M}_\mathcal{A} ))$ is defined by

  $$ \begin{aligned} \delta _{\mathbf{M}_\mathcal{A}}(X)= \{ (\alpha _1 + \ldots + \alpha _n, X'_1, \ldots , X'_n, X) \ |&\ n\ge 1 \ \& \ \lambda \alpha _1 = \ldots =\lambda \alpha _n \ \& \\&\ \ (\alpha _1, X'_{1} ), \ldots , (\alpha _n, X'_{n} )\in X \} \end{aligned}$$

• $(\mathbf{M}_\mathcal{A}, g, id )$ is a $\lambda$-bialgebra for $\lambda : GF \mathop {\rightarrow }\limits ^{\cdot } FG$ distributive law defined by

  $$ \lambda _A: \coprod _{n\ge 1} (\mathbf{M}_\mathcal{A}^n \times \mathcal{P}_{<\kappa } (\mathcal{M}_\mathcal{A} \times A)) \rightarrow \mathcal{P}_{<\kappa } (\mathcal{M}_\mathcal{A} \times \coprod _{n\ge 1} (\mathbf{M}_\mathcal{A}^n \times A)) $$
  $$ \begin{aligned} \lambda _A (X_1, \ldots , X_{n+1} ) = \{ (\alpha _1 + \ldots + \alpha _k ,&X'_1, \ldots , X'_{n+1} ) \ | \ k\ge 1 \ \& \ \\ \langle \alpha _1, X'_{i_1} \rangle \in X_{i_1}, \ldots ,&\langle \alpha _k, X'_{i_k} \rangle \in X_{i_k} \ \& \ 1\le i_1, \ldots , i_k \le n \ \& \ \\&\forall j\in \{ 1, \ldots , n\} \setminus \{ i_1, \ldots , i_k \}. \ X'_j = X_j \} \ . \end{aligned}$$

3.3 Operations on Polarized Multigames

Notice that polarized multigames are not closed under the operations defined above. However, one can define corresponding sums and linear implications on polarized multigames, simply by “pruning” the graphs of the resulting multigames. A similar construction has been considered also in [18], in the case of games. In our setting, the pruning operation of a multigame into a polarized one can be defined as a coalgebraic operation, using a definition by mutual recursion:

Definition 10

(Pruning). Let $(\ )_{+}, (\ )_{-}: \mathbf{M}_{\mathcal A} \longrightarrow \mathbf{M}_{\mathcal A}$ be the mutually recursive functions defined as:

$$ {\left\{ \begin{array}{ll} (X)_{+} =\{ \langle \alpha , (X')_{-} \rangle \ |\ \langle \alpha , X'\rangle \in X \ \& \ \lambda \alpha =L \} \\ (X)_{-} =\{ \langle \alpha , (X')_{+} \rangle \ |\ \langle \alpha , X'\rangle \in X \ \& \ \lambda \alpha = R\} \ . \end{array}\right. }\ $$

We define the pruning operation as $(\ )_{-}$.

Once we have the pruning operation, we can define polarized sums and linear implication:

Definition 11

(Polarized Operations). Let $X,Y$ be polarized multigames. We define:

• the polarized sum as the multigame $({X \triangledown {Y}})_{-}$;

• the polarized linear implication as the multigame $(X \multimap Y)_{-}$;

• the polarized infinite sum as the multigame $(\triangledown ^{\infty } X)_{-}$.

In the following, by abuse of notation, we will use the same symbols for polarized operations and the corresponding operations on all multigames.

4 Categories of Multigames and Strategies

We define a monoidal closed category ${\mathcal Y}_{\mathbf{M}_\mathcal{A}}$, whose objects are polarized multigames and whose morphisms are strategies. We work with polarized multigames, since the whole class of multigames fails to give a category, because of lack of identities, as we will see.

The main difficulty in defining this category is the definition of composition, which is based on a non-standard parallel composition of strategies. The difficulty arises from the fact that a move in a strategy between $X$ and $Y$ can include atomic moves on both $X$ and $Y$.

A Monoidal Closed Category of Multigames. Let ${\mathcal Y}_{\mathbf{M}_{\mathcal {A}}}$ be the category defined by:

Objects: polarized multigames.

Morphisms: a morphism between multigames $X$ and $Y$, $\sigma : X \multimap Y$, is a strategy for LII on $X \multimap Y$. Notice that in a strategy on $X\multimap Y$, Player R can only open in $Y$, but then the Player L can move in $X$ or $Y$ or in both components, and so on.

Identity: the identity $id _X : X \multimap X$ is the copy-cat strategy. This definition works thanks to the fact that multigames are polarized, so as, on the multigame $X\multimap X=(\overline{X} \triangledown X)$, R can only open on $X$, then L proceeds by copying the move on $\overline{X}$ and so on, at each step R has exactly one component to move in. Notice that, if the games were not polarized, then R could play on both components $X$ and $\overline{X}$, preventing L to apply the copy-cat strategy.

Composition: strategy composition is defined as follows.

Given strategies $\sigma : X \multimap Y$ and $\tau : Y \multimap Z$, $\tau \circ \sigma : X \multimap Z$ is obtained via the swivel-chair strategy, using the terminology of [7] (or the copy-cat strategy, in Game Semantics terminology), and a non-standard parallel application of strategies as follows.

The opening move by R on $X \multimap Z$ must be on $Z$, since multigames are polarized. Then consider the L reply given by the strategy $\tau$ on $Y\multimap Z$, if it exists, otherwise the whole composition is undefined. If L moves in $Z$, then we take this as the L move in the strategy $\tau \circ \sigma$. If the L move according to $\tau$ is in the $Y$ component of $Y\multimap Z$ or in both components $Y$ and $Z$, then we use the swivel chair to view the L move in the $Y$ component as a R move in the $Y$ component of $X\multimap Y$. Now, if L has a reply in $X \multimap Y$ according to $\sigma$, then L moves in $X$ or in $Y$ or in both $X$ and $Y$. In the first case, the L move in $X$ together with the possible previous move by L in $Z$ form the L reply to the opening R move. In the latter two cases, using the swivel chair, the move in $Y$ can be viewed as a R move in the $Y$ component of $Y\multimap Z$, and we go on in this way: three cases can arise. Eventually, the L multimove is all in $X$ or in $Z$, or $\sigma$ or $\tau$ is undefined, or the dialogue between the $Y$ components does not stop. In the first case, the last move on $X$ or $Z$, together with a possible previous move on $Z$ or $X$, form the answer to the opening R move, in the latter two cases the composition is undefined.

Now, in case of convergence, in order to understand how the strategy $\tau \circ \sigma$ behaves after the first pair of RL moves, it is convenient to list all situations which can arise after these initial moves, according to which player is next to move in each component. Namely, by case analysis, one can show that, after the first RL moves, the following four cases can arise:

• 1. $X^L\multimap Y^R\ \ \ Y^L\multimap Z^R$

• 2. $X^R\multimap Y^L \ \ \ Y^R\multimap Z^R$

• 3. $X^R\multimap Y^L \ \ \ Y^R\multimap Z^R$

• 4. $X^R\multimap Y^R \ \ \ Y^L\multimap Z^R$

where $X^L$ ($X^R$) denotes that L (R) is next to move in that component. Notice that case 1 above corresponds to the initial situation. Thus we are left to discuss the behavior of $\tau \circ \sigma$ in the other cases. In case 2, R can only open in $X$; this case can be dealt with similarly as the initial case 1, and after a pair of RL moves, it takes again in one of the four situations above. Cases 3 and 4 are the interesting ones, where we need to apply the strategies $\sigma$ and $\tau$ in parallel, by exploiting the parallelism of multigames. These two cases are dealt with similarly. Let us consider case 3. Then R can open in $Z$ or in $X$ or in both components.

• If R opens in $Z$, then the reply of L via $\tau$ must be in $Z$, since, by definition of configuration 3, L cannot play in the $Y$ component of $Y\multimap Z$. This will be also the reply of L in the composition $\tau \circ \sigma$, and the final configuration coincides with configuration 3.

• If R opens in $X$, then the L reply given by $\sigma$ can be in $X$, or in $Y$, or both in $X$ and $Y$. In the first case, i.e. if the L reply is in $X$, this will be the reply of $\tau \circ \sigma$, and the new configuration coincides with configuration 3. In the latter two cases, the L move in the $Y$ component of $X\multimap Y$ can be viewed, via the swivel chair, as a R move in $Y\multimap Z$. By definition of configuration 3, L can only reply in $Y$ via $\tau$, and, either after finitely many applications of the swivel chair the L reply via $\sigma$ ends up in $X$, or the dialogue between the $Y$ components goes on indefinitely, or $\sigma$ or $\tau$ are undefined. In the latter two cases, the overall composition is undefined, while in the first case the L move in $X$ will be the reply in $\tau \circ \sigma$ to the R move, and the final configuration still coincides with configuration 3.

• Finally, if R opens in $X$ and $Z$, we apply the two strategies $\sigma$ and $\tau$ in parallel: by the form of configuration 3, the L answer of $\tau$ must be in $Z$, while the L answer via $\sigma$ can be either in $X$ or in $Y$ or both in $X$ and $Y$. In this latter case, an infinite dialogue between the $Y$ components arises (or $\sigma$ or $\tau$ is undefined at some point), and hence the overall composition is undefined.

  If the L reply via $\sigma$ is in $X$, then this, together with the L reply via $\tau$ in $Z$, will form the L move in $\tau \circ \sigma$, and the final configuration coincides with configuration 3 itself. If the L reply via $\sigma$ is in $Y$, then again, either the dialogue between the $Y$ components goes on indefinitely, or $\sigma$ or $\tau$ is undefined at some point, or, after finitely many applications of the swivel chair, $\sigma$ will finally provide a L move in $X$. This, together with the L reply via $\tau$ in $Z$, will form the L move in $\tau \circ \sigma$, and the final configuration coincides with configuration 3 again.

Similarly, one can deal with case 4. This proves closure under composition of the category $\mathcal {Y}_{\mathbf{M}_\mathcal{A}}$.

Associativity of composition can also be proven by case analysis on the polarity of the current player in the various components.

Assume strategies $\sigma : X \multimap Y$, $\tau :Y\multimap Z$, $\theta :Z\multimap W$. We have to prove that $\theta \circ (\tau \circ \sigma )=(\theta \circ \tau )\circ \sigma$. Since multigames are polarized, in any of the two compositions, R can only open in $W$. Now, in any of the two compositions, one should consider the possible replies by L. We only discuss one case, the remaining being dealt with similarly. Assume the L reply via $\theta$ is in $Z$. In both compositions, we proceed to apply the swivel chair, by viewing this latter move as a R move in the $Z$ component of $Y\multimap Z$. Then, in both compositions, we consider the L reply via $\tau$. Assume L replies both in $Y$ and in $Z$. At this point, the two compositions proceed differently, since in $\theta \circ (\tau \circ \sigma )$ we first apply the swivel chair to the move in $Z$ and we go on until we get a L answer in $W$, and then we apply the swivel chair to the L move in $Y$. In $(\theta \circ \tau )\circ \sigma$, these two steps are reversed, first we apply the swivel chair to the L move in $Y$ until we get a L reply in $X$, then we apply the swivel chair to the L move in $Z$ until we get a L reply in $W$. The point is that these two steps, working on separate parts of the board (i.e. different components), are independent and can be exchanged. As a consequence, the behavior of $\theta \circ (\tau \circ \sigma )$ and $(\theta \circ \tau )\circ \sigma$ is the same.

The multigame constructions of tensor product and linear implication can be made functorial, determining a structure of a symmetric monoidal closed category on $\mathcal{Y}_{\mathbf{M}_{\mathcal {A}}}$, with the empty multigame as tensor unit. In particular, in defining the bifunctor $\triangledown$, we proceed as follows. Let $\sigma _1: X_1 \rightarrow Y_1$ and $\sigma _2: X_2 \rightarrow Y_2$ be strategies. In order to define the strategy $\sigma _1 + \sigma _2 : X_1 + X_2 \rightarrow Y_1 + Y_2$, we let the two strategies $\sigma _1$ and $\sigma _2$ play in parallel. I.e. we consider R opening move: if it is in the $Y_1$ ($Y_2$) component, then the L answer will be given by the strategy $\sigma _1$ ($\sigma _2$); if the R move is both in $Y_1$ and $Y_2$, then we apply the two strategies in parallel. We proceed in a similar way for the next moves. Clearly, for the above definition of $\sigma _1 + \sigma _2$, it is essential that in the sum multigame we keep track of the components from which each move comes from. Otherwise, without tags in the moves of the sum, when e.g. $Y_1 =Y_2$, we would not know on which component the R opening move on $Y_1 + Y_2$ comes, and then we do not know whether applying $\sigma _1$ or $\sigma _2$. This justifies our definition of sum in Sect. 3.2.

Summarizing, we have:

Theorem 1

The category $\mathcal{Y}_{\mathbf{M}_{\mathcal {A}}}$ is symmetric monoidal closed.

Finally, one could show that the infinite sum operation $\triangledown ^{\infty }$ induces a symmetric monoidal comonad, determining on $\mathcal{Y}_{\mathbf{M}_\mathcal{A}}$ a structure of linear category in the sense of [8]. We omit the details of this construction. Notice that, contrary to traditional Game Semantics, in our coalgebraic framework this construction does not require the definition of an equivalence on strategies and a quotient operation on them in the style of [1].

5 Relating Multigames to Games

In this section, we show that coalgebraic multigames are related to coalgebraic games, when a notion of parallel sum reminiscent of Conway’s selective sum is considered on games, in place of disjoint sum. Here we recall the notion of coalgebraic game as it has been defined in [17]:

Definition 12

(Coalgebraic Games)

• Let $\mathcal{A}$ be a set of atoms with functions:

  (i) $\mu : \mathcal{A} \rightarrow \mathcal{N}$ yielding the name of the move (for a set $\mathcal{N}$ of names),

  (ii) $\lambda :\mathcal{A} \rightarrow \{ L,R\}$ yielding the player who has moved.

  Assume $\mathcal{A}$ be closed under complementation.

• Let $F_{\mathcal{A}}: \text{ Set }^* \rightarrow \text{ Set }^*$ be the functor defined by

  $$\begin{aligned} F_{\mathcal{A} } (A) = {\mathcal P}_{<\kappa }(\mathcal{A} \times A) \end{aligned}$$

  with the usual definition on morphisms, and let $(\mathbf{G}_\mathcal{A} , id )$ be the final $F_{\mathcal{A}}$-coalgebra.

A coalgebraic game is an element $x$ of the carrier $\mathbf{G}_\mathcal{A}$ of the final coalgebra.

Plays and strategies are defined similarly as for multigames, see [17] for more details.

The above definition of coalgebraic games generalizes Conway games and games arising in Game Semantics, see [17] for more details. Following [11], coalgebraic games can be endowed with various notions of sum, the most studied being disjoint sum, which corresponds to tensor product in standard Game Semantics. Here we focus on a notion of parallel sum inspired by Conway’s selective sum, where at each step the current player can perform a move either in the first or in the second component or in both components. This notion of sum admits a straightforward definition by coiteration.

Definition 13

(Selective Sum). The selective sum of two games $\vee : \mathbf{G}_\mathcal{A} \times \mathbf{G}_\mathcal{A}\longrightarrow \mathbf{G}_\mathcal{A}$ is defined by:

$$ \begin{aligned} x\vee y = \{ \langle a', x' \vee y\rangle \ | \ \langle a,x'\rangle \in x\}&\cup \{ \langle b', x\vee y'\rangle \ |\ \langle b,y'\rangle \in y \}\ \cup \ \\&\{ \langle \langle a,b\rangle , x' \vee y'\rangle \ | \ \langle a,x'\rangle \in x\ \& \ \langle b,y'\rangle \in y \} , \end{aligned}$$

where $a',b'$ are obtained from $a,b$ by adding suitable tags, and $\langle a, b\rangle$ denotes the pairing of the moves $a,b$ (we assume the set of moves to be closed under pairing).

As usual, one can define negation and then linear implication on games, i.e.:

$$ \overline{x} = \{ \langle \overline{a}, \overline{x'} \rangle \ | \ \langle a, x' \rangle \in x \} \ \ \ \ \ x\multimap y = \overline{x} \vee y \ .$$

Similarly as for multigames, when we restrict to polarized games, these can be endowed with a structure of symmetric monoidal category where tensor is selective sum. As in the case of multigames, also in the present case strategy composition is defined via the swivel-chair and a non-standard parallel application of strategies. We skip the details of this construction. Let call $\mathcal{Y}_{\mathbf{G}_\mathcal{A}}$ be the category so obtained.

An analogous construction has been also carried out in [18] in the case of coalgebraic games and total strategies, and in [19] for a notion of game in the [1]-style.

5.1 Categorical Correspondence

The category $\mathcal{Y}_{\mathbf{G}_\mathcal{A}}$ of games with selective sum turns out to be equivalent to the category $\mathcal{Y}_{\mathbf{M}_\mathcal{A}}$ of multigames, i.e. there exist functors $S: \mathcal{Y}_{\mathbf{G}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{M}_\mathcal{A}}$ and $T: \mathcal{Y}_{\mathbf{M}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{G}_\mathcal{A}}$, and natural isomorphisms $\eta : G\circ F \mathop {\rightarrow }\limits ^{\cdot } Id _{\mathcal{Y}_{\mathbf{G}_\mathcal{A}}}$ and $\eta ': Id _{\mathcal{Y}_{\mathbf{M}_\mathcal{A}}} \mathop {\rightarrow }\limits ^{\cdot } F\circ G$.

Namely, given a multigame $X$ in $\mathbf{M}_\mathcal{A}$, this induces a game $X_g$, where the atomic moves are the sets of (multi)moves on the multigame $X$. Vice versa, given a game, $x$, one build a multigame $x_m$, where each atomic move $a$ is replaced by the singleton multimove $\{ a\}$. Clearly, for any multigame $X$, $(X_g)_m$ is isomorphic to $X$, and for any game $x$, $(x_m)_g$ is also isomorphic to $x$.

This allows us to define the object part of functors $S: \mathcal{Y}_{\mathbf{G}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{M}_\mathcal{A}}$ and $T: \mathcal{Y}_{\mathbf{M}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{G}_\mathcal{A}}$. Notice that $S$ and $T$ preserve tensor product on objects, up to isomorphism.

Functors $S$ and $T$ can be extended to strategies as follows.

For any strategy on multigames $\sigma : X\multimap Y$, we can associate a strategy $\sigma _g: X_g \multimap Y_g$, where the plays of $\sigma _g$ are obtained from the plays of $\sigma$ by splitting each multimove of $\sigma$ containing atomic moves both in $A$ and in $B$ into a pair of moves on $A$ and $B$, respectively. Vice versa, any strategy on games $\sigma : x \multimap y$ induces a strategy on multigames $\sigma _m: x_m \multimap y_m$, whose plays are obtained from the plays of $\sigma$ by transforming each move instance of $x$ or $y$ into a singleton multimove, and each pair of moves $\langle a, b\rangle$ as the multimove $\{a,b\}$.

Summarizing, we can define functors $S: \mathcal{Y}_{\mathbf{G}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{M}_\mathcal{A}}$ and $T: \mathcal{Y}_{\mathbf{M}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{G}_\mathcal{A}}$ by:

for any game $x$, $S x= x_m$, for any strategy $\sigma : X\multimap Y$, $S\sigma =\sigma _m$,

for any multigame $X$, $TX= X_g$, for any strategy $\sigma : X\multimap Y$, $T\sigma =\sigma _g$.

Then, we have:

Theorem 2

The functors $S: \mathcal{Y}_{\mathbf{G}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{M}_\mathcal{A}}$ and $T: \mathcal{Y}_{\mathbf{M}_\mathcal{A}} \rightarrow \mathcal{Y}_{\mathbf{G}_\mathcal{A}}$ are monoidal, and they give an equivalence between the categories $\mathcal{Y}_{\mathbf{G}_\mathcal{A}}$ and $\mathcal{Y}_{\mathbf{M}_\mathcal{A}}$.

6 Final Remarks and Directions for Future Work

We have introduced coalgebraic multigames, where at each step the current player performs a multimove, i.e. a (finite) set of atomic moves. Coalgebraic multigames introduce a certain level of parallelism, and they are situated half-way between traditional sequential games and concurrent games. Multigame operations are smoothly defined in our coalgebraic framework as final morphisms via (generalized) coiteration schemata. A monoidal closed category of multigames and strategies is built, where tensor is sum. The relationship between coalgebraic multigames and games is expressed in categorical terms via an equivalence between the category of multigames and a monoidal closed category of coalgebraic games where tensor is selective sum.

Here is a list of comments and directions for future work.

• Total strategies. In this paper, coalgebraic (multi)games are endowed with a notion of partial strategy, whereby the given player can possibly refuse to provide an answer and give up the game. Alternatively, one could consider notions of total strategies, in the line of [15, 17, 18], where the player is forced to give an answer, if there exists any. On total strategies one can then define the notion of winning/non-losing strategy for a player, if it generates winning/non-losing plays against any possible counterstrategy. A finite play is taken to be winning for the player who performs the last move, while infinite plays are taken to be winning for L/R or draws. In order to formalize winning/non-losing strategies, one shall introduce a payoff function on plays, and enrich the notion of multigame with a payoff. We claim that the results of the present paper can be rephrased also in the context of total strategies.

• Other notions of sum. In [11], Chap. 14 “How to Play Several Games at Once in a Dozen Different Ways”, Conway introduces a number of different ways in which games can be played. Apart from disjunctive and selective sum, Conway defines the conjunctive sum, where at each step the current player makes a move in each (non-ended) component. A first attempt to extend Joyal’s categorical construction to conjunctive sum fails, even in the case of polarized games, since trivially copy-cat strategies do not work. Alternative approaches are called for.

• Semantics of concurrency. In the literature, notions of concurrent games [2], asynchronous games [27], and distributed games [10, 13, 30] have been introduced as concurrent extensions of traditional games. Our categories of coalgebraic multigames and coalgebraic games with selective sum are more in the traditional line, but nonetheless, they reflect a form of parallelism. Namely, in [19] it has been shown that, in the context of functional languages, categories of multigames in the style of [1] accommodate parallel or. It would be interesting to explore to what extent multigames can be used for modeling concurrent and distributed languages, possibly featuring true concurrency. This would require an extension of our approach in order to account also for interference between moves/events.

• Relating multigames to domains. Since multigames introduce a level of parallelism, and as it is shown in [19], they accommodate for e.g. parallel or in functional programming, one may expect a tighter connection between multigames and traditional denotational semantics based on domains.