String-to-String Interpretations with Polynomial-Size Output

TL;DR

This paper characterizes string-to-string MSO interpretations as exactly the polyregular functions, showing they are closed under composition and have polynomial output size, connecting logical and automata-theoretic perspectives.

Contribution

It establishes that string-to-string MSO interpretations are equivalent to polyregular functions and are closed under composition, bridging logic and automata theory.

Findings

String-to-string MSO interpretations are exactly polyregular functions.

Polyregular functions are recognized by pebble transducers.

MSO interpretations are closed under composition.

Abstract

String-to-string MSO interpretations are like Courcelle's MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial in the input length, as opposed to MSO transductions, which have output of linear length. We show that string-to-string MSO interpretations are exactly the polyregular functions. The latter class has various characterizations, one of which is that it consists of the string-to-string functions recognized by pebble transducers. Our main result implies the surprising fact that string-to-string MSO interpretations are closed under composition.

Figures

Equations

$$abbb\mapsto \underbrace{a}\underbrace{ba}\underbrace{bba}\underbrace{bbba}.$$

$${\phi }_a(x_1,x_2)=a(x_2){\phi }_b(x_1,x_2)=b(x_2)$$

$${\phi }_{\le }(\underset{\begin{array}{c}\text{a position of}\\ \text{the output word}\end{array}}{\underbrace{x_1,x_2}},\underset{\begin{array}{c}\text{another position of}\\ \text{the output word}\end{array}}{\underbrace{x_1^{\prime },x_2^{\prime }}})=(x_1<x_1^{\prime })\vee (x_1=x_1^{\prime }\wedge x_2\ge x_2^{\prime }).$$

$$w\models \phi (\bar{x})\text{iff}f(w)\models \psi (\bar{x})\text{for every w∈Σ∗ and k-tuple of positions xˉ.}$$

$$=$$

$$\text{(first-order polyregular)}\circ \text{rational}$$

$$\text{(first-order interpretations)}\circ \text{rational}$$

$$\text{first-order string-to-string interpretations}\subseteq \text{first-order definable for-programs}$$

$$abbb\mapsto (1,1),(2,2),(2,1),(3,3),(3,2),(3,1),(4,4),(4,3),(4,2),(4,1)$$

$$x⊏y\text{if}\text{x is a position in wi and y is a position in wj for some i<j.}$$

$$w_i{\equiv }_{\omega }{w}_{i+1}\text{holds for all i∈{1,…,n−1} with at most m exceptions,}$$

$$x_d{⊏}^p{y}_d\text{implies}(x_1,\dots ,x_k)\prec (y_1,\dots ,y_k)\text{for all of type tx1,…,xk,of type ty1,…,yk in A}.$$

$$x_d{<}^p{y}_d\text{implies}(x_1,\dots ,x_k)\prec (y_1,\dots ,y_k)$$

$$w=w_1\cdots w_n$$

$$T:=\left\{\bar{x}\in X_1\times \cdots \times X_k:\text{xˉ has type t and is in the output of f(w)}\right\}$$

$$x_d{⊏}^p{y}_d\text{implies}(x_1,\dots ,x_k)\prec (y_1,\dots ,y_k)\text{for all of type tx1,…,xk,of type ty1,…,yk in A}.$$

$$v\in {\left\{\text{positions before X, X, positions after X}\right\}}^k$$

$$(a_1,a_n),\dots ,(a_n,a_1).$$

$$f(w)\in L\text{if and only if}w=⊢v⊣\text{ for some palindrome v without ⊢,⊣ }.$$

$$(a_i,a_1),(a_{i+1},a_2),\dots ,(a_n,a_{n-i+1}).$$

$$h:{\Sigma }^{+}\to S.$$

$$\displaystyle\begin{array}[]{ccc}S&\rightarrow&S\\ t&\mapsto&ts\end{array}\qquad\text{and}\qquad\begin{array}[]{ccc}S&\rightarrow&S\\ t&\mapsto&st\end{array}$$

$$h_T:T^{+}\to T$$

$$h_{\ne s}:(\Sigma -\left\{s\right\}{)}^{+}\to S$$

$$w=w_1{s}^{k_1}\cdots w_n{s}^{k_n}{w}_1,\dots ,w_n\in (\Sigma -\left\{s\right\}{)}^{+}{k}_1,\dots ,k_n\in \left\{1,2,\dots \right\}.$$

$$\mathfrak{A}:=\prod _{i\in I}{\mathfrak{A}}_i^{k_i}\text{such that ki≤k for all i},$$

$${\mathfrak{A}}_i={\mathfrak{A}}_{i,1}\cdots {\mathfrak{A}}_{i,n_i}\text{with }{\mathfrak{A}}_{i,1}{\equiv }_{r+k}\cdots {\equiv }_{r+k}{\mathfrak{A}}_{i,n_i}.$$

$$x[d][e]{⊏}^{p}y[d][e]\text{implies}x\prec y\text{for all x,y∈A of type t.}$$

$$\mathfrak{A}=\prod _{i\in I}(\left\{1,\dots ,n_i\right\},<).$$

$$\mathfrak{A}=(\left\{1,\dots ,n\right\},<{)}^k.$$

$$\mathfrak{A}=\prod _{i\in I}(\left\{1,\dots ,n_i\right\},<{)}^{k_i}.$$

Full text

String-to-String Interpretations with Polynomial-Size Output

Mikołaj Bojańczyk

  

Sandra Kiefer

  

Nathan Lhote

Our main result implies the surprising fact that string-to-string mso interpretations are closed under composition.

1 Introduction

A string-to-string function is called regular if it is computed by a deterministic two-way automaton with output. There are many equivalent models for the same class of functions: string-to-string mso transductions [10], streaming string transducers [1], and various kinds of combinator-based formalisms [2, 8, 5].

A deterministic two-way automaton can visit each input position at most once in each state, otherwise it would loop forever. This means that the length of the run – and also the size of the output word – is linear in the input string. One way to go beyond linear-sized outputs was proposed by Milo, Suciu, and Vianu [17], following earlier work by Globerman and Harel [12]: equip the automaton with $k$ pebbles which can be used to mark positions in the input word. To avoid making the model Turing-powerful, the pebbles are required to observe a so-called stack discipline: the pebbles are organised in a stack, and only the top-most pebble can be moved. In [3], it is shown that pebble transducers are equivalent to multiple other models: a higher-order functional programming language [3, Section 4], an imperative programming language with for-loops [3, Section 3], combinators [3, end of Section 4], and compositions of certain simple atomic functions [3, Section 1]. Because of the multitude of models and their polynomial size outputs, the class of functions recognised by these models is called polyregular functions.

The list of models for polyregular functions described in [3] does not include any logical model. In this paper, we fix that omission. As mentioned above, for the regular functions, which have linear size output, the logical model consists in string-to-string mso transductions. In an mso transduction, each position of the output string is interpreted as a single position of the input string. A natural idea to capture polyregular functions is to consider what we call string-to-string mso interpretations, where a position of the output string is represented by a $k$-tuple of positions in the input string. At first glance, this idea looks suspicious: if string-to-string mso interpretations were equivalent to polyregular functions, then they would be closed under composition, because the class of polyregular functions is. However, composing two string-to-string mso interpretations

[TABLE]

raises the following issue. Suppose that positions of the intermediate word in $\Gamma^{*}$ are represented by $k$-tuples of positions in the input word from $\Sigma^{*}$. If an mso formula defining $g$ quantifies over a set of positions in the intermediate word to define a property of the output word in $\Delta^{*}$, then this corresponds to quantifying over a set of $k$-tuples of positions in the input word. If we assume dimension $k=1$, then the problem dissolves, and this is why mso transductions have dimension $k=1$, whereas dimension $k>1$ is never used in the context of mso (as opposed to first-order logic, where the standard notion of transformation, i.e. first-order interpretation, uses higher dimension).

As our main result, we show that the problems discussed above only invalidate the natural construction for composing mso interpretations, which uses substitution of formulas. Still, and surprisingly, for structures that represent strings there exists a (less natural) construction. This follows from our main result which states that polyregular functions are exactly the string-to-string mso interpretations. Indeed, corollaries of the main result are that (a) string-to-string mso interpretations are closed under composition; and (b) for every regular string language, its inverse image under a string-to-string mso interpretation is also regular. This is because (a) and (b) are true for polyregular functions. Proving (a) and (b) directly for string-to-string mso interpretations seems hard; in fact an understandable (but wrong) first reaction to the claims (a) and (b) would be that they are false, for the reasons discussed in the previous paragraph.

It is easy to see that every polyregular function is a special case of a string-to-string mso interpretation. One argument is that a $k$-pebble automaton can be simulated using a string-to-string mso interpretation, where configurations of the pebble automaton are represented using $k$-tuples of positions in the input word. The difficulty lies in proving the opposite direction and it comes from the stack discipline required in a pebble automaton. A $k$-tuple of positions used by an mso interpretation can of course be viewed as a configuration of a pebble automaton, but there does not seem to be any reason why the resulting pebble automaton should observe stack discipline. It turns out – and this is the main technical insight of this paper – that any mso formula which defines a linear ordering on $k$-tuples of positions in strings must necessarily observe an implicit stack discipline, which makes it possible to translate a string-to-string mso interpretation into a pebble automaton.

Outline.

After describing string-to-string mso interpretations in Section 2, we revise polyregular functions via the formalism of for-programs in Section 3. In Section 4, we show that the models are equivalent.

2 Interpretations

In this section, we revise first-order and mso interpretations, which are transformations of relational structures using formulas.

2.1 Logic and interpretations

Relational vocabularies and logic.

A (relational) vocabulary is a set of relation names, each one associated with a natural number called its arity. For short, we refer to relational vocabularies simply as vocabularies. A structure over a vocabulary $\sigma$ consists of a set called the universe and for each relation name of $\sigma$ a corresponding relation of the same arity over the universe. To define properties of relational structures, we use monadic second-order logic and its first-order fragment with the usual syntax and semantics [20]. We use the convention that lower-case variables $x,y,z$ range over elements and upper-case variables $X,Y,Z$ range over sets of elements.

Interpretations.

Intuitively speaking, an interpretation is a function from relational structures to relational structures where each element of the universe of the output structure is a tuple of elements of the input structure, and the relations of the output structure are defined using formulas evaluated over the input structure.

Definition 2.1** (Interpretations over general structures).**

For $k\geq 1$, the syntax of a $k$-dimensional first-order interpretation consists of:

two vocabularies, called the input vocabulary and the output vocabulary 2. 2.

an fo formula over the input vocabulary with $k$ free variables, called the universe formula. 3. 3.

for each $n$ and each $n$-ary relation name $R$ of the output vocabulary, an associated fo formula $\varphi_{R}$ over the input vocabulary, with $k\cdot n$ free variables.

mso interpretations* are defined analogously, except that formulas of mso are used, but the free variables still range over elements and not over sets.*

The semantics of an interpretation is a function from structures over the input vocabulary to structures over the output vocabulary, defined as follows.

• •

The universe of the output structure is the set of $k$-tuples of elements in the universe of the input structure which satisfy the universe formula from item 2 in Definition 2.1.

• •

An $n$-ary relation name $R$ of the output vocabulary is interpreted as the set of $n$-tuples of $k$-tuples from the input structure, for which (a) each $k$-tuple is in the output universe, and (b) the entire $(n\cdot k)$-tuple satisfies the formula $\varphi_{R}$ in item 3 in Definition 2.1.

Composition.

First-order interpretations are closed under composition [14, p. 218]. Let us recall the proof. Suppose that we want to compose interpretations

[TABLE]

of dimensions $k_{1}$ and $k_{2}$, respectively. The $(k_{1}\cdot k_{2})$-dimensional composition is obtained from $\mathcal{I}_{2}$ as follows: (a) quantification over elements of $\mathcal{I}_{2}$ is replaced by a quantification over $k_{1}$-tuples of elements; and (b) relation names from $\sigma_{2}$ that appear in the input of $\mathcal{I}_{2}$ are replaced by the corresponding formulas from $\mathcal{I}_{1}$. This idea does not work for mso in general, since set quantification in $\mathcal{I}_{2}$ would need to be replaced by quantification over sets of $k_{1}$-tuples. It does work when $k_{1}=1$. This essentially corresponds to Courcelle’s transductions, for which closure under composition follows naturally [7, Theorem 7.14]. To recover closure under composition for $k_{1}\geq 2$, one can use (not necessarily monadic) second-order logic, which by Fagin’s Theorem [16, Corollary 9.9] corresponds to the polynomial hierarchy of computational complexity and is outside the scope of this paper.

2.2 String-to-string interpretations

We are interested in interpretations that transform structures which represent strings. While there are two natural ways to model strings as relational structures, namely with an order relation or with a successor relation, only the order relation is useful in our context.

Definition 2.2** (String-to-string interpretations).**

For a string $w\in\Sigma^{*}$, its ordered model is defined to be the following relational structure, denoted by $\underline{w}$:

• •

the universe consists of the positions in the string, i.e., natural numbers;

• •

there is a binary relation for the natural order on positions;

• •

for each $a\in\Sigma$ there is a unary relation which is satisfied by every position with label $a$.

A function $f\colon\Sigma^{*}\to\Gamma^{*}$ is called a first-order string-to-string interpretation if the corresponding transformation on ordered models is a first-order interpretation for strings with length at least two111A typical operation we want to model is string duplication. When the input length is at least two, one can represent additional copies of the input string using a higher dimension. For input length $n\leq 1$, the output length will be $n^{k}\leq 1$ regardless of the dimension $k$. Another solution to this issue would be to have duplication built into the definition of interpretations. . Likewise we define mso string-to-string interpretations.

Example 2.3**.**

Consider the function $f\colon\left\{a,b\right\}^{*}\to\left\{a,b\right\}^{*}$ which maps a word to the concatenation of all of its reversed prefixes, as in the following example (with prefixes grouped for better readability):

[TABLE]

This transformation is the running example in [3]. We show that $f$ can be seen as a string-to-string first-order interpretation. The dimension is $2$, i.e. positions in the output word represent pairs of positions in the input word. A pair $(x_{1},x_{2})$ of positions in the input word is used in the output word if it satisfies the universe formula $x_{2}\leq x_{1}$. The idea is that $x_{1}$ represents the length of the prefix, while $x_{2}$ is the position in that prefix. The label of a position $(x_{1},x_{2})$ is inherited from the second coordinate, as expressed by the formulas corresponding to labels on the output structure:

[TABLE]

The order on the positions of the output word is defined by the formula

[TABLE]

Note that the above formula defines the lexicographic ordering on pairs of positions, with the first coordinate being used in increasing order, and the second coordinate being used in decreasing order. This, as it will turn out, is not a coincidence, since our main technical result says that it is impossible to define a linear order on tuples of positions without implicitly using some kind of lexicographic ordering.

Successor instead of order.

When modelling a string as a relational structure, we use the order on positions. An alternative solution would be to use just the successor relation. The difference between the two solutions is that it is harder to define an order on $k$-tuples of positions than it is to define a successor relation. It turns out that the difference is crucial, and functions that output strings with successor can be ill-behaved. Note that whether or not the input string is equipped with an order or a successor relation makes no difference, since the order on the position of the input string can be recovered in mso, which can compute the transitive closure of binary relations on positions.

Define the successor model of a string in the same way as the ordered model from Definition 2.2, except that a binary relation for successor is used instead of the order. Define a successor-mso string-to-string interpretation to be a string-to-string function which is computed by an mso interpretation, assuming that strings are represented by their successor models. Likewise, we define successor-first-order string-to-string interpretations. Successor-first-order string-to-string interpretations are closed under composition, because first-order interpretations are closed under composition. On the other hand, successor-mso string-to-string interpretations are not closed under composition and lead to undecidability, as summarised in the following theorem. The proof can be found in Appendix A.

Theorem 2.4**.**

The class of successor-mso string-to-string interpretations is not closed under composition, and strictly contains the class of (order-)mso string-to-string interpretations. 2. 2.

The following is undecidable: given a successor-first-order string-to-string interpretation $f$ and a regular language $L$ over the output alphabet, decide if $f^{-1}(L)$ is nonempty.

3 Polyregular functions

Here we describe the class of polyregular functions. It has several equivalent characterisations, see [3, Theorem 4.4], one of which consists in the aforementioned pebble transducers. For the purposes of this paper, it will be most convenient to use a slightly more abstract characterisation in terms of for-programs, a machine model for string-to-string functions. We just explain the formalism on short examples, for a more detailed description see [3].

Most of the syntactic constructions that can be used in a for-program are illustrated in Figure 1(a): (1) variables ranging over positions in the input word; (2) for-loops in which a variable iterates over all positions in the input word in increasing or decreasing order; (3) if-statements which depend on the order/labels of variables; (4) instructions which output letters. Position variables cannot be declared or written to, they are implicitly declared by for-loops and their only updates are the iterations performed by the for-loops.

The only feature of for-programs that is not used in Figure 1(a) is (5) Boolean variables. Figure 1(b) shows a program that outputs only those letters in the input word which have even distance to the last position. In the program, the Boolean variable P is declared in the scope of a for-loop. On each iteration of the loop, the variable is reinitialised to false.

A for-program is called first-order definable if Boolean variables can only be updated from false, which is their initial value upon declaration, to true. In other words, the only allowed update for Boolean variables is P := true. For the first-order restriction, it is important that Boolean variables can be declared inside for-loops, and that they are reinitialised to false at each iteration of the loop that they are declared in. The reason for the name “first-order definable” is that one can define in first-order logic the reachability relation on program states of the for-program, see [3, Lemma 5.3].

Definition 3.1**.**

A string-to-string function is called polyregular if it is computed by a for-program. It is called first-order polyregular if it is computed by a first-order definable for-program.

The class of polyregular functions has other characterisations, including the string-to-string pebble transducers introduced by Milo, Suciu and Vianu [17], as well as a higher-order functional programming language [3, Section 4]. The main result of this paper, Theorem 4.1 in the next section, adds a logical characterisation, namely string-to-string mso interpretations.

Evaluating first-order formulas.

The for-programs described above take as input strings and also output strings. One can also consider for-programs which input a string with distinguished positions and which output a Boolean value, as in Figure 1(c). The distinguished positions are represented by free variables (here x1 and x2) while the output value is taken from some distinguished Boolean variable, here P.

Lemma 3.2**.**

Let $\varphi(x_{1},\ldots,x_{k})$ be an fo formula over strings. There is a first-order for-program which computes the following.

• •

Input.* A word $w\in\Sigma^{*}$ and positions $x_{1},\ldots,x_{k}$ in $w$;*

• •

Output.* Yes or No, depending on whether $w$ satisfies $\varphi(x_{1},\ldots,x_{k})$.*

Proof 3.3**.**

The for-program implements the semantics of an fo formula. For each quantifier, it loops over all possible values for the quantified position, and a Boolean variable is used to remember if some value has already been found which renders the formula true.

A similar result is true for mso formulas, but the proof for that statement uses automata.

4 Equivalence

We show that the models defined in Sections 2 and 3 are equivalent.

Theorem 4.1**.**

String-to-string mso interpretations are exactly the polyregular functions. 2. 2.

First-order string-to-string interpretations are exactly the first-order polyregular functions.

Since the class of polyregular functions is closed under composition222Closure under composition was proved for pebble transducers in [9, Theorem 11] and for the class of for-programs in [3, Section 8.1] as a step in proving equivalence with the other models of polyregular functions., we obtain:

Corollary 4.2**.**

String-to-string mso interpretations are closed under composition.

By using Theorem 4.1, the proof of the corollary passes through for-programs. We are not aware of any direct proof that does not exploit the equivalence to polyregular functions.

The rest of this paper is dedicated to the proof of Theorem 4.1. We begin with a reduction of the first to the second item. This reduction illustrates a general phenomenon, namely that results about first-order polyregular functions often imply results about general polyregular functions, despite the latter class being larger. The reason behind this phenomenon is the following lemma, which says that for every polyregular function, all of the behaviour that is not first-order definable can be pushed into a simple preprocessing step. Define a rational function, see [4, Section 13.2], to be a string-to-string function which is recognised by a nondeterministic automaton, where every transition is labelled by a pair consisting of a letter from the input alphabet and a string over the output alphabet, and which is unambiguous in the sense that every input string admits exactly one accepting run.

Lemma 4.3**.**

A function is polyregular if and only if it is a composition consisting of:

1. (a)

a (letter-to-letter) rational function; followed by 2. (b)

a first-order polyregular function. 2. 2.

A function is an mso string-to-string interpretation if and only if it is a composition consisting of:

1. (a)

a (letter-to-letter) rational function; followed by 2. (b)

a first-order string-to-string interpretation.

The proof of Lemma 4.3 is based on ideas from [6, 15, 3] and uses factorisation forests.

Proof 4.4**.**

The right-to-left implications in items 1 and 2 are proved the same way: both polyregular functions and mso string-to-string interpretations are closed under pre-composition with rational functions. For the class of polyregular functions, this holds because it is closed under composition and contains all rational functions [3, Theorem 1.6]. For mso string-to-string interpretations, one observes that rational functions are a special case of mso string-to-string interpretations of dimension 1 (see [11, Figure 7], where mso interpretations of dimension 1 are the same as the so-called regular functions), and mso interpretations are closed under pre-composition with such functions (see the remarks at the end of Section 2.1).

To prove the left-to-right implications in items 1 and 2, namely the decomposition into rational pre-processing and first-order post-processing, we use the following claim.

A letter-to-letter rational function is a rational function where every transition in the underlying automaton is labelled with exactly one output letter, in which case the input and output strings have the same set of positions.

Claim 1**.**

Let $\varphi$ be an mso formula which selects $k$-tuples of positions in strings over an alphabet $\Sigma$. There are a letter-to-letter rational function $f\colon\Sigma^{*}\to\Gamma^{*}$ and a first-order formula $\psi$ which selects $k$-tuples of positions in strings over the alphabet $\Gamma$ such that

[TABLE]

The claim is the special case of [6, Theorem 2] for finite strings instead of infinite trees, and its proof uses factorisation forests (see  [19]). Another proof of the above claim is in [15, Theorem 3.2]. Using the claim, we immediately get the left-to-right implications in item 2. For item 1, we also use Lemma 4.3 to obtain a first-order for-program realizing the function. The main idea is that if the reachability relation is first-order definable, then one can define a first-order query which accepts consecutive produced tuples.

With the lemma, we show that item 2 in Theorem 4.1 implies item 1, i.e. if first-order string-to-string interpretations are exactly the first-order polyregular functions, then mso interpretations are exactly the polyregular functions:

[TABLE]

It remains to prove item 2 in Theorem 4.1, i.e. that first-order string-to-string interpretations are exactly the first-order polyregular functions. The right-to-left inclusion follows immediately from [3, Lemma 5.3], which says that a formula in first-order logic can define the reachability relation on program states in first-order for-programs. We are left with the left-to-right-inclusion:

[TABLE]

The rest of the paper is devoted to showing the above inclusion. When simulating a first-order interpretation by a for-program, we will mainly be concerned with the universe of the output string (which is a set of $k$-tuples of positions in the input string) and its ordering. The labelling of the $k$-tuples can then be recovered using the for-program from Lemma 3.2. The main result is that every first-order definable linear ordering on tuples of positions can be implemented by a for-program. To be able to speak about this result, we introduce some notation for devices that produce lists of tuples of positions.

Enumerators.

Let $k\in\mathbb{N}$. A $k$-enumerator over an alphabet $\Sigma$ is a function of the following form:

• •

Input. A string $w\in\Sigma^{*}$;

• •

Output. A list of $k$-tuples of positions in $w$, which is nonrepeating333Every tuple appears at most once, but positions can appear in multiple tuples. We need this for the existence of the formulas stated in the following definitions..

We compare the following two ways of implementing $k$-enumerators:

A $k$-enumerator is called definable if there are two fo formulas: one with $k$ variables, which says when a tuple is part of the output list, and one with $2k$ variables, which defines a total order on the tuples selected by the first formula. 2. 2.

A $k$-enumerator is called programmable if its output can be computed by a first-order for-program which instead of outputting letters uses instructions of the form output (x1,...,xk) where x1$,\ldots,$xk are position variables.

For definable $k$-enumerators, the order on tuples in the output list is given explicitly by the formula $\varphi$, while in programmable ones, the order is implicit from the order in which the output instructions are executed during the computation.

Example 4.5**.**

We present an enumerator based on Example 2.3. Consider the $2$-enumerator which outputs all pairs of positions $(x_{1},x_{2})$ with $x_{2}\leq x_{1}$, listed in lexicographic order, where $x_{1}$ is ordered in increasing order and $x_{2}$ is ordered in decreasing order. Here is an example:

[TABLE]

This enumerator is definable, as witnessed by the formula $\varphi_{\leq}$ in Example 2.3. The formula $\varphi_{\leq}$ is quantifier-free, but in general, quantifiers are allowed. Here is a for-program which computes the same function:

The following lemma is the main technical result of this paper.

Lemma 4.6**.**

Every definable $k$-enumerator is also programmable.

Our proof of Lemma 4.6 uses two fundamental ingredients. The first is by now standard: this is Simon’s factorisation forest theorem [19], which roughly says that every string can be cut into pieces that are similar to each other. The second ingredient is new: the Domination Lemma, presented in Section 4.1, roughly says that if a string is cut into pieces that are similar to each other, then any first-order definable linear order on tuples of positions must observe an implicit stack discipline. These two results are combined in Section 4.2 to prove Lemma 4.6. Before we proceed with the proof of Lemma 4.6, we use it to complete the proof of Theorem 4.1.

Proof 4.7** (Proof of Theorem 4.1, second part).**

The only part of Theorem 4.1 that has not been proved yet is that every first-order string-to-string interpretation is polyregular. Suppose that $f$ is a $k$-dimensional first-order string-to-string interpretation. Consider the $k$-enumerator which inputs a string $w$ and outputs the list of $k$-tuples of positions in $w$ that are used to represent output positions of $f(w)$, in the appropriate order. Apply Lemma 4.6 to obtain a first-order for-program $g$ which computes the same list. To compute the original function $f$, we use a for-program which behaves as $g$, except that instead of outputting a $k$-tuple of positions like $g$, it uses the program described in Lemma 3.2 as a subroutine to check what is the output letter that should be produced for this tuple, and outputs that letter.

4.1 The Domination Lemma

In this section we present the Domination Lemma, which says that if $\prec$ is a first-order definable linear order on $k$-tuples of positions in a string, then there is an implicit stack discipline in the following sense. For every type (see below) $t$ of tuples of positions there is a coordinate $d\in\left\{1,\ldots,k\right\}$ such that for the subset of $k$-tuples of positions consisting in all of type $t$, the order $\prec$ is uniquely determined by the order of the $d$-th coordinates in the string.

We begin by explaining the notions of types. For $r\in\left\{0,1,\ldots\right\}$, the rank $r$ type of a structure ${\mathfrak{A}}$ with $k$ distinguished positions $\bar{x}\coloneqq(x_{1},\dots,x_{k})$ is defined to be the set of first-order formulas of quantifier rank at most $r$ and $k$ free variables that are true in ${\mathfrak{A}},\bar{x}$. The number $k$ is the arity of the type. For arity 0, we talk about the rank $r$ type of the structure ${\mathfrak{A}}$. If the structure ${\mathfrak{A}}$ is implicit from the context, then we talk about the rank $r$ type of the tuple $\bar{x}$. For every finite vocabulary, there are finitely many types of given arity and rank. We write $\equiv_{r}$ for the equivalence relation on structures with distinguished elements of having the same rank $r$ type. For a binary relation $R$, its inverse is the set $\{(v,u)\mid(u,v)\in R\}$. For $p\in\left\{1,-1\right\}$, define $R^{p}$ to be either $R$ or its inverse, depending on the value of $p$.

Lemma 4.8** (Domination Lemma).**

For all $k,m,r\in\left\{1,2,\ldots\right\}$, there is an $\omega\in\left\{1,2,\ldots\right\}$ with the following property. Let $n\in\{1,2,\ldots\}$, let $w_{1},\dotsc,w_{n}$ be strings over some alphabet $\Sigma$ and let ${\mathfrak{A}}$ be the ordered structure of the concatenation $w_{1}\cdots w_{n}$ extended with the block order defined by

[TABLE]

Let $\prec$ be a linear order on $k$-tuples in ${\mathfrak{A}}$ defined by a first-order formula of quantifier rank $r$, and let $t$ be a $k$-ary rank $\omega$ type over the vocabulary of ${\mathfrak{A}}$. If

[TABLE]

then there is a $d\in\left\{1,\ldots,k\right\}$, called the dominating coordinate, and a $p\in\left\{-1,1\right\}$, called the polarity, such that

[TABLE]

The Domination Lemma is the technical heart of this paper. The full proof is presented in Appendix C. To explain more intuitively some of the ideas that we use, we treat a special case in detail. In the Domination Lemma, the structure ${\mathfrak{A}}$ consists of blocks organised in a linear way. A very simple linear order – although infinite – is the natural one on the rational numbers; one reason for its simplicity is that quantifiers can be eliminated (see [13, Section 5.6.2]). Because of this, it is quite easy to prove a version of the Domination Lemma for the rational numbers and still its proof bears some similarity to the proof of the general case.

Lemma 4.9** (Rational Domination Lemma).**

Let $\prec$ be a linear ordering on $k$-tuples of rational numbers defined by a quantifier-free (equivalently, first-order) formula using only the usual ordering $<$ on rational numbers. Then there is a coordinate $d\in\left\{1,\ldots,k\right\}$ and a polarity $p\in\left\{-1,1\right\}$ such that

[TABLE]

for all tuples of rational numbers satisfying $x_{1}<\cdots<x_{k}$ and $y_{1}<\cdots<y_{k}$.

Proof 4.10**.**

We first prove the statement for $k=1$ and $k=2$ and then we deduce the general case.

When $k=1$, then the formula defining $\prec$ must be either $x<y$ or $x>y$. 2. 2.

For $k=2$, we do a case analysis. Note that whether $\bar{x}\prec\bar{y}$ or $\bar{y}\prec\bar{x}$ holds depends only on the order relationship of the positions in $\bar{x}$ and $\bar{y}$ in the rational numbers and not on the precise values in $\bar{x}$ and $\bar{y}$.

The following picture shows the two possible relationships for two pairs $\bar{x}$ and $\bar{y}$ when they are “consecutive” and the two possible relationships when they are “nested”:

Suppose we are given a pair $\bar{x}$ and without loss of generality, assume the “consecutive growing” case for a second pair $\bar{y}$. We only show the proof for the case that there is a pair $\bar{y}^{\prime}$ such that $\bar{x}$ and $\bar{y}$ are “nested growing” (“nested decreasing” works analogously). We prove that $d=1$ is dominating for $\prec$ with polarity $p=1$. Consider all three remaining configurations of pairs $\bar{x}$ and $\bar{y}$ with $x_{1}<y_{1}$. In all cases, $\bar{x}\prec\bar{y}$ is proved by finding an intermediate pair (drawn in yellow), whose order with respect to $\bar{x}$ and $\bar{y}$ follows from the assumptions “consecutive/nested growing” (in the pictures below, we assume that lower lines represent bigger tuples in the ordering $\prec$): 3. 3.

Consider the case $k>2$. Fix a “growing” tuple of $k$ rational numbers, i.e. a tuple $\bar{z}$ such that for $1\leq i<j\leq k$ it holds that $z_{1}\leq z_{i}<z_{j}\leq z_{k}$. Define $\prec^{\bar{z}}_{ij}$ to be the restriction of $\prec$ to tuples that agree with $\bar{z}$ on coordinates from $\left\{1,\ldots,k\right\}\setminus\left\{i,j\right\}$. Using the reasoning from the previous item, the ordering $\prec^{\bar{z}}_{ij}$ must admit some dominating coordinate $d\in\left\{i,j\right\}$ and one of the cases “growing” or “decreasing”. This must hold for every choice of $\bar{z}$ and $i,j$. Furthermore, the dominating coordinate $d$ depends only on $i$ and $j$ and not on $\bar{z}$, likewise for the choice of “growing” or “decreasing”. Let us write $i\to j$ if $j$ dominates, otherwise we write $j\to i$. The reasoning in the following picture shows that $\to$ is transitive, i.e. $i\to j$ and $j\to m$ implies $i\to m$:

Therefore, $\to$ is in fact a total order on $\left\{1,\ldots,k\right\}$. Let $d$ be the maximum with respect to this order. The following picture explains why $d$ is the dominating coordinate $d$ from the statement of Lemma 4.8.

Suppose without loss of generality that we are in the “growing” case for each pair of coordinates. Then we can first move all coordinates apart from $d$ to positions smaller than $\min\{x_{1},y_{1}\}$ or bigger than $\max\{x_{k},y_{k}\}$ and then use the dominations $i\to d$ to move them, one by one, to their final positions (always increasing the $d$-th coordinate slightly to a value in the open interval $(x_{d},y_{d})$).

4.2 Proof of Lemma 4.6

We now return to Lemma 4.6, i.e., we prove that every definable $k$-enumerator is also programmable. In the proof, we use the following version of the Factorisation Forest Theorem. We use the term interval for a connected set of positions in a string.

Theorem 4.11** (Factorisation Forest Theorem, aperiodic variant).**

Let $h\colon\Sigma^{+}\to S$ be a semigroup homomorphism, where $S$ is finite and aperiodic. Then there exists a function which assigns to each string in $\Sigma^{+}$ a partition of the positions into intervals (so-called blocks) such that:

All blocks are nonempty, and for each string in $\Sigma^{+}$ of length at least 2, there are at least two blocks. 2. 2.

If a string has at least three blocks, then all of the blocks have the same value under $h$. 3. 3.

There exists $M\in\mathbb{N}$ such that all strings have height at most $M$, where the height of a string is defined as follows: letters have height 1, for other strings the height is the maximum of the heights of its blocks + 1. 4. 4.

There is a first-order formula $\varphi$ such that for every string $w$, the positions satisfying $\varphi(x)$ are exactly the first positions of the blocks of $w$.

Apart from the Factorisation Forest Theorem and the Domination Lemma, our proof uses the following straightforward result on combining outputs of two for-programs. As a convention, if $\psi$ is a first-order formula with $k$ free variables and $f$ is a $k$-enumerator, then $f|\psi$ denotes the $k$-enumerator where the output list of $f$ is filtered so that it contains only tuples satisfying $\psi$.

Lemma 4.12** (Merging Lemma).**

Let $f$ be a definable $k$-enumerator. Let $\Phi$ be a finite set of fo formulas $\psi$, each one with $k$ free variables, such that every $k$-tuple of positions satisfies at least one formula from $\Phi$. Then $f$ is programmable if and only if every $f|\psi$ is programmable.

Proof 4.13**.**

For the left-to-right implication, we observe that the filtering $f|\varphi$ can be implemented by a for-program thanks to Lemma 3.2. We are left with the right-to-left implication. It suffices to examine the case $|\Phi|=2$. The general case follows by a straightforward induction.

Suppose that $f|\varphi_{1}$ and $f|\varphi_{2}$ are implemented by programs $f_{1},f_{2}$. First check whether the first tuple in the output satisfies $\varphi_{1}$ or $\varphi_{2}$ using the result from Lemma 3.2 and an if-statement, and then run a different program for each of the two outcomes. By symmetry, it suffices to consider inputs where the first tuple in the output of $f|(\varphi_{1}\vee\varphi_{2})$ satisfies $\varphi_{1}$. Take the code of $f_{1}$, and after each instruction which outputs a tuple of positions $\bar{x}$, run a copy of the code for $f_{2}$, with its output restricted to tuples $\bar{y}$ which satisfy:

• •

$\bar{y}$* is after $\bar{x}$ according to $f$; and*

• •

there are no other tuples from the output of $f_{1}$ between $\bar{x}$ and $\bar{y}$.

The first item can be checked by a for-program using the assumption that $f$ is definable and Lemma 3.2, while the second item can be checked by running a nested copy of $f_{1}$.

We are now ready to prove Lemma 4.6. Let $f$ be a definable $k$-enumerator. We need to describe a for-program which outputs the same list of tuples as $f$. Let $r$ be the maximal quantifier rank of the first-order formulas used in the definition of $f$. Apply the Domination Lemma to $k$, $m\coloneqq 5k$, and $r$, yielding a constant $\omega$. Define $h$ to be the function which maps a string $w\in\Sigma^{+}$ to the rank $\omega$ type of the corresponding ordered model of $w$. Compositionality of first-order logic (see [16, Section 3.4]) on strings says that the image of $h$, the set of rank $\omega$ types of strings, is a finite aperiodic semigroup and $h$ is a semigroup homomorphism. Apply the Factorisation Forest Theorem to $h$, yielding a function which partitions each string into blocks and an upper bound $M$ on heights of strings. By abuse of notation, we lift notions about strings to intervals inside strings: the height of an interval $X$ in a string $w$ is defined to be the height (in the sense of item 3 in Theorem 4.11) of the infix of $w$ induced by $X$. Likewise, we define the blocks of $X$ as the blocks of the infix induced by $X$, viewed as intervals contained in $X$.

To show that $f$ is also programmable, we use an induction over heights in factorisation forests. More precisely, we prove that for every $i\in\mathbb{N}$ there is a for-program which computes the following:

• •

Input. A string $w\in\Sigma^{+}$ with distinguished nonempty intervals $X_{1},\ldots,X_{k}$ that are pairwise equal or disjoint, and such that the sum of their heights (in the sense of Theorem 4.11) is at most $i$. Each interval is represented by its first and its last position.

• •

Output. The list $f(w)$ restricted to tuples in $X_{1}\times\cdots\times X_{k}$.

By item 3 in Theorem 4.11, the for-program with parameter $i\coloneqq kM$ will work for every choice of pairwise equal or disjoint intervals, in particular when all of the intervals are the entire string. The induction base $i=k$ (where every interval has the height $1$) is straightforward: each interval is a singleton, and the for-program simply checks if the unique tuple in $X_{1}\times\cdots\times X_{k}$ belongs to the output of $f$ by using the subroutines from Lemma 3.2. The rest of the proof is devoted to the induction step, more specifically, to producing the correct order of the tuples: whether a tuple belongs to the output or not can again be checked using the subroutines from Lemma 3.2.

Let $X_{1},\ldots,X_{k}$ be intervals in an input string $w$ that are pairwise disjoint or equal. Define $\mathcal{X}$ to be the coarsest partition of the positions in the input string into intervals that satisfies $X_{1},\ldots,X_{k}\in\mathcal{X}$. This partition uses at most $2k+1$ intervals. Consider a factorisation

[TABLE]

where each $w_{j}$ is a block of one of the elements of $\mathcal{X}$. Define ${\mathfrak{A}}$ as in the Domination Lemma, i.e. as the ordered structure of $w$ extended with an extra order $\sqsubset$ that describes the partition into factors $w_{1},\ldots,w_{n}$. By item 4 of the Factorisation Forest Theorem, the order $\sqsubset$ can be defined by a first-order formula which uses the input string and the endpoints of the intervals $X_{1},\ldots,X_{k}$. It follows that for every $k$-ary rank $\omega$ type $t$ over the vocabulary of ${\mathfrak{A}}$, there is a corresponding first-order formula which selects the $k$-tuples of positions in $w$ that have type $t$ in ${\mathfrak{A}}$. Since there are finitely many choices of $t$, it follows from the Merging Lemma that it is enough to show that for every $t$, there is a for-program which outputs the tuples of type $t$.

Let $t$ be a $k$-ary rank $\omega$ type over the vocabulary of ${\mathfrak{A}}$. We show a for-program which outputs all tuples in

[TABLE]

according to their order given by $f(w)$, call this order $\prec$.

If an interval from $\mathcal{X}$ has more than two blocks, then, by item 2 of the Factorisation Forest Theorem, all of these blocks have the same image under $h$, i.e., the same rank $\omega$ type. Since there are at most $2k+1$ intervals, it follows that with at most $2(2k+1)-1=4k+1<5k$ exceptions, consecutive strings $w_{j}$ and $w_{j+1}$ have the same rank $\omega$ type. Hence, for the order $\prec$ defined by $f(w)$, the Domination Lemma yields $d\in\left\{1,\ldots,k\right\}$ and $p\in\left\{-1,1\right\}$ such that

[TABLE]

This means that the tuples in $T$ are $\prec$-ordered as $T_{1}\prec^{p}T_{2}\prec^{p}\cdots\prec^{p}T_{s}$, where $s$ is the number of blocks in $X_{d}$ and $T_{j}$ consists of the tuples from $T$ where the coordinate $x_{d}$ is in the $j$-th block of $X_{d}$. Our for-program can simply loop over all the blocks of $X_{d}$ – in increasing or decreasing order depending on the choice of $p$ – because the endpoints of each block can be identified in first-order logic due to item 4 of the Factorisation Forest Theorem. In each iteration of the loop, the for-program outputs the tuples in the corresponding $T_{j}$ using the following claim, thus completing the proof of the lemma.

Claim 2**.**

There is a for-program which inputs the $i$-th block of $X_{d}$, given by its endpoints, and outputs the tuples from $T_{j}$ ordered according to $\prec$.

Proof 4.14** (Proof of the claim).**

The general idea is to replace $X_{d}$ with its $j$-th block (call this block $X$) and use the induction assumption. However, if there is an $i\neq d$ such that $X_{j}=X_{d}$, then replacing $X_{d}$ with $X$ would violate the assumption that the intervals are pairwise disjoint or equal (since $X\subsetneq X_{j}$). To overcome this issue, we use the following simple case disjunction. For each of the $3^{k}$ possible values of

[TABLE]

construct a for-program that outputs all tuples from $Y_{1}\times\cdots\times Y_{k}$, where $Y_{j}$ is the intersection of $X_{j}$ with the $j$-th entry of $v$. Since each $Y_{j}$ is a union of blocks of $X_{j}$, it is empty or its height is at most the height of $X_{j}$. Furthermore, if $Y_{d}$ is nonempty, then it is $X$, which is a block of $X_{d}$, and therefore its height is strictly smaller than the height of $X_{d}$. It follows that the induction assumption can be applied to produce all tuples in $Y_{1}\times\cdots\times Y_{k}$, for any given choice of $v$. These choices can be combined using the Merging Lemma.

Appendix A Successor instead of order

In this appendix, we prove Theorem 2.4, which says that:

The class of successor-mso string-to-string interpretations is not closed under composition, and strictly contains the class of (order-)mso string-to-string interpretations. 2. 2.

The following is undecidable: given a successor-first-order string-to-string interpretation $f$ and a regular language $L$ over the output alphabet, is $f^{-1}(L)$ is empty?

Proof A.1** (Proof of Theorem 2.4).**

We first show item 1. Fix an input alphabet $\Sigma$, and consider the function $f\colon\Sigma^{*}\to(\Sigma\times\Sigma)^{*}$ which inputs a string, and outputs all pairs of positions (with the corresponding pairs of labels) in the order depicted by the following picture:

It is not hard to see that the function $f$ is a succesor-mso string-to-string interpretation (in fact even first-order logic would be enough if the input string was equipped with a labelling indicating the parity of positions). Suppose that the alphabet $\Sigma$ contains two endmarkers $\vdash,\dashv$, and consider an input word of the form $\vdash a_{1}\cdots a_{n}\dashv$ where $a_{1},\ldots,a_{n}$ are letters that are not endmarkers and the length $n$ is even. In this case, the output contains the letter $(\vdash,\dashv)$ exactly once, it contains the letter $(\dashv,\vdash)$ also exactly once, and the word between these two letters is exactly:

[TABLE]

If and only if the word $a_{1}\cdots a_{n}$ is a palindrome, then the above word contains only letters from the diagonal $\left\{(a,a):a\in\Sigma\right\}$. Summing up, there is a regular (and therefore also mso-definable) language $L\subseteq\Sigma^{*}$ such that

[TABLE]

Define $\chi_{L}$ to be the characteristic function of $L$, i.e., the function from $\Sigma^{*}$ to $\left\{0,1\right\}$ which outputs $1$ or [math] depending on whether the input belongs to $L$ or not. We can view the characteristic function as a string-to-string function, where the output is in $\left\{0,1\right\}^{*}$ and which happens to only produce outputs with one letter. The following claim is not hard to see.

Claim 3**.**

A language $L\subseteq\Sigma^{*}$ is regular if and only if its characteristic function is a successor-mso string-to-string function.

From the claim, it follows that the characteristic function of the language $L$ in (2) is in the successor-mso class. If the class were closed under composition, then also $\chi_{L}\circ f$, the characteristic function of the palindrome language in (2), would be in successor-mso, and thus by Claim 3 the palindrome language would be regular, a contradiction. 2. 2.

We now show item 2 of Theorem 2.4, i.e., that for a successor-first-order string-to-string interpretation $f$ and a regular language $L$ over the output alphabet, the emptiness of $f^{-1}(L)$ is undecidable. The proof is a standard reduction from the halting problem for Turing machines.

Let $M$ be a Turing machine. Consider the string-to-string function $f$ defined as in the previous item, except that the order on positions is as follows:

The key observation is that the output $f(a_{1}\cdots a_{n})$ contains, for every odd $i\in\left\{1,\ldots,n\right\}$, an infix of the form

[TABLE]

In the picture, the blue colouring indicates this infix for $i=3$.

The above observation shows that the output of $f$ can be used to compare infixes of $w$ with other infixes; this can be used to check if an input word represents an accepting computation of the fixed Turing machine.

*The input will be required to be of the following shape: $|c_{1}|c_{2}|\ldots|c_{n}|$, where the *$c_{i}$s are words that represent the consecutive configurations of an accepting computation of the Turing machine.

*We mainly need to enforce two additional properties to obtain the reduction: first, that all the *$c_{i}$s have the same size and second, that each $c_{i+1}$ is the successor configuration of $c_{i}$ (and also that $c_{1}$ is initial and $c_{n}$ is final, which are simple regular properties). To enforce these two properties we only need to check properties of the infix $(a_{i},a_{1}),(a_{i+1},a_{2}),\ldots,(a_{n},a_{n-i+1})$ where $i$ is the position of the second $|$ separator symbol of the input word. We can easily enforce that this position is odd by asking that all configurations are of even length.

The proof of item 2 could be improved so that the function $f$ is a successor-first-order string-to-string interpretation, which shows that emptiness of $f^{-1}(L)$ is undecidable already when $f$ is successor-first-order and $L$ is regular. This shows that the class of successor-first-order string-to-string interpretations is not contained in the class of (ordered) first-order string-to-string interpretations considered in this paper, since by our main theorem, the latter class is contained in the class of polyregular functions, and emptiness of $f^{-1}(L)$ is decidable if $L$ is regular and $f$ is polyregular [3, Theorem 1.7].

Appendix B Proof of the Factorisation Forest Theorem

We provide a proof for the aperiodic variant of the Factorisation Forest Theorem (Theorem 4.11) here. Consider a surjective homomorphism

[TABLE]

We can assume without loss of generality that $\Sigma$ is a subset of $S$. The proof is by induction on (a) the size of $S$; (b) the size of $\Sigma$. The two parameters are ordered lexicographically, with (a) being more important.

When $\Sigma$ has one element, then the blocks of a string $w\in\Sigma^{+}$ are simply its letters; this covers the induction base. The partition of a string into letters is clearly first-order definable.

For the induction step, suppose that $\Sigma$ has more than one element. Take some $s\in\Sigma$ and consider the functions

[TABLE]

If one of these functions is surjective, then it is a permutation, and therefore it has to be the identity by aperiodicity of the semigroup. If both functions are surjective, then $s$ must be the identity element of the semigroup (which might not exist in some semigroups. Since $\Sigma$ has at least two elements, and there is at most one identity, there must be an $s\in\Sigma$ such that one of the functions in (7) is not surjective. Without loss of generality, assume that $t\mapsto ts$ is not surjective, and therefore $T\coloneqq Ss$ is a proper subset of the semigroup $S$.

Consider the following two semigroup homomorphisms: the first one is the product operation

[TABLE]

in the semigroup $T$, and the second one is

[TABLE]

obtained by restricting $h$ to the smaller alphabet. Both homomorphisms are smaller in our induction order: $h_{T}$ uses a smaller semigroup, and $h_{\neq s}$ has a smaller alphabet. Therefore, the induction assumption can be applied to obtain both partitions into blocks and bounds $M_{T}$ and $M_{\neq s}$ on the heights of the corresponding strings.

For a string $w\in\Sigma^{+}$, we define its partition into blocks with respect to the homomorphism $h$ as follows by case analysis.

Suppose that $w$ ends with $s$ and does not begin with $s$. Decompose $w$ as follows:

[TABLE]

1. (a)

If $n=1$, then the blocks are $w_{1}$ and $s^{k_{1}}$. The former word has height at most $M_{\neq s}$ by induction assumption and the latter word has height at most 2 because it uses only the letter $s$. It follows that $w$ has height at most $M_{\neq s}+2$. 2. (b)

Otherwise $n>1$. For $i\in\left\{1,\ldots,n\right\}$ define $t_{i}$ to be $h(w_{i}s^{k_{i}})$. Note that $t_{i}\in Ss=T$. Consider the partition into blocks of the word $t_{1}\cdots t_{n}$ with respect to the homomorphism $h_{T}$. The blocks of $w$ are the same as the blocks of $t_{1}\cdots t_{n}$, except that in each block, the letter $t_{i}$ is replaced with the corresponding infix $w_{i}s^{k_{i}}$. Since the height of $t_{1}\cdots t_{n}$ is at most $M_{T}$ from the induction assumption, and each $w_{i}s^{k_{i}}$ has height at most $M_{\neq s}+2$ from item (1a), we obtain a height of at most $M_{T}+M_{\neq s}+2$ for the word $w$. 2. 2.

We are left with the case when $w$ either begins with $s$ or does not end with $s$. In these cases, we simply decompose the word by shaving off the beginning and the end to reduce the decomposition to case (1).

1. (a)

If $w=usv$ such that $u$ and $v$ do not begin with $s$, and $v\in(\Sigma-\left\{s\right\})^{+}$ then we split $w$ into two blocks, $us$ and $v$. According to case (1), $us$ has height at most $M_{T}+M_{\neq s}+2$ and by induction assumption, $v$ has height at most $M_{\neq s}$, thus overall, $w$ has height at most $M_{T}+M_{\neq s}+3$. 2. (b)

Finally, let $w=s^{k}usv$ with $k\in\left\{1,2,\ldots\right\}$, $u,v$ not beginning with $s$, and $v\in(\Sigma-\left\{s\right\})^{+}$. In that case we split $w$ into two parts again: $s^{k}$ and $usv$, $s^{k}$ has height at most 2, and from the previous case, we have a final height of at most $M_{T}+M_{\neq s}+4$.

It is not hard to see the partition into blocks described above is first-order definable. This completes the proof of the Factorisation Forest Theorem.

Appendix C Proof of the Domination Lemma

This section is devoted to proving the Domination Lemma. The statement of the Domination Lemma in Section 4 was chosen so that it would be most easily applied to strings and their infixes. We begin by stating a more abstract version of the lemma, called the Product Domination Lemma, which is adapted to allow for a modular proof and implies the Domination Lemma in the shape in which we use it. Before stating the Product Domination Lemma, we introduce notation for the three kinds of product operations that are relevant to us.

Elements of the direct product $\prod_{i=1}^{k}{\mathfrak{A}}_{i}\coloneqq{\mathfrak{A}}_{1}\times\cdots\times{\mathfrak{A}}_{k}$ of structures ${\mathfrak{A}}_{1}$, …, ${\mathfrak{A}}_{k}$ are tuples $(a_{1},\ldots,a_{k})$ with $a_{i}\in{\mathfrak{A}}_{i}$ for every $i\in\left\{1,\ldots,k\right\}$. For every relation $R$ in some ${\mathfrak{A}}_{i}$, there is a corresponding relation of the same arity in the direct product, which says whether or not $R$ holds after projecting to the $i$-th coordinate. 2. 2.

The $k$-th power of a structure ${\mathfrak{A}}$ is similar to the $k$-fold direct product of ${\mathfrak{A}}$, except that different coordinates can be compared, i.e., for every two tuples $(a_{1},\ldots,a_{k}),(a^{\prime}_{1},\ldots,a^{\prime}_{k})$ in the $k$-th power of ${\mathfrak{A}}$ and all $i,j\in\{1,\dots,k\}$, we can compare $a_{i}$ and $a^{\prime}_{j}$. One way of modelling such comparisons is to say that the $k$-th power is obtained from the $k$-fold direct product by adding for all $i,j\in\left\{1,\ldots,k\right\}$ a function which swaps coordinates $i$ and $j$. 3. 3.

The ordered product ${\mathfrak{A}}_{1}\cdots{\mathfrak{A}}_{k}$ is obtained by taking the disjoint union of the structures ${\mathfrak{A}}_{1},\ldots,{\mathfrak{A}}_{k}$ and adding an extra binary predicate $\sqsubset$, called the block order, such that $x\sqsubset y$ holds if $x$ comes from an ${\mathfrak{A}}_{i}$ and $y$ comes from an ${\mathfrak{A}}_{j}$ with $i<j$.

The Product Domination Lemma uses all three kinds of products: it considers a direct product of powers of ordered products.

Recall that we write $\equiv_{r+k}$ for the equivalence relation on structures with distinguished elements of having the same rank $r+k$ type.

Lemma C.1** (Product Domination Lemma).**

Let $k,r\in\left\{1,2,\ldots\right\}$. Then there exists an $\omega_{*}\in\left\{1,2,\ldots\right\}$ such that the following holds. Let $I\subset\left\{0,1,\ldots\right\}$ be an initial segment of the natural numbers and let

[TABLE]

where each ${\mathfrak{A}}_{i}$ is an ordered product

[TABLE]

Let $\prec$ be a linear order on ${\mathfrak{A}}$ defined by a first-order formula of rank $r$, and let $t$ be a unary rank $\omega_{*}$ type over ${\mathfrak{A}}$. Then there exist $d\in I$, $e\in\left\{1,\ldots,k_{d}\right\}$, and $p\in\left\{-1,1\right\}$ such that

[TABLE]

Proof overview.

We begin by showing, in Section C.1, that the Product Domination Lemma implies the Domination Lemma in its original form from Section 4. The rest of Section C is then devoted to proving the Product Domination Lemma. This is done in four steps. In Section C.2, we show that if we can prove the Product Domination Lemma for some nonzero polarity other than $\left\{-1,1\right\}$, then we can reduce the polarity down to $\left\{-1,1\right\}$ at the cost of increasing the threshold $\omega$. Next, we prove the Product Domination Lemma in four steps, which deal with special cases of increasing generality, as described below.

• •

In Section C.3 we prove domination for direct products of linear orders, i.e. structures

[TABLE]

This can be viewed as the special case of the Product Domination Lemma when all $k_{i}$ are $1$, and furthermore all structures ${\mathfrak{A}}_{i,j}$ (called blocks in the proof) have size one.

• •

In Section C.4 we prove domination for powers of linear orders, i.e. structures

[TABLE]

This can be viewed as the special case of the Product Domination Lemma when $I$ has size one, and all blocks have size one.

• •

In Section C.5 we prove the joint generalisation of the results from the two previous sections, i.e. we consider direct products of powers of linear orders:

[TABLE]

This can be viewed as the special case of the Product Domination Lemma when all blocks have size one.

• •

In Section C.6 we complete the proof of the Product Domination Lemma.

Compositionality.

Before continuing with the proof, we state two compositionality properties of first-order logic with respect to products that will be heavily used in the proofs.

Theorem C.2** ([18]).**

The following holds for all $m,n,r\in\left\{1,2,\ldots\right\}$.

Consider structures ${\mathfrak{A}}_{1},\ldots,{\mathfrak{A}}_{n},\mathfrak{B}_{1},\ldots,\mathfrak{B}_{m}$ over the same vocabulary. The rank $r$ type of the ordered product

[TABLE]

is determined by the rank $r$ types of the two ordered products

[TABLE] 2. 2.

Let ${\mathfrak{A}}\coloneqq\prod_{i\in I}{\mathfrak{A}}_{i}$ be a direct product of structures ${\mathfrak{A}}_{i}$. For every $m$-ary rank $r$ type $t$ in ${\mathfrak{A}}$ and every $i\in I$ there is an $m$-ary rank $r$ type $t[i]$ in the structure ${\mathfrak{A}}_{i}$ such that for all $x_{1},\ldots,x_{m}\in{\mathfrak{A}}$

[TABLE]

Continuous functions.

Let $i\in\left\{0,1,\ldots\right\}$ and let ${\mathfrak{A}}$ and $\mathfrak{B}$ be relational structures over possibly different vocabularies. Let $f$ be a function from (the universe of) ${\mathfrak{A}}$ to (the universe of) $\mathfrak{B}$ and for all $k\in\left\{1,2,\ldots\right\}$, denote by $f_{k}$ the function mapping $k$-tuples of ${\mathfrak{A}}$ to $k$-tuples of $\mathfrak{B}$ by component-wise application of $f$. Then $f$ is called $i$-continuous if for every $k\in\left\{1,2,\ldots\right\}$ and every subset of $\mathfrak{B}^{k}$ defined by a formula in first-order logic with quantifier rank $r$, its inverse image under $f_{k}$ can be defined in first-order logic via a formula with quantifier rank $r+i$. A function is called continuous if it is [math]-continuous.

An alternative, equivalent characterisation, which we also use in this paper, is that a function is continuous if and only if it is type-preserving, i.e., it maps tuples of the same type to tuples of the same type.

C.1 Proof of the Domination Lemma

We begin by using the Product Domination Lemma to obtain the Domination Lemma in its statement from Section 4. Let $k,m,r\in\{1,2,\dots\}$. Apply the Product Domination Lemma to $k$ and $r$ yielding some threshold value $\omega_{*}$. Define

[TABLE]

We prove that $\omega$ satisfies the requirements of the Domination Lemma. Let $w_{1},\ldots,w_{n}$ and ${\mathfrak{A}}$ be as in the assumptions of the Domination Lemma. This means that ${\mathfrak{A}}$ is the ordered product of the (ordered structures associated with) the strings $w_{1},\ldots,w_{n}$ extended with the block order $\sqsubset$. Furthermore, the strings satisfy $w_{i}\equiv_{\omega}w_{i+1}$ with at most $m$ exceptions. (The order on the blocks is $\sqsubset$, while the orders corresponding to the ordered structures are $<$). Let $\prec$ be a linear order on ${\mathfrak{A}}^{k}$ defined by a first-order formula of quantifier rank $r$ and let $t$ be a $k$-ary rank $\omega$ type over the vocabulary of ${\mathfrak{A}}$. We intend to find a dominating coordinate and a polarity that satisfy

[TABLE]

Define $\sim$ to be the coarsest equivalence relation on $\left\{1,\ldots,n\right\}$ such that $i\sim i+1$ holds whenever $w_{i}\equiv_{\omega_{*}}w_{i+1}$. Equivalence classes of $\sim$ are intervals. Let $\mathcal{I}$ be the set consisting of these equivalence classes. Since $\omega\geq\omega_{*}$, we know from the assumptions of the Domination Lemma that $\mathcal{I}$ has at most $m$ elements. For an equivalence class $I\in\mathcal{I}$, define $\mathfrak{B}_{I}\subseteq{\mathfrak{A}}$ to be the substructure obtained by restricting ${\mathfrak{A}}$ to elements that come from $w_{i}$ with $i\in I$. We can view $\mathfrak{B}_{I}$ as an ordered product which only uses the words $w_{i}$ with $i\in I$. By definition, in $\mathfrak{B}_{I}$, all blocks (i.e., all $w_{i}$) have the same rank $\omega_{*}$ type. For every $I\in\mathcal{I}$, there is a first-order formula which selects the elements from $\mathfrak{B}_{I}$ inside the structure ${\mathfrak{A}}$: the formula counts the number of blocks $w_{i}$ to the left which satisfy $w_{i}\not\equiv_{\omega_{*}}w_{i+1}$, and therefore it has quantifier rank at most $\omega_{*}+m$. For $\bar{x}\in{\mathfrak{A}}^{k}$ of rank $\omega$ type $t$ and $I\in\mathcal{I}$, define

[TABLE]

This set does not depend on $\bar{x}$ once $t$ has been fixed, because, as we have argued above, one can express the containment in $\mathfrak{B}_{I}$ using a first-order formula with quantifier rank at most $\omega$. Define

[TABLE]

to be the injection that is defined in the following way (where an element in the universe of $\mathfrak{B}_{I}$ is seen as an element in the universe of ${\mathfrak{A}}$):

[TABLE]

The image of this injection contains all tuples in ${\mathfrak{A}}^{k}$ that have $k$-ary rank $\omega$ type $t$. Since the injection sends tuple of the same type to tuples of the same type, it is continuous.

Claim 4**.**

All elements in the inverse image of $t$ under $\iota$ have the same rank $\omega_{*}$ type.

Proof C.3**.**

Note that the continuity of $\iota$ is not useful for this result, because it only tells us that the inverse image of $t$ is a union of rank $\omega$ types. The image $\iota(\mathfrak{B})\subseteq{\mathfrak{A}}^{k}$ can be defined by a first-order formula of quantifier rank at most $\omega_{*}+r+k+m$. Therefore, if elements of $\mathfrak{B}$ have different rank $\omega_{*}$ types, then their images under $\iota$ have different rank $\omega$ types. This proves the claim.

By the above claim, all elements in the inverse image under $\iota$ of type $t$ have the same rank $\omega_{*}$ type over $\mathfrak{B}$, call it $t_{\mathfrak{B}}$. Define $\prec_{\mathfrak{B}}$ to be the linear order on $\mathfrak{B}$ which is the inverse image of $\prec$ under $\iota$, i.e.

[TABLE]

Since $\iota$ is continuous, it follows that $\prec_{\mathfrak{B}}$ is defined using a first-order formula of quantifier rank $r$. By the Product Domination Lemma, there exist $d\in\mathcal{I}$, $e\in C_{d}$and $p\in\left\{-1,1\right\}$ such that

[TABLE]

By pulling this result forward across the injection $\iota$, we get the corresponding conclusion for $\bar{x}$ and $\bar{y}$ in ${\mathfrak{A}}^{k}$ of type $t$.

This finishes the proof of the Domination Lemma, assuming the Product Domination Lemma holds. The rest of this section is devoted to proving the Product Domination Lemma.

C.2 Polarity reduction

In the Product Domination Lemma, we use powers $\sqsubset^{p}$ for polarities $p\in\left\{-1,1\right\}$. This notation also makes sense for other nonzero integers $p$, for example $x\sqsubset^{-3}y$ means that $y\sqsubset z_{1}\sqsubset z_{2}\sqsubset x$ holds for some $z_{1}$, $z_{2}$. (We extend this notation to other binary relations as well.) It would be easier to prove the Product Domination Lemma for polarities $p$ with larger absolute values, since for $s\in\left\{-1,1\right\}$ and for $p^{\prime}\in\left\{1,2,\ldots\right\}$, the implication

[TABLE]

has a stronger assumption than $x[d]\sqsubset^{s}y[d]$ and is therefore weaker than

[TABLE]

The following lemma shows that such weaker versions are indeed enough.

Lemma C.4** (Polarity Reduction Lemma).**

Let ${\mathfrak{A}}$ be a relational structure, and let $R$ and $\prec$ be binary relations on ${\mathfrak{A}}$ that are defined by first-order formulas of quantifier rank at most $r\in\left\{1,2,\ldots\right\}$. If $\prec$ is transitive and antisymmetric, then for every $p\in\left\{1,2,\ldots\right\}$

[TABLE]

Proof C.5**.**

Let $R$ and $\prec$ be as in the assumptions and let $p\in\left\{1,2,\ldots,\right\}$. Suppose the two conditions in the stated implication $\Downarrow$ hold. Let $x,y\in{\mathfrak{A}}$ be such that $R(x,y)$ and $x\equiv_{r+p}y$ hold. We need to show $x\prec y$. Let $t$ be the binary rank $r$ type that describes the pair $(x,y)$. Since $R$ is defined using quantifier rank at most $r$ and contains $(x,y)$, it follows that all pairs of type $t$ are contained in $R$. Because $\prec$ is defined by a formula of quantifier rank $r$, our assumptions imply that the set of pairs of type $t$ is contained in either $\prec$ or $\succ$. To prove the lemma, we need to show that it is contained in $\prec$. Define a chain to be a sequence of elements

[TABLE]

i.e. a walk in the directed graph on the universe of ${\mathfrak{A}}$ where $t$ is the edge relation. Note that every chain is either growing or decreasing with respect to $\prec$. We need to rule out the “decreasing” case. The property “there is a chain of length $i$ that begins in $x$” can be defined by a first-order formula of quantifier rank $r+i$. It follows inductively from $t(x,y)$ and $x\equiv_{r+p}y$ that there is a chain which begins in $x$ and has length at least $p$. Indeed, if the maximal length of a chain beginning in $y$ was some value $p^{\prime}<p$, there would be a chain of length $p^{\prime}+1$ beginning in $x$ since $(x,y)$ has type $t$. This would violate that $x\equiv_{r+p}y$.

As discussed at the beginning of this section, a corollary of the Polarity Reduction Lemma is that it is enough to prove a weaker version of the Product Domination Lemma, where the polarity $p$ from the conclusion is in $\left\{-\omega_{*},\omega_{*}\right\}$ instead of $\left\{-1,1\right\}$. To see why, suppose that we have proved the version of the Product Domination Lemma with polarity $p^{\prime}\in\left\{-\omega,\omega\right\}$, and we want to prove the version with polarity $p\in\left\{-1,1\right\}$. Let $t$ be a unary rank $w_{*}$ type. By the weaker version of the Product Domination Lemma, there is some $p\in\left\{-1,1\right\}$ such that

[TABLE]

Apply the Polarity Reduction Lemma for $p\coloneqq\omega_{*}$, the structure being ${\mathfrak{A}}$, and the relation $R$ defined by

[TABLE]

We obtain the conclusion of the Product Domination Lemma in its original form.

Thanks to the above reasoning, in the remaining sections it suffices to show variants of the Product Domination Lemma where the polarity $p$ in the conclusion is some nonzero number with a fixed upper bound, not necessarily 1, on its absolute value.

C.3 Direct products of linear orders

In this section, we show the special case of the Product Domination Lemma for direct products of linear orders. A corollary is going to be that every first-order definable ordering $\prec$ in a product of linear orders coincides with a lexicographic product of the underlying orders, at least when restricted to elements of the direct product that have the same type. The corollary is stated later in this section, but we begin with the underlying result about dominating coordinates.

Lemma C.6**.**

Let $r\in\left\{1,2,\ldots\right\}$ and let $\prec$ be a linear ordering on a direct product

[TABLE]

such that $\prec$ is defined by a first-order formula of quantifier rank $r$. Then for every unary rank $r$ type $t$ in ${\mathfrak{A}}$, there is a dominating coordinate $d\in I$ and $p\in\left\{-2\cdot 2^{r},2\cdot 2^{r}\right\}$ such that

[TABLE]

Note that in the above lemma, the polarity $p$ can have a value not contained in $\left\{-1,1\right\}$. As explained in Section C.2, at the cost of increasing the quantifier rank of the type $t$, the polarity can be reduced to values in $\left\{-1,1\right\}$.

To prove Lemma C.6, we use the following observation, which expresses that first-order logic formulas with quantifier rank $r$ can only measure distances up to $2^{r}$ in a linear order. Its proof is the same as for [16, Theorem 3.6].

Lemma C.7** (Threshold Lemma).**

Let $r\in\left\{1,2,\ldots\right\}$ and consider two $k$-tuples $x$ and $y$ in a linearly ordered set

[TABLE]

Then $x$ and $y$ have the same rank $r$ type if and only if they have the same quantifier-free type in the structure extended with relations $<^{i}$ for $i\in\left\{1,\ldots,2^{r}\right\}$and unary relations $min$ and $max$.

Proof C.8** (Proof of Lemma C.6).**

The proof proceeds by induction on the size of the set $I$, i.e. on the dimension of the product. Let $t$ be a unary rank $r$ type over the vocabulary of ${\mathfrak{A}}$. Consider its projections $t[i]$ for $i\in I$ as in Theorem C.2. By the Threshold Lemma, if an $|I|$-tuple $x\in{\mathfrak{A}}$ has type $t$, then $t[i]$ determines the distance of $x[i]$ from the first and last positions in $\left\{1,\ldots,n_{i}\right\}$, measured up to threshold $2^{r}$. If the distance from either the first or last position is $<2^{r}$, then the value of $x[i]$ is fixed by the type $t$. For such types, we can eliminate one coordinate, and obtain the result by using the induction assumption. We are left with the case when $t$ expresses that all coordinates are at least $2^{r}$ positions away from both the first and last positions.

Choose a tuple $x\in{\mathfrak{A}}$ such that for every $i\in I$, coordinate $x[i]$ is at least $3\cdot 2^{r}$ positions away from the first and last positions in $\left\{1,\ldots,n_{i}\right\}$, which can be achieved by the assumption that $n_{i}\geq 6\cdot 2^{r}$ for all $i\in I$. We say that $\delta\in\mathbb{Z}^{I}$ is small if for every $i\in I$, the absolute value of $\delta[i]$ is between $2^{r}$ and $2\cdot 2^{r}$. By the choice of $x$, we know that if $\delta$ is small, then $x+\delta$ has the same type as $x$. Define the sign vector of $\delta$ to be the subset of $I$ which contains the coordinates on which $\delta$ is positive, and define

[TABLE]

It is not hard to see that the family $\mathcal{I}$ is closed under set union, and the same is true for its complement.

Claim 5**.**

Consider a partition of the powerset $2^{I}$ into two families of sets, both of which are closed under union. Then there is a $d\in I$ such that one of the families is $\left\{J\subseteq I:d\in J\right\}$.

Proof C.9**.**

Since both families are closed under union, it follows from De Morgan’s law that both families are closed under intersection. One of the families does not contain the empty set, call this family $\mathcal{I}$. Since $\mathcal{I}$ is closed under intersection, it follows that the intersection $\cap\mathcal{I}$ of all sets in $\mathcal{I}$ is nonempty. The interesction $\cap\mathcal{I}$ cannot have more than one element, because otherwise it could be decomposed as a union of two sets outside $\mathcal{I}$, and therefore it would be outside $\mathcal{I}$. Hence, the intersection of all sets in $\mathcal{I}$ is a singleton $\left\{d\right\}$ for some $d\in I$. This means that all sets in $\mathcal{I}$ contain $d$. It follows that for every $i\neq d$, the singleton $\left\{i\right\}$ must belong to the complement of $\mathcal{I}$. Since this complement is closed under taking unions, every set that does not contain $d$ belongs to the complement of $\mathcal{I}$.

An application of the claim yields a coordinate $d\in I$ such that either $\mathcal{I}$ or its complement consists in exactly the sets that contain $d$. By symmetry, we may assume the first case. By unfolding the definition of $\mathcal{I}$, it follows that incrementing $x[d]$ by at least $2^{r}$ and at most $2\cdot 2^{r}$ and modifying all other coordinates by any number with absolute value between $2^{r}$ and $2\cdot 2^{r}$ yields a bigger tuple. Performing this procedure twice allows us to modify the coordinates other than $d$ by any value in $\left\{-2^{r},\ldots,2^{r}\right\}$, and therefore the result follows using the Threshold Lemma.

We end this section with an interesting consequence of Lemma C.6. Define a lexicographic ordering on

[TABLE]

to be an ordering that is the lexicographic product, under some ordering of $I$, of orderings in the coordinates that are either $<$ or $>$. If $I$ has $n$ elements, then there are $n!\cdot 2^{n}$ lexicographic orderings, since the coordinates can be ordered in $n!$ ways and for each ordering one can use $<$ or $>$ for each of the $n$ coordinates. By iteratively applying Lemma C.6 and then using the Polarity Reduction Lemma, we can infer the following result.

Corollary C.10**.**

For every $r\in\left\{1,2,\ldots\right\}$, there is a threshold $\omega\in\left\{1,2,\ldots\right\}$ with the following property. Let $\prec$ be a linear ordering on the product

[TABLE]

such that $\prec$ is defined by a first-order formula of quantifier rank $r$. For every unary rank $r$ type $t$ in ${\mathfrak{A}}$, the order $\prec$ restricted to tuples of type $t$ coincides with one of the lexicographic orderings on ${\mathfrak{A}}$.

C.4 Powers of linear orders

In this section, we prove a version of the Domination Lemma that considers powers of finite linear orders. The difference to the scenario treated in Section C.3 is that here we can compare different coordinates.

Lemma C.11** (Linear Domination Lemma).**

For all $k,r\in\left\{1,2,\ldots\right\}$, there exists a threshold $\omega\in\left\{1,2,\ldots\right\}$ such that the following holds. If $\prec$ is a linear ordering on ${\mathfrak{A}}^{k}$ with

[TABLE]

such that $\prec$ is defined by a first-order formula of rank $r$, then for every $k$-ary rank $\omega$ type $t$, there are $d\in\left\{1,\ldots,k\right\}$ and $p\in\left\{-\omega,\omega\right\}$ such that

[TABLE]

In the proof, we do a detailed case analysis of the expressive power of first-order logic on linear orderings, which relies on the Threshold Lemma.

For $m\in\left\{1,2,\ldots\right\}$, a tuple $x\in{\mathfrak{A}}^{k}$ is called $m$-separated if for all $i\neq j$ in $\left\{0,\ldots,k+1\right\}$ it holds that $x[i]<^{m}x[j]$ or $x[i]<^{-m}x[j]$, with the convention that $x[0]=min$ and $x[k+1]=max$. We can extend the notion of being separated to types. A rank $r$ type $t$ is called $m$-separated if every tuple of type $t$ is $m$-separated, and separated if every tuple of type $t$ is $2^{r}$-separated.

Claim 6** (Linear Domination Lemma - Separated Case).**

For all $k,r\in\left\{1,2,\ldots\right\}$, there exists a threshold $\omega\in\left\{1,2,\ldots\right\}$ such that the following holds. If $\prec$ is a linear order on ${\mathfrak{A}}^{k}$, where

[TABLE]

such that $\prec$ is defined by a first-order formula of rank $r$, then for every separated rank $\omega$ type $t$, there are $d\in\left\{1,\ldots,k\right\}$ and $p\in\left\{-\omega,\omega\right\}$ such that

[TABLE]

We first show that the separated version of the lemma implies the general version.

Proof C.12** (Proof of the Linear Domination Lemma).**

The proof proceeds by induction on the dimension $k$. For $k=1$, the statement holds by the Threshold Lemma. Let $k\geq 2$ and $r\in\left\{1,\ldots\right\}$ and assume that the Linear Domination Lemma holds for dimension $k-1$. Let $\omega_{1}$ be the value obtained using Claim 6 for dimension $k$ and quantifier rank $r$. Let $\omega_{2}$ be the value obtained using the induction hypothesis for arity $k-1$ and quantifier rank $\omega_{1}+2$. Let $\omega\coloneqq\max\left\{\omega_{1}+2,\omega_{2}\right\}$.

Let ${\mathfrak{A}}\coloneqq(\left\{1,\ldots,n\right\},<)$ for an $n>\omega$ and consider a rank $\omega$ type $t$ of arity $k$. Let $s$ be the rank $\omega_{1}$ type associated with $t$. Note that all tuples of type $t$ have type $s$ but the converse does not necessarily hold. By the Threshold Lemma, the type $s$ is entirely given by quantifier-free formulas using $<^{i}$ for $i\in\left\{1,\ldots,2^{\omega_{1}}\right\}$. If $s$ is separated, by Claim 6, the result holds for tuples of type $s$, and thus in particular for tuples of type $t$. Otherwise, if there is a $\delta\in\left\{0,\ldots,2^{\omega_{1}}-1\right\}$ such that $x[0]=min$ and $x[k+1]=max$ are exactly $\delta$ apart, then all coordinates are pairwise at most $\delta$ apart and thus, $s$ (and therefore also $t$) fixes all coordinates, such that the conclusion from the lemma trivially holds. Thus, assume that there are $i\in\left\{1,\ldots,k\right\}$, $j\in\left\{0,\ldots,k+1\right\}\setminus\left\{i\right\}$ and $\delta\in\left\{0,\ldots,2^{\omega_{1}}-1\right\}$ such that $x[i]$ and $x[j]$ are exactly $\delta$ apart. Without loss of generality, we assume $i=k$, $x[j]<^{\delta}x[k]$ and $x[j]\not<^{\delta+1}x[k]$.

Let $\pi\colon{\mathfrak{A}}^{k}\rightarrow{\mathfrak{A}}^{k-1}$ be the projection to the first $k-1$ coordinates. Define a linear ordering $\prec_{{k-1}}$ over the tuples of ${\mathfrak{A}}^{k-1}$ which are images of tuples of type $s$ with respect to $\pi$, and such that $x\prec y\Leftrightarrow\pi(x)\prec_{k-1}\pi(y)$ for all $x$ and $y$ of type $s$. This order can be defined using a formula of quantifier rank $\omega_{1}+2$, simply by existentially quantifying over the missing coordinates.

Moreover, by continuity of $\pi$, all tuples of $\omega$-type $t$ are mapped to tuples of $\omega$-type $t^{\prime}$. By the induction hypothesis, we know that there are $d\in\left\{1,\ldots,k-1\right\}$ and $p\in\left\{-\omega_{2},+\omega_{2}\right\}$ such that:

[TABLE]

Thus, we have in particular:

[TABLE]

which concludes the proof.

The proof of Claim 6 has three stages, depending on whether the arity $k$ is $1$, $2$ or bigger. The case $k=1$ is actually trivial, and the most interesting case is arity $k=2$.

Arity two

We first prove Claim 6 for $k=2$. We need to show that there are $d\in\left\{1,2\right\}$, $\omega>0$ and $p\in\left\{-\omega,\omega\right\}$ such that for every separated type $t$ of arity two (we use the name binary from now on) and rank $r$, we have:

[TABLE]

For two pairs $x,y$, we say that they are $\omega$-distant if for $i\in\left\{1,2\right\}$, it holds that $x[i]<^{\pm\omega}y[i]$ or $x[i]=y[i]$. We first show the following claim.

Claim 7**.**

If the statement from Claim 6 holds in the case of $\omega$-distant tuples, then it holds for all tuples.

Proof C.13**.**

This is shown in exactly the same way as the Polarity Reduction Lemma. If we have two tuples $x,y$ of the same type of sufficiently high rank, then we can ensure that there is a sufficiently long sequence $x_{0},\ldots,x_{\ell}$, such that the $r$-type of $(x,y)$ is the same as the one of $(x_{i-1},x_{i})$, for $i\in\left\{1,\ldots,\ell\right\}$. If the sequence is long enough, then $x_{0},x_{\ell}$ are $\omega$-distant.

Let $\omega\coloneqq 2^{r}$. Consider tuples $x$ (first row) and $y$ (second row) where the first coordinate of $y$ is at least $2^{r}$ larger than the second coordinate of $x$, as in the following picture.

By the Threshold Lemma, the order relationship $x\prec y$ does not depend on the choice of $x$ and $y$ (subject to the requirements in the picture above). There are two cases, namely

[TABLE]

The cases are symmetric, we assume A1 without loss of generality.

Consider the case as above with $x[1]<^{\omega}x[2]\leq y[1]<^{\omega}y[2]$, but the distance between $x[2]$ and $y[1]$ is $\delta<2^{r}$. We use a simplified version of the Polarity Reduction Lemma in the case of a linear order. Let $z\coloneqq(y[2]+\delta,y[2]+\delta+\omega)$, hence the $r$-type of $(x,y)$ is equal to the one of $(y,z)$. Then $x$ and $z$ are in situation A1, which means by the transitivity of $\prec$ that $x\prec y$.

Consider the case with $x[1]<^{\omega}y[1]<x[2]<^{\omega}y[2]$. By the Threshold Lemma, we can assume that the distance $\delta$ between $x[2]$ and $y[1]$ is at most $2^{r}$. Let $z\coloneqq(y[2]-\delta,y[2]-\delta+\omega)$, hence the $r$-type of $(x,y)$ is equal to the one of $(y,z)$. By transitivity of $\prec$, we have $x\prec y\Leftrightarrow x\prec z$. Now we have that $z[1]-x[2]=y[2]-\delta-x[2]\geq 0$ since $x[2]<^{\omega}y[2]$. Using the Threshold Lemma, we can assume that $x[1]<^{\omega}x[2]\leq z[1]<^{\omega}z[2]$, which means, according to the previous paragraph, that $x\prec y$.

Since we only compare distant separated tuples, the only remaining case is the one illustrated below. Consider now two tuples $x$ and $y$ that are related as follows:

Again there are two cases, namely

[TABLE]

Case B1 implies that the dominating coordinate is the first one and Case B2 the second.

General arity

In this section we complete the proof of the Separated Linear Domination Lemma. The main idea is that it suffices to compare tuples which differ in at most two coordinates.

Let $\prec$ be a linear order on $k$-tuples in $\left\{1,\ldots,n\right\}$ that is defined by a first-order formula of quantifier rank $r$. Let $t$ be a separated $k$-ary rank $r$ type and let $\omega=2^{r}$. We prove that there is a dominating coordinate $d\in\left\{1,\ldots,k\right\}$ and a $p\in\left\{-\omega,\omega\right\}$ such that

[TABLE]

Choose distinct coordinates $i,j\in\left\{1,\ldots,k\right\}$ and let $z$ be a tuple of type $t$. Define

[TABLE]

By the case of arity two, we have the following result:

Claim 8**.**

For every $z$ and distinct coordinates $i,j$ there is a dominating coordinate $d\in\left\{i,j\right\}$ and a polarity $p\in\left\{-\omega,\omega\right\}$ such that

[TABLE]

Proof C.14**.**

Without loss of generality, we assume $z[1]\leq\ldots\leq z[k]$. Let $i<j$. Since $T^{z}_{ij}=T^{z}_{ji}$, we can assume without loss of generality that $i<j$. We make a case analysis depending on whether $i+1=j$ holds or not. Assume $i+1=j$, and let $\mathfrak{B}\coloneqq\left\{z[i-1]+1,\ldots,z[j+1]-1\right\}$. We define the partial function $\pi$ from tuples of type $t$ of ${\mathfrak{A}}^{k}$ to pairs of elements in the universe of $\mathfrak{B}$ by keeping only the coordinates $i$ and $j$. We also consider the function $\sigma\colon\mathfrak{B}^{2}\rightarrow{\mathfrak{A}}^{k}$, which just fills in the missing coordinates by the coordinates of $z$. Note that the function $\sigma$ is continuous, hence $\prec_{\mathfrak{B}}=\sigma^{-1}(\prec)$ can be defined by a formula of quantifier rank $r$. Moreover, $\pi$ is also continuous, thus the tuples in the image of $\pi$ have the same $r$-type $t^{\prime}$. Therefore, applying the Linear Domination Lemma to the case of dimension 2, we obtain that there are $d\in\left\{1,2\right\}$, $\omega\in\left\{1,2,\ldots\right\}$, and $p\in\left\{-\omega,+\omega\right\}$ such that:

[TABLE]

Thus, we have in particular:

[TABLE]

Similarly, if $i+1<j$, we define the structure $\mathfrak{B}\coloneqq\left\{z[i-1]+1,\ldots,z[i+1]-1\right\}\times\left\{z[j-1]+1,\ldots,z[j+1]-1\right\}$. Using the same arguments and Lemma C.6, we obtain the result.

It is not hard to see that there is exactly one possibility for $d$ and $p$ – once $z$, $i$ and $j$ have been fixed – since otherwise we would get a cycle for the order $\prec$. By the Threshold Lemma, the dominating coordinate $d$ depends only on $i,j$ and not on the choice of $z$, and therefore we can write $d_{ij}$ for the dominating coordinate that is appropriate to coordinates $i,j$. Also the polarity $p$ depends only on $i$ and $j$. Let us write $i\stackrel{{\scriptstyle p}}{{\to}}j$ if, whenever the values at coordinates $i,j$ are distinct, then $j$ is the dominating coordinate for $i,j$ and the associated polarity is $p$.

Claim 9**.**

If $i,j,\ell$ are distinct, then $i\stackrel{{\scriptstyle p}}{{\to}}j\stackrel{{\scriptstyle q}}{{\to}}\ell$ implies $i\stackrel{{\scriptstyle q}}{{\to}}\ell$.

Proof C.15**.**

Choose $s\in\left\{-\omega,\omega\right\}$ arbitrarily. Consider a tuple $x$ which is $(2^{r+1})$-separated. This tuple has type $t$, and shifting any coordinate by offset in $\left\{-\omega,\omega\right\}$ still leads to a tuple that has type $t$, because the quantifier rank of $t$ is $r$. Define $y$ to be the tuple obtained from $x$ by adding $s$ to coordinate $i$ and adding $p$ to coordinate $i$, and define $z$ to be the tuple obtained from $x$ by adding $s$ to coordinate $i$ and adding $q$ to coordinate $\ell$. Here is a picture where $p=q=\omega$ and $s=-\omega$.

From the assumption of the claim it follows that $x\prec y\prec z$, and this holds regardless of the choice of $s$. It follows that $i\stackrel{{\scriptstyle q}}{{\to}}\ell$.

From the above lemma it follows that the relation $i\to j$ defined by

[TABLE]

is a linear order on the coordinates $\left\{1,\ldots,k\right\}$. Let $d$ be the maximal element according to this total order. Let $d^{\prime}$ be the second-to-maximal element in the total order, and let $p$ be such that $d^{\prime}\stackrel{{\scriptstyle p}}{{\to}}d$ holds. From Claim 9 it follows that $i\stackrel{{\scriptstyle p}}{{\to}}d$ holds for all $i\in\left\{1,\ldots,k\right\}\setminus\left\{d\right\}$. We show that coordinate $d$ dominates when comparing tuples where the values of coordinate $d$ are sufficiently far apart.

To finish the proof of the Linear Domination Lemma, we prove below (9) for polarity $2pk$, i.e., we show

[TABLE]

Assume without loss of generality that the coordinates in some (equivalently, every) tuple of type $t$ are ordered so that they are strictly increasing. Let $x$ and $y$ be tuples as in the assumptions of the claim.

Let $x$ and $y$ be such that $x[d]<^{2pk}y[d]$. We need to show $x\prec y$. By the Threshold Lemma, we can assume that all coordinates in the tuples $x$ and $y$ avoid the first and last $k\cdot 2^{\omega}$ positions. To prove $x\prec y$, we will find a chain of $2k$ tuples that begins in $x$, ends in $y$, and is growing with respect to $\prec$. We do the proof in the case where $k=7$ and $d=4$, but the general case works the same. Define

[TABLE]

In general, {\color[rgb]{1,0,0}z_{i}} is defined as $i\cdot 2^{\omega}$ when $i\neq d$ and otherwise it is defined as $n-(k-i+1)\cdot 2^{\omega}$. The choice of coordinates {\color[rgb]{1,0,0}z_{i}} is made so that they are far apart, and furthermore {\color[rgb]{1,0,0}z_{i}} is to the left/right of the tuples $x,y$, depending on whether $i<d$ or $i>d$. The chain that witnesses $x\prec z$ is given below:

[TABLE]

All tuples in the above chain have type $t$, by the assumption that coordinates {\color[rgb]{1,0,0}z_{i}} are far apart and to the left/right of the tuples $x,y$. Since the dominating coordinate is incremented as the chain progresses, and at most two coordinates change in each step, we can use the assumption that coordinate $d$ dominates when only two coordinates change to conclude that each consecutive step yields a tuple that is bigger with respect to $\prec$. By transitivity, it follows that $x=x_{1}\prec y_{1}=y$.

C.5 Direct products of powers of linear orders

In this section we prove the most general version of the Product Domination Lemma for linear orderings, namely the case of direct products of powers of linear orderings.

Lemma C.16**.**

For all $k,r\in\left\{1,2,\ldots\right\}$, there exists a threshold $\omega\in\left\{1,2,\ldots\right\}$ such that the following holds. If $\prec$ is a linear order on

[TABLE]

such that $\prec$ is defined by a first-order formula of rank $r$, then for every unary rank $\omega$ type $t$ over ${\mathfrak{A}}$, there are $d\in I$, $e\in\left\{1,\ldots,k_{i}\right\}$ and $p\in\left\{-\omega,\omega\right\}$ such that

[TABLE]

Let $\omega$ be a threshold that is large enough – we will specify the required bounds during the proof. Fix for the rest of this proof a unary rank $\omega$ type $t$ in ${\mathfrak{A}}$. Our goal is to find a dominating coordinate $(d,e)$ and a polarity $p$ as in the statement of Lemma C.16.

The general strategy is as follows. We begin in Section C.5 by looking, for every $i\in I$, at the projection

[TABLE]

We show that there exists $\sigma_{i}\colon{\mathfrak{A}}_{i}\to{\mathfrak{A}}$ which is a section of $\pi_{i}$ in the sense that $\pi_{i}\circ\sigma_{i}$ is the identity on ${\mathfrak{A}}_{i}$. By applying the results from Section C.4 about powers of linear orders, we show that there is a dominating coordinate $d_{i}$ which works for elements in the image of the section. Next, in Section C.5, we consider the projection

[TABLE]

which is defined in terms of the dominating coordinates $\left\{d_{i}\right\}_{i\in I}$ that were found in Section C.5. Again, we find a section $\sigma\colon\mathfrak{B}\to{\mathfrak{A}}$. By applying the results from Section C.3 about direct products of linear orders, we find a dominating coordinate $d\in I$ which works for elements in the image of the section. Finally, in Section C.5, we combine the results about the sections $\sigma_{i}$ and $\sigma$ to prove the conclusion of Lemma C.16 for $e=d_{i}$ where $i=d$.

Sections of $\pi_{i}$

For each $i\in I$, apply Lemma C.11 about domination for powers of linear orders to $r$ and $k_{i}$, leading to some threshold $\omega_{i}$. Define

[TABLE]

Our first condition on the threshold $\omega$ is that

[TABLE]

Let $t_{*}$ be the information of rank $\omega_{*}$ that is stored in the rank $\omega$ type $t$, i.e. $t_{*}$ is the unique rank $\omega_{*}$ type contained in type $t$.

Let $i\in I$. The general idea in this part of the proof is to study the order $\prec$ when comparing elements of ${\mathfrak{A}}$ that agree on all coordinates other than $i$. Consider the projection

[TABLE]

For $z\in{\mathfrak{A}}$ of type $t_{*}$ define

[TABLE]

to be the function which fills in the missing coordinates $j\in I-\left\{i\right\}$ by the values used in $z$. This function is a section of $\pi_{i}$ in the sense that $\pi_{i}\circ\sigma_{z}$ is the identity on ${\mathfrak{A}}_{i}$. Consider the preimage of $\prec$ under this section, i.e. the relation $\prec^{z}_{i}$ defined by

[TABLE]

By Theorem C.2, $\sigma^{z}_{i}$ is continuous, and therefore $\prec_{i}$ is defined by a first-order formula of same quantifier rank as $\prec$, namely $r$. Therefore, since the type $t_{*}$ has rank at least $\omega_{i}$ as obtained from Lemma C.11, it follows that there are a polarity $p_{i}\in\left\{-\omega_{i},\omega_{i}\right\}$ and a dominating coordinate $d_{i}\in\left\{1,\ldots,k_{i}\right\}$ such that

[TABLE]

By Theorem C.2, if $z$ and $z^{\prime}$ have the same type of rank $r$ then $\prec^{z}_{i}$ and $\prec^{z^{\prime}}_{i}$ are the same order. Therefore, since the quantifier rank of $t_{*}$ is at least $r$, it follows that the dominating coordinate $d_{i}$ and polarity $d_{i}$ do not depend on $z$, as long as it has type $t_{*}$. Because $\sigma^{z}_{i}$ is a section of $\pi_{i}$ and it preserves the appropriate orderings, it follows that

[TABLE]

By applying the above to $z=x$, we see that coordinate $d_{i}$ dominates whenever $x,y$ agree on coordinates other than $i$:

[TABLE]

Section of $\pi$

As announced in the proof strategy, we now consider the projection which uses only the dominating coordinates $d_{i}$ that were found in Section C.5:

[TABLE]

We will find a suitable section $\sigma$ of $\pi$ and prove that there is a dominating coordinate for the image of that section.

Recall the type $t_{*}$ discussed in Section C.5, which is obtained by keeping only the rank $\omega_{*}$ information from the type $t$. Define

[TABLE]

to be the section of $\pi$ that is defined by

[TABLE]

We argue why the section $\sigma$ is $(\omega_{*}+2k+r)$-continuous. Consider a subset $S$ of the universe of structure ${\mathfrak{A}}$ defined by a unary formula of some quantifier rank $q$. We want to show that the set of elements of $\mathfrak{B}$ that are sent to $S$ satisfy some formula of rank $q+\omega_{*}+2k+r$. This amounts to showing that, for a unary rank $q$ type $t$ of ${\mathfrak{A}}$, there is a unary formula $\phi$ over $\mathfrak{B}$ which selects elements whose image with respect to $\sigma$ has type $t$. Using Theorem C.2, the formula $\phi$ can be defined by quantifying over the missing coordinates and then checking that the whole tuple satisfies $t$, $t_{*}$ if possible, and that it is the minimal one to do so. Thus we obtain a formula of quantifier rank $q+\omega_{*}+2k+r$ (the $2$ comes from the fact that we need to check minimality).

Define $\prec_{\mathfrak{B}}$ as the inverse image of $\prec$ with respect to $\sigma$. From continuity, it follows that $\prec_{\mathfrak{B}}$ is defined by a first-order formula of quantifier rank at most $\omega_{*}+2k+2r$. Apply Lemma C.6 to this quantifier rank, yielding some threshold $\omega_{\mathfrak{B}}$. We assume that

[TABLE]

Since the projection $\pi$ is continuous, it follows that all elements of type $t$ in ${\mathfrak{A}}$ are mapped by $\pi$ to elements of the same rank $\omega$ type, call it $t_{\mathfrak{B}}$. By Lemma C.6 and the assumption (14), there are a dominating coordinate $d\in I$ and a polarity $p_{\mathfrak{B}}\in\left\{-\omega_{\mathfrak{B}},\omega_{\mathfrak{B}}\right\}$ such that

[TABLE]

Define $e$ to be $d_{i}$ for $i=d$. Because $\sigma$ is a section and it preserves the appropriate orderings, it follows that

[TABLE]

Proof of Lemma C.16

We now complete the proof of Lemma C.16. Define $p\coloneqq 2p_{i}+p_{\mathfrak{B}}$. Let $x,y\in{\mathfrak{A}}$ have type $t$ and assume that

[TABLE]

To prove $x\prec y$, as required in the conclusion of Lemma C.16, we will find an $\prec$-ascending chain which begins in $x$, ends in $y$, and such that each step in the ascending chain is proved using the results from Sections C.5 and C.5.

Claim 10**.**

There is an $x^{\prime}$ of type $t$ in the image of $\sigma$ such that $x\prec x^{\prime}$ and

[TABLE]

Proof C.17**.**

We say that $x$ is canonical on coordinate $i\in I$ if $x[i]=z[i]$ for some $z$ in the image of $\sigma$. By Theorem C.2, if $x$ is canonical on all coordinates $i\in I$, then it is in the image of $\sigma$. Therefore, we can prove the claim by induction on the number of coordinates $i\in I$ on which $x$ is canonical, and in the induction step we can make a single coordinate $i$ canonical, at the cost of shifting $x[i][d_{i}]$ by $p_{i}$ positions, thanks to (13).

Apply Claim 10 to $x$, yielding some $x^{\prime}$ of type $t$ with $x\prec x^{\prime}$. Apply a symmetric result to $y$, yielding some $y^{\prime}$ of type $t$ with $y^{\prime}\prec y$ and

[TABLE]

By definition of $p$ and the assumption (16), we see that

[TABLE]

and therefore (15) can be applied to conclude $x^{\prime}\prec y^{\prime}$, and thus also $x\prec y$.

C.6 Proof of the Product Domination Lemma

In this section, we complete the proof of the Product Domination Lemma, and therefore also of the Domination Lemma.

Let $\omega$ be a threshold that is high enough, we will specify the lower bounds on $\omega$ throughout the proof. Let $t$ be a unary rank $\omega$ type in ${\mathfrak{A}}$. Consider the projection

[TABLE]

which maps each element of ${\mathfrak{A}}$ to the appropriate tuple of block numbers. This function is continuous. Let $\omega_{*}$ be the threshold obtained by applying Lemma C.16 to quantifier rank $r$ and the product $\mathfrak{B}$. We assume that

[TABLE]

Let $t_{*}$ be the type of rank $\omega_{*}$ which stores the quantifier rank $\omega_{*}$ information of type $t$.

We say that $x,x^{\prime}\in{\mathfrak{A}}$ overlap if there is a block which intersects both $x$ and $x^{\prime}$. More formally,

[TABLE]

Note that overlapping is defined purely in terms of the image under $\pi$. The first step in the proof is the following claim, which shows that there is a dominating coordinate when only comparing non-overlapping elements.

Claim 11**.**

There exist $d\in I$, $e\in\left\{1,\ldots,k_{d}\right\}$ and $q\in\left\{-\omega_{*},\omega_{*}\right\}$ such that

[TABLE]

Proof C.18**.**

One can show that there is a continuous section $\sigma$ of $\pi$ such that $\sigma\circ\pi$ preserves the type $t_{*}$, i.e., it maps $t_{*}$ to a subset of itself. To define the section, one only needs to choose for each coordinate $(i,j)$ and each block of ${\mathfrak{A}}_{i}$ an appropriate representative such that tuples of type $t_{*}$ are mapped to tuples of type $t$. Using compositionality, we thus have that $\sigma$ maps tuples of the same type to tuples of the same type.

Define $\prec_{\mathfrak{B}}$ to be the pre-image of $\prec$ under this section. Since $\sigma$ is continuous, the order $\prec_{\mathfrak{B}}$ is definable using quantifier rank $r$. By Lemma C.16 and the definition of $\omega_{*}$, there exist dominating coordinates $d\in I$, $e\in\left\{1,\ldots,k_{d}\right\}$ and a polarity $q\in\left\{-\omega_{*},\omega_{*}\right\}$ such that

[TABLE]

We now extend the above result to non-overlapping elements of type $t_{*}$, as required in the statement of the claim. Using compositionality, one can show that if $x$ and $y$ are non-overlapping, then the binary rank $r$ type of the pair $(x,y)$ in ${\mathfrak{A}}$ is uniquely determined by the unary rank $r$ types of $x$ and $y$ as well as the binary rank $r$ type of $\pi(x,y)$. Since $\sigma\circ\pi$ does not change the value under $\pi$, it follows that $x$ and $y$ overlap if and only if their images with respect to $\sigma\circ\pi$ overlap. As we have argued at the beginning of this proof, $\sigma\circ\pi$ maps the set of tuples of type $t_{*}$ to a subset of itself, and therefore if $x$ and $y$ have type $t_{*}$, then also their images under $\sigma\circ\pi$ have type $t_{*}$. It follows that

[TABLE]

By combining this observation with (18), we obtain the conclusion of the claim.

The general idea in the rest of the proof is to show that if $x,y\in{\mathfrak{A}}$ of type $t$ are possibly overlapping, then one can find a $z$ which overlaps neither with $x$ nor with $y$ and where $x\prec z\prec y$ can be shown using Claim 11. To find this $z$, we will shift $x$ (or $y$) by several blocks to the left or right, as explained below.

For $b\in\mathfrak{B}$ and a possibly negative integer $\delta$, define $b+\delta$ to be the result of adding $\delta$ to all coordinates of $b$. Note that $x+\delta$ might fall out of $\mathfrak{B}$, e.g. because some coordinate might become negative. For $x\in{\mathfrak{A}}$, define $\Delta_{x}$ to be the set of integers $\delta$ such that

[TABLE]

The key observation is the following claim, which says that either $\Delta_{x}$ is big for all $x\in{\mathfrak{A}}$ of type $t$, or one can trivially find a dominating coordinate, because there is a choice of coordinates the values at which always lie in the same block.

Claim 12**.**

One of the following holds:

There are $i\in I$ and $j\in\left\{1,\ldots,k_{i}\right\}$ such that

[TABLE] 2. 2.

For every $x\in{\mathfrak{A}}$ of type $t$, the set $\Delta_{x}$ contains $\left\{-p,\ldots,p\right\}$.

Proof C.19**.**

For $s\in\left\{0,1,\ldots\right\}$ define $t^{s}$ to be rank $s$ information stored in type $t$, i.e. this is the unique rank $s$ type contained in $t$. By continuity of $\pi$, the image of $t^{s}$ under $\pi$ is a rank $s$ type in the structure $\mathfrak{B}$, call it $t^{s}_{\mathfrak{B}}$. By the Threshold Lemma, every rank $s$ type in $\mathfrak{B}$ amounts to measuring distances between coordinates and minimal and maximal elements, up to threshold $2^{s}$. We say that $t^{s}_{\mathfrak{B}}$ is anchored if it fixes the distance of some coordinate to either the minimal or maximal element, i.e. some (equivalently, every) $x$ in $\mathfrak{B}$ of type $t^{s}_{\mathfrak{B}}$ is such that $x[i][j]$ has distance $<2^{s}$ from either $1$ or $n_{i}$ for some $i\in I$ and $j\in\left\{1,\ldots,n_{i}\right\}$. If $t^{\omega}_{\mathfrak{B}}$ is anchored, then item 1 in the claim holds. Suppose that $t^{s+1}_{\mathfrak{B}}$ is not anchored. It follows from the Threshold Lemma that for every $b$ of type $t^{s+1}_{\mathfrak{B}}$ and every $\delta\in\left\{-2^{s},\ldots,2^{s}\right\}$, the shifted value $b+\delta$ has type $t^{s}_{\mathfrak{B}}$. In particular, if $s\geq\omega_{*}$ and $t^{s+1}_{\mathfrak{B}}$ is not anchored, then $\Delta_{x}$ has size at least $2^{s+1}$ for every $x$ of type $t^{s+1}_{\mathfrak{B}}$. Thus, with the assumption that

[TABLE]

the result follows.

Apply Claim 12. If the first case holds, then $i$ and $j$ are dominating coordinates by vacuous truth. We are left with the other case. We will show that $d$ and $e$, as in Claim 11, are dominating coordinates. Assume that $x,y\in{\mathfrak{A}}$ have type $t$ and assume $x\sqsubset^{p}y$. We will show $x\prec y$. By the assumption on $\Delta_{x}$, we know that for every integer $\delta$ with $0<\delta<p$, there is a $x_{\delta}$ of type $t_{*}$ such that

[TABLE]

For every $i\in I$ and $j\in\left\{1,\ldots,k_{i}\right\}$, there are at most two choices of $\delta$ such that

[TABLE]

By a counting argument and thanks to the definition of $p$, it follows that there is some $p_{\mathfrak{B}}$ with

[TABLE]

such that $x_{\delta}$ overlaps neither with $x$ nor with $y$. Therefore, we can use Claim 11 to get $x\prec x_{\delta}\prec y$.