In these past few days, I have been reading Martin Grohe’s survey on Finite Variable Logics in Descriptive Complexity Theory.
There I encountered a very interesting concept known as pebble games. These are used to characterize equivalence between structures in Finite variable logics.
This technique seems to be primarily used to show why certain properties cannot be expressed in some flavor of finite variable logic (The logic could be infinitary!)
The basic idea is as follows: Suppose we are given some vocabulary say and two -structures and . By -structure we mean a structure consisting of finite set and the definitions for each of the relation symbol in . These definitions are over the elements of that finite set. Then we pick a for a -pebble game.
Intuitively this is equivalent to a board game where the board comprises of two sections representing the two structures. One of the sections is colored red, while the other is colored blue. For convenience, let us suppose that section corresponding to is labelled red and the one corresponding to is labelled blue. Each section has squares which correspond to the members of the structure. Any relationships between the members are marked on the board. Finally, we also have two sets of pebbles where each set contains exactly pebbles numbered . The pebbles in the first set are coloured red and the pebbles in the second set are coloured blue.
There are two players. They are known as the spoiler and the duplicator.
A typical move would involve placing a pebble on some square. An important thing to note here is that the color of the pebble and the colour of the section in which it is placed should be the same. Also, the pebble could be a free pebble, i.e not placed on the board before this, or it could be a pebble that’s already on the board. The crucial thing to remember is the number on the pebble that has just been used in the move.
A round in the game consists of two moves. First one by the spoiler followed by a move by the duplicator. There could be several rounds as we shall see.
The very first round of the game begins with a blank board.
In each round, the spoiler starts with the board configuration from the end of the previous round and makes his move. If the move involves a a red coloured pebble, it is called a -move. If the spoiler makes the move with a blue coloured pebble, it is called the -move.
Once the spoiler has made his move, it’s the Duplicator’s turn. Suppose spoiler had made a move with pebble numbered . The Duplicator has to make a move with the pebble numbered . The colour of this pebble is different from the one used in the spoiler’s move. The square on which the duplicator places this pebble cannot be an arbitrary one. It should be such that having placed the pebble on the square, the configuration of the pebbles on the red section is isomorphic with the correspondingly numbered pebbles on the blue section. The isomorphism is with respect to the relationships between the squares on which they are placed. In other words, the Duplicator, as his name suggests, should place the same numbered, different colored pebble in such a manner that it duplicates the change in the configuration brought about by the spoiler, thereby making the blue section agree with the red section. If the Duplicator is able to do so, we say that the Duplicator wins this round.
We say that the Duplicator wins the game or has a winning strategy if for any round which begins with a board configuration where there is an isomorphism between the red and the blue sections, duplicator can win the round no matter what move is made by the spoiler.
Now what connection does this silly looking game have with Finite Variable logics ?
This is answered by an interesting theorem due to Barwise and Immerman.
Suppose , , and are as defined above then if and only if, the duplicator has a winning strategy for the -pebble game on with the initial position being the blank board.
Thus the -pebbles in the game capture values associated with in the -variables in some subformula of our -variable formula. Once we move to a different subformula, these variables are reused. This is captured by moving the pebble from one square to another thereby effectively forgetting previous square it was associated with.
Next question that would arise is: How are these pebble games used ?
We shall attempt to answer this in a subsequent post.