A formalization of abstract strategy games

Introduction

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:
• A set of valid board configurations.
• An initial board configuration.
• A relationship defining valid transitions between board configurations.
• A score function for final configurations.
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.
```df final_configurations( configurations : set, transitions subset configurations2)
= {p in configurations | not Exist q in configurations ((p,q) in transitions)}
```
```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*}
}
```
```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)
}
```
```df  playing_strategies((configurations, initial, transitions, score) in abstract_games)
= { function
from configurations - final_configurations(configurations, transitions)
to configurations
subset transitions
}
```
```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) )
```
```df  outcome(game in abstract_games, (p0, .., pn) in valid_games(game))
= score(pn)
where (configurations, initial, transitions, score) = game
```
```df  drawless(game in abstract_games)
= Forall played_game in valid_games(game) (not(outcome(game, played_game) = 0))
```
```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)
}
```
```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.
```df minimal_winning_patterns(points : set)
= { patterns subset powerset(points)
| Forall p1, p2 in patterns
(p1 = p2 or not(p1 propersubset p2))
}
```
```df strong_positional_games
= { (points : set, wps1, wps2)
|     wps1 in minimal_winning_patterns(points)
and wps2 in minimal_winning_patterns(points)
}
```
```df symmetric_strong_positional_games
= { (points, wps1, wps2) in strong_positional_games
| wps1 = wps2
}
```
```df excluding_strong_positional_games
= { (points, wps1, wps2) in strong_positional_games
| Forall wp1 in wps1, wp2 in wps2 (not(wp1 intersection wp2 = {}))
}
```
```df  winning_positions(points : set, wp in minimal_winning_patterns(points))
= { win subset points
| Exists w in wp (w subset win)
}
```
```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))
```
```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
}
```
```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
}
```
```df spg_game(pfg in strong_positional_games) in abstract_games
= (spg_configurations(pfg), ({},{}), spg_transitions(pfg), spg_score(pfg))
```

Tic-tac-toe

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}
,{1,4,7},{2,5,8},{3,6,9}
,{1,5,9},{3,5,7}}
```

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)*)
}
```
```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)
}
```
```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

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 }
```
```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
}
```
```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

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.
```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.
```df  Havannah_neighbours(size in Natural | size < 1)
= { (p,q) in Havannah_points(size)2
| Havannah_distance(size,p,q) = 1
}
```

```df  Havannah_groups(size in Natural | size < 1)
= groups(Havannah_points(size), Havannah_neighbours(size))
```
```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)
}
```
```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.
```df  Havannah_bridges(size in Natural | size < 1)
= { group in Havannah_groups(size)
| count( group intersection Havannah_corner_points(size) ) = 2
}
```
```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
}
```
```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
```

```