This document discusses stalemate situations in the Rule Game, and the procedure useds by the experiment plan validator to check whether a rule set can stalemate.
A stalemate is a state of the game (a board position plus the current value of the variables such as p or pc), with at least one piece remaining on the board, which allows no legal moves.
If a stalemate has been achieved, the current value of the counters in metered atoms and metered lines (see Syntax) is irrelevant. This is because in a stalemate situation the control will cycle through all lines of the rule set, and all lines' and aroms' counters will reset.
We will say that, given a set of allowed object types, a rule set can stalemate if there is at least one initial board composed of objects of those types such as that an episode with that initial board may result in a stalemate.
Given a rule set and an initial board, can we tell in advance whether the episode will end in a stalemate regardless of how the player plays, or will the outcome depend on the player's choices?
It turns out that this depends on the rule set. Let us use the term disappearing atom for an atom whose bucket expression may evaluate to a non-empty set during some part of the episode, and to an empty set during another part of the episode. With the currently supported rule syntax (as of GS 4.*), the only possible disappearing atoms are those that use bucket variables such as p, pc, ps. In particular, those that use the negation operator (!) in combination with certain variables may have a non-empty bucket set at the begining, but an empty one later on. Consider, for example, the following atom:
(*,Square,Red,*,!pc)
This atom can be applied to red square objects, and has a bucket expression !pc which evaluates to [1] when pc is not defined (i.e. when no red pieces have been moved yet), and to [] (the empty set) once the first red piece has been move. We can call this atom "disappearing" because after a certain piint in the episode (namely, after the first red game piece has been moved), this atom becomes permanently inactive for the rest of the episode.
The following propostion holds:
Proposition 1: If the rule set contains no disappearing atoms, then whether a given episode ends in a stalemate depends entirely on the game's rule set and the episode's intial board, and does not depend on the player's actions.
(It follows from Proposition 4 in the last section of this document).
As an example of how a rule set with disappearing atoms may have an initial board that may or may not result in a stalemate depending on the player's decisions, consider the following rule set:
(pos:36, bucket:[!p]) (pos:[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,33,35)The first atom of this set allows the player to remove game piece from cell No. 36, but only if no pieces have been removed yet. Hence, this rule can only be used once. The second atom allows the player to remove any number of pieces from cells No. 1 thru 35. Now, consider an initial board that has a game piece in cell No. 36, and one or more pieces in other cells of the board. If the player starts the episode with removing the piece from cell No. 36 (using the first atom), then he can remove all other game pieces using the second atom; thus, no stalemate. But if the player starts with using the first atom to remove any other piece than the one in cell No. 36, then he will never again have a chance to remove that piece; thus, once all other pieces have been removed, a stalemate will result.
There is a way to ensure that your rule set is without disappearing atoms (WODA). All you need to do is to make sure that every bucket expression always produces a non-empty set. This can be achieved by balancing parts with pc and !pc, and so on. E.g. an atom
(*,*,Red,T,pc)is "disappearing", because is produces an empty set before the first red piece has been moved. But it can be fixed by a adding to its bucket expression a clause that returns a non-empty set when pc is not defined, e.g.
(*,*,Red,T,[!pc*2, pc]), so that this atom produces a destination (bucket 2) if it is applied to the very first red piece to be moved.
An equivalent solution can be achieved by "duplicating" an atom, so that the two atoms have their shape and color sections (and any other property-based sections, if applicable) identical, and their bucket sections, if viewed together, always produce a non-empty set. For example, a rule set may contain these two atoms:
(1,*,Red,T,!pc*3) (*,*,Red,T,pc+1)In this example we see that once the first atom has been spent, the second is ensured to always produce a non-empty set of destination buckets. This ensures that, when viewed together, they (eventually) provide the same opportunities for "red pieces from the top non-empty row" to be moved as a non-disappearing atom
(*,*,Red,T,[3,pc+1])
Similarly, these two atoms put together:
(*,*,Red,T,!ps*1) (*,*,Red,T,ps-1)ensure that a red piece from the top non-empty row will always (possibly, after some cycling of the rule lines) have a destination bucket, regardless of whether any piece of the same shape has been moved yet.
The Rule Game server includes a stalemate tester component, which, starting in ver. 4.003, is used as a component of the experiment plan validator, to allow the experiment designer to detect possible stalemate situation in his or her rule set. The stalemate tester will also be used in the future as a component of the automatic rule generator (to de deployed).
When used as part of validating an experiment plan, the stalemate tester looks at how the parameter set in question specifies the set of objects allowed on the board. If the parameter set specifies the sets of colors and shapes, or (for image-and-property-based objects) speifies the set of objects, then the tester uses those sets. If no parameter set does not have any of those specifications, then the tester assumes that we have a GS-1.* style game with the 4 legacy shapes and 4 legacy colors.
The stalemate tester does not properly support parameter sets that specify that the games are to be played with prefedined initial boards. On such a parameter set the tester will ignore the initial board specifications, and will instead solve the stalemate problem for all boards using the legacy shapes and colors. This is not correct, especially if you intend the games to use custom shapes or colors.
When used as part of validating a "naked" rule set (without an experiment plan), the stalemate tester will assume that you intend the games to use the legacy shapes and colors.
Here we sketch the underlying "theory" for stalemate testing, without giving detailed proofs.
We will generalize the concept of a "board position" by introducing the concept of Multi-board. Unlike a normal board position in Rule Game, where each cell is either empty or contains a single game piece, a multi-board is defined as a position where each cell contains a set of game pieces. (A set is understood mathematically, i.e. as an assemblage of distinct pieces). A normal board position is, of course, a special case of multi-board, in which every cell happens to contain a set with no more than 1 element.
All game rules applied to our "normal" games can be applied to games with mutli-boards as well, in an obvious way. In the discussion below, a "position" will mean "mutli-board".
For a given set of allowed game pieces, the full board is a multi-board which contains a set of all possible pieces in each cell. Thus, for a legacy game (one with the 4 legacy colors and the 4 legacy shapes), the full board has a set of 16 game pieces (representing all possible combinations of shapes and colors) in each cell.
For any rule set without disappearing atoms (WODA rule set), we will define a stalemate position as a board position from which not a single game piece can be removed anymore.
We will define a lite rule set as a rule set which:
In other words, a "lite rule set" is one where all atoms are active at all times.
We will say that rule set R simplifies to lite rule set R' (R'=Simp(R)) if R' can be obtained from R by removing all counters (i.e. making all atoms and lines unmetered) and putting in all atoms into one rule line.
It is fairly easy to show that if R'=Simp(R), then any position A that is a stalemate position for R' is also a stalemate position for R. The converse is also true (any stalemate position for R' is also a stalemate position for R). Indeed, if A is a stalemate position for R', this means that no atom of R' can remove any game piece from A; but that also means that no atom of R can remove any piece from that position either, and therefore A is also a stalemate position from A'. Conversely, if A is a stalemate position for R, it means that even when the rule lines of R "cycle" and all counter reset their positions, none of the atoms of R can move a piece; thus, none of the atoms of R' can move a piece either.
The above equivalence means that, in the following discussion, it is sufficient to think only of "lite" rule sets, since any non-lite rule set R without disappearing atoms will behave the same way as the lite rule set obtained by the simplification of R.
We will say that position A is subsumed by position B (written, A ⊆ B) if every cell of B contains every game piece that the corresponding cell of A does (and perhaps some other pieces as well).
(It would have been so much easier to talk of A as a "subset of" B, but unfortunately we cannot, because positions aren't set. Technically, a multi-board can be defined as an N2-tuple of sets, each component of the tuple being the set of pieces in a particular cell. So if A is subsumed by B it means that A is a tuple each of whose components is a subset of the corresponding component of B.
Proposition 2: If C is a stalemate position for a WODA rule set R, and C' is some position that subsumes C, then when the position on the board in C', no piece from C is movable.
In other words, adding pieces to a stalemate position C will not make any pieces from C movable. The proof is based on the analysis on how atoms work. For an atom to allow moving a piece, the properties of the piece (such as shape and color) should match, and the position should match as well. The properties of the piece are not affected by adding more pieces to C. The position match can be never improved by adding pieces to C. That is, if the position expression refers to a fixed position (cell number), then it is not affected by adding extra pieces. If the position expression refers to an ordering (e.g. T, B, L1, etc), then the match requires the piece to be the first piece (or one of the piece in the first group) in the ordering; by adding more pieces, we can only make the position of the piece in the ordering "worse" (that is, a first piece can become a not-first piece, but not the other way around). Thus adding pieces to C can destroy a position match that existed in C, but cannot create a match where one did not exist in C.Proposition 3: In a WODA rule set, if the initial position A subsumes a stalemate position C, then any episode starting at A will stalemate, no matter how the player chooses to play
For a proof by contradiction, let's suppose that a player starts with postion A and eventually clears the board (i.e. does not get to a stalemate). During the process of clearing the board, one of the moves will transition from position P which subsumes C to position P' which does not subsume C. In other words, P contains all pieces from C and maybe some other pieces, while the next move removes one of the piece sfrom C. By proposition 2, the movability of pieces in P cannot be better than the movability of pieces in C. Thus, no pieces belonging to C can be moved when the position on the board is P. Thus we know that no pices from C will be ever removed, and the episode will stalemate at C or at some position B that subsumes C.
Although positions are not sets, we will use the expression union of A and B to mean a mutli-board each cell of which contains the union of the sets of pieces found in the respective cells of A and B.
Proposition 4: In a WODA rule set, if the initial position A subsumes a stalemate position C, then any episode starting with A will, no matter how the player choses to play, end with a stalemate in position B which is defined as the union of all stalemate positions subsumed by A.
This easily follows from the proof of the preceding proposition. If Q is a stalemate position subsumed by A, then we know that the player starting with A will never be able to remove any piece from A. Thus is B is a union of all stalemate positions subsumed by A, then no piece from B will be ever be removed by the player. On the other hand, every piece from A but not from B will be removed by the player at some point (otherwise, B will not be the union of all stalemate positions within A). Thus, B is the final position for the episode.
We will refer to B as the final position reachable from A, B=Fin(A). For an initial position A that does not lead to stalemate, Fin(A) is the empty board.
Proposition 5: In a WODA rule set, if A' ⊆ A, then the Fin(A') ⊆ Fin(A).
This directly follows from Prop. 4, as Fin(A) is a union of the same positions that form Fin(A') and then some.
Prop 5 immediately gives us the final proposition,
Proposition 6: In a WODA rule set, if position W is the full board, then Fin(W) subsumes Fin(B') for any position B.
Prop. 6 gives us an algorithm for finding whether a WODA rule set results in a stalemate. The stalemate tester starts with the full board W, and removes all removable pieces one by one, until either the board is empty or no more pieces can be removed. In the former case, we know that no initial position will result in a stalemate, and therefore the rule set cannot stalemate. In the latter case, we have obtained B=Fin(W), which is the union of all possible stalemate positions.
B=Fin(W) may be a multi-board, but it is easy to show that if we simplify B to some regular board position B' by leaving just 1 piece in any non-empty cell, B' will be also a stalemate position. This can be proven by reasoning similar to that used when proving Prop. 2: namely, all ordering-based position expressions return the same truth value for all pieces in B and in B'; thus if no atom of our rule set accepts any game piece of B, it won't accept any game piece of B' either.