A formalization of abstract strategy games


Abstract strategy games are games where both players have full information of the state of the game and where there are no random events. We shall restrict ourselves to games where there are two players that take alternating turns. A game usual starts with an initial board configuration and ends when there are no further moves possible. There is also a score function that for such final configurations defines the outcome in the form of an integer number where a positive value indicates a win for the first player, a negative value a win for the second player, and a zero value a draw. An abstract strategy game can thus be defined with: There is a division between symmetric and asymmetric abstract games. In symmetric abstract strategy games, the rules according a player can make a turn (change a board configuration in another valid configuration) are the same for both users. Asymmetric board games can be modelled as symmetric board games when the board includes a turn indicator. Then the rules are the same for both players, but effectively they are different. In games where cycles in the 'physical' board configurations can occur, it is usually not allowed to repeat the same move in order to avoid endless games. It is possible to model this by including in the board configuration a history of all previous 'physical' configurations and to exclude repeatitive moves from the transition relationship. In some games (such as go) the game ends when both users have passed without changing the 'physical' board configuration. This can be modelled by adding a pass counter to the board configuration. Games where the users are allowed to unilateral decided to finish a game, board configurations to signify this have to be added.

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

Strong positional games are a class of abstract strategy games where the players take turn adding one of the free points to their set of occupied points (usually by placing stones of their colour on a board) until their set of points contain one of their winning patterns. Usually, there are no restrictions on which points can be occupied at any moment in the game as long as it is not already occupied. This is not the case for a game like Connect Four.

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

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 is one of the simplest strong positional games. It can be specified in the following way:
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}

Connection games

Connection games are a class of strong positional games where the patterns consist of group of connected points that meet some criteria. A group of points is connected if there exists a path from each point to each other points through some neighbour relationship defined over all the points of the board. Possible criterias are that the pattern connects two or more groups of special points or that the group contains a cycle. Given a set of points and a neighbouring relationship the set of all groups can be defined as follows:
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 is a famous asymmetric connection game played on a rhombus, which was independently invented by Piet Hein and John Nash. Because it is asymmetric and each winning pattern excludes all winning patterns of the other user, it is an excluding strong positional game. It is also a drawless game. Given a size (common values are: 11, 13, 14, and 19), the points of the board can be defined with:
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 is symmetric connection game invented by Christian Freeling. It is played on a hexagonal board. (Independent formalization of Havannah.) The set of points on the board can be defined using:
df  Havannah_points(size in Natural | size < 1)
    =  { (x,y,z) in {1-size,..,size-1}3
       | x + y + z = 0
In this definition we start with a cube of points and take the points that are on the intersection of a plane, that goes right through the middle of six of the ribs, creating the desired hexagonal set of points. The coordinates with which the points are defined have a degree of freedom of only two. This means that each of the elements can always be calculated if the other two are known.

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
The sum of absolute differences of the coordinates is always even, because the degree of freedom is two. The points with the same distance to a given point are on the imaginary hexagon of which the corners are on the lines through this point and on the given distance.

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
With this definition we have established the board and some of its properties.

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)

home and email