Mikołaj Bojańczyk

The Zigzag Theorem says that two languages can be separated by a piecewise testable language if and only if there is no infinite zigzag between them. Therefore, to prove that separability is decidable, it suffices to decide if there exist infinite zigzags. We begin by phrasing the problem in purely monoid terms.

Let be a finite monoid. Define a zigzag between to be a zigzag over the alphabet , which alternates between words of type and type .  The following fact is easy to see.

Fact. Let languages be recognised by a surjective monoid morphism . Then there is a zigzag between and if and only if in the monoid there is a zigzag beteen for some and .

The zigzag game. By the above fact, deciding the existence of zigzags reduces to the question of deciding, for a given finite monoid, which pairs admits zigzags. To characterise this, we introduce a safety game, called the zigzag game of the monoid. The zigzag game is a special case of a safety game.

To highlight the character of the game, we call the two players Zigzag and Doubter, with player Zigzag playing the role of player in a safety game  (i.e. the player who wins when the game lasts forever).  The game has two kinds of positions. Positions owned by player Zigzag are pairs , while positions owned by player Doubter are words over the alphabet The intuitive idea is that represents a sequence that is growing in the Higman ordering, which begins with the empty word and then alternates between and , while represents a constant sequence which has the letter on all positions.

The game is played as follows. In a position of the form , player Zigzag chooses some word such that the product of the word, in the monoid , is equal to . If there is no such word then player Zigzag loses immediately. In a position of the form , player Doubter chooses some letter that appears in this word, and the game continues from position . If player Doubter cannot choose a letter, i.e. is empty, then player Doubter loses immediately.

If the game lasts forever, then player Zigzag wins (i.e. this is a safety game where player Zigzag is the player).

Theorem (Zigzag Game Theorem). In a finite monoid , there is a zigzag between and if and only if player Zigzag has a winning strategy from position .

Before proving the above theorem, we observe how it allows us to decide whether or not there exists a zigzag between and in the monoid. In principle, the game is infinite, because player Doubter has infinitely many positions. However, one can consider a reduced version of the game, which is equivalent, and has finitely many positions.

The reduced version of the zigzag game is defined as follows. The positions of player Zigzag are the same, i.e. they are pairs . The difference is in positions of player Doubter – these are now subsets of , of which there are finitely many. When in a position , instead of choosing a word in , player Zigzag chooses a subset such that there exists a word which evaluates to . In other words, player Zigzag chooses some which generates in in the monoid . In a set , player Doubter simply chooses an element and the game continues from position . It is easy to see that, when restricted to positions of the form , the two games are equivalent, i.e. player Doubter has a winning strategy in the zigzag game if and only if he has a winning strategy in the reduced zigzag game. Since the reduced zigzag game is a safety game with a finite arena, one can compute positions where player Zigzag has a winning strategy, and therefore, by equivalence of the two games and the Zigzag Game Theorem, one can decide which pairs in the monoid admit zigzags.

It remains to prove the Zigzag Game Theorem.

Proof. We only prove the more interesting left-to-right implication. We will prove that if there is a zigzag between and , then in position player Zigzag can choose some word , such that for every letter used by that word, there is a Zigzag between and .

To prove the above claim, we introduce some notation. Define a growing sequence to be a sequence which is growing with respect to the Higman ordering, but not necessarily strictly growing, i.e. consecutive elements can be equal.  The set of growing sequences forms a monoid when equipped with pointwise concatenation: Define the type of a growing sequence to be the sequence of types of the words in , i.e. the type is an element of . A zigzag between and is a growing sequence whose type is . The left-to-right part of the theorem follows immediately from the following lemma.

Lemma. If there exists a zigzag between , then there exist a zigzag which can be decomposed as where are growing sequences such that each one of them has a type of the form for some .

It remains to prove the lemma. Consider a zigzag between and . Here is a picture of such a zigzag, with the rows representing words in thezigzag, and columns representing the letters (the letter is black when it first appears, and in later rows it is grey): Note that the picture has actually infinitely many columns, because each row introduces a new letter (and therefore the set of columns is some countable totally ordered set). Each block of consecutive columns represents a growing sequence.  The first row in the zigzag has a finite number of letters, say . (In the above picture, .)  Let us distinguish these letters as columns (i.e. constant growing sequences), pictured in red below: The red columns are constant sequences, in particular growing sequences, and therefore each red column has a type of the form as required in the lemma. Let us group the remaining columns, so that columns are in the same group if they are not separated by red columns, i.e. columns that correspond to letters from the first row. This is shown in the  following picture, with the remaining columns grouped into blue groups:

Clearly there will be at most blue groups, and each one will be a growing sequence. Furthermore, each blue group begins with the empty word, i.e. its type begins with . Using the pigeon hole principle, we can remove rows so that the result is still a zigzag between and , but each of the blue groups has a type of the form as required by the lemma. This completes the proof of the lemma and of the the theorem. 