winning position

Stream: maths

[Yaël Dillies]

How does one define a winning position for a game (not the math game, just a type of positions along with sets of allowed moves and a set of winning positions) that might not end? Is it some kind of minimal fixed point and well-foundedness stuff? I suspect Mario knows how to do these things.

[Chris Hughes]

Can you do it inductively? Finishing positions that are winning are winning, and any other position is winning for player 1 if there is a winning move if it's player 1's turn, or if it's the other player's move, when every possible move leads to a losing position.

[Kyle Miller]

Are you talking about this?

variables {α : Type*} (r : α → α → Prop)
-- r x y means there is a move from position x to position y

inductive accessible_from (a₀ : α) : α → Prop
| start : accessible_from a₀
| move (x y : α) (ha : accessible_from x) (hr : r x y) : accessible_from y

/-- Is there a sequence of moves starting from `a₀` that can reach the `terminate` set? -/
def can_end_from (a₀ : α) (terminate : set α) : Prop :=
set_of (accessible_from r a₀) ∩ terminate ≠ ∅

(I'm just trying to understand the setup -- I'm not saying this is how to formalize it.)

[Kyle Miller]

The mathlib construction for the reflexive transitive closure of a relation is docs#relation.refl_trans_gen

def can_end_from {α : Type*} (r : α → α → Prop) (a₀ : α) (terminate : set α) : Prop :=
set_of (relation.refl_trans_gen r a₀) ∩ terminate ≠ ∅

[Chris Hughes]

Something like this is what I had in mind

variables
  {position : Type}
  (win_for_me : set position) -- A finishing position that is a win for me
  (legal_moves : position → set position)
  (my_turn : set position) -- Set of positions where it is my turn to move

inductive winning_for_me : position → Prop
| finish : ∀ p : position, p ∈ win_for_me → winning_for_me p
| my_move : ∀ p : position, p ∈ my_turn →
  ∀ q ∈ legal_moves p, winning_for_me q → winning_for_me p
| opponents_move : ∀ p : position, p ∉ my_turn →
  (∀ q ∈ legal_moves p, winning_for_me q) → winning_for_me p

[Mario Carneiro]

I would go for something like Chris Hughes 's version, but I wanted to mention that in some infinite game theory there is the concept of a winning game where the play itself is not finite (i.e. it's not like you played for finitely many rounds and reached the end, but rather you play countably many rounds and "looking back" determine that the whole play sequence was a win). This is used in the axiom of determinacy IIRC, and it can be formalized as a predicate on move sequences, or in the simple binary tree case, a coloring of 2^nat.

[Mario Carneiro]

For example, imagine where you and the opponent both play 0 or 1 in alternation to create a sequence, and you win if the sequence of zeros and ones has a natural density and the opponent wins if it doesn't

[Kevin Buzzard]

Right, in the axiom of determinacy stuff a game goes on forever with both players choosing digits and then looking at the resulting infinite string at the end. If you assume AC then there are games for which neither player has a winning strategy, which some logicians might argue is evidence against AC