An abstract two-person game

Suppose we have a two-person game given by

-

a set S of (game-)states

-

subsets

-

a relation characterizing the legal moves, such that
.

A game starts in an initial state with two opposing players taking turns to move. A player wins if his move reaches a terminal state. We are looking for conditions that guarantee a win for the first player.

In the following program we model the players with the two-element data type

        Player = ({You, Me }, = ).

Let myMove and yourMove be the functions realizing the moves of the players, that is once You are in state s you move to yourMove(s), similarly, the function myMove determines my moves. We assume that .

The abstract game-playing program, together with the stipulation that Me should win is :

        { Init(s) }
        turn := Me;
        WHILE not Terminal(s) DO         
          IF turn = Me 
            THEN 
              BEGIN  s := myMove(s)  ;  turn := You END
            ELSE 
              BEGIN  s := yourMove(s);  turn := Me  END ;                    
        IF turn = Me 
          THEN winner := You 
          ELSE winner := Me
        { winner = Me }

When verifying this program, we have to supply an invariant for the loop. In the absence of any further information about the rules of the game, we invent an abstract predicate depending on the relevant variables, P(player,s).

NPPV generates four verification conditions, which we simplify slightly using the trivial axioms of the Player-data type: and :

        Init(s)  ==> P(s,Me)
        P(s,Me)  ==> not Terminal(s)
        P(s,Me)  ==> P(myMove(s),You)
        P(s,You) and not Terminal(s) ==> P(yourMove(s),Me)

Let MyPos resp. YourPos be the sets defined by the unary predicates P(s,Me), and P(s,You). Note that in order to guarantee a win for every possible legal move the opponent (You) might make, the function yourMove must be considered a nondeterministic function, whereas myMove can be thought of as a Skolem function, choosing an appropriate new state if one exists. With this in mind, the above axioms can be reformulated in set language as:

Thus the set MyPos, if it exists, can be called a strategy. In order not to lose, I must (and can) always make a move resulting in a state within YourPos.