question about game theory

Stream: maths

[Scott Morrison]

Anyone here know the basics of combinatorial game theory? I don't understand why chess is not an impartial game. I want to consider chess as consisting of a normal chess board, along with a two-sided token, with sides black and white, which starts white side up. On each turn, a player moves a piece of the colour shown on the token (according to the usual rules of chess), and then flips the token over.

[Scott Morrison]

This interpretation of chess behaves differently under sum of games than "normal chess" does, but nevertheless, it still seems to be a perfectly reasonable description of chess as an impartial game...?

[Kenny Lau]

what is an impartial game?

[Scott Morrison]

Not sure what the best references are:

• https://mathigon.org/world/resources/Game_Theory/Combinatoial_Game_Theory.pdf
• http://web.mit.edu/sp.268/www/nim.pdf
• https://en.wikipedia.org/wiki/Impartial_game

[Kevin Buzzard]

It's not an impartial game because the winner of the game is "the person controlling the black pieces" or "the person controlling the white pieces", not "the person who happens to have made a move corresponding to to black when black won the game" or anything like that.

[Johan Commelin]

But in Scott's Chess' it is just the last player who could make a valid move that wins. You lose if you can't make a valid move.

[Scott Morrison]

I either don't understand your objection, Kevin, or agree that Johan's reply answers it.

[Scott Morrison]

Another example could be "tic-tac-toe" or "noughts-and-crosses" as an impartial game. Again there is a token (labelled "noughts" and "crosses" on the two sides) which is flipped after each move. On a players turn, if there is not already a line of three marks of the opposite symbol already on the board, they must add one mark of the current symbol to an unfilled square.

[Scott Morrison]

I think that is an impartial description of noughts and crosses. (Except that all draws are converted into 1st player wins, because whoever goes second in a drawn game will have no where to put their 5th mark.)

[Kenny Lau]

if you formalize impartial games and chess in Lean then maybe I can try to prove it :P

[Scott Morrison]

Notice that these games behave very differently under sum of games than the usual versions of chess and noughts and crosses do, which is I think why people don't usually say they are impartial.

[Scott Morrison]

I'd been thinking this was a great student project, but I've had this nagging worry I don't understand anything because of not understanding this "chess is not impartial" claim.

[Kevin Buzzard]

If you just regard a game like nim or noughts and crosses as a finite tree of possibilities (and make up some arbitrary rule as to who wins in the event of a tie in noughts and crosses) then of course you can evaluate every position, when considered a regular 2-player game, as a winning or a losing position, and then you can assign nimbers to every node on the tree and there you have it, nim theory applies. This would work for any game for which the game tree is finite. So in this weak sense every game is equivalent to an impartial game.

[Johan Commelin]

@Kevin Buzzard I think Scott is trying to use transport of structure. He has an equiv X =~ Y. Both sides are games, and the equiv seems to respect structure. One of them is impartial, so the other should also be impartial. That's our promise, our mathematician's honour code, right?

[Johan Commelin]

So somewhere this breaks down. But I don't see where.

[Johan Commelin]

Probably because I don't know what a game is.

[Scott Morrison]

So what is the stronger equivalence relation? I guess I'm failing to conceive of a definition of game that distinguishes Chess and Chess'.

[Scott Morrison]

Obviously they have different rule books.

[Kevin Buzzard]

But this is a step in the wrong direction, at least as far as combinatorial game theory goes. You can drop requirements about the normal play rule, you can consider games with "scores" such as dots and boxes, where the winner is not the player who moves last but the player with the biggest score -- all these games are just people wandering around a game tree, and every game tree can be made into an impartial game, but then I think you're throwing away the structure which Conway et al want to analyse.

[Johan Commelin]

You should go back to writing iso_induction. Then Lean can tell you the answer to your question.

[Mario Carneiro]

I think you are right Scott, but adding the token changes the game

[Scott Morrison]

okay -- but on the "score" issue --- don't you just say that there is a second phase in dots and boxes, where we take turns "counting" our captured squares? (so whoever captured fewer loses once they don't have a next one to count?)

[Mario Carneiro]

that is, it's not an isomorphism because it's not a bijection

[Mario Carneiro]

because two chess' positions become one chess position

[Scott Morrison]

oh.

[Mario Carneiro]

Another way to put it is, if we are playing chess, then stop and have lunch and come back, will we know who should continue?

[Johan Commelin]

Depends on how much alcohol was consumed

[Scott Morrison]

(friends at Berkeley would sometimes just continue their game over lunch, as they apparently didn't need the board or the pieces, let alone the damn token)

[Scott Morrison]

I'm not exactly sure what "two chess' positions become one chess position" means. I haven't been thinking of a game as a "set of positions". I thought a game is just a list of games.

[Scott Morrison]

(i.e. when you make a move, you've entered a new game)

[Kenny Lau]

is there a coordinated dance move that, after performing, will not change the chess board but render the opposite player the one to play?

[Kevin Buzzard]

The way chess or dots and boxes are played normally does not conform with the impartial combinatorial game theory story, but there's nothing to stop you playing them that way. They just become different games, so combinatorial game theory applied in this way will tell you nothing about chess played the usual way

[Scott Morrison]

:-( I'm still confused, sorry.

[Kevin Buzzard]

Combinatorial game theory is all about higher invariants beyond who is going to win

[Kevin Buzzard]

So it can tell you things about chess which nobody cares about

[Scott Morrison]

ah :-)

[Kevin Buzzard]

Such as what happens if we change the motivation of the players

[Kevin Buzzard]

Noam Elkies wrote an article about combinatorial game theory applied to chess

[Scott Morrison]

https://arxiv.org/abs/math/9905198 ?

[Kenny Lau]

pretty sure people who play chess have no motivation to start with :P

[Kevin Buzzard]

Not considered as an impartial game, but this whole issue of "how many moves ahead am I"

[Kenny Lau]

or else they would be doing perfectoid spaces in Lean

[Kevin Buzzard]

Yes that's the one

[Kevin Buzzard]

The difference between Elkies' analysis and what Scott is suggesting is that Elkies is considering the game in the following form: if black chooses to play in another game then white can choose to play a move on the board with their white pieces, even if white played last. With Scott's modification the moves would be forced to alternate. In the unlikely event that a game of chess does split up into two completely independent subgames then it's Elkies' interpretation which would be the correct one.

[Scott Morrison]

Ah, okay, I think I understand. This agrees with what I said above:

Notice that these games behave very differently under sum of games than the usual versions of chess and noughts and crosses do

[Scott Morrison]

(Man, I am trying really hard not to write this grant review tonight...)

[Scott Morrison]

inductive game : Type
| intro : Π L R : list game, game

[Kevin Buzzard]

Did you look at ONAG? That's the place to read about how to formalise the theory

[Scott Morrison]

In Chess, the lists L are R are different. In Chess', they are the same. The same player wins in either, but everything else is different.

[Scott Morrison]

Earlier I had just been missing that the definition of a game consisted of _two_ sets of moves, one for L and one for R.

[Kevin Buzzard]

By the way, Elkies' claim that combinatorial game theory has something to say about dots and boxes has not really stood the test of time. Many of the top players now know nothing at all about combinatorial game theory, they just know Euler's formula.

[Scott Morrison]

Oh, and that definition I gave is wrong, of course. It should be something like

import data.finset

inductive game : Type
| intro : Π L R : finset game, game

but that isn't allowed :-(

[Kevin Buzzard]

In Chess, the lists L are R are different. In Chess', they are the same. The same player wins in either, but everything else is different.

Aah, excellent! This is the correct answer: I was somehow edging towards it but this answer is much better. I should re-read ONAG now I know about Lean!

[Scott Morrison]

I guess we'll just have some equivalence relations later.

[Kevin Buzzard]

You have to be careful about the equivalence relation.

[Kevin Buzzard]

The same player wins in Chess and Chess'. But if that's your equivalence relation then there are only two games.

[Scott Morrison]

Apparently it is: G and G' are equivalent if G+H has the same outcome as G'+H for all impartial H.

[Kevin Buzzard]

It's a bit like bool and Prop ;-)

[Kevin Buzzard]

Apparently it is: G and G' are equivalent if G+H has the same outcome as G'+H for all impartial H.

Aah but then Chess and Chess' won't be equivalent at all.

[Scott Morrison]

(And impartial now has a clear meaning: L = R (... perhaps up to a permutation))

[Scott Morrison]

exactly, same outcome, different combinatorial games

[Kevin Buzzard]

I am now slightly annoyed that I am not going to work today -- my copy of ONAG is sitting on my shelf in my office.

[Mario Carneiro]

Oh, and that definition I gave is wrong, of course. It should be something like

import data.finset

inductive game : Type
| intro : Π L R : finset game, game

but that isn't allowed :-(

That's one thing that the QPF stuff should support!

[Kevin Buzzard]

Scott, this is exactly the sort of mathematics that people who like computer science are into. It would not surprise me if this stuff had all been formalised before in another prover.

[Scott Morrison]

QPF? Ah: https://lean-forward.github.io/lean-together/2019/slides/avigad.pdf

[Kevin Buzzard]

Scott -- this might be a really good project for your students. I searched online and nothing immediately jumped out at me

[Kevin Buzzard]

How come list game is allowed but finset game is not?

[Kevin Buzzard]

(In the definition of game)

[Kevin Buzzard]

You could define a game_aux with lists and then put some equivalence relation on it and then make the constructor and eliminator that you want

[Kenny Lau]

I feel obligatory to note that the version with one node instead of two nodes is the hereditarily finite sets and should be in mathlib

[Kevin Buzzard]

@Kenny Lau can you get Scott's definition to compile? The empty game is a game and all other games can be built using what Scott says. I think. Find a copy of Conway's "On numbers and games" to check the formal definition

[Kenny Lau]

it won't compile

[Kenny Lau]

this had been discussed before

[Kevin Buzzard]

But can you make it already? Wait -- I think all numbers are games too

[Mario Carneiro]

it is in mathlib, kenny

[Kevin Buzzard]

Take a look at Conway's definition in the book

[Kenny Lau]

that's what I mean

[Kenny Lau]

by "should"

[Kevin Buzzard]

I wish I could remember this stuff better, it's been a while

[Kenny Lau]

English is confusing

[Mario Carneiro]

it is set_theory.lists, although it hasn't been developed much

[Mario Carneiro]

I wanted to make a setting for naive set theory like you might find in Kevin's problem sets

[Mario Carneiro]

for stuff like {2, {3, 4}, {}}

[Kenny Lau]

i.e. construct a model of ZFC-I

[Kevin Buzzard]

It seems to us, however, that mathematics has now reached the stage where
formalisation within some particular axiomatic set theory is irrelevant,
even for foundational studies. It should be possible to specify conditions on a
mathematical theory which would suffice for embeddability within ZF
(supplemented by additional axioms of infinity if necessary), but which do
not otherwise restrict the possible constructions in that theory. Of course the
conditions would apply to ZF itself, and to other possible theories that have
been proposed as suitable foundations for mathematics (certain theories of
categories, etc.), but would not restrict us to any particular theory. This
appendix is in fact a cry for a Mathematicians' Liberation Movement!
Among the permissible kinds of construction we should have:
(i) Objects may be created from earlier objects in any reasonably con-
constructive fashion.
(ii) Equality among the created objects can be any desired equivalence
relation.

From ONAG, appendix to part 0. (i) says he wants a calculus of inductive constructions. (ii) says he wants to be able to transport certain constructions along equivalence relations. That's what I want too.

[Kevin Buzzard]

ONAG := Conway, "On numbers and games".

[Kevin Buzzard]

Seems to me that

inductive game : Type
| intro : Π L R : set game, game

[Kevin Buzzard]

And so you can start by constructing the zero game by letting L and R be the empty set. Notation G = {L|R} for game.intro L R

[Kevin Buzzard]

But then there's an equivalence relation on these games

[Kevin Buzzard]

Two games G and H have the same _value_ if G - H = 0; G - H is defined to be G+(-H), -{L|R} is defined to be {R|L}, addition is defined recursively with {GL|GR}+{HL|LR}={{g+H : g in GL} union {G+h : h in HL}|{g+H : g in GR} union {G+h : h in HR}}, and G=0 is defined to mean that the game is a second player win.

[Kevin Buzzard]

The winner of a game is defined recursively. Why can't I implement this all in Lean? Is it too wacky to be an inductive type?

[Scott Morrison]

It seems pretty reasonable. Lean compiles the inductive type a bit strangely. Defining addition requires some work to prove well-foundedness, but doesn't seem impossible.

[Scott Morrison]

inductive game : Type
| intro : Π L R : list game, game

def game.L : game → list game
| (game.intro L R) := L
def game.R : game → list game
| (game.intro L R) := R

instance : has_neg game :=
{ neg := λ G, game.intro G.R G.L }

-- fails with well-foundedness errors:
def add : game → game → game
| G₁@(game.intro L₁ R₁) G₂@(game.intro L₂ R₂) :=
  game.intro
    (L₁.map(λ G, add G G₂) ++ L₂.map(λ G, add G₁ G))
    (R₁.map(λ G, add G G₂) ++ R₂.map(λ G, add G₁ G))

[Scott Morrison]

I think we'd want to define list.map_mem, to get the sizeof inequalities. Something like:

def list.map_mem {α β : Type} : Π (L : list α) (f : Π a : α, a ∈ L → β), list β
| [] f := []
| L@(h :: t) f := f h (by simp) :: (list.map_mem t (λ a h, f a (or.inr h)))

def add : game → game → game
| G₁@(game.intro L₁ R₁) G₂@(game.intro L₂ R₂) :=
  game.intro
    (L₁.map_mem(λ G h, add G G₂) ++ L₂.map_mem(λ G h, add G₁ G))
    (R₁.map_mem(λ G h, add G G₂) ++ R₂.map_mem(λ G h, add G₁ G))

so now at the recursive site we have h : G ∈ L₁, etc.

[Scott Morrison]

(This still doesn't work.)

[Chris Hughes]

Ages ago I was playing around with this and wrote this file. https://github.com/ChrisHughes24/leanstuff/blob/master/game.lean I did define what it means for a position to be winning, and there's an unfinished proof of the winning strategy for the game discussed in this video https://www.youtube.com/watch?v=9KABcmczPdg I also started to define noughts and crosses.

[Scott Morrison]

Here's where I got to: https://gist.github.com/semorrison/8d9d72be5b89bc57c02a7c0f1e32a5ed

[Johan Commelin]

Awww, no syntax highlighting. I can't parse Lean without it :confounded:

[Scott Morrison]

I successfully defined addition of games using the definition above, and a very hackish tactic to proving monotonicity of the recursion.

[Scott Morrison]

Presumably a generic version of lemma game.sizeof_mem (L : list game) (G : game) (h : G ∈ L) : game.sizeof G < sizeof L := is already available somewhere?

[Mario Carneiro]

Seems to me that

inductive game : Type
| intro : Π L R : set game, game

It's in theory possible to have this inductive with finset. With set it's inconsistent:

import logic.function

constant game : Type
constant game.intro : set game → set game → game
constant {u} game.rec {C : game → Sort u} :
  (∀ L R, C (game.intro L R)) → ∀ g, C g
axiom {u} game.rec_eq {C : game → Sort u}
  (H : ∀ L R, C (game.intro L R)) (L R) :
  game.rec H (game.intro L R) = H L R

def game.right : game → set game := game.rec (λ L R, R)
theorem game.right_eq (L R) : (game.intro L R).right = R := game.rec_eq _ _ _

example : false :=
@function.cantor_injective game (game.intro ∅) $
λ R R' e,
  (game.right_eq ∅ _).symm.trans $
  (congr_arg game.right e).trans (game.right_eq ∅ _)

[Kevin Buzzard]

Hmm. game is a proper class, so Cantor's diagonal argument does not apply.

[Mario Carneiro]

Have you heard of the hypergame paradox? There is actually a contradiction lurking, and it has to do with thinking that there is only one type of all games. Saying it's a proper class doesn't save you, it only reinterprets what set game means

[Kevin Buzzard]

right -- I don't want to allow an arbitrary collection of games -- only collections "small enough to be sets".

[Mario Carneiro]

I think you have to do some kind of pSet like construction to get that

[Mario Carneiro]

it seems pretty essentially set-theoretic