## Stream: maths

### Topic: question about game theory

#### Scott Morrison (Mar 29 2019 at 08:49):

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 (Mar 29 2019 at 08:51):

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 (Mar 29 2019 at 08:51):

what is an impartial game?

#### Scott Morrison (Mar 29 2019 at 08:53):

Not sure what the best references are:

#### Kevin Buzzard (Mar 29 2019 at 09:00):

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 (Mar 29 2019 at 09:03):

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 (Mar 29 2019 at 09:09):

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 (Mar 29 2019 at 09:10):

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 (Mar 29 2019 at 09:11):

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

#### Scott Morrison (Mar 29 2019 at 09:11):

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 (Mar 29 2019 at 09:12):

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 (Mar 29 2019 at 09:19):

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 (Mar 29 2019 at 09:23):

@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 (Mar 29 2019 at 09:23):

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

#### Johan Commelin (Mar 29 2019 at 09:23):

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

#### Scott Morrison (Mar 29 2019 at 09:23):

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 (Mar 29 2019 at 09:23):

Obviously they have different rule books.

#### Kevin Buzzard (Mar 29 2019 at 09:24):

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 (Mar 29 2019 at 09:24):

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

#### Mario Carneiro (Mar 29 2019 at 09:25):

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

#### Scott Morrison (Mar 29 2019 at 09:25):

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 (Mar 29 2019 at 09:25):

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

#### Mario Carneiro (Mar 29 2019 at 09:25):

because two chess' positions become one chess position

oh.

#### Mario Carneiro (Mar 29 2019 at 09:26):

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 (Mar 29 2019 at 09:26):

Depends on how much alcohol was consumed

#### Scott Morrison (Mar 29 2019 at 09:27):

(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 (Mar 29 2019 at 09:29):

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 (Mar 29 2019 at 09:29):

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

#### Kenny Lau (Mar 29 2019 at 09:29):

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 (Mar 29 2019 at 09:29):

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 (Mar 29 2019 at 09:30):

:-( I'm still confused, sorry.

#### Kevin Buzzard (Mar 29 2019 at 09:30):

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

#### Kevin Buzzard (Mar 29 2019 at 09:31):

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

ah :-)

#### Kevin Buzzard (Mar 29 2019 at 09:31):

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

#### Kevin Buzzard (Mar 29 2019 at 09:32):

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

#### Kenny Lau (Mar 29 2019 at 09:33):

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

#### Kevin Buzzard (Mar 29 2019 at 09:33):

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

#### Kenny Lau (Mar 29 2019 at 09:33):

or else they would be doing perfectoid spaces in Lean

#### Kevin Buzzard (Mar 29 2019 at 09:33):

Yes that's the one

#### Kevin Buzzard (Mar 29 2019 at 09:45):

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 (Mar 29 2019 at 09:47):

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 (Mar 29 2019 at 09:47):

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

#### Scott Morrison (Mar 29 2019 at 09:47):

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


#### Kevin Buzzard (Mar 29 2019 at 09:48):

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

#### Scott Morrison (Mar 29 2019 at 09:50):

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 (Mar 29 2019 at 09:51):

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 (Mar 29 2019 at 09:51):

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 (Mar 29 2019 at 09:52):

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 (Mar 29 2019 at 09:54):

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 (Mar 29 2019 at 09:54):

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

#### Kevin Buzzard (Mar 29 2019 at 09:54):

You have to be careful about the equivalence relation.

#### Kevin Buzzard (Mar 29 2019 at 09:54):

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

#### Scott Morrison (Mar 29 2019 at 09:55):

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

#### Kevin Buzzard (Mar 29 2019 at 09:55):

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

#### Kevin Buzzard (Mar 29 2019 at 09:55):

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 (Mar 29 2019 at 09:55):

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

#### Scott Morrison (Mar 29 2019 at 09:55):

exactly, same outcome, different combinatorial games

#### Kevin Buzzard (Mar 29 2019 at 09:56):

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 (Mar 29 2019 at 09:57):

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 (Mar 29 2019 at 09:58):

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.

#### Kevin Buzzard (Mar 29 2019 at 10:10):

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

#### Kevin Buzzard (Mar 29 2019 at 10:11):

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

#### Kevin Buzzard (Mar 29 2019 at 10:11):

(In the definition of game)

#### Kevin Buzzard (Mar 29 2019 at 10:13):

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 (Mar 29 2019 at 10:13):

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 (Mar 29 2019 at 10:14):

@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

it won't compile

#### Kevin Buzzard (Mar 29 2019 at 10:15):

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

#### Mario Carneiro (Mar 29 2019 at 10:15):

it is in mathlib, kenny

#### Kevin Buzzard (Mar 29 2019 at 10:15):

Take a look at Conway's definition in the book

#### Kenny Lau (Mar 29 2019 at 10:15):

that's what I mean

by "should"

#### Kevin Buzzard (Mar 29 2019 at 10:16):

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

#### Kenny Lau (Mar 29 2019 at 10:16):

English is confusing

#### Mario Carneiro (Mar 29 2019 at 10:17):

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

#### Mario Carneiro (Mar 29 2019 at 10:17):

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

#### Mario Carneiro (Mar 29 2019 at 10:17):

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

#### Kenny Lau (Mar 29 2019 at 10:17):

i.e. construct a model of ZFC-I

#### Kevin Buzzard (Mar 29 2019 at 10:34):

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 (Mar 29 2019 at 10:35):

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

#### Kevin Buzzard (Mar 29 2019 at 10:44):

Seems to me that

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


#### Kevin Buzzard (Mar 29 2019 at 10:45):

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 (Mar 29 2019 at 10:45):

But then there's an equivalence relation on these games

#### Kevin Buzzard (Mar 29 2019 at 10:56):

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 (Mar 29 2019 at 11:00):

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 (Mar 29 2019 at 11:28):

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 (Mar 29 2019 at 11:29):

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


#### Scott Morrison (Mar 29 2019 at 11:35):

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 (Mar 29 2019 at 11:35):

(This still doesn't work.)

#### Chris Hughes (Mar 29 2019 at 11:47):

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 (Mar 29 2019 at 11:57):

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

#### Johan Commelin (Mar 29 2019 at 11:57):

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

#### Scott Morrison (Mar 29 2019 at 11:58):

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

#### Scott Morrison (Mar 29 2019 at 11:59):

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 (Mar 29 2019 at 17:36):

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 (Mar 29 2019 at 17:44):

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

#### Mario Carneiro (Mar 29 2019 at 18:05):

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 (Mar 29 2019 at 18:08):

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

#### Mario Carneiro (Mar 29 2019 at 18:12):

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

#### Mario Carneiro (Mar 29 2019 at 18:12):

it seems pretty essentially set-theoretic

Last updated: May 10 2021 at 06:13 UTC