Zulip Chat Archive

Stream: maths

Topic: question about game theory


view this post on Zulip 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.

view this post on Zulip 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...?

view this post on Zulip Kenny Lau (Mar 29 2019 at 08:51):

what is an impartial game?

view this post on Zulip Scott Morrison (Mar 29 2019 at 08:53):

Not sure what the best references are:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:07):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 29 2019 at 09:23):

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

view this post on Zulip Johan Commelin (Mar 29 2019 at 09:23):

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

view this post on Zulip 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'.

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:23):

Obviously they have different rule books.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 29 2019 at 09:25):

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

view this post on Zulip 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?)

view this post on Zulip Mario Carneiro (Mar 29 2019 at 09:25):

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

view this post on Zulip Mario Carneiro (Mar 29 2019 at 09:25):

because two chess' positions become one chess position

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:26):

oh.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 29 2019 at 09:26):

Depends on how much alcohol was consumed

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:29):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:30):

:-( I'm still confused, sorry.

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:30):

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:31):

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

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:31):

ah :-)

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:31):

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:32):

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

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:32):

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

view this post on Zulip Kenny Lau (Mar 29 2019 at 09:33):

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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Mar 29 2019 at 09:33):

or else they would be doing perfectoid spaces in Lean

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:33):

Yes that's the one

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:47):

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

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:47):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-(

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:54):

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:54):

You have to be careful about the equivalence relation.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 09:55):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:55):

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

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:55):

exactly, same outcome, different combinatorial games

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 29 2019 at 09:58):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:11):

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:11):

(In the definition of game)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 29 2019 at 10:14):

it won't compile

view this post on Zulip Kenny Lau (Mar 29 2019 at 10:14):

this had been discussed before

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:15):

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

view this post on Zulip Mario Carneiro (Mar 29 2019 at 10:15):

it is in mathlib, kenny

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:15):

Take a look at Conway's definition in the book

view this post on Zulip Kenny Lau (Mar 29 2019 at 10:15):

that's what I mean

view this post on Zulip Kenny Lau (Mar 29 2019 at 10:15):

by "should"

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:16):

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

view this post on Zulip Kenny Lau (Mar 29 2019 at 10:16):

English is confusing

view this post on Zulip Mario Carneiro (Mar 29 2019 at 10:17):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 29 2019 at 10:17):

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

view this post on Zulip Kenny Lau (Mar 29 2019 at 10:17):

i.e. construct a model of ZFC-I

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:35):

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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:44):

Seems to me that

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 10:45):

But then there's an equivalence relation on these games

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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
    (L₁.map(λ G, add G G₂) ++ L₂.map(λ G, add G₁ G))
    (R₁.map(λ G, add G G₂) ++ R₂.map(λ G, add G₁ G))

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 29 2019 at 11:35):

(This still doesn't work.)

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 29 2019 at 11:57):

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

view this post on Zulip Johan Commelin (Mar 29 2019 at 11:57):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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  _)

view this post on Zulip Kevin Buzzard (Mar 29 2019 at 17:44):

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

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip Mario Carneiro (Mar 29 2019 at 18:12):

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

view this post on Zulip Mario Carneiro (Mar 29 2019 at 18:12):

it seems pretty essentially set-theoretic


Last updated: May 10 2021 at 06:13 UTC