The game semantics of game theory

TL;DR

This paper bridges game theory and game semantics using a reformulation of compositional game theory, employing lenses and category theory to model open games and their interactions.

Contribution

It introduces a novel categorical framework connecting game theory with game semantics through the use of lenses and the Int-construction.

Findings

Reformulation of open games as systems and environments.

Construction of a compact closed category of computable open games.

Application of wave-style geometry of interaction to game semantics.

Abstract

We use a reformulation of compositional game theory to reunite game theory with game semantics, by viewing an open game as the System and its choice of contexts as the Environment. Specifically, the system is jointly controlled by $n \geq 0$ noncooperative players, each independently optimising a real-valued payoff. The goal of the system is to play a Nash equilibrium, and the goal of the environment is to prevent it. The key to this is the realisation that lenses (from functional programming) form a dialectica category, which have an existing game-semantic interpretation. In the second half of this paper, we apply these ideas to build a compact closed category of `computable open games' by replacing the underlying dialectica category with a wave-style geometry of interaction category, specifically the Int-construction applied to the cartesian monoidal category of directed-complete partial orders.

Equations

$${\rho }_{F(X)}\circ ({\mathrm{id}}_{F(X)}\otimes {\epsilon }_{F(X)})\circ a_{F(X),F(X{)}^{\ast },F(X)}\circ ({\eta }_{F(X)}\otimes {\mathrm{id}}_{F(X)})\circ {\lambda }_{F(X)}^{-1}$$

$$\displaystyle=\$$

$$X^{-};Y^{+};Y^{-};Z^{+};Q^{-};R^{+};R^{-};S^{+}$$

$$v_{\mu \circ \lambda }(x)=v_{\mu }(v_{\lambda }(x))$$

$$u_{\mu \circ \lambda }(x,q)=u_{\lambda }(x,u_{\mu }(v_{\lambda }(x),q))$$

$$\mathfrak{L}(\mathcal{C})\left(\left(\genfrac{}{}{0ex}{}{X}{S}\right),\left(\genfrac{}{}{0ex}{}{Y}{R}\right)\right)=\mathcal{C}(X,Y)\times \mathcal{C}(X\times R,S)$$

$$I\stackrel{h}{⟶}\left(\genfrac{}{}{0ex}{}{X}{S}\right)\stackrel{\lambda }{⟶}\left(\genfrac{}{}{0ex}{}{Y}{R}\right)$$

$$\left(\genfrac{}{}{0ex}{}{X}{S}\right)\stackrel{\lambda }{⟶}\left(\genfrac{}{}{0ex}{}{Y}{R}\right)\stackrel{k}{⟶}I$$

$$\mathfrak{L}\times {\mathfrak{L}}^{\mathrm{op}}\stackrel{\mathbb{V}\times \mathbb{K}}{\to }\mathbf{Set}\times \mathbf{Set}\stackrel{\times }{⟶}\mathbf{Set}$$

$$X_1^{-};X_2^{+};X_2^{-};Y_2^{+};Y_2^{-};Y_1^{+};R_1^{-};R_2^{+};R_2^{-};S_2^{+};S_2^{-};S_1^{+}$$

$$|\mathcal{H}\circ \mathcal{G}{|}_{\kappa }^{\sigma ,\tau }⟺|\mathcal{G}{|}_{\overline{\mathfrak{L}}(\mathrm{id},{\mathcal{H}}_{\tau })(\kappa )}^{\sigma }\wedge |\mathcal{H}{|}_{\overline{\mathfrak{L}}({\mathcal{G}}_{\sigma },\mathrm{id})(\kappa )}^{\tau }$$

$$\mathcal{G}\otimes \mathcal{H}:\left(\genfrac{}{}{0ex}{}{X_1\times X_2}{S_2\times S_1}\right)\to \left(\genfrac{}{}{0ex}{}{Y_1\times Y_2}{R_2\times R_1}\right)$$

$$X_1^{-};Y_1^{+};X_2^{-};Y_2^{+};R_2^{-};S_2^{+};R_1^{-};S_1^{+};$$

$$|\mathcal{G}\otimes \mathcal{H}{|}_{\kappa }^{\sigma ,\tau }⟺|\mathcal{G}{|}_{{\mathcal{H}}_{\tau }/\kappa }^{\sigma }\wedge |\mathcal{H}{|}_{{\mathcal{G}}_{\sigma }\setminus \kappa }^{\tau }$$

$$\left(\genfrac{}{}{0ex}{}{X}{Y}\right)$$

$$X^{+};S^{-};X^{+};S^{-};\cdots$$

$${\perp }_X;{\perp }_S;h({\perp }_S);k({\perp }_X);h(k({\perp }_X));k(h({\perp }_S));\cdots$$

$$X^{-};Y^{+};R^{-};S^{+};X^{-};Y^{+};R^{-};S^{+};\cdots$$

$$x_0$$

$$x_{n+1}$$

$$/:{\mathrm{hom}}_{\mathcal{C}}(X_2,Y_2)\to \left(\overline{\mathcal{C}}(X_1\otimes X_2,Y_1\otimes Y_2)\to \overline{\mathcal{C}}(X_1,Y_1)\right)$$

$$\setminus :{\mathrm{hom}}_{\mathcal{C}}(X_1,Y_1)\to \left(\overline{\mathcal{C}}(X_1\otimes X_2,Y_1\otimes Y_2)\to \overline{\mathcal{C}}(X_2,Y_2)\right)$$

$$\overline{\mathfrak{L}(\mathcal{C})}\left(\left(\genfrac{}{}{0ex}{}{X}{S}\right),\left(\genfrac{}{}{0ex}{}{Y}{R}\right)\right)={\mathrm{hom}}_{\mathcal{C}}(1,X)\times {\mathrm{hom}}_{\mathcal{C}}(Y,R)$$

$$|\mathcal{H}\circ \mathcal{G}{|}_{\kappa }^{\sigma ,\tau }⟺|\mathcal{G}{|}_{\overline{\mathcal{C}}({\mathrm{id}}_X,{\mathcal{H}}_{\tau })(\kappa )}^{\sigma }\wedge |\mathcal{H}{|}_{\overline{\mathcal{C}}({\mathcal{G}}_{\sigma },{\mathrm{id}}_Z)(\kappa )}^{\tau }$$

$$|\mathcal{G}\otimes \mathcal{H}{|}_{\kappa }^{\sigma ,\tau }⟺|\mathcal{G}{|}_{{\mathcal{H}}_{\tau }/\kappa }^{\sigma }\wedge |\mathcal{H}{|}_{{\mathcal{G}}_{\sigma }\setminus \kappa }^{\tau }$$

$$\overline{F}(X,Y):\overline{\mathcal{C}}(X,Y)\to \overline{\mathcal{D}}(F(X),F(Y))$$

$$\overline{\mathcal{C}}(X_1\otimes X_2,Y_1\otimes Y_2)$$

$$\overline{\mathbf{Int}(\mathcal{C})}\left(\left(\genfrac{}{}{0ex}{}{X}{S}\right),\left(\genfrac{}{}{0ex}{}{Y}{R}\right)\right)=\mathbf{Int}(\mathcal{C})\left(\left(\genfrac{}{}{0ex}{}{Y}{R}\right),\left(\genfrac{}{}{0ex}{}{X}{S}\right)\right)=\mathcal{C}(Y\otimes S,X\otimes R)$$

$$\overline{\ast }:\mathcal{C}(1,X)\times \mathcal{C}(Y,R)\to \mathcal{C}(Y\times S,X\times R)$$

$$\mathcal{C}(I,X)\times \mathcal{C}(Y,R)$$

Full text

In the second half of this paper, we apply these ideas to build a compact closed category of ‘computable open games’ by replacing the underlying dialectica category with a wave-style geometry of interaction category, specifically the Int-construction applied to the traced cartesian category of directed-complete partial orders.

1 Introduction

Although the mathematics of games shares a common ancestor in Zermelo’s work on backward induction, it split early on into two subjects that are essentially disjoint: game theory and game semantics. Game theory is the applied study of modelling real-world interacting agents, for example in economics or artificial intelligence. Game semantics, by contrast, uses agents to model – this time in the sense of semantics rather than mathematical modelling – situations in which a system interacts with an environment, but neither would usually be thought of as agents in a philosophical sense. On a technical level, game semantics not only restricts to the two-player zero-sum case, but moreover promotes one of the players to be the Player, and demotes the other to mere Opponent. This induces a deep logical duality that pervades game semantics, apparently destroying any hope of bridging the gap to game theory, which typically involves $n$ players treated symmetrically.

Compositional game theory [Hed16, GHWZ18], as its name suggests, is an attempt to introduce the principle of compositionality into game theory, motivated by practical concerns about modelling large (for example economic) systems. It is loosely inspired by game semantics, as well as categorical quantum mechanics [AC04, CK17] and much recent work in applied category theory (e.g. [Fon16]). On a technical level, game semantics involves (typically monoidal) categories in which games are the objects and strategies (with various conditions) are the morphisms, whereas open games form the morphisms of a monoidal category. This means that open games can be denoted by string diagrams, which is invaluable for working with them in practice. As with other categories of open systems, ordinary “closed” games are recovered as scalars, or endomorphisms of the monoidal unit (see [Abr05]), and depicted as string diagrams with trivial boundary.

Central to understanding open games is the concept of a context, which is a compressed representation of a game-theoretic situation in which an open game can be played. Whereas an ordinary game has a set of strategy profiles and a subset of those which are Nash equilibria, in an open game the equilibria depend on the context. This is the key to reuniting game theory and game semantics: we ignore the linguistic coincidence of the term player, and instead view an open game as the System and the choice of contexts as the Environment.

The essence of this idea is already contained in the following quote from the introduction of [Abr97]: “If Tom, Tim and Tony converse in a room, then from Tom’s point of view, he is the System, and Tim and Tony form the Environment; while from Tim’s point of view, he is the System, and Tom and Tony form the Environment.” The view of open games presented in this paper makes this precise when Tom, Tim and Tony are players in a noncooperative game.

In [Hed18] open games were reformulated in terms of lenses from functional programming [PGW17]. This was extremely useful as a technical trick, but lenses are usually used as destructive update operators on data structures and it is unclear what they have to do with game theory, if anything. The key was a comment by Dusko Pavlovic to the author that the category of lenses $\mathfrak{L}$ is a dialectica category [dP91]; combined with a game-semantic view of dialectica categories [Bla91] we can see open games in their true form: as an interleaving of game theory and game semantics.

Specifically we find that an open game is a dialogue of a particular sort played between a system and its environment. The system is jointly controlled by $n\geq 0$ noncooperative players, each independently optimising a real-valued payoff. The winning condition turns out to be Nash equilibrium: the goal of the system is to play an equilibrium, and the goal of the environment is to prevent it. Specifically, an open game consists of three pieces of data: a set $\Sigma$ of strategy profiles, a labelling function $\Sigma\to\{P\text{-strategies}\}$, and a winning (for $P$) relation $\mathbf{E}\subseteq\Sigma\times\{O\text{-strategies}\}$.

Taking a step back, this is a rare example of a cross-link in the family tree of the mathematics of games. From the common ancestor in Zermelo’s theorem [SW01] there was an almost immediate split, with little contact or commonality between the branches. One branch led to game theory via [vNM44] and [Nas51], and eventually found its home as a central tool in microeconomics [OR94], as well as applications in biology and computer science. The other branch concerned applications in logic and focussed on two-player zero-sum games, including dialogical semantics [LL78], Borel games [Mar75] and eventually game semantics in its modern sense [AJ94, HO00, AJM00, AM99].

Perhaps the only systematic attempt to bridge the two branches is the work of van Benthem and collaborators on game logics [vB14]. Other examples of more ad-hoc bridges can be found for example in [HM13, lR14, GW14]. The work of Pavlovic [Pav09], which is not specifically about game semantics, is perhaps the most closely related to this paper.

In the second half of this paper, we apply these ideas to build a compact closed category of ‘computable open games’ by replacing the underlying dialectica category with a wave-style geometry of interaction category, specifically the Int-construction applied to the traced cartesian category of directed-complete partial orders. (The category of directed-complete partial orders and Scott-continuous maps is a standard setting for the semantics of possibly-nonterminating recursive computations.) Ultimately we rely on the following transport of structure result:

Proposition 1**.**

Let $\mathcal{C}$ be a compact closed category, $\mathcal{D}$ a symmetric monoidal category and $F:\mathcal{C}\to\mathcal{D}$ a strict symmetric monoidal functor that is bijective on objects. Then $\mathcal{D}$ can be given a compact closed structure, with duals given by $F(X)^{*}=F(X^{*})$, units by $\eta_{F(X)}=F(\eta_{X})$ and counits by $\varepsilon_{F(X)}=F(\varepsilon_{X})$.

Proof.

The assumption that $F$ is bijective on objects means that every object of $\mathcal{D}$ is uniquely assigned a dual, unit and counit. It is simple to check the yanking equations [KL80]:

[TABLE]

and similarly for the other equation. ∎

The hypotheses of this theorem are already satisfied by a particular functor $\mathfrak{L}\to\mathbf{OG}$ that identifies $\mathfrak{L}$ with the subcategory of zero-player open games. Thus it suffices to replace the source category with one that is compact closed, while preserving the hypotheses (and the game-theoretic interpretation).

We end with a worked example, a ‘paradoxical’ variant of matching pennies where both players have the ability and incentive to play a strategy that is contingent on the other’s move - something that appears causally absurd, and can result in the play deadlocking while each player waits for the other to move first.

2 Dialogues

While the name ‘dialectica’ should bring to mind dialogues in the tradition of philosophical logic (for example via Hegel’s dialectics), this is apparently a coincidence. The dialectica interpretation is named after the journal Dialectica, who published Gödel’s paper in their Paul Bernays festschrift [Göd58]. But the dialectica interpretation does have a very dialectical feeling to it.

The game semantic viewpoint on Gödel’s dialectica interpretation [AF98] and de Paiva’s dialectica categories [dP91] was described in Blass’ paper that first introduced game semantics [Bla91]. In this section we recall this viewpoint in detail.

We first introduce a category $\mathfrak{L}$ of dialogues and strategies, which is the dialectica category over an inconsistent (1-valued) logic.

An object of $\mathfrak{L}$ is a 2-stage dialogue $X^{+};S^{-}$ in which first the System chooses $x:X$, and then the Environment chooses $s:S$, where $X$ and $S$ are any sets. This breaks a common requirement in game semantics that the Environment moves first. We denote the dialogue $X^{+};S^{-}$ by $\binom{X}{S}$.

Notice that the set of $P$-strategies for $\binom{X}{S}$ is $X$, and the set of $O$-strategies is $S^{X}$, the set of functions $X\to S$.

We introduce a monoidal product operator given by synchronous parallel play. Specifically, the parallel play of $\binom{X}{S}$ and $\binom{Y}{R}$ is the 4-stage dialogue $X^{+};Y^{+};R^{-};S^{-}$. This peculiar ordering of moves, with the right-hand dialogue being played in the middle of the left-hand dialogue, is characteristic of dialectica. This 4-stage dialogue is strategically equivalent to the 2-stage dialogue $(X\times Y)^{+};(R\times S)^{-}$, so we set $\binom{X}{S}\otimes\binom{Y}{R}=\binom{X\times Y}{R\times S}$.

Next, given objects $\binom{X}{S}$ and $\binom{Y}{R}$, we consider the same 4-stage dialogue but with the players interchanged in the former. That is, we consider the dialogue $X^{-};Y^{+};R^{-};S^{+}$. We consider this to be $\binom{Y}{R}$ played relative to $\binom{X}{S}$, and denote it by $\binom{X}{S}\to\binom{Y}{R}$.

The set of $P$-strategies for $\binom{X}{S}\to\binom{Y}{R}$ is $Y^{X}\times S^{X\times R}$, or isomorphically $(Y\times S^{R})^{X}$. The set of $O$-strategies is $X\times R^{Y}$. We denote the set of $P$-strategies for $\binom{X}{S}\to\binom{Y}{R}$ by $\mathfrak{L}\left(\binom{X}{S},\binom{Y}{R}\right)$. As the notation suggests, these are the morphisms of $\mathfrak{L}$.

Given an object $\binom{X}{S}$, there is a copycat $P$-strategy for $\binom{X}{S}\to\binom{X}{S}=X^{-};X^{+};S^{-};S^{+}$. As an element of $X^{X}\times S^{X\times S}$ it is the pair consisting of the identity and the projection. This is the identity morphism for $\binom{X}{S}$. Following [Abr97] we denote this strategy by a string diagram:

X^{-}$$X^{+}$$S^{-}$$S^{+}

A major theme of this paper is that we take this notation seriously, pushing it far beyond what was originally intended. While it is common for papers to contain a caveat that string diagrams are ‘officially’ informal pending a coherence theorem, in this case they are far more informal than usual: it is completely unclear what category they live in, or exactly which topological moves they are invariant under. While there is an immediate surface similarity to grammatical reductions in pregroups [PL07, CSC10], there appears to be a much deeper connection to string diagrams in the bicategory of finite product categories, Tambara modules (profunctors compatible with the cartesian product) and natural transformations [Boi20] (see also [PS08]), something we leave for later work.

Now suppose we are given $P$-strategies $\lambda$ for $\binom{X}{S}\to\binom{Y}{R}=X^{-};Y^{+};R^{-};S^{+}$ and $\mu$ for $\binom{Y}{R}\to\binom{Z}{Q}=Y^{-};Z^{+};Q^{-};R^{+}$. There is a way to combine them to produce a $P$-strategy $\mu\circ\lambda$ for $\binom{X}{S}\to\binom{Z}{Q}=X^{-};Z^{+};Q^{-};S^{+}$. Namely, $P$ simulates playing the two together with $O$ playing a copycat strategy for the middle moves. That is, she simulates the 8-stage dialogue

[TABLE]

with the assumption that $O$ uses a copycat strategy for the moves $Y^{-}$ and $R^{-}$. By then hiding the $Y$ and $R$ moves we get a $P$-strategy for the required 4-stage dialogue.

We denote this $P$-strategy by the following string diagram:

\lambda$$\mu$$X^{-}$$Y^{+}$$Y^{-}$$Z^{+}$$Q^{-}$$R^{+}$$R^{-}$$S^{+}

Whereas the cap denotes a copycat $P$-strategy, the cup denotes a copycat $O$-strategy.

A little calculation shows that if $\lambda$ is given by $v_{\lambda}:X\to Y$ and $u_{\lambda}:X\times R\to S$, and $\mu$ is given by $v_{\mu}:Y\to Z$ and $u_{\mu}:Y\times Q\to R$, then the composite is given by

[TABLE]

and

[TABLE]

It is routine to check that this is associative, with identities given by copycat. Thus $\mathfrak{L}$ is indeed a category. These equations are commonly known in functional programming as composition of lenses [FGM*+*07, GS16].

Given this category structure we can also make $\otimes$ into a genuine symmetric monoidal product. Given $P$-strategies $\lambda:\binom{X_{1}}{S_{1}}\to\binom{Y_{1}}{R_{1}}$ and $\mu:\binom{X_{2}}{S_{2}}\to\binom{Y_{2}}{R_{2}}$, we can combine them to produce a $P$-strategy $\lambda\otimes\mu:\binom{X_{1}\times X_{2}}{S_{2}\times S_{1}}\to\binom{Y_{1}\times Y_{2}}{R_{2}\times R_{1}}$.

Finally, we notice that all of the above can be generalised to any base category $\mathcal{C}$ with finite products, replacing sets and functions, yielding a category $\mathfrak{L}(\mathcal{C})$ whose morphisms are strategies internal to $\mathcal{C}$. Specifically, we set

[TABLE]

(By writing it this way, we do not need to assume that $\mathcal{C}$ is cartesian closed.) The category we have been considering so far is $\mathfrak{L}=\mathfrak{L}(\mathbf{Set})$.

Proposition 2**.**

For any category $\mathcal{C}$ with finite products, $\mathfrak{L}(\mathcal{C})$ is a symmetric monoidal category.

There is a much less obvious generalisation of $\mathfrak{L}(\mathcal{C})$ when $\mathcal{C}$ is only a monoidal category [Ril18], but we will not need it in this paper.

3 Negation and $O$-strategies

To talk about open games, we need to talk explicitly about $O$-strategies in a dialogue. However, the categorical structure of $\mathfrak{L}$ is built on $P$-strategies. In turns out, however, that we can use $P$-strategies to talk about $O$-strategies, in a way that respects composition.

The monoidal unit of $\mathfrak{L}$ is the trivial game $I=\binom{1}{1}=1^{+};1^{-}$. The dialogue $I\to\binom{X}{S}$ is $1^{-};X^{+};S^{-};1^{+}$, which is strategically equivalent to $\binom{X}{S}$. Thus the set of $P$-strategies for $I\to\binom{X}{S}$ is $X$.

If we fix a $P$-strategy $h:X$ for $\binom{X}{S}$ and another $P$-strategy $\lambda:\binom{X}{S}\to\binom{Y}{R}$, we can compose them to yield a $P$-strategy $\lambda\circ h$ for $\binom{Y}{R}$, by

[TABLE]

Succinctly, there is a functor $\mathbb{V}:\mathfrak{L}\to\mathbf{Set}$ taking every object to its set of $P$-strategies, namely the covariant functor represented by $I$. Explicitly, $\mathbb{V}\binom{X}{S}=X$ and $\mathbb{V}(\lambda)=v_{\lambda}$.

On the other hand, the dialogue $\binom{X}{S}\to I$ is $X^{-};1^{+};1^{-};S^{+}$, which is equivalent to $X^{-};S^{+}$. This is not an object, but is $\binom{X}{S}$ with players interchanged. Thus the set of $P$-strategies for $\binom{X}{S}\to I$ is equal to the set of $O$-strategies for $\binom{X}{S}$, namely $S^{X}$.

Given an $O$-strategy $k$ for $\binom{Y}{R}$ and a $P$-strategy $\lambda:\binom{X}{S}\to\binom{Y}{R}$, we obtain an $O$-strategy $k\circ\lambda$ for $\binom{X}{S}$ by

[TABLE]

In this, $O$ ‘hijacks’ $P$’s strategy to produce an element of $S$, since $\lambda$ is a $P$-strategy for a dialogue in which $P$ plays the role of $O$ in $\binom{X}{S}$.

Succinctly, there is a functor $\mathbb{K}:\mathfrak{L}^{\mathrm{op}}\to\mathbf{Set}$ taking every object to its set of $O$-strategies, namely the contravariant functor represented by $I$. In the terminology of categorical quantum mechanics, $P$-strategies are states and $O$-strategies are effects.

Since an $O$-strategy for $\binom{X}{S}\to\binom{Y}{R}$ is precisely an element of $X\times Y^{R}$, it can be equivalently seen as a $P$-strategy for $\binom{X}{S}$ and an $O$-strategy for $\binom{Y}{R}$. This defines a functor $\overline{\mathfrak{L}}:\mathfrak{L}\times\mathfrak{L}^{\mathrm{op}}\to\mathbf{Set}$, namely

[TABLE]

On objects, it is concretely given by $\overline{\mathfrak{L}}\left(\binom{X}{S},\binom{Y}{R}\right)=X\times R^{Y}$, or more generally over a category $\mathcal{C}$ with finite products, $\overline{\mathfrak{L}(\mathcal{C})}\left(\binom{X}{S},\binom{Y}{R}\right)=\mathcal{C}(1,X)\times\mathcal{C}(Y,R)$.

Given an $O$-strategy $\kappa=(h,k)$ for $\binom{X_{1}}{S_{1}}\to\binom{Y_{1}}{R_{1}}$, a $P$-strategy $\lambda:\binom{X_{1}}{S_{1}}\to\binom{X_{2}}{S_{2}}$ and a $P$-strategy $\mu:\binom{Y_{2}}{R_{2}}\to\binom{Y_{1}}{R_{1}}$, we obtain an $O$-strategy $\overline{\mathfrak{L}}(\lambda,\mu)(h,k)=(\lambda\circ h,k\circ\mu)$ for $\binom{X_{2}}{S_{2}}\to\binom{Y_{2}}{R_{2}}$. This is the $O$-strategy for the dialogue

[TABLE]

with appropriately hidden copycat moves, as given by the string diagram

\lambda$$\mu$$X_{1}^{-}$$X_{2}^{+}$$X_{2}^{-}$$Y_{2}^{+}$$Y_{2}^{-}$$Y_{1}^{+}$$R_{1}^{-}$$R_{2}^{+}$$R_{2}^{-}$$S_{2}^{+}$$S_{2}^{-}$$S_{1}^{+}$$\kappa

4 Open games

We can now give an equivalent definition of open games [Hed16, GHWZ18] in terms of dialogues. The treatment in this section and the next will be conceptual, with examples deferred until the end of section 6 after building up some theory.

An open game $\binom{X}{S}\to\binom{Y}{R}$ is in one dimension a dialogue played between a System and an Environment, and in another dimension it is a non-cooperative game in the sense of economics, in which several players jointly control the System while independently optimising payoffs.

An open game $\mathcal{G}:\binom{X}{S}\to\binom{Y}{R}$ is defined by three pieces of data:

• •

A set $\Sigma_{\mathcal{G}}$ of strategy profiles

• •

A labelling function $\mathcal{G}_{-}:\Sigma_{\mathcal{G}}\to\mathfrak{L}\left(\binom{X}{S},\binom{Y}{R}\right)$, by which every element $\sigma:\Sigma_{\mathcal{G}}$ labels a $P$-strategy $\mathcal{G}_{\sigma}$ for the 4-stage dialogue $\binom{X}{S}\to\binom{Y}{R}$

• •

A winning condition, which is a relation between $\Sigma_{\mathcal{G}}$ and the set of $O$-strategies of $\binom{X}{S}\to\binom{Y}{R}$, namely $|\mathcal{G}|\subseteq\Sigma_{\mathcal{G}}\times\overline{\mathfrak{L}}\left(\binom{X}{S},\binom{Y}{R}\right)$.

We write $|\mathcal{G}|^{\sigma}_{\kappa}$ for $(\sigma,\kappa)\in|\mathcal{G}|$. We say that $\sigma$ is a winning strategy profile if $|\mathcal{G}|^{\sigma}_{\kappa}$ for all $O$-strategies $\kappa:\overline{\mathfrak{L}}\left(\binom{X}{S},\binom{Y}{R}\right)$.

We interpret $|\mathcal{G}|$ as an equilibrium condition. That is, from the dialogue perspective the goal of the System is to reach equilibrium and the goal of the Environment is to prevent equilibrium. In real examples there is rarely a winning strategy profile, and so we focus on $|\mathcal{G}|$ as a binary relation, or ask about winning strategy profiles for the System against a fixed $O$-strategy.

From the dialogue perspective, the order of play in an open game $\binom{X}{S}\to\binom{Y}{R}$ is:

The Environment chooses an initial state of the game from $X$ 2. 2.

The System chooses the final state of the game from $Y$ 3. 3.

The Environment chooses payoffs for the System from $R$ 4. 4.

The System chooses payoffs for the Environment from $S$

An $O$-strategy is a pair $\kappa=(h,k)$ where $h:X$ and $k:Y\to R$. The history $h$ determines the initial state of the game. The continuation $k$ determines the payoffs for System given the final state. The pair $(h,k)$ completely determines the strategic context in which the players that make up System make their choices, reducing the open game to an ordinary normal-form game. For this reason, we also call an $O$-strategy a context for the open game.

We only need two families of examples of open games to generate a large family of examples, corresponding roughly to extensive-form games, using the sequential and parallel play operators we will define in the next section. These two generating families are the zero-player open games and the decisions, which could loosely be called one-player open games.

The zero-player open games $\binom{X}{S}\to\binom{Y}{R}$ are in bijection with the $P$-strategies $\lambda:\binom{X}{S}\to\binom{Y}{R}$, and correspond to the situation in which the System has no strategic choices but always follows the strategy $\lambda$ like an automaton. Specifically, the zero-player open game $\lambda$ is defined by:

• •

The set of strategy profiles is the singleton $\Sigma_{\lambda}=\{*\}$, where $*$ is a token representing the $P$-strategy $\lambda$

• •

The labelling function is $\lambda_{*}=\lambda$

• •

$*$ is a winning strategy profile, that is, $|\lambda|^{*}_{\kappa}$ for all $O$-strategies $\kappa$

Perhaps the only surprising part of this definition is that $*$ is a winning strategy profile. The reason for this ultimately comes down to agreeing with Nash equilibrium on real examples. Nash equilibrium is a negative definition: a strategy profile should fail to be a Nash equilibrium if some particular player has positive incentive to deviate from it. Since there are no players in $\lambda$, $*$ is declared a Nash equilibrium by default.

The second family of examples are the decisions. There is one such open game $\mathcal{D}=\mathcal{D}_{Y|X}:\binom{X}{1}\to\binom{Y}{\mathbb{R}}$ for every nonempty set $X$ and $Y$, representing a single agent’s choice from $Y$ given an observation from $X$. In this game:

The Environment chooses an initial state from $X$ 2. 2.

The (now unique) Player chooses a final state from $Y$ 3. 3.

The Environment chooses a payoff from $\mathbb{R}$

The winning condition of this game is intensional by being a property of the strategies of both Player and Environment, and cannot be written in terms of the play alone. This is because optimality in game theory is a counterfactual: if the System had made a different choice then the resulting payoff would have been lower.

Observe that a $P$-strategy for this game is a function $\sigma:X\to Y$, and we choose the set of strategy profiles $\Sigma_{\mathcal{D}_{Y|X}}$ to be precisely the set of $P$-strategies. An $O$-strategy is a pair $(h,k)$ where $h:X$ and $k:Y\to\mathbb{R}$. By definition, the Player wins this game iff $\sigma(h)\in\arg\max(k)$, that is to say, if $k(\sigma(h))\geq k(y)$ for all $y:Y$.

This is a small shift in perspective that is quite natural from the perspective of game semantics. In game theory there is no concept of winning, only optimality and equilibrium. Declaring a player to have won if they make an optimal choice may not be meaningful as game theory, but it is appropriate terminology when combining game theory with game semantics.

Writing this out:

• •

The set of strategy profiles is $\Sigma_{\mathcal{D}}=Y^{X}$

• •

The labelling function takes $\sigma:X\to Y$ to itself considered as a $P$-strategy $\mathcal{D}_{\sigma}:\binom{X}{1}\to\binom{Y}{\mathbb{R}}$, via the bijection $\mathfrak{L}\left(\binom{X}{1},\binom{Y}{\mathbb{R}}\right)\cong Y^{X}$

• •

The winning condition is $|\mathcal{D}|^{\sigma}_{h,k}$ iff $\sigma(h)\in\arg\max(k)$

5 Composing open games

We can make open games into the morphisms of a symmetric monoidal category. The two composition operators, categorical composition and tensor product, correspond to sequential play and simultaneous play.

Suppose we are given open games $\mathcal{G}:\binom{X}{S}\to\binom{Y}{R}$ and $\mathcal{H}:\binom{Y}{R}\to\binom{Z}{Q}$. The sequential composition $\mathcal{H}\circ\mathcal{G}:\binom{X}{S}\to\binom{Z}{Q}$ has set of strategy profiles $\Sigma_{\mathcal{H}\circ\mathcal{G}}=\Sigma_{\mathcal{G}}\times\Sigma_{\mathcal{H}}$. Informally, the idea is that $\mathcal{G}$ and $\mathcal{H}$ are each associated with sets $G,H$ of decisions. Each decision $g\in G,h\in H$ has an associated set $\Sigma_{g},\Sigma_{h}$ of strategies, and the set of strategy profiles in each case should be thought of as the set of tuples of strategies, one for each decision: $\Sigma_{\mathcal{G}}=\prod_{g\in G}\Sigma_{g}$ and $\Sigma_{\mathcal{H}}=\prod_{h\in H}\Sigma_{h}$. The set of decisions made in a composite game is the disjoint union of the decisions made in the components, and so $\Sigma_{\mathcal{H}\circ\mathcal{G}}=\prod_{g\in G+H}\Sigma_{g}=\prod_{g\in G}\Sigma_{g}\times\prod_{h\in H}\Sigma_{h}=\Sigma_{\mathcal{G}}\times\Sigma_{\mathcal{H}}$.

The labelling function for a sequential composition can be defined using the underlying composition in $\mathfrak{L}$: $(\mathcal{H}\circ\mathcal{G})_{\sigma,\tau}=\mathcal{H}_{\tau}\circ\mathcal{G}_{\sigma}$.

In order to define the winning condition of $\mathcal{H}\circ\mathcal{G}$, we must modify a context for $\mathcal{H}\circ\mathcal{G}$ into contexts for $\mathcal{G}$ and $\mathcal{H}$. We can do this using the fact that $\overline{\mathfrak{L}}$ is a functor, together with the fact that we have strategy profiles for $\mathcal{G}$ and $\mathcal{H}$ available. A strategy profile $(\sigma,\tau)$ for $\mathcal{H}\circ\mathcal{G}$ is winning (that is to say, a Nash equilibrium) against the $O$-strategy $\kappa$ iff $\sigma$ is winning in $\mathcal{G}$ against the $O$-strategy $\overline{\mathfrak{L}}(\mathrm{id},\mathcal{H}_{\tau})(\kappa)$, and $\tau$ is winning in $\mathcal{H}$ against the $O$-strategy $\overline{\mathfrak{L}}(\mathcal{G}_{\sigma},\mathrm{id})(\kappa)$. That is to say,

[TABLE]

This makes open games into the morphisms of a category (or, more properly, the 1-cells of a bicategory).

Next we consider simultaneous play. Given open games $\mathcal{G}:\binom{X_{1}}{S_{1}}\to\binom{Y_{1}}{R_{1}}$ and $\mathcal{H}:\binom{X_{2}}{S_{2}}\to\binom{Y_{2}}{R_{2}}$, we combine them to form an open game

[TABLE]

As before the strategy profiles of $\mathcal{G}\otimes\mathcal{H}$ are pairs, $\Sigma_{\mathcal{G}\otimes\mathcal{H}}=\Sigma_{\mathcal{G}}\times\Sigma_{\mathcal{H}}$, for the same reason as before: we take the disjoint union of the set of decisions. The strategy profile $(\sigma,\tau)$ labels the synchronous parallel play of $\mathcal{G}_{\sigma}$ and $\mathcal{H}_{\tau}$, that is, $(\mathcal{G}\otimes\mathcal{H})_{\sigma,\tau}=\mathcal{G}_{\sigma}\otimes\mathcal{H}_{\tau}$.

In order to define the winning condition for $\mathcal{G}\otimes\mathcal{H}$ we need to do some more work.

Given strategy profiles $\sigma:\Sigma_{\mathcal{G}}$ and $\tau:\Sigma_{\mathcal{H}}$, and an $O$-strategy $\kappa$ for $\binom{X_{1}\times X_{2}}{S_{2}\times S_{1}}\to\binom{Y_{1}\times Y_{2}}{R_{2}\times R_{1}}$, we need to ‘project’ $\kappa$ to $\mathcal{G}$ and $\mathcal{H}$’s view of it, as $O$-strategies for $\binom{X_{1}}{S_{1}}\to\binom{Y_{1}}{R_{1}}$ and $\binom{X_{2}}{S_{2}}\to\binom{Y_{2}}{R_{2}}$.

We can indeed do this. To produce an $O$-strategy for $\binom{X_{1}}{S_{1}}\to\binom{Y_{1}}{R_{1}}$, consider the dialogue

[TABLE]

with the strategy

\mathcal{H}_{\tau}$$X_{1}^{-}$$Y_{1}^{+}$$X_{2}^{-}$$Y_{2}^{+}$$R_{2}^{-}$$S_{2}^{+}$$R_{1}^{-}$$S_{1}^{+}$$\kappa

We call this $O$-strategy $\mathcal{H}_{\tau}/\kappa$. When $\kappa=((h_{1},h_{2}),k)$ for $k:Y_{1}\times Y_{2}\to R_{2}\times R_{1}$, we write $\mathcal{H}_{\tau}/\kappa=(h_{1},k_{1}^{h_{2},\mathcal{H}_{\tau}})$. Concretely, the new continuation is $k_{1}^{h_{2},\mathcal{H}_{\tau}}(y_{1})=k(y_{1},v_{\mathcal{H}_{\tau}}(h_{2}))_{2}$.

Similarly, we can produce an $O$-strategy $\mathcal{G}_{\sigma}\setminus\kappa$ for $\binom{X_{2}}{S_{2}}\to\binom{Y_{2}}{R_{2}}$ by considering the same dialogue with the strategy

\mathcal{G}_{\sigma}$$X_{1}^{-}$$Y_{1}^{+}$$X_{2}^{-}$$Y_{2}^{+}$$R_{2}^{-}$$S_{2}^{+}$$R_{1}^{-}$$S_{1}^{+}$$\kappa

When $\kappa=((h_{1},h_{2}),k)$ we write $\mathcal{G}_{\sigma}\setminus\kappa=(h_{2},k_{2}^{h_{1},\mathcal{G}_{\sigma}})$, where $k_{2}^{h_{1},\mathcal{G}_{\sigma}}(y_{2})=k(v_{\mathcal{G}_{\sigma}}(h_{1}),y_{2})_{1}$.

With this, we can finally define the winning condition for $\mathcal{G}\otimes\mathcal{H}$: The strategy profile $(\sigma,\tau)$ is winning against $\kappa$ in $\mathcal{G}\otimes\mathcal{H}$ iff $\sigma$ is winning against $\mathcal{H}_{\tau}/\kappa$ in $\mathcal{G}$ and $\tau$ is winning against $\mathcal{G}_{\sigma}\setminus\kappa$ in $\mathcal{H}$, that is to say,

[TABLE]

Proposition 3**.**

There is a symmetric monoidal (bi)category $\mathbf{OG}$ whose objects are pairs of sets and morphisms are open games.

Although $\mathbf{OG}$ should properly be thought of as a bicategory with 2-cells given by appropriately compatible functions between sets of strategy profiles, this is an uninteresting technicality and we will instead quotient out these 2-cells, treating open games as defined only up to compatible bijections of strategy profiles. The details of this can be found in [Hed18].

6 Picturing open games

Since open games are the morphisms of a monoidal category, we can depict them by string diagrams, and in fact this turns out to be invaluable for working with them in practice. As a special case of this we also obtain string diagrams for the monoidal category of $P$-strategies, which are equivalently the wide subcategory of zero-player open games. These diagrams should not be confused with the (less well understood) diagrams for dialogues that have appeared so far in this paper, which are very different, although to some extent it is possible to translate between them. This section contains nothing new, but is included from [GHWZ18] for completeness.

A $P$-strategy $\lambda:\binom{X}{S}\to\binom{Y}{R}$, viewed as a zero-player open game, is depicted as a string diagram

X$$Y$$R$$S$$\lambda

We regard the forwards-oriented strings labelled $X$ and $Y$ as respectively representing the objects $\binom{X}{1}$ and $\binom{Y}{1}$, and the backwards-oriented strings labelled $R$ and $S$ are respectively representing the objects $\binom{1}{R}$ and $\binom{1}{S}$. Thus we are implicitly using the natural isomorphisms $\binom{X}{1}\otimes\binom{1}{S}=\binom{X\times 1}{S\times 1}\cong\binom{X}{S}$ and $\binom{Y}{1}\otimes\binom{1}{R}=\binom{Y\times 1}{R\times 1}\cong\binom{Y}{R}$.

As special cases of this, a function $f:X\to Y$ can be regarded as a $P$-strategy and as a zero-player open game either covariantly as $f:\binom{X}{1}\to\binom{Y}{1}$, or contravariantly as $f^{*}:\binom{1}{Y}\to\binom{1}{X}$. We depict these respectively with the diagrams

X$$Y$$f$$X$$Y$$f

As a further special case, the liftings $\Delta_{X}:\binom{X}{1}\to\binom{X\times X}{1}$ and $\Delta_{X}^{*}:\binom{1}{X\times X}\to\binom{1}{X}$ of the copy functions are given the special syntax

X$$X$$X$$X

X$$X$$X

For any set $X$ there is a copycat $P$-strategy $\varepsilon_{X}:\binom{X}{X}\to I$, arising from the copycat $O$-strategy for $X^{+};X^{-}$ via the representation $\mathbb{K}\cong\mathfrak{L}(-,I)$. We depict this $P$-strategy and the corresponding zero player open game by a cap

X$$X

However, there is no corresponding family of cups $\eta_{X}:I\to\binom{X}{X}$, so we do not allow wires to bend the other way in our diagrams.

The $P$-strategies $\varepsilon_{X}:\binom{X}{X}\to I$ are dinatural in $X$, which means that for any function $f:X\to Y$ the diagram

[TABLE]

in $\mathfrak{L}$ commutes. In string diagrams, this equation is depicted

X$$Y$$f$$=$$X$$Y$$f

The reader should visualise $f$ flipping over rather than rotating within the plane. This comes from the convention that $\otimes$ reverses the contravariant part of an object, and corresponds to the choice of algebraic rather than diagrammatic transpose in [CK17, section 4.2.2].

This can be seen as a sort of partial duality, which is defined on all objects by $\binom{X}{S}^{*}=\binom{S}{X}$ (which is interchange of players in a dialogue) and on $P$-strategies of the form $f$ and $f^{*}$, but on no other open games besides these. In the last section of this paper we will extend this to a fully-fledged duality in the sense of compact closure.

A decision $\mathcal{D}_{Y|X}:\binom{X}{1}\to\binom{Y}{\mathbb{R}}$ and its special case $\mathcal{D}_{Y}=\mathcal{D}_{Y|1}:I\to\binom{Y}{\mathbb{R}}$ are respectively depicted

X$$Y$$\mathbb{R}$$\mathcal{D}_{Y|X}$$Y$$\mathbb{R}$$\mathcal{D}_{Y}

The string diagrams built from these diagram elements correspond to the open games generated from zero-player open games and decisions by sequential and parallel composition. Given a pair of payoff matrices $U:X\times Y\to\mathbb{R}\times\mathbb{R}$, the resulting bimatrix game corresponds to the diagram

\mathcal{D}_{X}$$\mathcal{D}_{Y}$$U$$X$$Y$$\mathbb{R}$$\mathbb{R}$$\mathbb{R}$$\mathbb{R}

in the sense that the scalar open game $\mathcal{G}:I\to I$ defined by the diagram has as strategy profiles $\Sigma_{\mathcal{G}}=X\times Y$ the pure strategy profiles of the bimatrix game, and as equilibria the pure strategy Nash equilibria of the bimatrix game: $|\mathcal{G}|^{x,y}$ holds iff $x\in\arg\max_{x^{\prime}}U_{1}(x^{\prime},y)$ and $y\in\arg\max_{y^{\prime}}U_{2}(x,y^{\prime})$. This directly generalises to normal-form games with any finite number of players.

Similarly, the diagram

\mathcal{D}_{X}$$\mathcal{D}_{Y|X^{\prime}}$$f$$U$$X$$X$$X$$X^{\prime}$$Y$$\mathbb{R}$$\mathbb{R}$$\mathbb{R}$$\mathbb{R}

describes a 2-player sequential game in which the first player chooses $x$ and then the second player chooses $y$ after observing $f(x)$ for some function $f:X\to X^{\prime}$, which is equivalently an extensive form with player 2’s information sets given by the equivalence relation on $X^{\prime}$ induced by $f$. As special cases, if $f$ is the identity function then the $f$ node can be drawn as a plain wire and we obtain a game of perfect information, and if $f:X\to 1$ is the delete function then $f$ cancels with the copy function and the diagram can be deformed into the previous one to obtain a bimatrix game. The scalar game $\mathcal{G}:I\to I$ defined by the diagram has $\Sigma_{\mathcal{G}}=X\times Y^{X^{\prime}}$ given by the pure strategy profiles, and $|\mathcal{G}|^{x,f}$ holds iff $x\in\arg\max_{x^{\prime}}U_{1}(x^{\prime},f(x^{\prime}))$ and $f(x)\in\arg\max_{y^{\prime}}U_{2}(x,y^{\prime})$. Notice that these are the Nash equilibria of the extensive form game, rather than the subgame perfect equilibria. Again, this generalises to extensive form games with any finite number of players.

7 Dialogues and wave-style geometry of interaction

In order to obtain a connection between the dialectica and $\mathbf{Int}$ constructions, we need to apply the $\mathbf{Int}$ construction to categories that are traced cartesian monoidal. This is wave-style geometry of interaction, so-called because every point in our string diagrams is consistently assigned a value [Abr96]. (It is contrasted with particle-style GoI, which applies to monoidal categories built on a coproduct and in which we imagine a token moving around the diagram.)

Game-semantic interpretations of wave-style GoI have not been widely considered. In this section we suggest such an interpretation that will be suitable for our purposes.

The $\mathbf{Int}$-construction can be defined over any traced monoidal category $\mathcal{C}$, but we restrict to traced cartesian categories. These are equivalent to Conway cartesian categories, or cartesian categories with a natural family of fixpoint operators [Has99] (see also [PS14]). A canonical example is the category $\mathbf{DCPO}$ of directed-complete partial orders and Scott-continuous maps.

By definition, an object of the category $\mathbf{Int}(\mathcal{C})$ is a pair $\binom{X}{S}$ of objects of $\mathcal{C}$, and a morphism $\binom{X}{S}\to\binom{Y}{R}$ in $\mathbf{Int}(\mathcal{C})$ is a morphism $X\times R\to Y\times S$ in $\mathcal{C}$. Since $\mathcal{C}$ is cartesian monoidal, a morphism $\binom{X}{S}\to\binom{Y}{R}$ is equivalently a pair of morphisms $X\times R\to Y$ and $X\times R\to S$.

The identity on $\binom{X}{S}$ in $\mathbf{Int}(\mathcal{C})$ is the identity on $X\times S$ in $\mathcal{C}$. The composition of $\lambda:\binom{X}{S}\to\binom{Y}{R}$ and $\mu:\binom{Y}{R}\to\binom{Z}{Q}$ in $\mathbf{Int}(\mathcal{C})$ is given by

X$$Z$$Q$$S$$\lambda$$\mu$$Y$$Q$$S$$R$$R

in $\mathcal{C}$, using the string diagram language for traced monoidal categories [Sel11, section 5.7].

The monoidal product of $\mathbf{Int}(\mathcal{C})$ is defined on objects by $\binom{X_{1}}{S_{1}}\otimes\binom{X_{2}}{S_{2}}=\binom{X_{1}\otimes X_{2}}{S_{2}\otimes S_{1}}$, with the obvious definition on morphisms. As is well known, $\mathbf{Int}(\mathcal{C})$ can be equipped with the structure of a compact closed category, which satisfies the universal property of being the free compact closed category on the traced monoidal category $\mathcal{C}$. Note that there are two different conventions in use: we follow [JSV96], which defines $\otimes$ with a twist in the contravariant place, rather than [Abr96] which does not.

The idea of interpreting objects and morphisms of $\mathbf{Int}(\mathcal{C})$ as dialogues is to view them as repeated play of the corresponding dialogues for $\mathfrak{L}(\mathcal{C})$, starting from $\bot$ and converging to a fixpoint, after which the play terminates and all moves except the final ones are hidden.

We view the object $\binom{X}{S}$ as a dialogue

[TABLE]

We do not allow arbitrary strategies, but restrict the allowed $P$-strategies to $\mathcal{C}$-morphisms $S\to X$, and the allowed $O$-strategies to the $\mathcal{C}$-morphisms $X\to S$. Given such a pair of strategies $(h,k)$, the play that results is by definition

[TABLE]

When $\mathcal{C}$ is $\mathbf{DCPO}$ or another suitable category, this play stabilises after finitely many stages to the $(x,s)$ that is the least fixpoint of the recursion $x=h(s)$, $s=k(x)$. By hiding the approximating moves, we consider the play resulting from $(h,k)$ to be $(x,s)$.

Given objects $\binom{X}{S}$ and $\binom{Y}{R}$, the dialogue $\binom{X}{S}\to\binom{Y}{R}$ is

[TABLE]

We restrict the allowed $P$-strategies to $\mathcal{C}$-morphisms $X\times R\to Y\times S$ and the allowed $O$-strategies to $\mathcal{C}$-morphisms $Y\times S\to X\times R$. Given a $P$-strategy $\lambda=\left<v,u\right>$ and an $O$-strategy $\kappa=\left<h,k\right>$, the resulting play is

[TABLE]

This stabilises after finitely many stages to $(x,y,r,s)$ which is the least fixpoint of $(x,r)=\kappa(y,s)$, $(y,s)=\lambda(x,r)$. Again we hide the approximating moves so that $(x,y,r,s)$ is the visible play.

8 From dialectica to geometry of interaction

The previous section suggests that every $P$-strategy in $\mathfrak{L}(\mathcal{C})\left(\binom{X}{S},\binom{Y}{R}\right)$ can also be viewed as a $P$-strategy in $\mathbf{Int}(\mathcal{C})\left(\binom{X}{S},\binom{Y}{R}\right)$. We could also discover this fact simply by inspecting the definitions, without thinking in terms of dialogues.

Incidentally, [HH17] refers to the Int-construction as “bidirectional computation”, a technical term that usually refers to lenses and related constructions (e.g. [GS16]).

In this section we use string diagrams in the underlying category $\mathcal{C}$. This is the language of traced symmetric monoidal categories [Sel11, section 5.7] which are cartesian monoidal [Sel11, section 6.1]. Implicitly, string diagrams for cartesian monoidal categories use the fact that a monoidal product is cartesian iff every object can be compatibly equipped with a commutative comonoid structure making every morphism into a comonoid homomorphism [Fox76].

Proposition 4**.**

Let $\mathcal{C}$ be a traced cartesian category. Then there is a strict monoidal functor $-^{*}:\mathfrak{L}(\mathcal{C})\to\mathbf{Int}(\mathcal{C})$, which is identity on objects and takes the strategy $(v,u)$ to

X$$Y$$R$$S$$v$$u

Proof.

The identity morphism $\binom{X}{S}\to\binom{X}{S}$ of $\mathfrak{L}(\mathcal{C})$ is sent to

X$$X$$S$$S

which is equal to the identity on $X\times S$ since the black structure is a comonoid. This is the identity morphism $\binom{X}{S}\to\binom{X}{S}$ of $\mathbf{Int}(\mathcal{C})$.

Next, consider morphisms $\lambda:\binom{X}{S}\to\binom{Y}{R}$ and $\mu:\binom{Y}{R}\to\binom{Z}{Q}$ in $\mathfrak{L}(\mathcal{C})$. If we compose them in $\mathbf{Int}(\mathcal{C})$ we obtain the morphism $\mu^{*}\circ\lambda^{*}$ with string diagram

X$$Q$$Z$$S$$v_{\lambda}$$u_{\lambda}$$v_{\mu}$$u_{\mu}

Using the fact that $v_{\lambda}$ is a comonoid homomorphism, followed by coassociativity and symmetry of the black structure, we can transform this to

X$$Q$$Z$$S$$v_{\lambda}$$v_{\lambda}$$u_{\lambda}$$v_{\mu}$$u_{\mu}

On the other hand, if we compose in $\mathfrak{L}(\mathcal{C})$, we obtain $(\mu\circ\lambda)^{*}$ with string diagram

X$$Q$$Z$$S$$v_{\lambda}$$v_{\mu}$$v_{\lambda}$$u_{\mu}$$u_{\lambda}

By inspection, we see that these string diagrams are equivalent. Equality of the two morphisms then follows from the coherence theorem for traced symmetric monoidal categories [Sel11, theorem 5.22].

Finally, it can be seen by inspection that the functor is strict monoidal, since $\mathfrak{L}(\mathcal{C})$ and $\mathbf{Int}(\mathcal{C})$ have the same objects and the monoidal product is defined in the same way. ∎

The previous result is still true when $\mathcal{C}$ is an arbitrary traced monoidal category, where $\mathfrak{L}(\mathcal{C})$ is replaced with the more general category of optics [Ril18]. This was proved by Elena Di Lavore and Mario Román (private communication).

We also note that the functor $-^{*}$ takes the $P$-strategy $\varepsilon_{X}:\binom{X}{X}\to I$ to the morphism $\varepsilon_{X}:\binom{X}{X}\to I$ that is the counit of the compact closed structure of $\mathbf{Int}(\mathcal{C})$.

9 Abstracting open games

Inspecting the definition of open games, it appears that we can define open games replacing $\mathfrak{L}$ with any symmetric monoidal category $\mathcal{C}$ with a chosen functor $\overline{\mathcal{C}}:\mathcal{C}\times\mathcal{C}^{\mathrm{op}}\to\mathbf{Set}$. This does indeed give us a category of open games, but defining a monoidal product of open games requires an additional piece of structure, namely the ability to project individual $P$-strategies out of a $O$-strategy for a composite. This is axiomatised by the following definition.

Definition 1**.**

A context for a symmetric monoidal category $\mathcal{C}$ is a symmetric monoidal functor $\overline{\mathcal{C}}:\mathcal{C}\times\mathcal{C}^{\mathrm{op}}\to\mathbf{Set}$ together with a natural family of functions

[TABLE]

The naturality condition required is that for all morphisms $W_{1}\overset{\lambda_{1}}{\longrightarrow}X_{1}$, $Y_{2}\overset{\nu_{1}}{\longrightarrow}Z_{1}$ and $W_{2}\overset{\lambda_{2}}{\longrightarrow}X_{2}\overset{\mu_{2}}{\longrightarrow}Y_{2}\overset{\nu_{2}}{\longrightarrow}Z_{2}$, the diagram

\overline{\mathcal{C}}(Z_{1}\otimes Z_{2},W_{1}\otimes W_{2})$$\overline{\mathcal{C}}(Z_{1},W_{1})$$\overline{\mathcal{C}}(Y_{1}\otimes Y_{2},X_{1}\otimes X_{2})$$\overline{\mathcal{C}}(Y_{1},X_{1})$$(\nu_{2}\circ\mu_{2}\circ\lambda_{2})/-$$\overline{\mathcal{C}}(\nu_{1},\lambda_{1})$$\overline{\mathcal{C}}(\nu_{1}\otimes\nu_{2},\lambda_{1}\otimes\lambda_{2})$$\mu_{2}/-

in $\mathbf{Set}$ commutes.

Using the symmetry, we can derive from this a natural family of functions

[TABLE]

and vice versa.

The structures we defined earlier do indeed give a context on $\mathfrak{L}(\mathcal{C})$, namely

[TABLE]

There are trivial examples of contexts that carry no game-theoretic information, which we will ignore. For example, we can always take $\overline{\mathcal{C}}$ to be a constant functor. We give a second family of nontrivial examples, which we will use later.

Proposition 5**.**

Every traced symmetric monoidal category $\mathcal{C}$ can be equipped with the context $\overline{\mathcal{C}}(X,Y)=\hom_{\mathcal{C}}(Y,X)$, with $\lambda/\kappa$ defined by

Y_{1}$$X_{1}$$\kappa$$\lambda$$X_{2}$$X_{2}$$Y_{2}$$Y_{2}

Proof.

Let $\kappa:\hom_{\mathcal{C}}(Z\otimes Z^{\prime},W\otimes W^{\prime})$, $\lambda_{1}:W_{1}\to X_{1}$, $\nu_{1}:Y_{2}\to Z_{1}$ and $W_{2}\overset{\lambda_{2}}{\longrightarrow}X_{2}\overset{\mu_{2}}{\longrightarrow}Y_{2}\overset{\nu_{2}}{\longrightarrow}Z_{2}$. We chase111The author has named this proof technique ‘string diagram chasing’, i.e. chasing an element around a commuting diagram whose nodes are all formed from homsets in a monoidal category. the context $\kappa$ around the commuting diagram in definition 1. By the upper route we obtain

Y$$X$$\kappa$$\nu_{1}$$\lambda_{1}$$\lambda_{2}$$\mu_{2}$$\nu_{2}

and by the lower route we obtain

Y$$X$$\kappa$$\nu_{1}$$\nu_{2}$$\lambda_{1}$$\lambda_{2}$$\mu_{2}

By the coherence theorem for traced monoidal categories, these denote equal morphisms. ∎

Definition 2**.**

Let $\mathcal{C}$ be a symmetric monoidal category with a context $\overline{\mathcal{C}}$, and let $X,Y$ be objects of $\mathcal{C}$. An open game $\mathcal{G}:X\to Y$ over $\mathcal{C}$ consists of

• •

A set $\Sigma_{\mathcal{G}}$ of strategy profiles

• •

A labelling function $\mathcal{G}_{-}:\Sigma_{\mathcal{G}}\to\mathcal{C}(X,Y)$

• •

A winning condition $|\mathcal{G}|\subseteq\Sigma_{\mathcal{G}}\times\overline{\mathcal{C}}(X,Y)$

Given open games $\mathcal{G}:X\to Y$ and $\mathcal{H}:Y\to Z$ over $\mathcal{C}$, their sequential composition $\mathcal{H}\circ\mathcal{G}:X\to Z$ is defined by $\Sigma_{\mathcal{H}\circ\mathcal{G}}=\Sigma_{\mathcal{G}}\times\Sigma_{\mathcal{H}}$, $(\mathcal{H}\circ\mathcal{G})_{\sigma,\tau}=\mathcal{H}_{\tau}\circ\mathcal{G}_{\sigma}$ and

[TABLE]

Given open games $\mathcal{G}:X_{1}\to Y_{1}$ and $\mathcal{H}:X_{2}\to Y_{2}$ over $\mathcal{C}$, their simultaneous composition $\mathcal{G}\otimes\mathcal{H}:X_{1}\otimes X_{2}\to Y_{1}\otimes Y_{2}$ is defined by $\Sigma_{\mathcal{G}\otimes\mathcal{H}}=\Sigma_{\mathcal{G}}\times\Sigma_{\mathcal{H}}$, $(\mathcal{G}\otimes\mathcal{H})_{\sigma,\tau}=\mathcal{G}_{\sigma}\otimes\mathcal{H}_{\tau}$ and

[TABLE]

Proposition 6**.**

For any symmetric monoidal category $\mathcal{C}$ with a context, there is a symmetric monoidal category $\mathbf{OG}(\mathcal{C})$ of open games over $\mathcal{C}$. When $\mathcal{C}=\mathfrak{L}(\mathbf{Set})$ with the usual context, we obtain the original category of open games.

The proof of this proposition formally follows the proof that $\mathbf{OG}$ is a symmetric monoidal category. (The clearest presentation is in [Hed18, section 5 & appendix].) The definition of a context contains precisely the conditions needed for this proof to work.

Given a morphism $\lambda:X\to Y$ of $\mathcal{C}$, we define an open game $\lambda:X\to Y$ over $\mathcal{C}$ by $\Sigma_{\lambda}=\{*\}$, $\lambda_{*}=\lambda$ and $|\lambda|^{*}_{\kappa}$ holding for all $\kappa$.

Proposition 7**.**

This defines a faithful identity-on-objects symmetric monoidal functor $\mathcal{C}\to\mathbf{OG}(\mathcal{C})$.

10 Morphisms of contexts

Given a pair of categories with contexts $\mathcal{C}$, $\mathcal{D}$, it is possible to relate open games in $\mathbf{OG}(\mathcal{C})$ to open games in $\mathbf{OG}(\mathcal{D})$ if we have a strict monoidal functor $\mathcal{C}\to\mathcal{D}$ that is compatible with the context functors (despite the fact that $\mathbf{OG}(-)$ is not functorial due to mixed variance). In this section we will prove (mostly for completeness of the presentation) that when $\mathcal{C}$ is traced cartesian, the functor $-^{*}:\mathfrak{L}(\mathcal{C})\to\mathbf{Int}(\mathcal{C})$ satisfies the required properties. This allows us to compare open games over $\mathfrak{L}(\mathbf{DCPO})$ and $\mathbf{Int}(\mathbf{DCPO})$ for example.

The reason we do not develop this idea fully is that it does not seem possible to obtain a strict (or even strong) monoidal functor $\mathfrak{L}(\mathbf{Set})\to\mathfrak{L}(\mathbf{DCPO})$ that would allow us to understand ‘computable game theory’ as far as possible in terms of classical game theory. Ultimately this stems from the lack of a suitable product-preserving functor $\mathbf{Set}\to\mathbf{DCPO}$.

It does seem possible to overcome this using machinery that is known. One possibility is to consider $\mathbf{DCPO}$ with the smash product, which is a monoidal product that is not the categorical product, and then consider optics over this. Open games over a particular category of optics (over the monoidal category of conditional probability distributions) were considered in the context of Bayesian games [BHZ19], but they are more subtle and less intuitive so we leave this for future work.

Definition 3**.**

Let $\mathcal{C}$ and $\mathcal{D}$ be symmetric monoidal categories with contexts $\overline{\mathcal{C}}$ and $\overline{\mathcal{D}}$. A strict morphism of contexts is a strict symmetric monoidal functor $F:\mathcal{C}\to\mathcal{D}$ together with a monoidally natural family of functions

[TABLE]

such that

[TABLE]

commutes for all $f:X_{2}\to Y_{2}$.

Defining non-strict morphisms of contexts takes a bit more care, but is not necessary for our purposes.

Given a traced monoidal category $\mathcal{C}$, the category $\mathbf{Int}(\mathcal{C})$ is compact closed, and hence in particular traced monoidal. We consider it to have the context defined for traced monoidal categories. That is,

[TABLE]

Proposition 8**.**

Let $\mathcal{C}$ be a traced cartesian category. Then $-^{*}:\mathfrak{L}(\mathcal{C})\to\mathbf{Int}(\mathcal{C})$ can be made into a strict morphism of contexts, by defining

[TABLE]

to take $(h,k)$ to

Y$$S$$X$$R$$h$$k

Proof.

We already checked that $-^{*}$ is strict symmetric monoidal. We get naturality for free by noting that $\overline{\ *\ }$ can be equivalently defined by

[TABLE]

Suppose we have a $P$-strategy $\lambda:\binom{X_{2}}{S_{2}}\to\binom{Y_{2}}{R_{2}}$. We must verify that the square

[TABLE]

commutes. Chasing a context $(h,k)$ around the top yields

Y_{1}$$S_{1}$$X_{1}$$R_{1}$$h$$h$$v_{\lambda}$$k$$X_{2}$$R_{2}$$X_{1}$$X_{2}$$Y_{2}

As a useful intermediate point, since $h$ is a comonoid homomorphism this is equivalent to

Y_{1}$$S_{1}$$X_{1}$$R_{1}$$h$$v_{\lambda}$$k$$R_{2}$$Y_{2}$$X_{2}

On the other hand, chasing $(h,k)$ around the bottom yields

Y_{1}$$Y_{2}$$S_{2}$$S_{1}$$X_{2}$$R_{2}$$X_{1}$$X_{2}$$R_{2}$$R_{1}$$Y_{2}$$S_{2}$$h$$k$$v_{\lambda}$$u_{\lambda}

To see the equivalence of this diagram to the previous one modulo traced cartesian categories, trace the deletion on $S_{2}$ backwards. ∎

11 Compositional computable game theory

We can finally put all the pieces together, by considering the category $\mathbf{OG}(\mathbf{Int}(\mathbf{DCPO}))$. Concretely, for DCPOs $X,S,Y,R$, such an open game $\mathcal{G}:\binom{X}{S}\to\binom{Y}{R}$ consists of:

A set $\Sigma$ of strategy profiles 2. 2.

A family of continuous play functions $\mathbf{P}_{\mathcal{G}}(\sigma):X\times R\to Y$ 3. 3.

A family of continuous coplay functions $\mathbf{C}_{\mathcal{G}}(\sigma):X\times R\to S$ 4. 4.

An equilibrium set $\mathbf{E}_{\mathcal{G}}(h,k)\subseteq\Sigma$ for each continuous history $h:Y\times S\to X$ and continuation $k:Y\times S\to R$

This definition is written in the style of the original concrete definition of open games in [GHWZ18] for ease of comparison. Specifically, besides changing the base category from $\mathbf{Set}$ to $\mathbf{DCPO}$ this definition differs by making $\mathbf{C}_{\mathcal{G}}$ additionally a function of $R$, $h$ a function of $Y$ and $S$, and $k$ a function of $S$.

The category $\mathbf{OG}(\mathbf{Int}(\mathbf{DCPO}))$ is compact closed, as a result of applying proposition 1 to the zero-player functor $\mathbf{Int}(\mathbf{DCPO})\to\mathbf{OG}(\mathbf{Int}(\mathbf{DCPO}))$.

As an exercise, we work out the transpose $\mathcal{G}^{*}:\binom{R}{Y}\to\binom{S}{X}$ of a general open game $\mathcal{G}:\binom{X}{S}\to\binom{Y}{R}$ over $\mathbf{Int}(\mathcal{C})$. The set of strategy profiles stays the same up to isomorphism, $\Sigma_{\mathcal{G}^{*}}\cong\Sigma_{\mathcal{G}}$, because the transpose is defined by composition with various open games whose set of strategy profiles is $1$. The play function is modified by taking the transpose in $\mathbf{Int}(\mathcal{C})$, which in the end simply exchanges the play and coplay functions $X\times R\to Y$, $X\times R\to S$ and swaps their inputs. A context $(h,k)$, for $h:S\times Y\to R$ and $k:S\times Y\to X$ is again swapped to give a context $h^{\prime}=k:Y\times S\to X$ and $k^{\prime}=h:Y\times S\to R$ for $\mathcal{G}$, so equilibrium is defined by $|\mathcal{G}^{*}|^{\sigma}_{h,k}\iff|\mathcal{G}|^{\sigma}_{k,h}$.

Given a continuous function $f:X\to Y$, the covariant and contravariant liftings $f:\binom{X}{1}\to\binom{Y}{1}$ and $f^{*}:\binom{1}{Y}\to\binom{1}{X}$ are now transposes of each other. Thus we are conservatively extending the notion of duality that already exists in categories of open games.

Recall that for a decision $\mathcal{D}_{Y|X}:\binom{X}{1}\to\binom{Y}{\mathbb{R}}$ over $\mathfrak{L}(\mathbf{Set})$, a context is a pair $h:X$ and $k:Y\to\mathbb{R}$, and the equilibrium condition for a strategy $\sigma:X\to Y$ is that $\sigma(h)\in\arg\max(k)$. We can make a similar definition over $\mathfrak{L}(\mathbf{DCPO})$ given a suitable domain of reals $\mathbb{R}$ and a suitable $\arg\max$ operator defined on continuous functions $Y\to\mathbb{R}$. There are several options for defining these, and we remain largely agnostic between them. (We do not assume that $\arg\max$ is internalised in $\mathbf{DCPO}$ as a function $\mathbb{R}^{Y}\to\mathcal{P}(Y)$ for some powerdomain $\mathcal{P}$, since a naive definition would not be continuous.)

A simple example of a domain of reals that can serve as a mental model is the domain of closed intervals $[x,y]$ with the reverse inclusion order, together with $\bot_{\mathbb{R}}=(-\infty,+\infty)$. Here $[x,y]$ represents an approximation of some $z\in[x,y]$, and a standard real number $z$ is represented by the degenerate interval $[z,z]$. Note that the $\arg\max$ operator is still defined for the standard order on reals (which must be extended to all elements of the domain), which is not related to the inclusion order. As a minimal requirement in order to work out an example later, we suppose that $\bot_{\mathbb{R}}$ is below every standard real in the extended standard order. This corresponds to the assumption that players always prefer a terminating payoff, no matter how small, to a nonterminating one.

Over $\mathbf{Int}(\mathbf{DCPO})$, the context for a decision $\mathcal{D}_{X,Y}$ has the form

[TABLE]

Notice that since the coutility type $S=1$ is the terminal DCPO, the only difference from a context over $\mathfrak{L}(\mathcal{C})$ is that the history $h$ may depend on the move from $Y$. That is, the future action may affect the past observation.

We define the decision $\mathcal{D}=\mathcal{D}_{Y|X}:\binom{X}{1}\to\binom{Y}{\mathbb{R}}$ over $\mathbf{Int}(\mathbf{DCPO})$ to have $\Sigma_{\mathcal{D}}=\mathbf{DCPO}(X,Y)$, and the play function

[TABLE]

given by composition with the projection. A natural definition for equilibrium is that the least fixpoint $y$ of $y=\sigma(h(y))$ is in $\arg\max(k)$, which we write

[TABLE]

As a worked example, we can build a 2-player game in which each player’s strategy may be contingent on the choice of the other, something that is causally absurd. Let the game $\mathcal{G}:I\to I$ be defined by the string diagram

\mathcal{D}_{X|Y}$$\mathcal{D}_{Y|X}$$U$$X$$Y$$X$$Y$$X$$Y$$\mathbb{R}$$\mathbb{R}$$\mathbb{R}$$\mathbb{R}

We suppose $X$ and $Y$ to be finite flat domains, say $X=Y=\{\bot,a,b\}$. We also suppose that $U$ is zero-player and encodes some function $U:X\times Y\to\mathbb{R}\times\mathbb{R}$, where $\mathbb{R}$ in the latter is the set of standard real numbers. That is to say, every $U(x,y)$ is some pair of total real numbers for $x,y\neq\bot$. As a specific example, let $U$ be the payoff matrix of matching pennies, extended as follows:

[TABLE]

Matching pennies is an interesting example here because it exhibits second-move advantage: either player would benefit from the ability to play contingently on the other’s move.

The set of strategy profiles of this game is $\Sigma=\mathbf{DCPO}(X,Y)\times\mathbf{DCPO}(Y,X)$. The equilibrium condition $|\mathcal{G}|^{\sigma,\tau}$ holds iff

[TABLE]

[TABLE]

We can now check these conditions on some specific examples. First suppose that $\sigma$ and $\tau$ are both constant functions, say $\sigma(y)=a$ and $\tau(x)=b$, including for $y=\bot$ and $x=\bot$. (These are ‘lazy’ functions: they terminate with a total value even when their input does not.) We can then directly calculate that $\mu x.\sigma(\tau(x))=a$ and $\mu y.\tau(\sigma(y))=b$. The first player has incentive to deviate because $a\not\in\arg\max_{x}U_{1}(x,b)=\{b\}$, although the second player is satisfied since $b\in\arg\max_{y}U_{2}(a,y)=\{b\}$. Thus $(\sigma,\tau)$ is not an equilibrium of this game. By this reasoning $\mathcal{G}$ has no ‘lazy’ equilibria of this form, since matching pennies has no pure strategy Nash equilibria.

Next consider the strategies $\sigma(y)=y$ and $\tau(x)=a$, in which player 1 seizes the second-move advantage by playing the optimal response to player 2’s move, namely copying it. Then $\mu x.\sigma(\tau(x))=\mu y.\tau(\sigma(y))=a$, and $(\sigma,\tau)$ is an equilibrium since $\arg\max_{x}U_{1}(x,a)=\{a\}$ and $\arg\max_{y}U_{2}(y,y)=\{a,b\}$. There is another equilibrium given by $\sigma(y)=y$ and $\tau(x)=b$. Notice that player 2 could play $\bot$ and deadlock the play, but we assume that she prefers the ‘losing’ total payoff of [math]. Similarly there are two more equilibria in which it is player 2 who takes the second-move advantage with $\tau(x)=\overline{x}$, given by $\overline{a}=b$ and $\overline{b}=a$ (and in consequence, $\overline{\bot}=\bot$).

Finally, suppose that both players attempt to move second, with the strategy profile $\sigma(y)=y$ and $\tau(x)=\overline{x}$. Then $\mu x.\sigma(\tau(x))=\mu y.\tau(\sigma(y))=\bot$: the play deadlocks as each player waits for the other to move first. However $\arg\max_{x}U_{1}(x,\overline{x})=\arg\max_{y}U_{2}(y,y)=\{a,b\}$, so both players have incentive to deviate and $(\sigma,\tau)$ is not an equilibrium. Given our assumptions, either player would prefer to move first and take the losing total payoff, rather than deadlocking the play.