Poset games

Stream: maths

[Violeta Hernández]

I think we have all the necessary tools in Mathlib to start formalizing some concrete families of games. Perhaps the simplest one to begin with would be poset games.

[Violeta Hernández]

Two well-known examples of Poset games are chomp and Hackenbush with only green edges

[Violeta Hernández]

I have a question about this definition though, what would the required conditions on the poset be in order to have a finite game?

[Violeta Hernández]

I think (but I'm not 100% sure) that they'd be that the order is a well quasi-order

[Violeta Hernández]

Do we already have wqos in Mathlib? If not, what would be the easiest way to define them?

[Violeta Hernández]

@Yaël Dillies Do we perhaps have something like "all antichains are finite"? If so, we can define a wqo as just Preorder α + WellFoundedLT α + FiniteAntichains α

[Violeta Hernández]

@Tristan Figueroa-Reid you were interested in this too

[Daniel Weber]

Violeta Hernández said:

Do we already have wqos in Mathlib? If not, what would be the easiest way to define them?

I think it's docs#Set.PartiallyWellOrderedOn

[Violeta Hernández]

It seems potentially annoying that this is a predicate on sets rather than a predicate on types

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think (but I'm not 100% sure) that they'd be that the order is a well quasi-order

I believe so as well. I was also interested in applying the strategy stealing argument for posets with an infimum to show that the left player always wins those games.

[Violeta Hernández]

"posets with an infimum" is that the same as an OrderBot?

[Kim Morrison]

Violeta Hernández said:

It seems potentially annoying that this is a predicate on sets rather than a predicate on types

Yes, I encountered the same thing a long time back. (Something Grobner basis related...?)

[Violeta Hernández]

I guess that turning predicates on subtypes into predicates of sets are a common enough pattern, e.g. docs#Set.Countable

[Violeta Hernández]

But PartiallyWellFoundedOn is a set predicate without a corresponding type predicate

[Daniel Weber]

Violeta Hernández said:

"posets with an infimum" is that the same as an OrderBot?

Isn't that docs#SemilatticeInf ?

[Violeta Hernández]

Perhaps that can be a first PR? Defining PartiallyWellFounded for types and copying over the API

[Violeta Hernández]

To then redefine PartiallyWellFoundedOn as the predicate on the subtype

[Daniel Weber]

Please request my review when you make this PR, as I'm working with PartiallyWellFoundedOn for Kruskal's theorem

[Bas Spitters]

The Nim game was formalized in Coq:
https://yubocai-poly.github.io/project/203/

You might also enjoy Coqoban, a Coq version of Sokoban, which Jasper did some twenty years ago.
https://github.com/coq-community/coqoban
https://en.wikipedia.org/wiki/Sokoban

We used it as a basis for a graphical calculator in Coq.
Russell O’Connor. A Computer Verified Theory of Compact Sets. SCSS 2008, RISC-Linz Report Series 08–08: 148–162, Jul 2008, Proceedings
http://www.risc.uni-linz.ac.at/publications/download/risc_3448/SCSS2008_Proceedings.pdf

[Tristan Figueroa-Reid]

On the topic of different games, after poset games, it may be valuable to formalize:

• Red-Blue-Green Hackenbush for its (potential?) construction of every game
• Octal games and Wythoff's game for their expanded theory within combinatorial game theory

It would also be interesting to formalize games that are already weakly solved, like Cram. There are some strongly solved positional games, but I don't believe we have the theory to formalize them yet.

[Violeta Hernández]

We already have Nim and Sprague-Grundy in Mathlib too: docs#SetTheory.PGame.nim

[Violeta Hernández]

It's one-pile nim, though obviously multiple-pile nim is just a sum of one-pile nim games. I've also formalized the fact that nim a + nim b ≈ nim (∗a + ∗b) (the nim sum of piles is the nimber sum)

[Violeta Hernández]

Daniel Weber said:

Please request my review when you make this PR, as I'm working with PartiallyWellFoundedOn for Kruskal's theorem

Will do!

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I have to admit that I'm a bit suspicious of the current docs#PartiallyWellOrderedOn definition. Like, it's mathematically correct, but it's a very different definition in nature to the one that we use for docs#WellFounded.

Is there no way to come up with some inductive predicate that captures partial well-orders in the same way docs#Acc captures well-foundedness? That might potentially make proofs a bit easier, or at least more homologous with well-foundedness proofs.

[Violeta Hernández]

(of course, the current definition should be a theorem no matter what we end up doing with the PWF API)

[Violeta Hernández]

Actually, I think I'm a bit confused. Wikipedia says ℤ is not a PWO because it's not well-founded. But Lean proves as docs#partiallyWellOrderedOn_iff_finite_antichains that a set is PWO iff all its antichains are finite. So shouldn't any linear order be PWO?

[Violeta Hernández]

Oh of course the Lean lemma assumes a symmetric relation (so, not an order relation)

[Violeta Hernández]

I think I need to play a bit with the concept and the API. I'll be back once I have a more informed opinion on all of this

[Violeta Hernández]

Also new thread for PWOs: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Partial.20well-orders/near/485168962

[Violeta Hernández]

I just realized the name docs#Set.PartiallyWellOrderedOn isn't even correct! A well partial-order (not a partial well-order) is a partial well quasi-order, whereas this definition does not require antisymmetry.

[Bernhard Reinke]

Tristan Figueroa-Reid said:

On the topic of different games, after poset games, it may be valuable to formalize:

• Red-Blue-Green Hackenbush for its (potential?) construction of every game
• Octal games and Wythoff's game for their expanded theory within combinatorial game theory

It would also be interesting to formalize games that are already weakly solved, like Cram. There are some strongly solved positional games, but I don't believe we have the theory to formalize them yet.

Hi, I would be interested in the formalization of Octal games (or slightly more generally, Impartial take and break games), but I am not sure whether it would be good to start now of wait a bit until the IGame vs PGame issue has been settled. Or did somebody else already start working on this?

[Tristan Figueroa-Reid]

I don't think anyone else is working on it. I would say it's safe to work on as long as you work with Game, but there's still a good chance you might have to refactor a little after the IGame PR is merged.

[Bernhard Reinke]

Hm, I think one way to proceed would be to go into a similar direction as State.lean, but introduce one more level of Finset in the options. In that file, the target is PGame. If I want to work with Finset, it would be nice if a finite summation of games with indexing set is possible. It is not clear to my if this works nicely on the PGame level

[Tristan Figueroa-Reid]

Right - I forgot that the theory of State is built on PGame (though it really shouldn't..)

[Tristan Figueroa-Reid]

Bernhard Reinke said:

Hm, I think one way to proceed would be to go into a similar direction as State.lean, but introduce one more level of Finset in the options. In that file, the target is PGame. If I want to work with Finset, it would be nice if a finite summation of games with indexing set is possible. It is not clear to my if this works nicely on the PGame level

Are you looking for something like IGame.Short or Game.Short? I'm a little confused by the notion of introducing Finset in the options.

[Bernhard Reinke]

Thinking a bit about it, I should have said Multiset and not Finset, but the point stands. I envision something like this:

class BreakState (S : Type u) where
  height : S → ℕ
  l : S → Finset (Multiset S)
  r : S → Finset (Multiset S)
  left_bound : ∀ {s t u}, t ∈ l s → u ∈ t → height u < height s
  right_bound : ∀ {s t u}, t ∈ r s → u ∈ t → height u < height s

that would model an abstract "breaking game", positions would be given by Multiset S. For octal games one can take S = ℕ and l = r to be the allowed partitions of a heap of a given height.

Written like this it should be still a short game

[Tristan Figueroa-Reid]

I had forgotten to respond to this!

I'm wary of this being finite by definition (given that l returns a Finset of broken down heaps, and height isn't an Ordinal), but:

• I've yet to see a developed theory of transfinite heap games (other than Nim)
• For a finite definition, this seems fine.

[Tristan Figueroa-Reid]

I would make this definition transfinite mainly to have Nim be related to BreakState in some way.

[Violeta Hernández]

An update on this. I've been a bit busy bikeshedding some stuff related to the PartiallyWellOrdered API. But in the meanwhile I think I can just copy over my new WellQuasiOrderedLE typeclass and build a basic definition for poset games.

[Violeta Hernández]

The main relevant result is the following. We can define a posetMove relation on Set \a by posetMove s t when there exists a \in s with s = t \ Ici a. In a wqo, this relation is well-founded.

[Violeta Hernández]

To prove this, we can first show this is a subrelation of \ssubset. Which means its transitive closure is too.

Suppose there were an infinite decreasing sequence f. Let g be the sequence of elements a you take at each step. By the wqo condition there are m < n with g m ≤ g n, and in particular g n must be in f n and thus f m. But this can't be so since f (m + 1) = f m \ Icc (g m) and thus doesn't contain g n.

[Violeta Hernández]

And once you have this, you can simply define a position in a poset game for a set s recursively, as the game whose left and right sets are both the positions corresponding to sets related by posetMove to s.

[Violeta Hernández]

The next steps from here would be to prove that this is an impartial game, and to then prove via a strategy stealing argument that any poset with a top element is won by the first player (i.e. the game is fuzzy with 0). I do currently have a lot of my metaphorical plate though, so I think I'll let someone else take over at that point :smile:

[Violeta Hernández]

Even though this is a strategy stealing argument, I don't think we actually need to formalize strategies to prove it. The basic idea should be "if s ≈ 0, then s \ top ≈ 0, which is absurd since s \ top is subsequent to s".

[Violeta Hernández]

I managed to define poset games! Was a bit easier than expected.

[Violeta Hernández]

This has a bunch of dependencies and auxiliary lemmas that have to be PR'd first; which is not to mention that we don't even know if this belongs in Mathlib... But for the moment we can work on the branch.

[Violeta Hernández]

#21003

[Violeta Hernández]

By the way, this seems as good a time as any to bring this issue back up. Should we make Impartial into a normal predicate instead of a typeclass?

[Tristan Figueroa-Reid]

I just split the Impartial refactor into a separate PR #21006, so this is actually a wonderful time to ask!

[Violeta Hernández]

It's compositional, in the sense that Impartial x → Impartial y → Impartial (x + y). But there's a few problems:
a) this is a class on terms, not types, and we've previously established these are somewhat more frowned upon.
b) we're only ever going to have a handful of "basic" instances, like Impartial 0 or Impartial (nim o), so the usefulness is a bit limited.
c) having this as a typeclass argument means that we often have to provide the term explicitly, which hampers the convenience of composability.

[Violeta Hernández]

I think it would be better to instead have this as a def, and provide dot notation Impartial.add in order to do composition instead.

[Violeta Hernández]

(I've brought this up a bunch of times before, but at that point I think I was the only person actively working in this part of the library, so my PR #16054 fell through the cracks)

[Tristan Figueroa-Reid]

I agree with those points - I also see no reason for it to stay as a typeclass.

[Violeta Hernández]

I'll revive the PR then :smile:

[Tristan Figueroa-Reid]

Once you update the PR, I'll base #21006 off of #16054 :+1:

[Violeta Hernández]

It'll take a bit for me to get it compiling again, since I did some breaking changes on the nim file since I last merged master. I'll let you know when it's ready.

[Violeta Hernández]

Tristan Figueroa-Reid said:

Once you update the PR, I'll base #21006 off of #16054 :+1:

I really do think we make a great team :smile:

[Violeta Hernández]

@Tristan Figueroa-Reid Wait a sec, what's going on in #21006? Those two definitions aren't equivalent!

[Violeta Hernández]

Under our current definition, {∗1 + ∗2 | ∗3} is an impartial game, whereas it wouldn't be impartial under your definition!

[Violeta Hernández]

I think the docstring should make this a bit clearer, our definition of an impartial game is slightly broader than in the literature, since the weaker assumptions are still enough to prove Sprague-Grundy.

[Tristan Figueroa-Reid]

since the weaker assumptions are still enough to prove Sprague-Grundy.

Right! I got misled by this. This change was bundled in with the #7162 pull request, and I justified it by noticing that the Sprague-Grundy theorem still held, but I forgot it holds if Impartial has a weaker condition.

[Violeta Hernández]

#16054 is once again ready for review.

[Violeta Hernández]

You know, if I'm being honest, I'm no longer sure this is an improvement.

[Violeta Hernández]

I first raised this issue back in Lean 3, where working with typeclasses as assumptions was much more painful involved using haveI all over the place. In Lean 4, this isn't nearly as problematic anymore.

[Violeta Hernández]

And, even though these are typeclasses on terms, the terms themselves behave a lot like types, in the sense that they're almost never composed in any nontrivial ways. There's a lot of ways to write down 37 but there's not a lot of ways to write down "the poset game on ℕ × ℕ".

[Violeta Hernández]

I think I'll close that PR, and port my miscellaneous golfs to other smaller PRs.

[Violeta Hernández]

#21007

[Violeta Hernández]

Oops, I realized I had my definition for poset games wrong! The relation I was proving well-founded was actually just the empty relation...

[Violeta Hernández]

I've fixed my mistake and pushed to the branch. I also added some boilerplate API and proved that poset games are impartial.

[Violeta Hernández]

Oh and also, I managed to prove

theorem poset_fuzzy_zero {α : Type*} [PartialOrder α] [WellQuasiOrderedLE α] [OrderTop α] :
    poset α ‖ 0 := sorry

[Violeta Hernández]

This was surprisingly easy, and only took 8 lines of code

[Violeta Hernández]

Goes to show that strategy stealing doesn't require strategies at all!

[Violeta Hernández]

In fact, I think we can turn strategy stealing into a Mathlib theorem proper.

example [Impartial x]
    (h : \ex i, \forall j, \ex k, (x.moveLeft i).moveLeft j ≈ x.moveLeft k) : x || 0 :=
  sorry

[Violeta Hernández]

If there's some initial move such that any subsequent move could've also been made by the first player, then the game is won by the first player.

[Violeta Hernández]

Actually, I suspect that impartiality isn't too relevant here. Is there a version of this for any game?

[Tristan Figueroa-Reid]

Hex is partizan and is susceptible to the strategy stealing argument.

[Tristan Figueroa-Reid]

I believe the Hex argument relies on an extra move never being a disadvantage.

[Violeta Hernández]

@Tristan Figueroa-Reid how exactly would having the intermediate lemma you mention on GitHub help?

[Violeta Hernández]

Morally, the mathematical argument is "left moves and right moves in an impartial game are exactly the same". But I think even G ≡ -G is too weak of a condition for Lean to understand this in a verbatim sense.

[Tristan Figueroa-Reid]

Yeah, the actual working proof would be different, but I still think you can use the BiTotal nature of Identical to make the left move corresponding to the right in the fuzzy_zero_of_forall_exists_moveRight proof - it wouldn't be exactly the same, but you should be able to construct a left move with the extra Identical constraint.

[Tristan Figueroa-Reid]

Though, that would be out of scope for the PR, as to constructively make an impartial game where G ≡ -G from G ≈ -G would require being able to construct the canonical form of a game.

[Violeta Hernández]

Would it make sense to have a new typeclass StronglyImpartial or something like that for G identical to -G?

On the one hand this might make it easier, given extra API, to translate statements on left moves of impartial games to right moves. On the other, I really don't think this definition would give us many new theorems, and it comes at some generally cost that could come back to bite us.

[Tristan Figueroa-Reid]

I think a new typeclass is too much, as it's just something that would be invoked in proofs. I'm unfamiliar with the best lean practices for that specific construction, but I agree that a new type class would cost more than what it would bring.

My best guess would be to have a definitional theorem that proves that canonical G for a (G : PGame) [Impartial G] is equivalent to the impartial definition with Identical instead of Equiv, that way you can rewrite the goal in fuzzy_zero_of_forall_exists_moveRight from G || 0 to canonical G || 0.

[Violeta Hernández]

I don't think we have any best practice for introducing auxiliary definitions whose sole purpose is to be used in proofs. Generally those sorts of things would be hidden behind a tactic.

[Violeta Hernández]

And if that's what we're going to do, why not go the extra mile, and show that any impartial game is equivalent to one where both the left and right types and indexing functions are equal?

[Tristan Figueroa-Reid]

That would be a better idea and it's something we could do now!

[Violeta Hernández]

Though alternatively, we could just do nothing. The impartial file is only about 200 lines long, and we're unlikely to get any substantial golfs that don't just end up taking as much code as is saved.

[Violeta Hernández]

Are we likely to expand the current API further in a way that requires us to duplicate theorems between left and right variants?

[Violeta Hernández]

Or actually, do we even gain anything by having both left and right versions of our theorems instead of sticking to one always?

[Tristan Figueroa-Reid]

Violeta Hernández said:

Or actually, do we even gain anything by having both left and right versions of our theorems instead of sticking to one always?

We wouldn't gain much if we had the backing information that an impartial game G is equivalent to a game G' where G' = -G', but it's currently useful as is.

[Tristan Figueroa-Reid]

Perhaps there is a good reason to have more API surrounding a 'strongly impartial' game using heterogeneous? equality - we haven't formalized heap games.

[Violeta Hernández]

Wait! Don't we already have this!

[Violeta Hernández]

This has a name: Sprague-Grundy

[Tristan Figueroa-Reid]

Right!

[Violeta Hernández]

And in fact, our definition of nim serendipitously satisfies - nim x = nim x

[Violeta Hernández]

Let me see if I can use this in order to golf the theorem

[Violeta Hernández]

Hmm... I don't think this will actually work. Strategy stealing relies on us being able to give a specific move for which the strategy can be stolen. But moves don't transfer over equivalences.

[Violeta Hernández]

This idea might still work in order to golf other theorems, but I think it won't work for this one.

[Violeta Hernández]

Maybe we're thinking about this wrong? It's not too hard to get the goal state to this:
image.png

[Violeta Hernández]

The goal should be the same as H, modulo some equivalences

[Violeta Hernández]

Maybe we could add some lemma like (∀ i : (-x).LeftMoves, p i) ↔ (∀ i : x.RightMoves, p (toLeftMovesNeg i))

[Violeta Hernández]

In fact, I suspect we can already get this through some lemma on equivalences.

[Violeta Hernández]

I got it!

theorem fuzzy_zero_of_forall_exists_moveRight (i : G.RightMoves)
    (H : ∀ j, ∃ k, (G.moveRight i).moveRight j ≈ G.moveRight k) : G ‖ 0 := by
  rw [← neg_fuzzy_zero_iff]
  apply fuzzy_zero_of_forall_exists_moveLeft (-G) (toLeftMovesNeg i)
  rw [moveLeft_neg_toLeftMovesNeg]
  simpa [← toLeftMovesNeg.forall_congr_right, ← toLeftMovesNeg.exists_congr_right]

[Violeta Hernández]

I think we could add these specializations of Equiv.forall_congr_right, etc. to our simp set. That is, any statement about the left/right moves of a negative should get turned into a statement about the right/left moves of a game, with the appropriate casts inserted.

[Violeta Hernández]

This should hopefully then make it so that we can prove more theorems by simply passing to the negative.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think we could add these specializations of Equiv.forall_congr_right, etc. to our simp set. That is, any statement about the left/right moves of a negative should get turned into a statement about the right/left moves of a game, with the appropriate casts inserted.

I can't think of any place where proving the negative of games is more useful :+1:

[Violeta Hernández]

I opened PR #21110 which combines a bunch of improvements I've made to the impartial file. Most notably, I managed to scrape off some 15-odd lines using these new simp lemmas.

[Violeta Hernández]

...actually nvm, there were even simpler proofs of the theorems I golfed!

[Violeta Hernández]

Still, I can attest that the new simp lemmas work and are useful.

[Tristan Figueroa-Reid]

Violeta Hernández said:

...actually nvm, there were even simpler proofs of the theorems I golfed!

Interesting - are the newly golfed changes currently on any PRs?

[Violeta Hernández]

They're on the latest version of the PR I linked.

[Violeta Hernández]

Specifically: fb495f86-6b37-4ee3-8012-2dd1d9468479.jpg

8498b66f-9d30-4ae1-8252-f192169793c8.jpg

[Violeta Hernández]

I've got an unrelated question. Now that I've formalized poset games, what's next?

[Violeta Hernández]

Are there any more interesting kinds of games that can be (nontrivially) considered as special cases of them?

[Violeta Hernández]

If not, what other families of games are worth formalizing, and how should we go about doing it?

[Tristan Figueroa-Reid]

• Hackenbush would be a good game to formalize in general
• (n-dimensional) Chomp is an excellent special-case poset game
• Heap games would have the biggest theory out of any impartial game.

[Tristan Figueroa-Reid]

Violeta Hernández said:

If not, what other families of games are worth formalizing, and how should we go about doing it?

I think Hackenbush and Heap games would be the two biggest game families worth formalizing - Chomp and Hackenbush have two very nice connections to algorithmic combinatorial game theory that we can formalize.

[Tristan Figueroa-Reid]

It would also be nice to prove that red/blue Hackenbush forms the Surreals/is cold, and red/blue/green Hackenbush forms the cold and tepid games.

[Violeta Hernández]

Is there anything that can be said about Chomp that can't be said about general poset games?

We are currently missing the results that a finite product of WQOs is a WQO, and that a subtype of a WQO is a WQO too. But other than that Chomp is very directly just the poset game on a finite product of well-orders minus their bottom element.

[Tristan Figueroa-Reid]

Violeta Hernández said:

Is there anything that can be said about Chomp that can't be said about general poset games?

Very little - I believe even PSPACE-completeness can be proven for poset games in general.

[Violeta Hernández]

Hackenbush would definitely be worth formalizing. We could also formalize a version of strategy stealing on all-green Hackenbush (which is just a poset game in disguise).

[Violeta Hernández]

What are heap games?

[Violeta Hernández]

Something else I think might be worth is formalizing/reformalizing IMO game problems in terms of PGame, as a way to stress-test the API and show that it's actually practical in "real world" scenarios.

[Tristan Figueroa-Reid]

Violeta Hernández said:

What are heap games?

They are a special type of impartial game with (I believe) the most theory built on them other than Nim.

I believe they were designed as a generalization of Nim (to represent 'heaps' with different rules)

Heap games have 8 rules, and heap games are represented both by their actual state and a number (I believe it is a real number, but I don't think that conjecture holds for transfinite heap games) that represents the rules at each number of tokens starting at 0.

For example, rule 3 states, "It is legal to remove $i$ tokens always (but the remaining tokens must be left in a single heap)," rule 0 states, "It is never legal to remove $i$ tokens," and Nim is represented as 0.3333333...

[Violeta Hernández]

Do you have a link to that?

[Tristan Figueroa-Reid]

(The 0 at the start is there because you can't remove 0 tokens: you can't make an empty move)

I went to send a reference article, and I'm surprised there's no Wikipedia article on this; I'll probably write one later. (edit: just wrote a stub.)

My information is from Aaron Siegel's book, but I'll see if I can find what it references :+1:

[Tristan Figueroa-Reid]

It makes sense why I was having trouble finding a reference - I made a mistake. I confused the general class of heap games for the class of octal games.

[Violeta Hernández]

If there's one thing I've learned these past few months is that Aaron Siegel should be our canonical referent for all CGT

[Tristan Figueroa-Reid]

Octal games are already written about, but heap games are much more generic: singe-heap games are impartial games that are naturally represented by a heap of tokens, and a game is played on them. Heap games are the disjunctive sums of these single-heap games.

[Tristan Figueroa-Reid]

Speaking of special impartial games, Wythoff's game might also be worth formalizing.

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

Octal games are already written about, but heap games are much more generic: singe-heap games are impartial games that are naturally represented by a heap of tokens, and a game is played on them. Heap games are the disjunctive sums of these single-heap games.

I think someone earlier had a definition for a generic (finite) heap game.

[Tristan Figueroa-Reid]

Bernhard Reinke said:

Thinking a bit about it, I should have said Multiset and not Finset, but the point stands. I envision something like this:

class BreakState (S : Type u) where
  height : S → ℕ
  l : S → Finset (Multiset S)
  r : S → Finset (Multiset S)
  left_bound : ∀ {s t u}, t ∈ l s → u ∈ t → height u < height s
  right_bound : ∀ {s t u}, t ∈ r s → u ∈ t → height u < height s

that would model an abstract "breaking game", positions would be given by Multiset S. For octal games one can take S = ℕ and l = r to be the allowed partitions of a heap of a given height.

Written like this it should be still a short game

Yes - in this thread, too! I did have some complaints about it being restricted to finite games, but that conversation ended shortly after.

[Tristan Figueroa-Reid]

By the way, we can probably generalize Poset games to restrict what players can take what elements, make the current definition of poset games an impartial version of the generic poset game, and define Hackenbush as the special poset game with a top element.

[Violeta Hernández]

Doing this raises an important question though: what conditions would be necessary for the game to terminate?

[Tristan Figueroa-Reid]

Violeta Hernández said:

Doing this raises an important question though: what conditions would be necessary for the game to terminate?

The literature says all non-transfinite games terminate, which should be true of IGame. IGame.Short should probably be defined as: some IGame I is IGame.Short if there is an instance of a PGame P such that P is PGame.Short, and P is identical to the original IGame. This should probably not be an existential quantifier because we want to be able to compute the outcome of IGames and Games.

[Violeta Hernández]

I'm pretty sure the WQO condition is both necessary and sufficient in the impartial case, but in the general case it's trivial to see that the condition is too strong. Take a non-wqo with a bottom element like WithBot ℤ, and make the only valid move for player 2 to take the bottom element.

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

Violeta Hernández said:

Doing this raises an important question though: what conditions would be necessary for the game to terminate?

The literature says all non-transfinite games terminate, which should be true of IGame. IGame.Short should probably be defined as: some IGame I is IGame.Short if there is an instance of a PGame P such that P is PGame.Short, and P is identical to the original IGame. This should probably not be an existential quantifier because we want to be able to compute the outcome of IGames and Games.

I did not notice this was a different thread.

[Violeta Hernández]

Oh yeah, any PGame / IGame always terminates. But poset games on a general poset don't always, e.g. consider the poset game on ℕ with the empty relation

[Tristan Figueroa-Reid]

Hm. I hoped that a quick re-look at some of the more creative Hackenbush games in the Winning Ways series would be enlightening, but I can't think of any good condition, either.

[Violeta Hernández]

I mean, we could still require poset games to be wqos for the sake of simplicity, even if it's too strong of a condition in some weird edge cases.

[Tristan Figueroa-Reid]

It might work if one could partition the left/right/impartial parts of the poset into their own poset transitively and show that at least one is a WQO.

[Tristan Figueroa-Reid]

Though I can't think of a good concrete definition for the 'transitively' part.

[Violeta Hernández]

Isn't the idea that any element can be taken by one or both of the players?

[Violeta Hernández]

So speaking of the red/blue poset should be completely well-defined

[Violeta Hernández]

Even that is still too strong of a condition in some really weird edge cases, though

[Violeta Hernández]

Consider {x} ⊕ₗ ℤ ⊕ₗ ℤ where the middle ℤ is blue and everything else is red. After blue's first turn, red is forced to remove x, and then the game immediately terminates, even though none of the red/blue parts are wqos on their own.

[Tristan Figueroa-Reid]

Are there any situations where a game terminates without both left/right posets being WQOs, or either player having a 'partial', or a disjunctively added WQO? - that was weirdly worded.

[Violeta Hernández]

In my example, the full poset isn't a wqo either.

[Violeta Hernández]

Every subset of a wqo is a wqo

[Tristan Figueroa-Reid]

Violeta Hernández said:

Consider {x} ⊕ ℤ ⊕ ℤ where the middle ℤ is blue and everything else is red. After blue's first turn, red is forced to remove x, and then the game immediately terminates, even though none of the red/blue parts are wqos on their own.

Wait - could red continue playing on the rightmost ℤ in this example? I think that's where my misunderstanding is from.

[Tristan Figueroa-Reid]

Oh, it's supposed to represent ℤ ⊕ ℤ being green. I should have caught that :+1:

[Violeta Hernández]

No, I actually meant for the order to be lexicographic

[Violeta Hernández]

Forgot that this isn't the default order on a sum type

[Violeta Hernández]

image.png
here's a quick MS Paint drawing

[Violeta Hernández]

This game can last at most 3 turns

[Tristan Figueroa-Reid]

Right! Okay!

[Violeta Hernández]

But wait, is this even a valid combinatorial game?

[Violeta Hernández]

This has the odd property that the game tree, if you don't require the players to alternate, is not well-founded

[Violeta Hernández]

I had never considered the possibility that a game that is always finite, isn't in fact a game in Conway's formalism!

[Tristan Figueroa-Reid]

I believe I've seen a game like this before, but I'll recheck.

[Violeta Hernández]

In fact, I think this implies the most general condition for Hackenbush to be a CGT is the same as for a poset game: it has to be a wqo.

[Violeta Hernández]

Follow-up question: is the partizan variant of a poset game you describe not completely isomorphic to Hackenbush?

[Tristan Figueroa-Reid]

Violeta Hernández said:

In fact, I think this implies the most general condition for Hackenbush to be a CGT is the same as for a combinatorial game: it has to be a wqo.

It seems so! I agree that that construction isn't well-founded :+1:

[Tristan Figueroa-Reid]

Violeta Hernández said:

Follow-up question: is the partizan variant of a poset game you describe not completely isomorphic to Hackenbush?

I was hoping there would be some slightly extra generalization, but I don't think it can form any hot game, so I think it is.

[Violeta Hernández]

In fact, this has the silly implication that Chomp is just a particular Hackenbush game

[Violeta Hernández]

image.png
3 × 4 chomp as an example

[Tristan Figueroa-Reid]

Wait - I do get the main point, but I don't think that's true for that particular case.

[Violeta Hernández]

Wait, you're right. Hackenbush is about deleting segments, not deleting points

[Tristan Figueroa-Reid]

3 by 4 chomp would correspond to Schuh's game with two primes, i.e., 7 and 3, with exponentiation 7^2 and 3^3. Drawing that out seems annoying, but absolutely possible :+1:

[Violeta Hernández]

Yeah, now I'm not so sure anymore about my conjecture

[Violeta Hernández]

It'd be nice if there were some simple/canonical way to convert poset games into Hackenbush and/or the other way around. The less formalisms we need to build from scratch, the better.

[Violeta Hernández]

But it's entirely possible these are just two separate constructions.

[Tristan Figueroa-Reid]

Violeta Hernández said:

Yeah, now I'm not so sure anymore about my conjecture

I think it is true both *by an explicit construction and by the proof of Hackenbush's temperature :+1:. Making an explicit construction doesn't seem too complex but not too trivial either.

[Tristan Figueroa-Reid]

Chomp is still a type of Poset game, but the Poset is based on divisors which is more annoying to construct by hand.

[Violeta Hernández]

Chomp is just the poset game on a product of ordinals, minus the bottom element

[Violeta Hernández]

Just so happens that the poset for a product of naturals n_k is also the poset for the divisors of the product p_k^(n_k - 1)

[Violeta Hernández]

That's also why I don't think it's worth formalizing separately from poset games.

[Tristan Figueroa-Reid]

Agreed - all of the interesting Chomp results can be generalized to any impartial Poset game.