This is the second post in catching up on aspects of open-games-hs that are ahead of my papers, following open games with stateful payoffs. Subgame perfection has been an embarrassing thorn in my side since 2016 when I had to do major surgery on my PhD thesis because the category of “open games with subgame perfect equilibria” turned out to not be monoidal. Currently there are two approaches: One in iterated open games which is quite pragmatic and requires the “user” specifying an open game to manually mark where the subgames are by applying a functor; and one in morphisms of open games which I find very elegant but requires both an extra categorical dimension and an equivalent amount of effort by the “user”.

I always wanted an “automatic” approach to subgame perfection in open games, like I failed to do in my thesis – just draw the usual string diagram, and get subgame perfect equilibria out. I now have a way to do it, implemented in OpenGames.Engine.SubgamePerfect, which I’ll document here.

The starting point is an idea that doesn’t work. In the category of deterministic open games, a decision has strategy profiles , and equilibria given by . Here plays the role of the on-equilibrium subgame. Here is an idea that doesn’t work: instead define it by for all .

To see why this doesn’t work, form the game , where lifts the copy function. Given a context with history and continuation , its equilibrium condition is equivalent to and then to where . If we keep the true definition of then this is carefully balanced to give us Nash. But if we use our proposed modified definition, the equilibrium condition becomes for all . This is wrong – the subgame perfect equilibrium condition should be for all .

What is happening is that the context of should keep track of how a conterfactual change to its history, from the on-equilibrium subgame to an off-equilibrium subgame , should propagate to the continuation, which should change from to .

Fortunately we’re in luck. The heavy machinery developed in Bayesian open games is able to handle exactly this sort of situation. The first thought is to replace the category of stochastic maps with the category of relations. Pushing forward the state through the copy map yields the diagonal set , which contains exactly enough information to propagate a counterfactual change in one output backwards and then forwards again to the other output. That is to say, if we take the pushfoward state and condition on one output being some , the other output collapses to the same . This much is standard reasoning in the category of relations.

This is almost right, but not quite. We also need to keep track of what *actually* happens, and not just the counterfactual alternatives, in particular because they are still used for payoffs: a player’s preferences are indifferent to payoffs that might have occurred, but did not. We actually need to simultaneously keep track of 3 levels of possibility: (1) what *actually* happened, (2) what counterfactually *might have* happened, but did not, and (3) what *could not* have happened. Pushing forward through illustrates this well. If the input play is then what actually happens is , what could have happened is any element of , and any with could not have happened even counterfactually.

This motivates the following definition. Let be given by . I call the *pointed powerset monad*, and it is a hybrid of the identity and powerset monads. The monad unit is given by , and the multiplication by . admits monad morphisms to both identity and powerset. The kleisli category of is “pointed relations”: a kleisli morphism is a relation together with a function satisfying for all . Since is commutative, its kleisli category admits a monoidal product. (I’ve never seen this monad before in the literature.)

Fortunately we can save some work and *hack* this monad in Haskell by pretending that ordinary lists are pointed subsets, using the head as the basepoint. Nothing goes wrong as long as we are careful to only use lists in ways that are invariant under permutation and duplication (ie. we treat free monoids in ways that are also valid for free commutative idempotent monoids). All of the list monad operations are “head-preserving” in the appropriate way.

Just as for Bayesian open games, we set up coend optics for the kleisli category of this monad. In category theoretic notation a kleisli optic is an element of , and in Haskell notation it is an element of the GADT `data Optic x s y r where Optic :: (x -> [(a, y)]) -> (a -> r -> [s]) -> Optic x s y r`

. The type of contexts is also exactly as for Bayesian open games: it is an element of or `data Context x s y r where Context :: [(a, x)] -> (a -> y -> [r]) -> Context x s y r`

. The definition of the monoidal category of open games can be done generically for an arbitrary monad, so almost all of the code follows for free.

The *only* thing that needs to be specialised to the pointed powerset monad is the definition of a decision . This isn’t trivial. The set of strategies is still . For a strategy we must produce an optic . We take the bound variable to be , so the backward part is trivial and we need only give the view . We take , the pointed subset with basepoint . This means that what happens is , but any element of could happen counterfactually, because the agent has a free choice. (This is an unusually clear appearance of *free will* in mathematics.)

In Haskell I always write decisions to take an exhaustive list of possible moves as a parameter in order to brute force , because implementing a decent is an orthogonal problem. So the implementation of a decision begins:

```
decision :: [y] -> OG (x -> y) x () y Double
decision ys = OG {
play = \f -> let v x = zip (repeat ()) (f x : ys)
u () _ = [()]
in Optic v u
...
```

Here `f x : ys`

is the list representing the pointed subset .

Finally, we must evaluate a strategy in a context, which is a triple with and . Here we get right to the heart of what subgame perfection is all about: we ignore the factual part of and only use the set of counterfactuals, but we ignore the counterfactual part of and only use the factual. Specifically, the equilibrium condition is that for every , we have , where means the basepoint of . Information about is transferred to via , which is *entangled* with in the state .

In Haskell, the definition concludes:

```
...
equilibrium = \(Context h k) f ->
and [head (k a (f x)) >= head (k a y) | (a, x) <- h, y <- ys]}
```

And that’s it! I have no intention to *prove* that this always gives subgame perfect equilibrium any time soon – correctness proofs for open games are always extremely painful (they go by induction on extensive form) and I put them off as long as I realistically can. It passes the ultimatum game test, which is illustrated in OpenGames.Examples.SubgameTest. For me this is enough evidence to start using it first and ask questions later.