A formalization of abstract strategy games

Introduction

• A set of valid board configurations.
• An initial board configuration.
• A relationship defining valid transitions between board configurations.
• A score function for final configurations.

We first give a definition for final configurations, given a set of configurations and a transition relationship:

df final_configurations( configurations : set, transitions subset configurations2)
    = {p in configurations | not Exist q in configurations ((p,q) in transitions)}

Now we can define the collection of all possible abstract games, where we require that all configurations can be reached from the initial configuration:

df abstract_games
   = { ( configurations : set
       , initial in configurations
       , transitions subset configurations2
       , score : function
                 from final_configurations(configurations, transitions)
                 to integer
       )
     | configurations = {q in configurations | (initial, q) in transitions*}
     }

Now we can define the set of all valid games as sequences of configurations, where the first configuration is the initial configurations and the last configuration one of the final configurations. All pairs of consecutive configurations must be valid transistions. This can be defined with:

df  valid_games((configurations, initial, transitions, score) in abstract_games)
    = { (p0, .., pn) in configurationsn
      |     p0 = initial
        and pn in final_configurations(configurations, transitions)
        and Forall 0<i<=n ((pi-1, pi) in transitions)
      }

A playing strategy is defined as a function of non final configurations to a configuration that is valid according to the transition. The set of all playing strategies can be defined as follows:

df  playing_strategies((configurations, initial, transitions, score) in abstract_games)
    = { function
        from configurations - final_configurations(configurations, transitions)
        to configurations
        subset transitions
      }

Given two players from the set of players, we can define the game that they would have played together. This is defined by the following function:

df  played_game(game in abstract_games, strategy0 in playing_strategies(game), strategy1 in playing_strategies(game))
    = (p0, .., pn) in valid_games(game)
      where Forall 0<i<=n (pi = strategyi mod 2(pi-1) )

Given a valid game, we can define the outcome by applying the score function on the last configuration as follows:

df  outcome(game in abstract_games, (p0, .., pn) in valid_games(game))
    = score(pn)
      where (configurations, initial, transitions, score) = game

An abstract game is drawless when all played games always result in a win for one of the two players. This can be defined as follows:

df  drawless(game in abstract_games)
    = Forall played_game in valid_games(game) (not(outcome(game, played_game) = 0))

Finally, we define the set of super strategies for a game. These are strategies that never lose from any other player (except themselves).

df super_strategies(game in abstract_games)
     = { strategy in playing_strategies(game)
       | Forall other_strategy in playing_strategies(game) - {strategy}
            (    outcome(played_game(strategy,other_strategy)) >= 0
             and outcome(played_game(other_strategy,strategy)) >= 0)
       }

It is possible that for a certain game there are no super strategies, because there exist more than one winning strategy. Maybe it is possible to define the a strategy quality on the basis of the sum of both outcomes, in the following manner:

df strategy_quality(game in abstract_games, strategy in playing_strategies(game))
     = Minimum { outcome(played_game(strategy,other_strategy)) + outcome(played_game(other_strategy,strategy))
               | other_strategy in playing_strategies(game) - {strategy}
               }

Strong positional games

We require that a set of winning patterns is minimal, meaning that it does not contain two patterns that are a proper subset of each other, because removing the larger pattern of the two would result in exactly the same game. Given a set of points, all collections of winning patterns can be defined with:

df minimal_winning_patterns(points : set)
    = { patterns subset powerset(points)
      | Forall p1, p2 in patterns
           (p1 = p2 or not(p1 propersubset p2))
      }

Now the set of all strong positional games can be characterized with the following:

df strong_positional_games
    = { (points : set, wps1, wps2)
      |     wps1 in minimal_winning_patterns(points)
        and wps2 in minimal_winning_patterns(points)
      }

We can also define symmetric pattern games as all games for which the winning patterns for both players are the same:

df symmetric_strong_positional_games
    = { (points, wps1, wps2) in strong_positional_games
      | wps1 = wps2
      }

We can also define all exclusive strong positional games as all games for which the winning patterns for one player exclude all winning patterns of the other player:

df excluding_strong_positional_games
    = { (points, wps1, wps2) in strong_positional_games
      | Forall wp1 in wps1, wp2 in wps2 (not(wp1 intersection wp2 = {}))
      }

For each of the strong positional games it is possible to define a abstract game. For this we need to construct parts of the abstract game based on a characterisation for a strong positional game. First we need to define all possible board configurations. Because the game ends when one of the players has created a winning configuration, it is not possible that the sets of occupied points of both players contain a winning configuration for that player. For this we need to define the collection of all winning positions as all subsets of the points that contain a winning pattern:

df  winning_positions(points : set, wp in minimal_winning_patterns(points))
    = { win subset points
      | Exists w in wp (w subset win)
      }

Now we can define all configurations for a strong positional game:

df spg_configurations((points, wps1, wps2) in strong_positional_games)
    = { (ps1,ps2) in (powerset(points))2
      |     ps1 intersection ps2 = {}
        and (count(a) = count(b) or count(ps1) = count(ps2) + 1)
        and not(    ps1 in winning_positions(points, wp1)
                and ps2 in winning_positions(points, wp2))

Next we can define all transtions for a strong positional game:

df spg_transitions(pfg in strong_positional_games)
    = { ((fps1,fps2),(tps1,tps2)) in spg_configurations(game)
      |     fps1 subset tps1 and fps2 subset tps2
      	and count(tps1) + count(tps2) = count(fps1) + count(fps2) + 1
      }

Last we need to define the scoring function:

df spg_score((points, wps1, wps2) in strong_positional_games)
    = { ((ps1,ps1, value) in spg_configurations(game)x{-1,0,1}
      | value = if ps1 in winning_positions(points, wps1)
                then 1
                elif ps2 in winning_positions(points, wps2)
                then -1
                else 0
                fi
      }

With the above definitions it is now easy to define a function that returns an abstract game for any strong positional game. We define this as follows:

df spg_game(pfg in strong_positional_games) in abstract_games
    = (spg_configurations(pfg), ({},{}), spg_transitions(pfg), spg_score(pfg))

Tic-tac-toe

df tic_tac_toe
    = ( (1,2,3,4,5,6,7,8,9), rows, rows )
      where rows = {{1,2,3},{4,5,6},{7,8,9}
                   ,{1,4,7},{2,5,8},{3,6,9}
                   ,{1,5,9},{3,5,7}}

Connection games

df groups(points : set, neighbours subset points2)
    = { group subset points
      | Forall a,b in group ((a,b) in (neighbours intersection group2)*)
      }

Thus the set of all possible connections games for a set of points and a neighbour relationship, can be defined as follows:

df connection_games( points : set, neighbours subset points2)
    = { (points, wps1, wps2) in strong_positional_games
      |     wps1 subset groups(points, neighbours)
        and wps2 subset groups(points, neighbours)
      }

Usually, a game also is maximal under a certain condition for winning patterns. For this we define a maximal function that given a set of games returns the one game (presuming that it exists) that is maximal.

df maximal( games in connection_games( points : set, neighbours subset points2))
    = (points, wps1, wps2) in games
      such Forall (points, owps1, owps2) in games (owps1 subset wps1 and owps2 subset wps2)

Hex

df Hex_points(size in Natural | size < 1)
    =  { (x,y) in {0,..,size-1}2 }

The neighbours relationship on the points can be defined with:

df Hex_neighbours(size in Natural | size < 1)
    = { ((x1,y1),(x2,y2)) in Hex_points(size)2
      | (x1-x2)2 + (y1-y2)2 - (x1-x2)(y1-y2) = 1
      }

From this the game of Hex can be defined as a connection game in the following way:

df Hex_game(size in Natural | size < 1)
    = maximal({ (points, wps1, wps2) in connection_games(Hex_points(size), Hex_neighbours(size))
              |     Forall wp in wps1 (    Exist x1 ((x1,0) in wp
                                       and Exist x2 ((x2,size-1) in wp)
                and Forall wp in wps2 (    Exist y1 (0,(y1) in wp
                                       and Exist y2 (size-1,(y2) in wp)
              })

Havannah

df  Havannah_points(size in Natural | size < 1)
    =  { (x,y,z) in {1-size,..,size-1}3
       | x + y + z = 0
       }

We can define the distance between two points as the length of the shortest path between the points. We can do so using:

df  Havannah_distance(size in Natural | size < 1, (x1,y1,z1) in Havannah_points(size), (x2,y2,z2) in Havannah_points(size))
    = ( |x1-x2| + |y1-y2| + |z1-z2| )/2

With this definition it is also possible to define the neighbour relation:

df  Havannah_neighbours(size in Natural | size < 1)
    = { (p,q) in Havannah_points(size)2
      | Havannah_distance(size,p,q) = 1
      }

The Havannah groups are defined with:

df  Havannah_groups(size in Natural | size < 1)
    = groups(Havannah_points(size), Havannah_neighbours(size))

And a function that returns all neighbours of a point:

df  Havannah_neighbours_of(size in Natural | size < 1, p in Havannah_points(size))
    = { q  in Havannah_points(size)
      | (p,q) in Havannah_neighbours(size)
      }

The points on the board can be divided into different kinds. Two of these kinds are the corner and side points. These we can define using:

df  Havannah_corner_points(size in Natural | size < 1)
    =  { p in Havannah_points(size)
       | count(Havannah_neighbours_of(size, p)) = 3
       }

df  Havannah_side_points(size in Natural | size < 1)
    =  { p in Havannah_points(size)
       | count(Havannah_neighbours_of(size, p)) = 4
       }

We start with the simplest winning figure, the bridge, which connects two corner points. The set of all positions that contain a bridge is defined by:

df  Havannah_bridges(size in Natural | size < 1)
    = { group in Havannah_groups(size)
      | count( group intersection Havannah_corner_points(size) ) = 2
      }

Next we look at the forks, which a groups of connected points that touch on three different sides. The definition of the set of all positions that contain a fork:

df  Havannah_forks(size in Natural | size < 1)
    = { group in Havannah_groups(size)
      | count({ { b in Havannah_side_points(size)
                | (s,b) in (Havannah_side_points(size)2 intersection Havannah_neighbours(size))*
                }
              | s in (group intersection Havannah_side_points(size))
              }) = 3
      }

Finanlly, we look at the cycles. The definition of the set of all positions that contain a cycle:

df  Havannah_cycles(size in Natural | size < 1)
    = { {p0,..,pn-1} in Havannah_groups(size)
      | Forall  1<=i<n
           (    Havannah_distance(size, pi,p(i+1) mod n) = 1
            and Havannah_distance(size, pi,p(i+2) mod n) >= 2
           )
      }

From this the game of Havannah can be defined as a connection game in the following way:

df Havannah_game(size in Natural | size < 1)
   = (Havannah_points(size), wps, wps) in connection_games(Havannah_points(size), Havannah_neighbours(size))
      where wps = Havannah_cycles(size) union Havannah_bridges(size) union Havannah_forks(size)