pre-games

Stream: general

[Kenny Lau]

this is the definition of a pre-game in set_theory/pgame:

inductive pgame : Type (u+1)
| mk : ∀ α β : Type u, (α → pgame) → (β → pgame) → pgame

Should α and β be interpreted as the moves Left and Right have? If so, what should I do if the moves Right has depends on what Left does?

[Johan Commelin]

That's a dependent pgame :grinning_face_with_smiling_eyes: :oops:

[Johan Commelin]

@Kenny Lau The joy of alphas and betas all over the library (-;

[Kenny Lau]

also, how overlapping would my work be if I wanted to formalize the Sprague–Grundy theorem?

[Kevin Buzzard]

what should I do if the moves Right has depends on what Left does?

Does this make sense?

[Kevin Buzzard]

The idea of a Conway-like game is that it is a position but it doesn't come with a fixed concept of "whose move it is"

[Kenny Lau]

can it be both player's turn in the same pre-game? maybe this is the interpretation

[Kenny Lau]

aha, I didn't know that

[Kevin Buzzard]

Think of a chess position

[Kevin Buzzard]

But no indication of whose move it is

[Kevin Buzzard]

Alpha is the list of legal white moves, beta the list of legal black moves

[Kenny Lau]

ok, thanks

[Kenny Lau]

then I should really start by defining impartial games

[Bryan Gin-ge Chen]

Impartial games would make a nice addition. I don't know if @Scott Morrison has already done something along these lines.

[Kenny Lau]

I'm planning to make Nim a kata

[Kenny Lau]

like the one-heap Nim

[Kevin Buzzard]

Nice

[Kevin Buzzard]

To play dots and boxes you need to know about poker nim

[Kevin Buzzard]

Where you can add to a pile as well

[Scott Morrison]

I didn't ever do impartial games (that I can remember??)

[Kenny Lau]

@Scott Morrison I think Kevin was just worried about maybe one of you guys have some private repo

[Kenny Lau]

inductive impartial_pgame : Type (u+1)
| mk : ∀ α : Type u, (α → impartial_pgame) → impartial_pgame

def impartial_pgame.to_pgame : impartial_pgame.{u} → pgame.{u}
| (impartial_pgame.mk α f) := ⟨α, α, λ x, (f x).to_pgame, λ x, (f x).to_pgame⟩