In this post, I will begin to formalize a small part of combinatorial game theory using Coq. Combinatorial game theory attempts to model sequential, deterministic games between two players, both of which take turns causing the game state to change. It restricts itself to perfect information games, where the current configuration of the game is known to both players. Thus, it can be used to study games such as chess, tic-tac-toe, and go, but not games such as poker or blackjack. The power of combinatorial game theory comes from abstracting away details that are too specific to each game, such as whether it is played moving pieces on a board, how the pieces can move, etc. It defines a single mathematical object that can represent all games uniformily, allowing us to study general situations that could occur in many kinds of games. In this post, I will present this representation and discuss why it makes sense. I will start with a more intuitive formalization of combinatorial games, and then show how combinatorial game theory applies to all of those.

Defining combinatorial games

In combinatorial games, players are traditionally called left and right.

Each combinatorial game has a set of positions. In chess, for instance, a position is a chess board with black and white pieces on it. The rules of the game determine which moves are available to each player at a given position. They also describe how the game ends, and which player wins in that case. To simplify our analysis, we will assume that games end when some player must play but has no moves left, in which case the other player wins. This frees us from having to model how matches end separately for each game. We will also consider only finite games, i.e. ones that can't be played indefinitely. Notice that these two assumptions taken together, strictly speaking, rule out many interesting games: chess can end in a draw, something that can't happen in our model. Translating the above requirements into code results in the following definition:

To formalize how games are played, we define a predicate Match cg first winner m that represents a match of game cg where player first starts and player winner wins. m is the sequence of positions traversed during the match, from first to last.

In the Match_end clause, we check that the current player has no moves left. In Match_move, we check that the current player can make a move and that the match can then proceed with the other positions.

A universal game

We will now define a combinatorial game that is, in a precise sense to be explained later, the most general one. This is what combinatorial game theory uses to study combinatorial games. The crucial observation is that in the definition of Match we only care about the moves that can be made from a given position, but not about what the positions themselves are. This suggests a definition where each position is just a pair of sets, one for each player's moves. This forms the type game of games.

Each position in this game can be pictured as an arbitrarily-branching tree with two sets of children. On each player's turn, they choose one child in their set of moves to be the new position, and lose if they can't choose anything. The simplest game is zero, where both players have no moves available. It is a game where the first player always loses.

Using zero we can define star, where the first player always wins by making a move to zero.

A small variation gives us one and minus_one, where Left and Right always win, respectively.

It should be possible to encapsulate game in a combinatorial_game record. Defining moves is simple, but proving that games are finite requires some additional work. The nested inductive in the definition of game makes Coq generate an induction principle that is too weak to be useful:
game_ind
     : forall P : game -> Prop,
       (forall left_moves right_moves : list game,
        P {| left_moves := left_moves; right_moves := right_moves |}) ->
       forall g : game, P g

The usual solution is to define a new one by hand that gives us induction hypotheses to use:

Using this principle, we can now prove that games always terminate and define a combinatorial_game for game.

Game embeddings

I claimed that game is the most general combinatorial game. One way of seeing this is that we lose no information by representing each position in a combinatorial game as the tree of all possible moves, and such a tree can always be encoded as a game. To make this intuition formal, we can define a notion of game embedding between two combinatorial games. This will be a mapping between the positions of each combinatorial game that preserves matches. Thus, if we have an embedding of cg1 into cg2, then we can study cg1 matches by regarding them as cg2 matches.

With this notion of game embedding, combinatorial games form a category. I will now show that every combinatorial game can be embedded in game, making game a terminal object in this category and the most general combinatorial game. In this formulation, it is only a weakly terminal object (i.e., embeddings are not unique), as we are using Coq lists to represent sets. To embed an arbitrary combinatorial game into game, we can define a function by well-founded recursion over the proof that games are finite. In order to do this, we need a higher-order function map_game that allows us to perform a well-founded recursive call on a list of next moves. map_game acts like map, but passes to its argument function a proof that the element is a valid_move.

Using this function and the Fix combinator in the standard library, we write a generic embedding function embed_in_game. Like a regular fixpoint combinator, Fix takes a function that does a recursive call by applying its argument (here, F). The difference is that this argument must take a proof that shows that the recursive call is valid. The behavior of embed_in_game is simple: it calls itself recursively for each possible next position, and includes that position in the set of moves of the appropriate player.

Definitions that use Fix can be hard to manipulate directly, so we need to prove some equations that describe the reduction behavior of the function. I've hidden some of the auxiliary lemmas and proofs for clarity; as usual, you can find them in the original .v file. The proof that we can unfold embed_in_game once uses the Fix_eq lemma in the standard library.

With this lemma, we can show that moves and embed_in_game commute.

We are now ready to state and prove our theorem: every combinatorial game can be embedded in game.

Summary

We've developed the foundations of combinatorial game theory, showing how it can model combinatorial games in a simple yet general way. We haven't explored yet how to use this representation in practice to study games, something I plan to do on future posts. Update: I'll leave the list of posts in this series here.

• Summing combinatorial games