Theorem [efr-MLF1]

As defined above, \oplus is a symmetric monoidal structure on \widetilde {\mathsf {Game}}(\mathsf {SLens}(\mathcal {D})).

Proof

The monoidal coherences come from the monoidal structure of +, and it is trivial to see that they preserve the selection relations. The only nontrivial part is proving that \oplus is functorial. Hence let G_1: A_1 \to B_1, G_1' : B_1 \to C_1, G_2: A_2 \to B_2, G_2' : B_2 \to C_2 be games. The strategy set of (G_1' \oplus G_2')\circ (G_1 \oplus G_2) is given by (\Sigma _1 \& \Sigma _2) \otimes (\Sigma _1' \otimes \Sigma _2') For (G_1' \circ G_1) \oplus (G_2' \circ G_2), by (\Sigma _1 \otimes \Sigma _1') \& (\Sigma _2 \otimes \Sigma _2').

In the base, these are the same object \Sigma _1 \otimes \Sigma _2 \otimes \Sigma _1' \otimes \Sigma _2'. In the fiber, they are given respectively by (\overline {\Sigma _1} + \overline {\Sigma _2}) \otimes (\overline {\Sigma _1}' + \overline {\Sigma _2'}) and (\overline {\Sigma _1} \otimes \overline {\Sigma _1'}) + (\overline {\Sigma _2} \otimes \overline {\Sigma _2}'). Note the coproducts here are the fiberwise ones. There is an obvious lens from the former to the latter (given by the identity map on the base, and the inclusion of two summands in a fourfold coproduct---note that lenses go backwards in the fiber). Letting I \to (A_1 \oplus A_2) \otimes M, (C_1 \oplus C_2) \otimes M \to I be a context, and going through the definitions, it is clear that the resulting contexts for the former game factors as this lens followed by the context for the latter game. In other words, this lens is a reparametrization map between the two games. It suffices to verify it is an equivalence.

Unpacking the equivalence relation on (G_1' \oplus G_2')(G_1 \oplus G_2), note that (in all the possible contexts,) the signal to G_1 does not depend on the action of G_2' and vice versa, and so for G_1' and G_2. Hence they are in equilibrium if and only if they are in equilibrium in G_1'G_1 for the given context (conditioned on that branch), and similarly the other two. This proves the desired equivalence.

Context

Open Games with External Choice [efr-SREZ]

Let \mathcal {C} be an extensive Markov category. Let \mathcal {D} be a monoidal stochastic module fibration with Markov structure, which has coproducts which are preserved by the pullbacks. Recall that \mathsf {SLens}(\mathcal {D}) acquires two monoidal structures: one from dualizing the given monoidal structure on \mathcal {D}, which we simply denote \otimes ,I, and one from taking the coCartesian monoidal structure in the fiber (which is Cartesian after taking the fiberwise dual, of course), which we denote \&, \top . Note that (\mathsf {SLens}(\mathcal {D}), \&) is a Markov category. For the rest of this section, fix \mathcal {D}, \mathcal {C} like this.

Lemma [efr-Y2ZN]

Let \bar {X},\bar {Y} be objects in \mathsf {SLens}(\mathcal {D}), and let I \to I + I be a morphism in \mathcal {C}. Then there is a canonical map \bar {X} \& \bar {Y} \to \bar {X} + \bar {Y}, so that the underlying map is X \otimes Y \to (X \otimes Y) \otimes (I + I) \cong X \otimes Y + X \otimes Y \to X + Y

Proof

The first map in the factorization has a deterministic retract (deleting the I+I component,) and using the coproduct-preservation, the coproduct over X + Y and \bar {X} \& \bar {Y} pull back to the same object over X \otimes Y \otimes (I + I). Composing the induced stochastic-Cartesian map and the Cartesian map gives the canonical map we wanted.

With the interpretation that \overline {X} \& \overline {Y} is the object \overline {X}_x + \overline {Y}_y indexed over X \otimes Y, this map simply selects one branch randomly and marginalizes to that coordinate in X \otimes Y, then includes the returned value into the coproduct.

Definition [efr-98DR]

When \mathcal {C}, \mathcal {D} as above, \widetilde {\mathsf {Game}}(\mathsf {SLens}(\mathcal {D})) acquires a monoidal structure which we call external choice, and write \oplus , given on objects by the coproduct + in \mathsf {SLens}(\mathcal {D}), and on morphisms by the following formula:

Given two open games G_1 = (\overline {\Sigma _A} \otimes \overline {A_1} \to \overline {A_2}, \epsilon _A), G_2 = (\overline {\Sigma _B} \otimes \overline {B_1} \to \overline {B_2}, \epsilon _B), their external choice is has parameter \Sigma _A \& \Sigma _B. The play map is given by (\Sigma _A \& \Sigma _B) \otimes (A_1 + B_1) \cong (\Sigma _A \& \Sigma _B) \otimes A_1 + (\Sigma _A \& \Sigma _B) \otimes B_1 \to \Sigma _A \otimes A_1 + \Sigma _B \otimes B_1 \to A_2 + B_2 The selection relation \epsilon _A \oplus \epsilon _A is given (up to equivalence) as follows: Given a context k: \overline {\Sigma _A} \& \overline {\Sigma _B} \to I, and a deterministic state I \to \overline {\Sigma _A} \& \overline {\Sigma _B}, they are in equilibrium if

  1. k factors over the canonical \overline {\Sigma _A} \& \overline {\Sigma _B} \to \overline {\Sigma _A} + \overline {\Sigma _B} for some c: I \to I + I.
  2. The factorization being given by k_A, k_B : \overline {\Sigma _A}, \overline {\Sigma _B} \to I ,and I \to \overline {\Sigma _A} \& \overline {\Sigma _B} being given by \sigma _A, \sigma _B : I \to \overline {\Sigma _A}, \overline {\Sigma _B}, we have \epsilon _A(\sigma _A,k_A), \epsilon _B(\sigma _B, k_B)

The idea behind the external choice operator is that, for all the contexts which can actually occur as a result of pasting a game G \oplus G' into a larger string diagram, the map X \times X' \to \overline {X} + \overline {X}' has the given form---that is, the probability of landing in each of the two fibers does not depend on the chosen x,x' and the conditional distributions on the \overline {X} component of the fiber depend only on x \in X. Hence we need only concern ourselves with which states are equilibria for contexts of this form. The choice of the empty set of equilibria for other contexts is merely a convention.

[efr-VB6A]

Given a state I \to A + B in a Markov category with coproducts, we say a pair I \to A, I \to B form a pair of conditionals if the copairing I + I \to A + B is a Bayesian inverse of the map A + B \to I + I.

Given a state I \to \bar {X} + \bar {Y} in \mathsf {SLens}(\mathcal {D}), we say a pair of maps I \to \bar {X}, I \to \bar {Y} form a pair of conditionals if the underlying maps do.

Theorem [efr-MLF1]

As defined above, \oplus is a symmetric monoidal structure on \widetilde {\mathsf {Game}}(\mathsf {SLens}(\mathcal {D})).

Proof

The monoidal coherences come from the monoidal structure of +, and it is trivial to see that they preserve the selection relations. The only nontrivial part is proving that \oplus is functorial. Hence let G_1: A_1 \to B_1, G_1' : B_1 \to C_1, G_2: A_2 \to B_2, G_2' : B_2 \to C_2 be games. The strategy set of (G_1' \oplus G_2')\circ (G_1 \oplus G_2) is given by (\Sigma _1 \& \Sigma _2) \otimes (\Sigma _1' \otimes \Sigma _2') For (G_1' \circ G_1) \oplus (G_2' \circ G_2), by (\Sigma _1 \otimes \Sigma _1') \& (\Sigma _2 \otimes \Sigma _2').

In the base, these are the same object \Sigma _1 \otimes \Sigma _2 \otimes \Sigma _1' \otimes \Sigma _2'. In the fiber, they are given respectively by (\overline {\Sigma _1} + \overline {\Sigma _2}) \otimes (\overline {\Sigma _1}' + \overline {\Sigma _2'}) and (\overline {\Sigma _1} \otimes \overline {\Sigma _1'}) + (\overline {\Sigma _2} \otimes \overline {\Sigma _2}'). Note the coproducts here are the fiberwise ones. There is an obvious lens from the former to the latter (given by the identity map on the base, and the inclusion of two summands in a fourfold coproduct---note that lenses go backwards in the fiber). Letting I \to (A_1 \oplus A_2) \otimes M, (C_1 \oplus C_2) \otimes M \to I be a context, and going through the definitions, it is clear that the resulting contexts for the former game factors as this lens followed by the context for the latter game. In other words, this lens is a reparametrization map between the two games. It suffices to verify it is an equivalence.

Unpacking the equivalence relation on (G_1' \oplus G_2')(G_1 \oplus G_2), note that (in all the possible contexts,) the signal to G_1 does not depend on the action of G_2' and vice versa, and so for G_1' and G_2. Hence they are in equilibrium if and only if they are in equilibrium in G_1'G_1 for the given context (conditioned on that branch), and similarly the other two. This proves the desired equivalence.

Example [efr-4CSL]

Consider the (Grothendieck) fibration \mathsf {Set}^\to \to \mathsf {Set}, which can be viewed as a Markov fibration. Let f: {\mathbb {R} \choose \Sigma } \otimes {\bar {X} \choose X} \leftrightarrows {\bar {Y} \choose Y} be a parameterized lens. Denote by \mathrm {argmax}_f the open game {\bar {X} \choose X} \to {\bar {Y} \choose Y} with parameters {\mathbb {R} \choose \Sigma }, underlying parameterized lens f, and equilibrium relation given by \mathrm {argmax}.

Then if g: {\mathbb {R} \choose \Sigma '} \otimes {\overline {X'} \choose X'} \leftrightarrows {\overline {Y'} \choose Y'} is another parameterized lens, we have \mathrm {argmax}_f \oplus \mathrm {argmax}_g \cong \mathrm {argmax}_{f \oplus g}, where by an abuse of notation f \oplus g denotes the paramterized lens {\mathbb {R} \choose \Sigma \times \Sigma '} \otimes ({\overline {X} \choose X} \oplus {\overline {X'} \choose X'}) \to {\overline {Y} \choose Y} \oplus {\overline {Y'} \choose Y'} given by distributing into the coproduct, then projecting into the relevant factor of the product \Sigma \times \Sigma ' and applying either f or g

A context for either of these games consists of an element of X + X' and a function k: Y + Y' \to \mathbb {R}. The external choice game can be seen as having two players, one who gets to play if the context chooses an element in X, who must output an element y \in Y and optimize k(y) (according to his private utility function \Sigma \times X \times \bar {Y} \to \mathbb {R}), the other playing when the input is in X' and who must choose an element in y'. The single argmax game can be seen as a single player, who is constrained to play inside the same "branch" of the game as the input (this constraint is encoded in the lens f \oplus g), and whose utility function is given by the first players' in the first branch, and the second players' in the second branch.x

Example [efr-BNT1]

Let G: {* \choose X} \to {R \choose Y} be a game, representing an agent who is optimizing the return value r \in R in some sense. Then G \otimes (1_I \oplus 1_I = 1_{I + I}) represents the same agent, whose payoff may now depend on an additional bit (a value in I + I), but whose decisions may not depend on that bit (his selection function may still depend on its distribution).

On the other hand, G \oplus G (\cong G \otimes 1_I \oplus G \otimes 1_I) represents the same situation, but where the player's strategy may depend on the bit---he provides two strategies \sigma _1,\sigma _2, one for each possibility.

This proves that \otimes does not distribute over \oplus