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.