The game semantics of game theory
Jules Hedges

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 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Computability, Logic, AI Algorithms
The game semantics of game theory
Jules Hedges
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 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 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 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 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 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 of strategy profiles, a labelling function , and a winning (for ) relation .
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 be a compact closed category, a symmetric monoidal category and a strict symmetric monoidal functor that is bijective on objects. Then can be given a compact closed structure, with duals given by , units by and counits by .
Proof.
The assumption that is bijective on objects means that every object of 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 that identifies 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 of dialogues and strategies, which is the dialectica category over an inconsistent (1-valued) logic.
An object of is a 2-stage dialogue in which first the System chooses , and then the Environment chooses , where and are any sets. This breaks a common requirement in game semantics that the Environment moves first. We denote the dialogue by .
Notice that the set of -strategies for is , and the set of -strategies is , the set of functions .
We introduce a monoidal product operator given by synchronous parallel play. Specifically, the parallel play of and is the 4-stage dialogue . 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 , so we set .
Next, given objects and , we consider the same 4-stage dialogue but with the players interchanged in the former. That is, we consider the dialogue . We consider this to be played relative to , and denote it by .
The set of -strategies for is , or isomorphically . The set of -strategies is . We denote the set of -strategies for by . As the notation suggests, these are the morphisms of .
Given an object , there is a copycat -strategy for . As an element of it is the pair consisting of the identity and the projection. This is the identity morphism for . 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 -strategies for and for . There is a way to combine them to produce a -strategy for . Namely, simulates playing the two together with playing a copycat strategy for the middle moves. That is, she simulates the 8-stage dialogue
[TABLE]
with the assumption that uses a copycat strategy for the moves and . By then hiding the and moves we get a -strategy for the required 4-stage dialogue.
We denote this -strategy by the following string diagram:
\lambda$$\mu$$X^{-}$$Y^{+}$$Y^{-}$$Z^{+}$$Q^{-}$$R^{+}$$R^{-}$$S^{+}
Whereas the cap denotes a copycat -strategy, the cup denotes a copycat -strategy.
A little calculation shows that if is given by and , and is given by and , then the composite is given by
[TABLE]
and
[TABLE]
It is routine to check that this is associative, with identities given by copycat. Thus 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 into a genuine symmetric monoidal product. Given -strategies and , we can combine them to produce a -strategy .
Finally, we notice that all of the above can be generalised to any base category with finite products, replacing sets and functions, yielding a category whose morphisms are strategies internal to . Specifically, we set
[TABLE]
(By writing it this way, we do not need to assume that is cartesian closed.) The category we have been considering so far is .
Proposition 2**.**
For any category with finite products, is a symmetric monoidal category.
There is a much less obvious generalisation of when is only a monoidal category [Ril18], but we will not need it in this paper.
3 Negation and -strategies
To talk about open games, we need to talk explicitly about -strategies in a dialogue. However, the categorical structure of is built on -strategies. In turns out, however, that we can use -strategies to talk about -strategies, in a way that respects composition.
The monoidal unit of is the trivial game . The dialogue is , which is strategically equivalent to . Thus the set of -strategies for is .
If we fix a -strategy for and another -strategy , we can compose them to yield a -strategy for , by
[TABLE]
Succinctly, there is a functor taking every object to its set of -strategies, namely the covariant functor represented by . Explicitly, and .
On the other hand, the dialogue is , which is equivalent to . This is not an object, but is with players interchanged. Thus the set of -strategies for is equal to the set of -strategies for , namely .
Given an -strategy for and a -strategy , we obtain an -strategy for by
[TABLE]
In this, ‘hijacks’ ’s strategy to produce an element of , since is a -strategy for a dialogue in which plays the role of in .
Succinctly, there is a functor taking every object to its set of -strategies, namely the contravariant functor represented by . In the terminology of categorical quantum mechanics, -strategies are states and -strategies are effects.
Since an -strategy for is precisely an element of , it can be equivalently seen as a -strategy for and an -strategy for . This defines a functor , namely
[TABLE]
On objects, it is concretely given by , or more generally over a category with finite products, .
Given an -strategy for , a -strategy and a -strategy , we obtain an -strategy for . This is the -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 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 is defined by three pieces of data:
- •
A set of strategy profiles
- •
A labelling function , by which every element labels a -strategy for the 4-stage dialogue
- •
A winning condition, which is a relation between and the set of -strategies of , namely .
We write for . We say that is a winning strategy profile if for all -strategies .
We interpret 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 as a binary relation, or ask about winning strategy profiles for the System against a fixed -strategy.
From the dialogue perspective, the order of play in an open game is:
The Environment chooses an initial state of the game from 2. 2.
The System chooses the final state of the game from 3. 3.
The Environment chooses payoffs for the System from 4. 4.
The System chooses payoffs for the Environment from
An -strategy is a pair where and . The history determines the initial state of the game. The continuation determines the payoffs for System given the final state. The pair 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 -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 are in bijection with the -strategies , and correspond to the situation in which the System has no strategic choices but always follows the strategy like an automaton. Specifically, the zero-player open game is defined by:
- •
The set of strategy profiles is the singleton , where is a token representing the -strategy
- •
The labelling function is
- •
is a winning strategy profile, that is, for all -strategies
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 , is declared a Nash equilibrium by default.
The second family of examples are the decisions. There is one such open game for every nonempty set and , representing a single agent’s choice from given an observation from . In this game:
The Environment chooses an initial state from 2. 2.
The (now unique) Player chooses a final state from 3. 3.
The Environment chooses a payoff from
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 -strategy for this game is a function , and we choose the set of strategy profiles to be precisely the set of -strategies. An -strategy is a pair where and . By definition, the Player wins this game iff , that is to say, if for all .
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
- •
The labelling function takes to itself considered as a -strategy , via the bijection
- •
The winning condition is iff
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 and . The sequential composition has set of strategy profiles . Informally, the idea is that and are each associated with sets of decisions. Each decision has an associated set 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: and . The set of decisions made in a composite game is the disjoint union of the decisions made in the components, and so .
The labelling function for a sequential composition can be defined using the underlying composition in : .
In order to define the winning condition of , we must modify a context for into contexts for and . We can do this using the fact that is a functor, together with the fact that we have strategy profiles for and available. A strategy profile for is winning (that is to say, a Nash equilibrium) against the -strategy iff is winning in against the -strategy , and is winning in against the -strategy . 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 and , we combine them to form an open game
[TABLE]
As before the strategy profiles of are pairs, , for the same reason as before: we take the disjoint union of the set of decisions. The strategy profile labels the synchronous parallel play of and , that is, .
In order to define the winning condition for we need to do some more work.
Given strategy profiles and , and an -strategy for , we need to ‘project’ to and ’s view of it, as -strategies for and .
We can indeed do this. To produce an -strategy for , 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 -strategy . When for , we write . Concretely, the new continuation is .
Similarly, we can produce an -strategy for 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 we write , where .
With this, we can finally define the winning condition for : The strategy profile is winning against in iff is winning against in and is winning against in , that is to say,
[TABLE]
Proposition 3**.**
There is a symmetric monoidal (bi)category whose objects are pairs of sets and morphisms are open games.
Although 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 -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 -strategy , 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 and as respectively representing the objects and , and the backwards-oriented strings labelled and are respectively representing the objects and . Thus we are implicitly using the natural isomorphisms and .
As special cases of this, a function can be regarded as a -strategy and as a zero-player open game either covariantly as , or contravariantly as . We depict these respectively with the diagrams
X$$Y$$f$$X$$Y$$f
As a further special case, the liftings and of the copy functions are given the special syntax
X$$X$$X$$X
X$$X$$X
For any set there is a copycat -strategy , arising from the copycat -strategy for via the representation . We depict this -strategy and the corresponding zero player open game by a cap
X$$X
However, there is no corresponding family of cups , so we do not allow wires to bend the other way in our diagrams.
The -strategies are dinatural in , which means that for any function the diagram
[TABLE]
in commutes. In string diagrams, this equation is depicted
X$$Y$$f$$=$$X$$Y$$f
The reader should visualise flipping over rather than rotating within the plane. This comes from the convention that 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 (which is interchange of players in a dialogue) and on -strategies of the form and , 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 and its special case 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 , 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 defined by the diagram has as strategy profiles the pure strategy profiles of the bimatrix game, and as equilibria the pure strategy Nash equilibria of the bimatrix game: holds iff and . 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 and then the second player chooses after observing for some function , which is equivalently an extensive form with player 2’s information sets given by the equivalence relation on induced by . As special cases, if is the identity function then the node can be drawn as a plain wire and we obtain a game of perfect information, and if is the delete function then cancels with the copy function and the diagram can be deformed into the previous one to obtain a bimatrix game. The scalar game defined by the diagram has given by the pure strategy profiles, and holds iff and . 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 constructions, we need to apply the 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 -construction can be defined over any traced monoidal category , 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 of directed-complete partial orders and Scott-continuous maps.
By definition, an object of the category is a pair of objects of , and a morphism in is a morphism in . Since is cartesian monoidal, a morphism is equivalently a pair of morphisms and .
The identity on in is the identity on in . The composition of and in is given by
X$$Z$$Q$$S$$\lambda$$\mu$$Y$$Q$$S$$R$$R
in , using the string diagram language for traced monoidal categories [Sel11, section 5.7].
The monoidal product of is defined on objects by , with the obvious definition on morphisms. As is well known, 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 . Note that there are two different conventions in use: we follow [JSV96], which defines with a twist in the contravariant place, rather than [Abr96] which does not.
The idea of interpreting objects and morphisms of as dialogues is to view them as repeated play of the corresponding dialogues for , starting from and converging to a fixpoint, after which the play terminates and all moves except the final ones are hidden.
We view the object as a dialogue
[TABLE]
We do not allow arbitrary strategies, but restrict the allowed -strategies to -morphisms , and the allowed -strategies to the -morphisms . Given such a pair of strategies , the play that results is by definition
[TABLE]
When is or another suitable category, this play stabilises after finitely many stages to the that is the least fixpoint of the recursion , . By hiding the approximating moves, we consider the play resulting from to be .
Given objects and , the dialogue is
[TABLE]
We restrict the allowed -strategies to -morphisms and the allowed -strategies to -morphisms . Given a -strategy and an -strategy , the resulting play is
[TABLE]
This stabilises after finitely many stages to which is the least fixpoint of , . Again we hide the approximating moves so that is the visible play.
8 From dialectica to geometry of interaction
The previous section suggests that every -strategy in can also be viewed as a -strategy in . 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 . 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 be a traced cartesian category. Then there is a strict monoidal functor , which is identity on objects and takes the strategy to
X$$Y$$R$$S$$v$$u
Proof.
The identity morphism of is sent to
X$$X$$S$$S
which is equal to the identity on since the black structure is a comonoid. This is the identity morphism of .
Next, consider morphisms and in . If we compose them in we obtain the morphism with string diagram
X$$Q$$Z$$S$$v_{\lambda}$$u_{\lambda}$$v_{\mu}$$u_{\mu}
Using the fact that 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 , we obtain 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 and have the same objects and the monoidal product is defined in the same way. ∎
The previous result is still true when is an arbitrary traced monoidal category, where 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 -strategy to the morphism that is the counit of the compact closed structure of .
9 Abstracting open games
Inspecting the definition of open games, it appears that we can define open games replacing with any symmetric monoidal category with a chosen functor . 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 -strategies out of a -strategy for a composite. This is axiomatised by the following definition.
Definition 1**.**
A context for a symmetric monoidal category is a symmetric monoidal functor together with a natural family of functions
[TABLE]
The naturality condition required is that for all morphisms , and , 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 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 , namely
[TABLE]
There are trivial examples of contexts that carry no game-theoretic information, which we will ignore. For example, we can always take 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 can be equipped with the context , with defined by
Y_{1}$$X_{1}$$\kappa$$\lambda$$X_{2}$$X_{2}$$Y_{2}$$Y_{2}
Proof.
Let , , and . 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 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 be a symmetric monoidal category with a context , and let be objects of . An open game over consists of
- •
A set of strategy profiles
- •
A labelling function
- •
A winning condition
Given open games and over , their sequential composition is defined by , and
[TABLE]
Given open games and over , their simultaneous composition is defined by , and
[TABLE]
Proposition 6**.**
For any symmetric monoidal category with a context, there is a symmetric monoidal category of open games over . When with the usual context, we obtain the original category of open games.
The proof of this proposition formally follows the proof that 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 of , we define an open game over by , and holding for all .
Proposition 7**.**
This defines a faithful identity-on-objects symmetric monoidal functor .
10 Morphisms of contexts
Given a pair of categories with contexts , , it is possible to relate open games in to open games in if we have a strict monoidal functor that is compatible with the context functors (despite the fact that is not functorial due to mixed variance). In this section we will prove (mostly for completeness of the presentation) that when is traced cartesian, the functor satisfies the required properties. This allows us to compare open games over and 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 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 .
It does seem possible to overcome this using machinery that is known. One possibility is to consider 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 and be symmetric monoidal categories with contexts and . A strict morphism of contexts is a strict symmetric monoidal functor together with a monoidally natural family of functions
[TABLE]
such that
[TABLE]
commutes for all .
Defining non-strict morphisms of contexts takes a bit more care, but is not necessary for our purposes.
Given a traced monoidal category , the category 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 be a traced cartesian category. Then can be made into a strict morphism of contexts, by defining
[TABLE]
to take to
Y$$S$$X$$R$$h$$k
Proof.
We already checked that is strict symmetric monoidal. We get naturality for free by noting that can be equivalently defined by
[TABLE]
Suppose we have a -strategy . We must verify that the square
[TABLE]
commutes. Chasing a context 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 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 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 backwards. ∎
11 Compositional computable game theory
We can finally put all the pieces together, by considering the category . Concretely, for DCPOs , such an open game consists of:
A set of strategy profiles 2. 2.
A family of continuous play functions 3. 3.
A family of continuous coplay functions 4. 4.
An equilibrium set for each continuous history and continuation
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 to this definition differs by making additionally a function of , a function of and , and a function of .
The category is compact closed, as a result of applying proposition 1 to the zero-player functor .
As an exercise, we work out the transpose of a general open game over . The set of strategy profiles stays the same up to isomorphism, , because the transpose is defined by composition with various open games whose set of strategy profiles is . The play function is modified by taking the transpose in , which in the end simply exchanges the play and coplay functions , and swaps their inputs. A context , for and is again swapped to give a context and for , so equilibrium is defined by .
Given a continuous function , the covariant and contravariant liftings and 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 over , a context is a pair and , and the equilibrium condition for a strategy is that . We can make a similar definition over given a suitable domain of reals and a suitable operator defined on continuous functions . There are several options for defining these, and we remain largely agnostic between them. (We do not assume that is internalised in as a function for some powerdomain , 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 with the reverse inclusion order, together with . Here represents an approximation of some , and a standard real number is represented by the degenerate interval . Note that the 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 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 , the context for a decision has the form
[TABLE]
Notice that since the coutility type is the terminal DCPO, the only difference from a context over is that the history may depend on the move from . That is, the future action may affect the past observation.
We define the decision over to have , and the play function
[TABLE]
given by composition with the projection. A natural definition for equilibrium is that the least fixpoint of is in , 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 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 and to be finite flat domains, say . We also suppose that is zero-player and encodes some function , where in the latter is the set of standard real numbers. That is to say, every is some pair of total real numbers for . As a specific example, let 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 . The equilibrium condition holds iff
[TABLE]
[TABLE]
We can now check these conditions on some specific examples. First suppose that and are both constant functions, say and , including for and . (These are ‘lazy’ functions: they terminate with a total value even when their input does not.) We can then directly calculate that and . The first player has incentive to deviate because , although the second player is satisfied since . Thus is not an equilibrium of this game. By this reasoning has no ‘lazy’ equilibria of this form, since matching pennies has no pure strategy Nash equilibria.
Next consider the strategies and , in which player 1 seizes the second-move advantage by playing the optimal response to player 2’s move, namely copying it. Then , and is an equilibrium since and . There is another equilibrium given by and . Notice that player 2 could play 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 , given by and (and in consequence, ).
Finally, suppose that both players attempt to move second, with the strategy profile and . Then : the play deadlocks as each player waits for the other to move first. However , so both players have incentive to deviate and 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.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[Abr 96] Samson Abramsky. Retracing some paths in process algebra. In CONCUR ’96: Concurrency Theory , volume 1119 of Lecture Notes in Computer Science , pages 1–17. Springer, 1996.
- 2[Abr 97] Samson Abramsky. Semantics of interaction. In Semantics and logics of computation . Cambridge University Press, 1997.
- 3[Abr 05] Samson Abramsky. Abstract scalars, loops, and free traced and strongly compact closed categories. In Proceedings of CALCO’05 , volume 3629 of Lectures notes in computer science , pages 1–29, 2005.
- 4[AC 04] Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. In Proeedings of Logic in Comptuer Science (Li CS) 2004 , 2004.
- 5[AF 98] Jeremy Avigad and Solomon Feferman. Gödel’s functional (“Dialectica”) interpretation. In Handbook of proof theory , volume 137 of Studies in logic and the foundations of mathematics , pages 337–405. Elsevier, 1998.
- 6[AJ 94] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of symbolic logic , 59(2):543–574, 1994.
- 7[AJM 00] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation , 163(2):409–470, 2000.
- 8[AM 99] Samson Abramsky and Guy Mc Cusker. Game semantics. In Computational logic , volume 165 of NATO ASI Series . Springer, 1999.
