|
Comments
Summing combinatorial games
In the previous
post, we've introduced the concept of combinatorial game and
saw how we can employ a simple formalism to model all such games
uniformly, the game type. To see what this point of view can bring
us, we'll discuss the idea of summing combinatorial games, which can
be used to analyze games by decomposing them into smaller, simpler
ones. As we'll see, this notion has a straightforward computational
interpretation for the game type, making it convenient to
manipulate and reason about.
The intuition behind summing games is that they often evolve to a
point where they can be seen as several smaller ones being played
"simultaneously". In go, for instance, the board is progressively
partioned into different regions, and each player must choose in which
of those to play during their turn. This suggests a representation
where the state of a game is given by the product of the states of the
subgames. To make a move, a player modifies the state of one of the
subgames according to its rules, leaving the rest of the state
untouched.
To define the sum of two combinatorial games (as given by the
combinatorial_game type), we can simply combine the lists of moves
available for each game component. We must still show that this
results in a terminating game, but it suffices to observe that the
valid_move relation in this case is equivalent to the product of two
well-founded relations, and the Coq standard library provides lemmas
for dealing with this case.
Definition cg_pair_order {cg1 cg2} :=
symprod _ _ (valid_move cg1) (valid_move cg2).
Definition cg_pair_order_wf {cg1 cg2} : well_founded cg_pair_order :=
wf_symprod _ _ _ _ (finite_game cg1) (finite_game cg2).
Program Definition sum_cg (cg1 cg2 : combinatorial_game)
: combinatorial_game :=
{| position := position cg1 * position cg2;
moves p pos := map (fun pos1' => (pos1', snd pos))
(moves cg1 p (fst pos)) ++
map (fun pos2' => (fst pos, pos2'))
(moves cg2 p (snd pos)) |}.
Next Obligation.
match goal with
| |- well_founded ?R =>
assert (EQ : RelationClasses.relation_equivalence R cg_pair_order)
end.
(* ... *)
rewrite EQ.
apply cg_pair_order_wf.
Qed.
A problem with this definition is that it is not directly amenable
to computation. We can overcome this problem by defining game sums
directly over the game type. Since game is universal, we can hope
this should be enough to define what a sum of games is generically. A
naive adaptation doesn't work, as recursive calls to sum don't have
a single decreasing argument, e.g.
Fail Fixpoint sum (g1 g2 : game) : game :=
Game (map_game game_as_cg g1 Left (fun g1' P => sum g1' g2) ++
map_game game_as_cg g2 Left (fun g2' P => sum g1 g2'))
(map_game game_as_cg g1 Right (fun g1' P => sum g1' g2) ++
map_game game_as_cg g2 Right (fun g2' P => sum g1 g2')).
(* Error: Cannot guess decreasing argument of fix. *)
One solution is again to pair both arguments and use the Fix combinator
with cg_pair_order_wf. Manipulating proof terms in the recursive calls can be
made less awkward by using the simple refine tactic:
Definition sum (g1 g2 : game) : game.
simple refine (
Fix cg_pair_order_wf (fun _ => game)
(fun gs =>
match gs with
| (g1, g2) => fun sum =>
let sum_fst g1' P := sum (g1', g2) _ in
let sum_snd g2' P := sum (g1, g2') _ in
Game (map_game game_as_cg g1 Left sum_fst ++
map_game game_as_cg g2 Left sum_snd)
(map_game game_as_cg g1 Right sum_fst ++
map_game game_as_cg g2 Right sum_snd)
end) (g1, g2));
clear - P; constructor; trivial.
Defined.
As with all definitions involving Fix, we must now prove a lemma
that shows how sum unfolds. The proof is very similar to the one of
embed_in_game_eq, and is thus omitted.
Lemma sum_eq (g1 g2 : game) :
sum g1 g2 =
Game (map (fun g1' => sum g1' g2) (left_moves g1) ++
map (fun g2' => sum g1 g2') (left_moves g2))
(map (fun g1' => sum g1' g2) (right_moves g1) ++
map (fun g2' => sum g1 g2') (right_moves g2)).
The name sum suggests that combinatorial games could behave like
numbers. We won't discuss this correspondence in much detail for now,
but some interesting identities do show up already:
Lemma zero_plus_zero : sum zero zero = zero.
Lemma one_plus_zero : sum one zero = one.
Showing that sum correctly computes what it should is not
difficult: we proceed by well-founded induction combining simple
lemmas about the behavior of sum, embed_in_game, and map. We
need an auxiliary result that allows us to apply our inductive
hypothesis:
Lemma map_ext_strong :
forall {A B}
(l : list A)
(f g : A -> B)
(EXT : forall x, In x l -> f x = g x),
map f l = map g l.
The statement of lemma just says that embed_in_game exchanges
sum and sum_cg.
Lemma sum_is_sum (cg1 cg2 : combinatorial_game)
(pos1 : position cg1) (pos2 : position cg2) :
embed_in_game (sum_cg cg1 cg2) (pos1, pos2) =
sum (embed_in_game cg1 pos1) (embed_in_game cg2 pos2).
Proof.
remember (pos1, pos2) as pos.
replace pos1 with (fst pos) by (destruct pos; simpl; congruence).
replace pos2 with (snd pos) by (destruct pos; simpl; congruence).
clear.
induction pos as [[pos1 pos2] IH]
using (well_founded_ind cg_pair_order_wf).
rewrite embed_in_game_eq, sum_eq. simpl.
repeat rewrite (embed_in_game_moves _ _ Left).
repeat rewrite (embed_in_game_moves _ _ Right).
repeat rewrite map_app. repeat rewrite map_map.
do 2 f_equal;
apply map_ext_strong; intros pos IN; apply IH; constructor; eexists; eauto.
Qed.
In the next posts, we will see how to use this machinery when
decomposing games as sums and comparing subgames.