Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computational Modelling for Combinatorial Game Strategies

Răzvan Diaconescu

TL;DR

The work develops a generic equational-logic framework to establish winning strategies in finite two-player games by recasting Zermelo's theorem in terms of strategies-as-subtrees. It encodes this framework as a parameterized Maude module (WINS) within the OBJ-family, enabling executable computation of brute strategies through game-tree instantiations. By applying the approach to concrete games such as heaps, board colouring, and transition systems, the authors demonstrate experimental mathematics methods for discovering pattern-based strategies and guiding proofs, while addressing complexity with symmetry and tracing techniques. The paper also discusses non-deterministic rewriting (POA) and outlines future directions for extending the methodology to broader classes of games and tooling improvements.

Abstract

We develop a generic computational model that can be used effectively for establishing the existence of winning strategies for concrete finite combinatorial games. Our modelling is (equational) logic-based involving advanced techniques from algebraic specification, and it can be executed by equational programming systems such as those from the OBJ-family. We show how this provides a form of experimental mathematics for strategy problems involving combinatorial games. We do this by defining general methods and by illustrating these with case studies.

Computational Modelling for Combinatorial Game Strategies

TL;DR

The work develops a generic equational-logic framework to establish winning strategies in finite two-player games by recasting Zermelo's theorem in terms of strategies-as-subtrees. It encodes this framework as a parameterized Maude module (WINS) within the OBJ-family, enabling executable computation of brute strategies through game-tree instantiations. By applying the approach to concrete games such as heaps, board colouring, and transition systems, the authors demonstrate experimental mathematics methods for discovering pattern-based strategies and guiding proofs, while addressing complexity with symmetry and tracing techniques. The paper also discusses non-deterministic rewriting (POA) and outlines future directions for extending the methodology to broader classes of games and tooling improvements.

Abstract

We develop a generic computational model that can be used effectively for establishing the existence of winning strategies for concrete finite combinatorial games. Our modelling is (equational) logic-based involving advanced techniques from algebraic specification, and it can be executed by equational programming systems such as those from the OBJ-family. We show how this provides a form of experimental mathematics for strategy problems involving combinatorial games. We do this by defining general methods and by illustrating these with case studies.
Paper Structure (20 sections, 1 theorem, 4 equations, 3 figures)

This paper contains 20 sections, 1 theorem, 4 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Prerequisites.
  3. The structure of the paper
  4. Zermelo's theorem in a strategies-as-subtrees perspective
  5. Some game examples
  6. Strategies as subtrees
  7. Game trees.
  8. Strategies as subtrees.
  9. No strategy means that the opponent has a strategy
  10. Computing brute strategies
  11. A quick reminder of equational logic in $\mathit{MSA}$
  12. $\mathit{MSA}$ signatures.
  13. Equations.
  14. Algebras.
  15. The satisfaction relation.
  16. ...and 5 more sections

Key Result

Theorem 2.1

$B$ and $R$ play a game that has the following characteristics: Then the absence of a winning $R$-strategy implies the existence of a non-losing $B$-strategy.

Figures (3)

  • Figure 1: A board colouring play -- red wins.
  • Figure 2: The tree of the game of Example \ref{['heap-game']} with the heaps containing initially $2$ and $5$ tokens, respectively.
  • Figure :

Theorems & Definitions (6)

  • Example 1: A heaps of tokens game
  • Example 2: A board colouring game
  • Example 3: A transition systems game
  • Definition 2.1
  • Theorem 2.1
  • proof