# Rank-decreasing transductions

Mikołaj Bojańczyk and Pierre Ohlmann

###### Abstract.

We propose to study transformations on graphs, and more generally structures,
by looking at how the cut-rank (as introduced by Oum) of subsets is affected
when going from the input structure to the output structure. We consider
transformations in which the underlying sets are the same for both the input
and output, and so the cut-ranks of subsets can be easily compared. The
purpose of this paper is to give a characterisation of logically defined
transductions that is expressed in purely structural terms, without referring
to logic: transformations which decrease the cut-rank, in the asymptotic
sense, are exactly those that can be defined in monadic second-order logic.
This characterisation assumes that the transduction has inputs of bounded
treewidth; we also show that the characterisation fails in the absence of any
assumptions.

Cut-rank, transductions, monadic second-order logic

††ccs: Mathematical logic and formal languages

##  1\. Introduction

One of the central themes of logic in computer science is the equivalence of
recognisability (by automata, or algebras) and definability in logic, see
(Thomas97, ) and (bojanczyk_recobook, ) for surveys. This equivalence was
proved originally for strings by Büchi (Buchi60, , Thms 1 and 2), Elgot
(Elgot61, , Thm 5.3) and Trakhtenbrot (trakthenbrot1958, , Thms 1 and 2). It
has been extended to many other structures, such as infinite words (Buchi62, ,
Thm 1), or finite (thatcher1968generalized, , Thm 17) and infinite trees
(rabinDecidabilitySecondOrderTheories1969, , Thm 1.7). The logic that appears
in such theorems is usually some variant of monadic second-order logic mso.

In words and trees, there are usually natural automata models, and the
challenges are mainly about dealing with infinity. In graphs, the challenge is
different – it is not clear how a graph should be parsed by an automaton. The
study of recognisability and logic for graphs started in the late 1980’s,
mainly with the work of Courcelle. The resulting theory, see the book
(courcelleGraphStructureMonadic2012, ) for a reference, is technically
difficult, and is tightly connected to structural graph theory, in particular
to treewidth. (One can consider more general structures, such as ternary
relations, or even hypergraphs, but graphs contain already many of the
important difficulties. We will talk about more general structures later in
the paper. ) As was the case for words or trees, a central theme in this
theory is

$\displaystyle\text{definable in
{{mso}}}\quad\Leftrightarrow\quad\text{recognisable}.$

The $\Rightarrow$ implication is known as Courcelle’s Theorem
(courcelleMonadicSecondorderLogic1990, , Thm 4.4). This is a highly
influential result, especially due to its application to linear time mso model
checking on graphs of bounded treewidth, which initiated the field of
algorithmic meta-theorems (grohe2011methods, ). The implication $\Leftarrow$
is known to fail in general, but has been proved for various kinds of tree-
decomposable graphs, such as graphs of bounded treewidth
(bojanczykDefinabilityEqualsRecognizability2016a, , Theorem 2.10) or graphs of
bounded linear cliquewidth (linearcliquewidth2021, , Theorem 3.5). It is
conjectured that the $\Leftarrow$ implication holds for all tree-decomposable
graphs (DBLP:journals/corr/abs-2305-18039, , Conjecture 5.3).

The equivalence of definability and recognisability explains the importance of
mso logic, by describing it in an alternative way that does not refer to
logic. This way we know that mso is not just some fluke of the syntax. In this
paper, we initiate a similar apologetic project, except that instead of
languages we consider transductions.

Transductions, as considered in this paper, are transformations that input
graphs and output other graphs, in a nondeterministic fashion (one input may
yield several outputs). The importance of transductions, and especially those
that can be defined in mso, was observed independently by all early authors in
this topic, namely by Arnborg et al. (arnborg1991easy, , Sec 4), Engelfriet
(engelfriet1991, , Def 6) and Courcelle (courcelle1991, , Def 2.2). The goal
of this paper is to prove that mso transductions are the canonical choice of
graph transformation, by characterising them in a way that does not use logic,
and refers only to the structural properties of the input and output graphs.
Informally speaking, our main result says that a transduction is definable in
mso if and only if simple subsets of the input graph are mapped to simple
subsets of the output graph.

Let us explain this informal statement in more detail.

We begin with the notion of simple subsets in a graph. The general idea is
that to each subset of vertices in a graph we can assign a number, called its
rank, which quantifies the amount of communication between the subset and its
complement. This rank can be formalised in a number of different ways,
including a Myhill-Nerode style definition as used in clique-width, or an
algebraic definition proposed by Oum (oum2005rank, , Sec 2) which computes the
rank of a certain matrix. Although the various formalisations of rank give
different numbers, these numbers are asymptotically equivalent, which means
that one is bounded if and only if the other is bounded. Such asymptotic
equivalence is all we need in this paper.

We now explain what we mean by mapping simple subsets to simple subsets. In
order to relate subsets of the input graph with subsets of the output graph,
we consider transductions in which the input and output graphs use the same
vertex set. This allows us to identify subsets of the input graph with subsets
of the output graph, as in the following picture:

(The usual notion of transduction allows to remove some vertices and copy some
others, the restriction on having the same vertex set will not incur any real
loss of generality, while simplifying notation.) We say that a transduction is
_rank-decreasing_ if for every $k$ there is some $\ell$ such that if a subset
of an input graph has rank at most $k$, then the same subset in every
corresponding output graph has rank at most $\ell$. Intuitively speaking, such
a transduction can only forget information from the input graph. To the best
of our knowledge, the notion of rank-decreasing transductions is new. It is a
simple notion, and yet it seems to be important.

We are now ready to state the main result of this paper, Theorem 2.11: a
transduction is rank-decreasing if and only if it is contained in an mso
transduction. This result is proved under the assumption that the input graphs
of the transduction have bounded treewidth, and we give counterexamples which
show that the result can fail without this assumption. We conjecture that the
result can be extended to graphs of bounded cliquewidth, and structures beyond
graphs, such as structures with ternary relations.

As mentioned before, one of the reasons to characterise mso transductions in
non-logical terms is to understand what features of the logic are essential.
One such feature is modulo counting. In our main theorem, we use a variant of
mso that allows modulo counting, and we present evidence that this variant is
necessary, i.e. transductions without modulo counting are not sufficient to
capture all rank-decreasing transductions. This situation is broadly
reminiscent of the Seese conjecture (seese1991structure, , Sec 4), which in
its present state boils down to the importance of counting (the conjecture has
been proved with modulo counting (courcelle2007vertex, , Thm 5.6), but remains
open without modulo counting).

The paper is organised as follows. Section 2 contains an overview, with the
minimal definitions needed to understand the main result of the paper. The
overview is phrased in terms of graphs, but later in the paper we develop the
framework in terms of general structures (although the main result is proved
only for graphs). The main result is proved in Sections 3 and 4. In Section 3,
we show the implication

$\displaystyle\text{definable in {{mso}}}\quad\Rightarrow\quad\text{rank-
decreasing}.$

We do this by giving several descriptions of rank, which have an increasingly
logical character; with the last description the implication $\Rightarrow$
becomes self-evident. In Section 4, we prove the converse implication
$\Leftarrow$ (under the assumptions that the input graphs have bounded
treewidth; this assumption is not needed for $\Rightarrow$). We first prove
$\Leftarrow$ for transductions that input trees, and then we extended to
inputs of bounded treewidth by using the definable tree decompositions from
(bojanczykDefinabilityEqualsRecognizability2016a, , Thm 2.4). In Section 5, we
present some conjectures about how our main theorem could be extended beyond
graphs of bounded treewidth, and we discuss some consequences of these
conjectures. Finally, in Appendix B we make some limited progress on these
conjectures. Although Appendix B is not the main conceptual contribution of
this paper, it is the most technically involved part.

##  2\. Overview

In this section, we describe the minimal definitions that are needed to
understand the main result of the paper. In later sections, these definitions
are generalized, e.g. from graphs to structures that allow relations of arity
bigger than two. These generalizations will be used both to prove the main
result and to state conjectures.

### Cut-rank

We begin by describing the cut-rank parameter of Oum, which is a measure that
associates a number to every subset of vertices in a graph. Consider an
undirected graph. For a subset $X$ of the vertices, consider the following
matrix which has values in $\\{0,1\\}$. The rows are vertices $x\in X$, the
columns are vertices $y\not\in X$, and the value of the matrix corresponding
to a pair $(x\in X,y\not\in X)$ is $0$ or $1$ depending on whether there is an
edge connecting the two vertices. The _cut-rank_ of the subset $X$ is defined
to be the rank of this matrix (i.e. number of linearly independent rows, or
equivalently, columns) when viewed as a matrix over the two-element field.

###### Example 2.1.

The cut-rank of a subset is at most its size, because a matrix with $n$ rows
can have rank at most $n$.

###### Example 2.2.

Consider a graph that is a path together with a connected subset $X$:

The corresponding matrix has at most two rows that contain exactly one $1$,
and the remaining rows contain only $0$. Hence, the cut-rank is at most $2$.
More generally, the cut-rank of a subset in the path is proportional to the
number of edges that are cut.

###### Example 2.3 (Cut-rank in a grid).

Consider a graph that is a square $n\times n$ grid, as in the following
picture:

If a subset $X$ of vertices in this grid contains at most half of all the
vertices, then its cut-rank is approximately its size, as expressed in the
following formula:

$\displaystyle\sqrt{|X|}\quad\leq\quad\text{cut-rank of
$X$}\quad\leq\quad|X|.$

Since the cut-rank of a set is the same as the cut-rank of its complement, it
follows that for every subset in the square grid, its cut-rank is
approximately the same as minimum of $\\{$size of the subset, size of its
complement$\\}$.

### Transductions

The other main topic of this paper is transductions, which are transformations
that input and output graphs, or more general structures. We begin with a very
general notion of transduction.

######  Definition 2.4.

A _graph-to-graph transduction_ is any binary relation between graphs, such
that for every pair in the transduction, both graphs have the same vertices.

The assumption that the two graphs have the same vertices will allow us to
relate vertices in two graphs111The ability to relate vertices in the input
and output graphs (which is implemented here by simply using the same vertices
in both graphs) is similar to the origin information in
(bojanczykTransducersOriginInformation2014, ). . We will be mainly interested
in comparing the cut-rank of the same subset of vertices in both graphs, see
Definition 2.6. In the paper, we use the following terminology: if a
transduction contains a pair of graphs $(G,H)$, then $G$ is called the input
graph and $H$ is called the output graph. We do not even make any assumptions
about the transduction being closed under isomorphism, although all examples
considered in this paper will be closed under isomorphism in the following
way: if we take a pair of graphs that is related by a transduction, and apply
the same bijection to the vertices of both graphs, then the new pair is also
in the transduction.

###### Example 2.5 (Examples of transductions).

Here are some examples of graph-to-graph transductions.

  1. (1)

the output graph is obtained from the input graph by removing any subset of
edges;

  2. (2)

as in 1, but also the input graph has treewidth $\leq 7$.

For each of the above examples, there is also a converse transduction, where
the input and output graphs are swapped. Taking the converse will not preserve
some properties of graph-to-graph transductions that will be considered in
this paper, such as being definable in mso or being rank-decreasing.

### Rank-decreasing transductions

We now present the main definition of this paper, which is rank-decreasing
transductions. The idea is that the cut-rank of a subset in the output graph
is bounded by a function of the cut-rank for the same subset in the input
graph.

######  Definition 2.6 (Rank-decreasing transduction).

A graph-to-graph transduction is called _rank-decreasing_ if there is some
function $f:{\mathbb{N}}\to{\mathbb{N}}$ such that

$\displaystyle\text{cut-rank of $X$ in $H$}\leq f(\text{cut-rank $X$ in $G$})$

for every $(G,H)$ in the transduction and subset of vertices $X$.

In the above definition, we do not need to specify if we refer to vertices of
the input or output graph, since both graphs have the same vertices. The rank
does not need to strictly decrease when applying the transduction, so it might
be more formal to call it rank-non-increasing, but we use the name rank-
decreasing for brevity.

###### Example 2.7.

Consider the transduction from item 1 in Example 2.5, which removes edges from
a graph. If the input graph is a clique, then every subset has cut-rank $1$.
However, after removing some edges, the same subset can have an arbitrarily
large cut-rank. Therefore, this transduction is not rank-decreasing. The same
kind of argument applies to the converse transduction, which adds edges.

Consider the transduction from item 2, which removes edges, but where the
input graphs are restricted to treewidth $\leq 7$. As we will explain later in
this paper, this transduction is definable222The transduction is clearly
definable in the model which allows quantification over subsets of the edges,
but it is also definable with quantification over subsets of the vertices when
the inputs have bounded treewidth, which follows from a result called the
Sparseness Theorem (courcelleGraphStructureMonadic2012, , Section 9.4).  in
monadic second-order logic, and therefore it is rank-decreasing. Consider now
the converse of this transduction, i.e. the transduction that adds edges, but
subject to the assumption that output graph has treewidth $\leq 7$. This
transduction is not rank-decreasing. Indeed, suppose that the input graph has
no edges. Then every subset of vertices has cut-rank $0$. However, if the
output graph is a path, which has treewidth 1, then there can be subsets of
vertices in the output graph that have arbitrarily large cut rank.

###### Example 2.8.

Consider any transduction where every input graph is a grid. Then, by Examples
2.1 and 2.3, this transduction is necessarily rank-decreasing.

### Definable transductions

In this paper, we will be mainly interested in transductions that can be
defined in logic. The logic that we use is cmso, which is monadic second-order
logic equipped with modulo counting (i.e. one can check if the size of a set
is divisible by two, or by three, etc.). We assume that the reader is familiar
with the syntax and semantics of monadic second-order logic, see (Thomas97, ,
Section 2). In this paper, we model a graph as a structure where the universe
is the vertices, and the edges are represented by a binary relation (which is
symmetric for undirected graphs).

######  Definition 2.9 (Definable graph-to-graph transductions).

The syntax of a _definable graph-to-graph transduction_ is given by:

  * •

A set of _colours_ , which is a finite set.

  * •

An _edge formula_ , which is a formula of cmso that has two free variables,
and uses the vocabulary of graphs (a single binary relation), extended with a
family of unary predicates that has one unary predicate per colour.

The semantics of the transduction is defined as follows. Let $G$ be a graph,
which will be treated as an input graph. A _colouring_ is a function that maps
vertices of the graph to colours from the transduction. Every colouring
induces a structure, in which apart from the edge relation there is a unary
predicate for each colour. The output graph is then defined over the same
vertices as the input graph, with edges defined by the edge formula. (The
output graph should be undirected, i.e. the edge formula should define a
symmetric relation for every input graph and colouring; otherwise, the
transduction is ill-formed.) Note that there is one output graph per
colouring, some of which may coincide, and therefore if the input graph has
$n$ vertices and there are $k$ colours, then there are at most $k^{n}$ output
graphs.

In the literature, transduction usually have additional features, namely,
copying, removing vertices, and filtering. Copying and removing vertices are
irrelevant here because we will only consider transductions which preserve the
set of vertices. Likewise, filtering can be omitted for our purposes because
we will work with sub-definable transductions (see below). For these reasons,
we prefer to work with the slightly simpler notion of transductions presented
above.

### Rank-decreasing equivalent to sub-definable

We now present the main result of the paper, which is that for graph-to-graph
transductions with inputs of bounded treewidth, being rank-decreasing is the
same as being definable. There is a small caveat: since being rank-decreasing
is closed under removing (input, output) pairs from a transduction, a similar
closure must be applied to definable transductions.

######  Definition 2.10 (Sub-definable).

A graph-to-graph transduction is called _sub-definable_ if it is contained, as
a binary relation on graphs, in some definable transduction.

For example, since the identity transduction is definable, it follows that
every subset of the identity is sub-definable, e.g. the identity on graphs
restricted to graphs with a prime number of vertices. Here is the main theorem
of this paper.

######  Theorem 2.11.

Let $\alpha$ be a graph-to-graph transduction with inputs of bounded
treewidth. Then $\alpha$ is rank-decreasing if and only if it is sub-
definable.

The right-to-left implication is true without the assumption on bounded
treewidth, see Corollary 3.6. The assumption is used for the left-to-right
implication. The proof of the theorem is described in the rest of this paper.
Our proof does not rely on the outputs being graphs, and it would work for
other classes of output structures, such as hypergraphs or matroids. It would
also work for transductions that input more general structures, e.g. with
ternary relations, subject to the bounded treewidth restriction (using the
usual generalisation of treewidth to structures, in terms of the Gaifman
graph). We conjecture that the result can be extended to transductions with
inputs of bounded cliquewidth (or, equivalently, bounded rankwidth), and also
inputs more general than graphs, see Section 5 for more information. However,
some restrictions on the input are necessary, as explained in the following
example.

###### Example 2.12.

Recall that in Example 2.8 we have shown that every transduction that inputs
grids is rank-decreasing. We will now show that there is a transduction that
inputs grids and which is not sub-definable, and therefore this transduction
will be a witness for the failure of the implication

$\displaystyle\text{rank-decreasing}\quad\not\Rightarrow\quad\text{sub-
definable.}$

Consider the graph-to-graph transduction that consists of all pairs $(G,H)$
where $G$ is a square grid and $H$ is a graph on the same set of vertices. If
the input grid has $n$ vertices (this $n$ is necessarily a square number),
then the number of possible outputs is $2^{n\choose 2}$. In the limit, this
number is bigger than $k^{n}$ for every $k$, which is the maximal number of
outputs for a transduction that uses $k$ colours.

The main theorem is proved in the following two sections.

##  3\. Sub-definable implies rank-decreasing

In this section, we prove the easier implication in the theorem, which says
that every definable transduction is necessarily rank-decreasing. (This
implies that every sub-definable transduction is rank-decreasing since rank-
decreasing transductions are downward closed.) This implication does not need
the assumption that the inputs have bounded treewidth.

###  3.1. Structures and logic

Although the overview in Section 2 discussed undirected graphs, we will
consider other structures in this paper, e.g. directed graphs or structures
with a ternary relation. We begin by fixing some logical terminology. A
_vocabulary_ is defined to be a set of relation names, each one with a
distinguished _arity_ in $\\{1,2,\ldots\\}$, which says how many arguments the
relation takes. A _structure_ over such a vocabulary consists of a set, called
the _universe of the structure_ , together with an interpretation which maps
each relation name in the vocabulary to a relation on the universe of
corresponding arity. All structures in this paper are finite, which means that
the universe is finite. The vocabularies are also finite. When we talk about a
_class of structures_ , we assume that all structures in the class have the
same vocabulary, and that the class is closed under isomorphism of structures.
Here are some classes of structures that will appear in this paper.

###### Example 3.1 (Orders).

In the class of _linear orders_ , the vocabulary has one binary relation
$x\leq y$, and the class consists of all structures where this binary relation
is a linear order, i.e. antisymmetric, total, reflexive and transitive.

###### Example 3.2 (Directed graphs).

The class of _directed graphs_ is the class of all structures over a
vocabulary with one binary relation, without any restrictions such as
symmetry.

To define properties of structures, we use monadic second-order logic with
counting, denoted by cmso.

#### Transductions

In Section 2, we have defined the special case of graph-to-graph
transductions. The extension to arbitrary structures is defined in the obvious
way. If ${\mathcal{C}}$ and ${\mathcal{D}}$ are classes of structures, then a
${\mathcal{C}}$-to-${\mathcal{D}}$ transduction is any set of pairs of
structures, where the inputs are from the class ${\mathcal{C}}$ and the
outputs are from the class ${\mathcal{D}}$, and furthermore the input
structure has the same universe as the output structure. Recall that a class
of structures is required to use a single vocabulary, and therefore there will
be two vocabularies involved in a transduction: the input vocabulary and the
output vocabulary.

The notion of definable transductions is lifted to structures in the obvious
way. The formulas in the transduction use the input vocabulary, and instead of
having a binary edge formula, there is one formula with $n$ free variables for
every relation name in the output vocabulary that has $n$ arguments.

###  3.2. Cut-rank for general structures

We begin by generalizing cut-rank from undirected graphs to general
structures. This will be useful later on in the paper, where we measure the
cut-rank in structures that do not have a clear graph representation.

Consider a structure over some vocabulary. The _quantifier-free type_ of a
$k$-tuple of elements in the universe is defined to be the set of quantifier-
free formulas with $k$ free variables that are true for the tuple. If the
vocabulary is fixed and the number of variables $k$ is fixed, then there are
finitely many possible quantifier-free types. This is because we use finite
vocabularies.

######  Definition 3.3 (Cut-rank and type matrix).

Let $\mathbb{A}$ be a structure whose vocabulary has maximal arity $m$. Define
the _type matrix_ of a subset $X$ of its universe to be the following matrix:

  1. (1)

Rows. Tuples $(x_{1},\ldots,x_{m})\in X^{m}$.

  2. (2)

Columns. Tuples $(y_{1},\ldots,y_{m})\in(\mathbb{A}\setminus X)^{m}$.

  3. (3)

Values. Quantifier-free type $\bar{x}\bar{y}$.

The _cut-rank_ of a subset of the universe $X$ is defined to be the number of
distinct rows in this matrix.

In Lemma 3.4, we will justify that essentially the same notion of cut-rank
will arise if count the number of distinct columns, or if we compute the rank
under a suitable representation of quantifier-free types as elements of a
finite field. Furthermore, in the case of structures which are graphs, all of
these notions are essentially the same as the version of cut-rank from Section
2. First, however, we explain what we mean by “essentially the same notion”.

###  3.3. Asymptotic equivalence

We will consider two notions of rank to be equivalent if they are bounded by
each other. In this section, we introduce a notation for boundedness that will
be used in the paper.

Consider a number-valued function, i.e. a function that assigns natural
numbers to inputs from some domain $X$. The example that will be relevant here
is when the domain $X$ is the set of pairs (structure, subset of its universe)
and the function is the cut-rank. We say that this function is bounded on a
subset of the domain if its outputs on that subset have a finite upper bound.
Consider two number-valued functions $\mu_{1},\mu_{2}$ with the same domain
$X$. We say that $\mu_{1}$ is _bounded_ by $\mu_{2}$ if every subset
$X\subseteq Y$ satisfies

$\displaystyle\text{$\mu_{2}$ bounded on
$Y$}\quad\Rightarrow\quad\text{$\mu_{1}$ is bounded on $Y$}.$

We say that the functions are _asymptotically equivalent_ if they are bounded
by each other.

###  3.4. Equivalent variants of cut-rank

Define a _rank function_ over a class of structures to be a function that
assigns a natural number in $\\{0,1,\ldots\\}$ to every pair consisting of a
structure from the class and a subset of its universe. Cut-rank is one
example. The following lemma and its proof justify the choice made in
Definition 3.3 by showing that other choices are equivalent.

######  Lemma 3.4.

For every class of structures, the following rank functions are asymptotically
equivalent:

  1. (1)

the number of distinct rows in the type matrix;

  2. (2)

the number of distinct columns in the type matrix;

  3. (3)

the (algebraic) rank of the type matrix, when its values are embedded
arbitrarily into a finite field.

###### Proof.

Recall that the type matrix takes values in the set of quantifier-free types
with $2m$ variables; let $t$ denote the number of such types and $c$ and $r$
respectively denote the number of columns and rows of the matrix. Then each
row is a sequence of $c$ quantifier-free types with $2m$ variables, therefore
there are at most $t^{c}$ different rows, which is asymptotically equivalent
to $c$. Likewise, $t\leq r^{c}$.

Finally, it is a well known fact that the algebraic rank is comprised between
$\Omega(\log r)$ and $r$. ∎

Note that the type matrices of a set and its complement are transpositions of
each other; therefore it follows from the lemma that both ranks are
asymptotically equivalent.

#### Formulas with quantifiers

When defining cut-rank, we use the type matrix which stores quantifier-free
types. One could also consider a version of the type matrix which stores types
for formulas with quantifiers. For $d\in\\{0,1,\ldots\\}$, define the _cmso
theory of quantifier depth $d$_ of a $k$-tuple of elements in a structure to
be the set of cmso formulas that are true for the tuple, and which use at most
$d$ nested quantifiers. The _$d$ -type matrix_ is defined in the same way as
the type matrix, except that the values are cmso theories of quantifier depth
$d$. In particular, the 0-type matrix is the original notion of type matrix.

######  Theorem 3.5.

For every class of structures and $d\in\\{0,1,\ldots\\}$, cut-rank as defined
in Definition 3.3 is asymptotically equivalent to the function that counts the
number of distinct rows in the $d$-type matrix.

The theorem can be derived as an application of Ehrenfeucht-Fraïssé games;
this is presented in Appendix A.

We have now collected all the ingredients needed to prove the easier
implication of our main theorem, even without any assumption on inputs having
bounded treewidth.

######  Corollary 3.6.

Every sub-definable transduction is rank-decreasing.

###### Proof.

Clearly, transductions which are rank-decreasing are closed under composition.
Every definable transduction is a composition of three definable
transductions: (1) add some colouring to the universe; (2) extend the
vocabulary with all relations that can be defined using definable formulas
with at most $k$ variables and quantifier depth at most $d$; (3) remove some
relations from the vocabulary. It is easy to see that step (1) is rank-
decreasing. Step (2) is rank-decreasing thanks to Theorem 3.5. Finally, step
(3) is rank-decreasing. Let us point out that a strict decrease of the ranks
can only occur in step (3). ∎

#### Rank functions in selected classes of structures.

So far, we have discussed asymptotic equivalence for rank functions over all
structures for a given vocabulary. We finish this section with some examples
that use restricted structures, such as linear orders or equivalence
relations.

###### Example 3.7 (Rank in undirected graphs and grids).

For undirected graphs, cut-rank as in Definition 3.3 is asymptotically
equivalent to the original notion of cut-rank that was described in Section 2.
As discussed in Example 2.3, in the class of grids, cut-rank is equivalent to
the minimum of (size of the set, size of its complement).

###### Example 3.8 (Rank in linear orders).

Consider the class of linear orders from Example 3.1. Over this class, cut-
rank is asymptotically equivalent to the function that maps a subset $X$ of
the universe to the minimal number $k$ such that $X$ is a union of $k$
intervals.

###### Example 3.9 (Rank in equivalence relations).

Consider the class of equivalence relations, i.e. undirected graphs that are
disjoint unions of cliques. Over this class, cut-rank is asymptotically
equivalent to the measure that maps a set to the number of equivalence classes
that are cut by it (i.e. equivalence classes that contain elements in the set
and also outside the set).

The following lemma is often convenient.

######  Lemma 3.10.

The cut-rank of $X\cup Y$ is asymptotically bounded by the maximal cut-rank of
$X$ and $Y$.

###### Proof.

Assume that there are $\ell$ different rows in the type matrix of $X\cup Y$,
we should prove that there are at least $f(\ell)$ different rows in the type
matrix of either $X$ or $Y$, where $f$ goes to infinity. Without loss of
generality, we assume that the different rows in the matrix are labelled with
tuples $\bar{z}_{i}=\bar{x}_{i}\bar{y}_{i}$, where $\bar{x}_{i}$ is a tuple of
elements of $X$ and $\bar{y}_{i}$ is a tuple of elements of $Y$. By
definition, for each $i<j$, there is an tuple $\bar{c}$ of elements outside
$X\cup Y$ such that the quantifier-free types of
$\bar{x}_{i}\bar{y}_{i}\bar{c}$ and $\bar{x}_{j}\bar{y}_{j}\bar{c}$ differ.

This implies that the quantifier-free type of $\bar{x}_{i}\bar{y}_{j}\bar{c}$
differs with either the one of $\bar{x}_{i}\bar{y}_{i}\bar{c}$ or of
$\bar{x}_{j}\bar{y}_{j}\bar{c}$. By Ramsey’s theorem, we may assume that the
same case holds for all $i<j$, say, the first one (they are symmetrical), up
to reducing the number of rows to $f(\ell)$. Then the fact that the
quantifier-free types of $\bar{x}_{i}\bar{y}_{j}\bar{c}$ and
$\bar{x}_{j}\bar{y}_{j}\bar{c}$ implies that the type matrix of $X$ has
$f(\ell)$ different rows. ∎

A consequence of the lemma is that the cut-rank of a boolean combination of
$n$ subsets of bounded cut-rank is asymptotically bounded by $n$.

##  4\. Rank-decreasing implies sub-definable

We now turn to the more difficult implication of Theorem 2.11. Here, we use
the assumption on inputs having bounded treewidth. We prove this implication
in three steps: first for inputs that have no structure except for equality,
then for tree inputs, and finally for inputs of bounded treewidth.

###  4.1. Inputs with equality only

Define a _structure with equality only_ to be a structure over the empty
vocabulary. In this structure, logic can only use equality on the elements,
since we assume that equality is built-in to the logic. We use the name set-
to-$\mathscr{C}$ transduction for any transduction where the input vocabulary
is empty, and the output class is contained in $\mathscr{C}$. The following
lemma shows that for such transductions, rank-decreasing is the same as sub-
definable.

######  Lemma 4.1.

If a set-to-$\mathscr{C}$ transduction is rank-decreasing, then it is sub-
definable.

We actually prove and use a slightly stronger result, which describes the
structures that can arise from rank-decreasing transductions that input
structures with equality only. Define an _informative colouring_ of a
structure $\mathbb{A}$ to be a function that assigns a colour to each element
of the universe, such that for every tuple of distinct elements in the
universe, their quantifier-free type depends only on the corresponding tuple
of colours. In the following lemma, a set-to-$\mathscr{C}$ transduction is
called surjective if every structure from $\mathscr{C}$ arises as an output
for at least one input.

######  Lemma 4.2.

The following conditions are equivalent for every class of structures
$\mathscr{C}$:

  1. (1)

there is a surjective rank-decreasing sets-to-$\mathscr{C}$ transduction;

  2. (2)

there is some $k$ such that for every structure in $\mathscr{C}$, all subsets
of its universe have rank at most $k$;

  3. (3)

there is some $k$ such that every structure in $\mathscr{C}$ has an
informative colouring with at most $k$ colours.

Lemma 4.2 immediately implies Lemma 4.1. This is because for every $k$ there
is a definable transduction which inputs a set with equality only, and outputs
all possible structures that have this set as the universe, and admit an
informative colouring with at most $k$ colors.

The rest of Section 4.1 is devoted to proving Lemma 4.2. The equivalence 1
$\Leftrightarrow$ 2 and the implication 2 $\Leftarrow$ 3 are straightforward
exercises left to the reader. We concentrate on the implication 2
$\Rightarrow$ 3. We prove this implication by induction on the maximal arity
of relations in the vocabulary of $\mathscr{C}$. The induction base is when
the maximal arity is one, i.e. all relations have one argument. In this case,
there is a straightforward informative colouring: map each element to the
unary predicates that it satisfies. Consider now the induction step: suppose
that have proved the lemma for vocabularies with maximal arity $m-1$, and we
want to prove it for a vocabulary of maximal arity $m$.

In the proof, we use the following notion of _twin_ : we say that two elements
$a,a^{\prime}$ in a structure $\mathbb{A}$ are _twins_ if

$\displaystyle\mathbb{A}\models\varphi(a,b_{1},\ldots,b_{n})\quad\Leftrightarrow\quad\mathbb{A}\models\varphi(a^{\prime},b_{1},\ldots,b_{n})$

for every quantifier-free formula $\varphi$ and elements

$\displaystyle b_{1},\ldots,b_{n}\in\mathbb{A}\setminus\\{a,a^{\prime}\\}.$

Twins will be useful to get an informative colouring, as explained in the
following claim.

######  Claim 4.3.

Consider a colouring of a structure such that every two distinct elements of
the same colour are twins. Then by, possibly multiplying the number of colours
by at most $m$, we can get an informative colouring.

###### Proof.

We increase the number of colours to guarantee the following property (*):
there is no colour class whose size is in $\\{2,\ldots,m\\}$. This can be done
by splitting every colour class of bad size into singleton colour classes; the
number of colours is at most multiplied by $m$. Consider two non-repeating
tuples of elements $\bar{a},\bar{b}\in\mathbb{A}^{m}$ that induce the same
colours coordinate-wise. Thanks to the assumption (*), one can gradually
transform the tuple $\bar{a}$ into the tuple $\bar{b}$, in each step replacing
one coordinate by another element of the same colour, and getting a non-
repeating tuple. Such a step does not affect the quantifier-free type.
Therefore, the quantifier-free types of $\bar{a}$ and $\bar{b}$ are the same.
∎

Define the _twin graph_ of a structure to be the undirected graph where the
set of vertices is the universe, and the edge relation is the twin relation. A
_twin independent set_ is an independent set in this graph, i.e. a set of
elements in the universe that are pairwise unrelated by the twin relation. The
following claim uses the assumption from item 2 from Lemma 4.2, i.e. that the
rank is universally bounded, i.e. there is some fixed upper bound on the rank
of all subsets in all structures from the class.

######  Claim 4.4.

If a class of structures has universally bounded rank, then twin independent
sets from $\mathscr{C}$ have bounded size.

###### Proof.

Consider two elements $a,a^{\prime}\in\mathbb{A}$ that are not twins. This
means that there is some tuple of elements $\bar{b}$, in which the elements
$a$ and $a^{\prime}$ do not appear, such that $a\bar{b}$ and
$a^{\prime}\bar{b}$ have different quantifier-free types. Such a tuple is
called a _witness_ for $a$ and $a^{\prime}$. Observe that the size of a
witness can be bounded by the maximal arity $m$ of relations in the
vocabulary. This is because two different quantifier-free types must differ on
some relation from the vocabulary. Therefore, if two elements have a witness,
then they have a witness that uses $m-1$ elements.

We prove the claim by contradiction – if there are arbitrarily large twin
independent sets, then the rank is not universally bounded. We will show that
if there are arbitrarily large twin independent sets, then there are
arbitrarily large twin independent sets with the following _external witness
property_ : for every pair of elements in the set, the corresponding witness
is disjoint with the set. A twin independent set of size $n$ with the external
witness property gives a subset of the universe that has rank $n$, because in
the corresponding type matrix all rows are different, with the columns being
the elements that appear in the witness. Therefore, by the assumption that all
subsets in the class $\mathscr{C}$ have bounded rank, it will follow that
there cannot be arbitrarily large twin independent sets with the external
witness property.

To ensure the external witness property, we will use the Ramsey Theorem.
Suppose that there are twin independent sets

$\displaystyle a_{1},\ldots,a_{n}\in\mathbb{A}\in\mathscr{C}$

of arbitrarily large size $n$. Formally, for all indices $i<j$, there exists a
witness $\bar{c}_{i,j}$ such that the quantifier-free types of
$x_{i}\bar{c}_{i,j}$ and $x_{j}\bar{c}_{i,j}$ differ. Let $A_{0}$ denote the
set of elements $a_{i}$ with $i$ even. By the Ramsey Theorem, we may extract
an arbitrarily large twin independent set which has the following homogeneity
property: every subset of size $2m$ has the same type of quantifier-depth $m$,
if the elements in the subset are listed according to the order inherited from
$a_{1},\ldots,a_{n}$, in the structure augmented by a unary predicate
colouring $A_{0}$. Thus, we now assuming without loss of generality that the
homogeneity property is granted.

We claim that the set $A_{0}$ has the external witness property. Let $i<j$ be
two even indices. Without loss of generality, we may write
$\bar{c}_{i,j}=\bar{d}\bar{e}$ where $\bar{d}$ contains only elements of the
form $a_{i}$ with $i$ even, and $\bar{e}$ contains elements that are not of
this form. By definition of $\bar{c}_{i,j}$, the quantifier-free types of
$x_{i}\bar{d}\bar{e}$ and of $x_{j}\bar{d}\bar{e}$ differ. Therefore there
exists a quantifier free formula $\phi$ such that the formula
$\psi=\exists\bar{y}\phi(\bar{z}\bar{y})\text{ and coordinates of $\bar{y}$ do
not belong to }A_{0}$ holds for $\bar{z}=x_{i}\bar{d}$ but not for
$\bar{z}=x_{j}\bar{d}$.

Now let $\bar{d}^{\prime}$ be obtained from $\bar{d}$ by shifting all indices
of coordinates $x_{k}$ to $x_{k+1}$; note that elements of $\bar{d}^{\prime}$
do not belong to $A_{0}$. By the homogeneity property, the quantifier-depth
$m$ types of $x_{i}x_{j}\bar{d}$ and of $x_{i}x_{j}\bar{d}^{\prime}$ are the
same, therefore $\psi$ holds for $x_{i}\bar{d}^{\prime}$ and not for
$x_{j}\bar{d}^{\prime}$. We conclude that $A_{0}$ has the external witness
property. ∎

Let $d$ be the maximal size of twin independent sets. If we take a twin
independent set in the structure that has maximal size, then it will also be a
_twin dominating set_ , which is defined to be a set with the following
property: every element of the universe is either in the set, or a twin of
some element in the set. Therefore, every structure in $\mathscr{C}$ has a
twin dominating set of size at most $d$.

Consider a structure $\mathbb{A}\in\mathscr{C}$ and a twin dominating set of
size at most $d$ that is listed in some order $\bar{c}=c_{1},\ldots,c_{d}$. We
can use repetitions in the sequence if there are fewer than $d$ elements in
the structure. Define a new structure, call it $\mathbb{A}_{\bar{c}}$ as
follows. For every pair $(i,\varphi)$ where $i\in\\{1,\ldots,d\\}$ and
$\varphi$ is a quantifier-free formula with $m$ variables over the vocabulary
of $\mathscr{C}$, the structure has a relation of arity $m-1$ which is
interpreted as

$\displaystyle\\{\ \ (a_{2},\ldots,a_{m})\in\mathbb{A}^{m-1}\ \
|\begin{tabular}[]{l}$\mathbb{A}\models\varphi(c_{i},a_{2},\ldots,a_{m})$\end{tabular}\\}.$

Let $\mathscr{D}$ be the class of all structures $\mathbb{A}_{\bar{c}}$ that
arise this way. This class can be obtained from the original class
$\mathscr{C}$ by applying a definable transduction, and therefore it must also
have universally bounded rank. Since the vocabulary of $\mathscr{D}$ has
smaller maximal arity than $\mathscr{C}$, we can use the induction assumption
to conclude that $\mathscr{D}$ has informative colourings that use a bounded
number of colours, say at most $\ell$ colours.

Take some structure $\mathbb{A}\in\mathscr{C}$ and choose a sequence
$\bar{c}=c_{1},\ldots,c_{d}$ that describes some twin dominating set. Consider
a colouring that assigns the following information to an element
$a\in\mathbb{A}$:

  1. (1)

which of the elements in $\bar{c}$ are twins of $a$;

  2. (2)

the colour in the informative colouring for
$\mathbb{A}_{\bar{c}}\in\mathscr{D}$.

The number of colours in this colouring is bounded, since it depends on the
constant $d$ from Claim 4.4 and the bound from the induction assumption on
$\mathscr{D}$. To complete the proof of Lemma 4.2, we will show that this
colouring is informative. By Claim 4.3, it is enough to show that elements $a$
and $a^{\prime}$ with the same colour are twins. We need to show that for
every tuple $\bar{b}$ of length $m-1$, the tuples $a\bar{b}$ and
$a^{\prime}\bar{b}$ have the same quantifier-free type. Let $c$ be some
element in the twin dominating set $\bar{c}$ that is a twin of both $a$ and
$a^{\prime}$; such an element must exist since $a$ and $a^{\prime}$ have the
same colour. If $c$ does not appear in the tuple $\bar{b}$, then we can go
from $a\bar{b}$ to $a^{\prime}\bar{b}$ in two steps: first replace $a$ with
$c$ and then replace $c$ with $a^{\prime}$. Both steps keep the quantifier-
free type unchanged. If $c$ does appear in the tuple $\bar{b}$, then use the
colouring from the induction assumption on $\mathscr{D}$ to show that
$a\bar{b}$ and $a^{\prime}\bar{b}$ have the same quantifier-free type. This
completes the proof of Lemma 4.2.

###  4.2. Inputs are trees

In this section, we prove a special case of the main theorem, in which the
inputs are trees. We begin by

####  4.2.1. Trees and their representation

One way to think about trees is that these are undirected graphs that are
acyclic and connected. This will _not_ be the kind of trees that we use in
this paper. In the kind that we do use, the universe of the structure is only
the leaves of the tree, and the remaining nodes of the tree are represented as
subsets of the leaves, as in the following picture:

######  Definition 4.5 (Tree).

A _tree_ over a set is a family of subsets, called _subtrees_ , subject to the
following axioms: (a) every singleton is a subtree; (b) the entire set is a
subtree; and (c) if two subtrees are not disjoint, then one is contained in
the other.

In the picture before the definition, we did not draw the circles
corresponding to singleton subtrees, we follow this convention when drawing
trees in the paper to avoid clutter.

We use the usual tree terminology, such as leaf, parent, child, root,
descendant and ancestor. The trees as defined above are unordered, which means
that there is no left-to-right ordering on the children of a given node. Also,
there are no unary nodes, i.e. every subtree is either a leaf, or it has at
least two children.

We will be using transductions that input or output trees, so we need to say
how trees are represented using structures. Arguably the most natural way
would be to give a monadic second-order relation $\text{subtree}(X)$. Although
such predicates would not break the theory developed here, we choose to stick
with first-order relations, and thus we will represent the subtrees using a
ternary relation on leaves. The idea is that a pair of leaves $x$ and $y$
specifies a subtree, namely the least subtree that contains both leaves. Since
every subtree arises this way, we can use the pairs to represent subtrees, as
described in the following definition.

######  Definition 4.6 (Ternary representation of a tree).

For a tree, its _ternary representation_ is the structure in which the
universe is the leaves and there is a ternary relation defined by

$z$ is contained in the least subtree containing $x$ and $y$.

When using transductions that input or output trees, we use the above
representation. Define a _sub-forest_ in a tree to be any set that is obtained
by taking some union of sibling subtrees. Sub-forests are easily seen to have
bounded cut-rank; in fact, they characterise the cut-rank in trees.

######  Lemma 4.7.

In a tree $\mathbb{T}$, the cut-rank of a subset $X$ is asymptotically
equivalent to the minimal number of sub-forests of which $X$ is a boolean
combination.

###### Proof.

It follows from Lemma 3.10 together with the observation (Lemma 3.4) that cut-
ranks are (asymptotically) preserved under complements, that the cut-rank of
$X$ is asymptotically bounded by the minimal number $m$ of subforest of which
$X$ is a boolean combination.

We now focus on the converse: we should show that if $m$ is large, then the
rank of $X$ is large. Say that a node $Y$ in $\mathbb{T}$ is dull if it has a
child $Y^{\prime}$ such that $X\cap(Y\setminus Y^{\prime})$ is either
$Y\setminus Y^{\prime}$ or the empty set. Otherwise, say that $Y$ is
interesting.

Let $\ell$ denote the maximal size of a chain of interesting nodes, and $d$
denote the maximal number of interesting siblings. It is easy to see that if
both $\ell$ and $d$ are small, then $m$ is small; therefore either $\ell$ or
$d$ is large.

If $d$ is large then consider a node $Y$ with $d$ interesting children
$Y_{1},\dots,Y_{d}$, and for each $i\in\\{1,\dots,d\\}$, pick an element
$x_{i}\in X\cap Y_{i}$ and $z_{i}\in Y_{i}\setminus X_{i}$. Then for each
$i<j$, $z_{i}$ belongs to the least subtree containing $x_{i}$ and $z_{j}$
(which is $Y$), but does not belong to the least subtree containing $x_{j}$
and $z_{j}$ (which is $Y_{j}$), and therefore the quantifier-free types of
$x_{i}z_{i}z_{j}$ and $x_{j}z_{i}z_{j}$ differ. We conclude that the $x_{i}$’s
define different row in the type matrix, and therefore the cut-rank of $X$ is
$\geq d$.

If $\ell$ is large then consider a chain of interesting nodes
$Y_{1}\subseteq\dots\subseteq Y_{m}$. Note that for each
$i\in\\{2,\dots,m\\}$, since $Y_{i}$ is interesting and $Y_{i-1}$ is contained
in a subtree of $Y_{i}$, the intersection of $X$ with $Y_{i}\setminus Y_{i-1}$
is neither full nor empty. Pick $x_{i}\in(Y_{i}\setminus Y_{i-1})\cap X$ and
$z_{i}\in(Y_{i}\setminus Y_{i-1})\setminus X$. As previously, it is easy to
see that for $i<j$ the quantifier-free types of $x_{i}z_{i}z_{j}$ and
$x_{j}z_{i}z_{j}$ differ, which concludes. ∎

##### Coloured trees.

We will also be using trees where the subtrees are coloured by some fixed set
of colours. One way to represent this colouring is to have, for every colour
$c$, a second-order relation $c(X)$ which selects subtrees of colour $c$. If
we want to use the ternary representation, then colouring can be represented
by giving for every colour $c$ a binary predicate which selects the pairs of
nodes $(x,y)$ such that the least subtree containing $x$ and $y$ has colour
$c$. In some constructions of this paper, we will want a transduction or
formula to be able to guess a colouring for a tree. It is not immediately
clear how this can be done, since the subtrees are not part of the universe of
the structure under our chosen representation, and therefore one cannot simply
use subsets of the universe to represent the colouring. However, this will be
possible, as stated in the following lemma.

######  Lemma 4.8.

For every finite set of colours $C$, the following transduction is definable.

$\displaystyle\\{\ \ (\mathbb{T},\mathbb{S})\ \
|\begin{tabular}[]{l}$\mathbb{T}$ is a tree, and $\mathbb{S}$ is a
$C$-coloured tree\\\ that is obtained by some colouring of
$\mathbb{T}$\end{tabular}\\}$

###### Proof.

The proof has two steps. In the first step, we produce certain coloured trees,
which we call orientations. These are used in the second step to produce
arbitrary colourings.

##### Step 1. Orientations.

Define an _orientation_ of a tree $\mathbb{T}$ to be any colouring
$\mathbb{S}$ of this tree with colours, called “left”, “right” and
“anonymous”, such that every non-leaf subtree has exactly one child with label
“left”, and exactly one child with label “right”. We first show that a
definable transduction can map an input tree to at least one orientation.

Consider a colouring of the leaves in a tree with elements from the cyclic
group ${\mathbb{Z}}_{3}$333 To implement the transduction, we will need to use
counting modulo three. The same proof works for all orders at least three, and
a slightly more elaborate proof works for order two. Therefore, counting
modulo any number $k>1$ would be enough to make the proof work.. Extend this
colouring to subtrees of $\mathbb{T}$, by defining the colour of a subtree to
be the sum (modulo three) of the colours of the leaves in that subtree. We say
that a subtree has a _unique sum_ if none of its siblings have the same sum.
We will show:

  * (*)

For every tree $\mathbb{T}$ and $c\in{\mathbb{Z}}_{3}$, one can colour the
leaves of $\mathbb{T}$ with colours from ${\mathbb{Z}}_{3}$ so that: (1) the
sum of the root subtree is $c$; and (2) every non-leaf has at least two
children with unique sum.

From (*) we easily get an orientation, by defining the “left” and “right”
children to be the first two children with unique sum, ordered according to
their sums. To prove (*), we use a simple induction on the number of leaves.
For the induction base, when $\mathbb{T}$ has one leaf, there is nothing to
do. For the induction step, choose two children of the root subtree. To these
two children, apply the induction assumption with colours $c$ and $-c$, and
for the remaining children of the root apply the induction assumption with
colour 0.

##### Step 2. Arbitrary colourings.

We now use the orientation produced in the previous step to define an
arbitrary colouring. Consider some orientation $\mathbb{S}$ of a tree
$\mathbb{T}$. For a subtree $X$, define its _chosen leaf_ to be the leaf that
is obtained using the following procedure which uses the colours from the
orientation: start in the “left” child of $X$, and then continue taking
“right” children until a leaf is reached444This idea is taken from (Thomas97,
, Proposition 3.1).. The _chosen leaf_ function is an injective map from (non-
leaf) subtrees to leaves, which can be defined using mso. Therefore, a
colouring of the subtrees can be represented using a colouring of the leaves,
which can be implemented by a definable transduction since the leaves are the
universe. ∎

As mentioned in Footnote 3, the construction in the above lemma uses modulo
counting (although the modulus can be any number $m>1$). In fact, we
conjecture modulo counting is necessary.

######  Conjecture 4.9.

The transduction from Lemma 4.8 cannot be defined without modulo counting,
even when restricted to binary trees, i.e. trees where every subtree has zero
or two children.

Since the transduction in the conjecture is easily seen to be rank-decreasing
(for example, because it is sub-definable with modulo counting), the
conjecture would imply that modulo counting is necessary to define all rank-
decreasing transductions, even for inputs that are binary trees. The
conjecture could be seen as evidence in favour of viewing modulo counting as a
necessary feature of monadic second-order logic. (A mentioned in the
introduction, a related phenomenon appears in the Seese conjecture.)

####  4.2.2. Transductions that input trees

Having defined trees and their representation, in this section, we prove that
the implication

$\displaystyle\text{rank-decreasing}\quad\Rightarrow\quad\text{sub-definable}$

holds for all transductions that input trees, with no assumptions on the
output structures. In the following, a tree-to-$\mathscr{C}$ transduction is a
transduction that inputs trees, with the representation discussed in the
previous section, and outputs structures from a class $\mathscr{C}$. The
output class $\mathscr{C}$ need not be a class of graphs; it can use relations
of arity more than two.

######  Theorem 4.10.

Let $\mathscr{C}$ be a class of structures. If a tree-to-$\mathscr{C}$
transduction is rank-decreasing, then it is sub-definable.

This theorem is proved using a combination of the results from Sections 4.1
and 4.2.1. The general idea is that a pair $(\mathbb{T},\mathbb{A})$ in a
rank-decreasing transduction can be seen as a tree decomposition of
$\mathbb{A}$, where every subtree of the tree $\mathbb{T}$ describes a part of
the structure $\mathbb{A}$, and this part is further partitioned by the
children of the subtree555Some parts of our proof are inspired by ideas dating
back to (courcelle1995logical, )..

We will use a tree automaton to reconstruct the structure $\mathbb{A}$ by a
bottom-up pass through this tree. The run of the automaton will be represented
using the coloured trees from Section 4.2.1, while the local update which uses
the states in the child subtrees to compute the state in their parent will be
handled using the results from Section 4.1.

#### Induced sub-structures.

We begin by explaining how a part of a structure is viewed as a structure. The
idea is that we want to retain information about how the sub-structure
communicates with its exterior. This is formalized in the following
definition.

######  Definition 4.11.

Let $\mathbb{A}$ be a structure with maximal arity $m$ and let $X$ be a subset
of its universe. The structure $\mathbb{A}|X$ is defined as follows. The
universe is $X$. For every $\ell\leq m$, every
$c_{1},\ldots,c_{\ell}\in\mathbb{A}\setminus X$ and every quantifier-free
formula

$\displaystyle\varphi(x_{1},\ldots,x_{k},y_{1},\ldots,y_{\ell})$

with up to $m$ variables over the vocabulary of $\mathbb{A}$, the structure
$\mathbb{A}|X$ has a relation of arity $k$ which is interpreted as

$\displaystyle\\{\ \ (a_{1},\ldots,a_{k})\in X^{k}\ \
|\begin{tabular}[]{l}$\mathbb{A}\models\varphi(a_{1},\ldots,a_{k},c_{1},\ldots,c_{\ell})$\end{tabular}\\}.$

The vocabulary of the structure in the above definition is unbounded and
depends on the elements of the structure that are not in $X$. This will not be
an issue, since we will be interested in induced sub-structures of bounded
rank, and for such sub-structures the vocabulary will be essentially bounded,
as explained in the following lemma.

######  Lemma 4.12.

Let $\mathscr{C}$ be a class of structures with maximal arity $m$. For
$\mathbb{A}\in\mathscr{C}$ and $X$ is a subset of its universe, the number of
quantifier-free types with $m$ variables in $\mathbb{A}|X$ is asymptotically
equivalent to the rank of $X$ in $\mathbb{A}$.

Induced sub-structures are well behaved with respect to cut-rank as witnessed
by the following lemma.

######  Lemma 4.13.

For any structure $\mathbb{A}$ and $X$ and $Y$ two subsets of its universe
such that $Y\subseteq X$, the cut-ranks of $Y$ in $\mathbb{A}$ or in
$\mathbb{A}|X$ are the same.

Consider a structure $\mathbb{A}$, and a partition of its universe into
subsets $X_{1},\ldots,X_{n}$. In the proof below, we will be interested in how
the type of a tuple $\bar{a}$ in $\mathbb{A}$ can be deduced from the type of
this tuple in the induced sub-structures
$\mathbb{A}|X_{1},\ldots,\mathbb{A}|X_{n}$. Since the induced sub-structures
might not contain some elements of the tuple, we will want to talk about
partial tuples, defined as follows. A _partial $n$-tuple_ in a structure is a
tuple of length $n$, where every component is either an element of the
structure, or an “undefined” value. Such partial tuples arise when restricting
a structure to a subset: if $\bar{a}$ is a (complete) $n$-tuple in
$\mathbb{A}$, and $X$ is a subset of the universe in $\mathbb{A}$, then
$\bar{a}$ can be viewed as a partial $n$-tuple in $\mathbb{A}|X$, which is
undefined on those coordinates that use elements not in $X$. The type of a
partial $n$-tuple is defined in the same way as the type of a complete
$n$-tuple, except that it stores information about which coordinates are
defined/undefined. The following lemma is an immediate corollary of the
definitions.

######  Lemma 4.14 (Compositionality).

Let $\mathbb{A}$ be a structure, and let $\mathcal{X}$ be a family of subsets
that partition its universe. The type of a tuple $\bar{a}$ in $\mathbb{A}$
depends only on the types of this tuple projected into the structures
$\mathbb{A}|X$ for $X\in\mathcal{X}$.

We now rephrase the Compositionality Lemma in more precise terms, preparing
the ground for the proof below.

######  Lemma 4.15.

For every fixed vocabulary and $k,\ell,m\in\\{1,2,\ldots\\}$ one can find a
finite set of colors $Q$ with the following property. Let $\mathbb{A}$ be a
structure over the fixed vocabulary together with a family of subsets
$\mathcal{X}$ that partitions its universe, such that every subfamily
${\mathcal{Y}}\subseteq\mathcal{X}$ has union of rank at most $k$. Then there
is a family of functions

$\displaystyle\lambda_{X}:\text{types of partial $m$-tuples in
$\mathbb{A}|X$}\to Q,$

with one function for every part $X\in\mathcal{X}$, and a function

$\displaystyle\gamma:\ $ $\displaystyle Q^{\ell}\to\text{types of partial
$m$-tuples in $\mathbb{A}$}$

such that for every distinct parts $X_{1},\ldots,X_{\ell}\in\mathcal{X}$ and
every partial $m$-tuple $\bar{a}$ in $\mathbb{A}$ that is contained in
$X_{1}\cup\cdots\cup X_{\ell}$, the type of $\bar{a}$ in $\mathbb{A}$ is
obtained by applying $\gamma$ to

$\displaystyle(\lambda_{X_{1}}(\text{type of $\bar{a}$ in
$\mathbb{A}|X_{1}$}),\ldots,\lambda_{X_{\ell}}(\text{type of $\bar{a}$ in
$\mathbb{A}|X_{\ell}$})).$

We now have all the ingredients that are needed to prove Theorem 4.10.
Consider a pair $(\mathbb{T},\mathbb{A})$ that belongs to a rank-decreasing
tree-to-$\mathscr{C}$ transduction. For every node $X$ of the tree
$\mathbb{T}$, we will be interested in the structure $\mathbb{A}|X$ along with
the partition $\mathcal{X}_{X}$ that corresponds to the partition of $X$ into
its children subtrees. The following lemma shows that this equivalence
relation satisfies the assumptions of Lemma 4.15.

######  Lemma 4.16.

There is some $k$ such that for every $(\mathbb{T},\mathbb{A})$ in the
transduction, every node $X$ of $\mathbb{T}$, and every subfamily
${\mathcal{Y}}\subseteq\mathcal{X}_{X}$, the rank of the union of
${\mathcal{Y}}$ in $\mathbb{A}|X$ is at most $k$.

###### Proof.

By the assumption that the transduction is rank-decreasing. (to-do: expand
this justification) ∎

Apply Lemma 4.15 to the $k$ from the above lemma, and $m$ being the maximal
arity of relations in the vocabulary of the class $\mathscr{C}$. For every
node $X$ in the tree, apply Lemma 4.15 to the structure $\mathbb{A}|X$ and the
partition of $X$ into its children, yielding some functions

(1) $\displaystyle\\{\lambda_{Y}\\}_{\text{$Y$ is a child of
$X$}}\quad\text{and}\quad\gamma_{X}.$

The family of functions described above can be viewed as a node-coloured tree
$\mathbb{S}$, where the colour of each node $X$ indicates the functions
$\lambda_{X}$ and $\gamma_{X}$. We say that $\mathbb{S}$ follows from applying
Lemma 4.15 to $(\mathbb{T},\mathbb{A})$ if it arises as a result of the above
construction. The following lemma shows that the structure $\mathbb{A}$ can be
recovered from the node-labelled tree $\mathbb{S}$ using a sub-definable
transduction.

######  Lemma 4.17.

The following transduction is sub-definable

$\displaystyle\\{\ \ (\mathbb{S},\mathbb{A})\ \
|\begin{tabular}[]{l}$\mathbb{S}$ follows from applying
Lemma~{}\ref{lem:transition-function-on-types} to $(\mathbb{T},\mathbb{A})$
for\\\ some $\mathbb{T}$ such that $(\mathbb{T},\mathbb{A})$ is in the
transduction\end{tabular}\\}.$

###### Proof.

The functions $\lambda_{X}$ and $\gamma_{X}$ that are stored in the tree
$\mathbb{S}$ give an inductive procedure to compute the type of an $n$-tuple
of elements in the structure $\mathbb{A}$, which only uses the nodes and their
colors in $\mathbb{S}$. For an $m$-tuple $\bar{a}$ of elements in $\mathbb{A}$
(or equivalently, in $\mathbb{S}$, because these have the same universe),
define its _run_ to be the labelling

nodes of $\mathbb{S}$ $\displaystyle\to Q$ $\displaystyle X$
$\displaystyle\mapsto\lambda_{X}(\text{type of $\bar{a}$ in $\mathbb{A}|X$}).$

By Lemma 4.15, this run has an inductive structure: for every node $X$, its
label in the run depends only on the labels of its children, more specifically
the labels of the constant number of children that contain elements of the
tuple $\bar{a}$. This inductive procedure can be implemented in mso, even
without modulo counting, by guessing the run in the usual way (guess the run,
and then check that it is correctly computed in every node), since mso is
allowed to quantify over colourings of the nodes in a tree. ∎

Theorem 4.10 follows by pre-composing the transduction from the above lemma
with the transduction that maps a tree $\mathbb{T}$ to all possible colourings
$\mathbb{S}$ that use colors $Q$. The latter transduction is sub-definable
thanks to Lemma 4.8.

####  4.2.3. A criterion for being rank-decreasing.

We finish this section with a criterion for checking if a transduction that
inputs trees is rank-decreasing. In principle, one should check if for every
$k$ there is some $\ell$ such that sets with rank $k$ in the input have rank
$\leq\ell$ in the output. It turns out that if the transduction inputs trees,
then it is enough to check this for some single $k$. Our criterion says that a
transduction that inputs trees is rank-decreasing if and only if the ranks are
bounded for images of sub-forests.

######  Theorem 4.18.

Let $\mathscr{C}$ be a class of structures. A tree-to-$\mathscr{C}$
transduction $\alpha$ is rank-decreasing if and only if the rank is bounded
for

$\displaystyle\\{\ \ (\mathbb{A},X)\ \ |\begin{tabular}[]{l}$X$ is a sub-
forest of some $\mathbb{T}$ with
$(\mathbb{T},\mathbb{A})\in\alpha$\end{tabular}\\}$

###### Proof.

Recall from Lemma 4.7 that the rank in trees of subsets of trees is
asymptotically equivalent to the least $m$ such that the subset can be written
by a boolean combination of $m$ subforests. Furthermore, a Boolean combination
of $n$ sets that have bounded rank will have rank bounded by a function of
$n$, thanks to Lemmas 3.10 and 3.4. ∎

###  4.3. Transductions that input graphs of bounded treewidth

In this section, we complete the proof of Theorem 2.11, by generalizing the
results from the previous sections to transductions that input graphs of
bounded treewidth.

For completeness, we recall the definition of treewidth. This is not really
necessary for the present paper, since we use treewidth as a black box, by
citing a result about definable tree decompositions from
(bojanczykDefinabilityEqualsRecognizability2016a, ). Let $G$ be a graph. A
_tree decomposition_ of $G$ is a tree, where the leaves are vertices of $G$.
The _adhesion_ of a subtree $X$ in the tree decomposition is defined to be the
vertices that are not $X$, but share an edge with some vertex in $X$. The
width of a tree decomposition is the maximal size of an adhesion. The
_treewidth_ of a graph is the minimal width of tree decompositions.

The key technical tool here, apart from the results developed so far, is the
existence of definable tree decompositions for graphs of bounded treewidth
(bojanczykDefinabilityEqualsRecognizability2016a, ). We state this result in a
form that is more appropriate for this paper. In the following theorem, we say
that a transduction is _sub-definable in both directions_ if both the
transduction and its converse are sub-definable.

######  Theorem 4.19.

(bojanczykDefinabilityEqualsRecognizability2016a, ) Let $\mathscr{C}$ be a
class of graphs that has bounded treewidth. Then there is a $\mathscr{C}$-to-
tree transduction that is sub-definable in both directions.

###### Proof.

We do not reprove this theorem, but only explain how the original result can
be rephrased in the way stated here. The main technical result of
(bojanczykDefinabilityEqualsRecognizability2016a, ) can be stated as follows:

  * (*)

for every $k$ there is some $\ell$ and a transduction which inputs a graph of
treewidth at most $k$, and outputs the same graph together a tree
decomposition of width at most $\ell$.

The statement (*) is implicit in
(bojanczykDefinabilityEqualsRecognizability2016a, , Theorem 2.4), and it is
explicit in the survey (bojanczyk_recobook, , Theorem 6.22). The transduction
(*) is the transduction from the statement of the theorem, in the
$\mathscr{C}$-to-tree direction.

Let us now argue that the converse of the transduction described in (*) is
sub-definable. This is a transduction that inputs trees, and therefore it is
enough by Theorem 4.10 to show that it is rank-decreasing. Here, we can apply
the criterion from Theorem 4.18: for every sub-forest in a tree decomposition,
the corresponding subset in the graph has bounded rank. This is easily seen to
be true for tree decompositions of bounded width. ∎

Using the above theorem, we complete the proof of Theorem 2.11. Consider some
rank-decreasing graph-to-graph transduction $\alpha$ that inputs graphs of
treewidth at most $k$. Apply Theorem 4.19, yielding a graph-to-tree
transduction $\beta$ whose inputs contain all inputs of $\alpha$, and such
that both $\beta$ and its converse $\bar{\beta}$ are sub-definable. Consider
the following diagram:

graphstreesgraphs$\scriptstyle{\beta}$$\scriptstyle{\alpha}$$\scriptstyle{\bar{\beta};\alpha}$

Since $\beta;\bar{\beta}$ contains the identity relation on inputs of
$\alpha$, it follows that $\alpha$ is contained in $\beta;\bar{\beta};\alpha$.
Both $\beta$ and $\bar{\beta}$ are sub-definable. Therefore, $\bar{\beta}$ is
rank-decreasing by Corollary 3.6, and thus the composition
$\bar{\beta};\alpha$ is rank-decreasing. Since $\bar{\beta};\alpha$ inputs
trees, it is sub-definable by Theorem 4.10. Thus, $\beta;\bar{\beta};\alpha$
is sub-definable, and so is $\alpha$ as its subset. This completes the proof
of Theorem 2.11.

Observe that our proof did not need to assume that the transduction outputs
graphs, and it would also work for transductions that output structures from
any class.

##  5\. Some conjectures

In this section, we state some conjectures about how our main theorem could be
extended beyond graphs of bounded treewidth. The conjectures in this section
are closely related to conjectures that were posed in
(DBLP:journals/corr/abs-2305-18039, ).

In the proof of our main theorem, the main external ingredient was Theorem
4.19, about the existence of a graph-to-tree transduction which is sub-
definable in both directions, and whose inputs contain all graphs with a given
treewidth bound. We conjecture that a similar result holds not just for
treewidth, but also for rankwidth (and also for structures beyond graphs, i.e.
for classes of structures that can use relations of arity more than two). We
begin by recalling the notion of rankwidth. This is defined in the same way as
treewidth, except that we use the rank function to measure the complexity of
subtrees in a tree decomposition.

######  Definition 5.1 (Rankwidth).

A _tree decomposition_ of a structure $\mathbb{A}$ is a tree where the leaves
are the elements of the structure. The _width_ of this tree decomposition is
the maximal rank of its subtrees. The _rankwidth_ of a structure is the
minimal width among its tree decompositions.

The following conjecture is essentially the same as Conjecture 5.4 in
(DBLP:journals/corr/abs-2305-18039, ).

######  Conjecture 5.2 (Main conjecture).

Let $\mathscr{C}$ be a class of structures of bounded rankwidth. Then there is
a surjective tree-to-$\mathscr{C}$ transduction that is sub-definable in both
directions.

As discussed in Section 4.3, this conjecture is true for classes of graphs of
bounded treewidth. Another case where the conjecture is true is graphs of
linear rankwidth. This is the special case of rankwidth, where we require the
trees to be linear orders (a linear order can be seen as a tree, where the
subtrees are the prefixes). A corollary of (linearcliquewidth2021, , Theorem
3.3) is that the main conjecture holds for every class of graphs of bounded
linear rankwidth. Therefore, the consequences of the main conjecture will hold
for classes of graphs of bounded linear rankwidth.

Even in the linear case, however, much remains open: we do not know if the
main conjecture is true for classes of structures that have linear rankwidth,
but use a vocabulary with ternary relations (see
(DBLP:journals/corr/abs-2305-18039, , Example 9) for some evidence on why
ternary relations could be harder than binary ones). We return to bounded
linear rankwidth in Appendix B.

Below we discuss some consequences of the conjecture.

#### Rank-decreasing equivalent to sub-definable.

The first consequence is the one that was stated at the beginning of this
section: generalizing our main result, Theorem 2.11, to bounded rankwidth.
Using the same proof as in Section 4.3, the main conjecture would entail that
for transductions that input structures of bounded rankwidth, being rank-
decreasing is the same as being sub-definable.

######  Conjecture 5.3 (Implied by main conjecture).

Consider a transduction whose inputs have bounded rankwidth. Then this
transduction is rank-decreasing if and only if it is sub-definable.

As explained in Example 2.7, some assumptions on the input class are necessary
for the conjecture. Although we have not investigated this enough to make
conjectures, it could be the case that the assumption on bounded rankwidth is
tight: maybe for every class $\mathscr{C}$ of unbounded rankwidth there is a
$\mathscr{C}$-to-$\mathscr{C}$ transduction that is rank-decreasing but not
sub-definable.

#### Recognisable languages.

One of the main themes of logic in computer science is the relation between
recognisability (by automata, or algebras) and definability (in monadic
second-order logic or its variants). A recent proposal on this topic was
presented in (DBLP:journals/corr/abs-2305-18039, , Section 5), which proposed
a generic definition of recognisability of a language $L$ contained in a class
of structures $\mathscr{C}$. This proposed notion of recognisability coincides
with all known pre-existing notions of recognisability for specific classes of
structures (DBLP:journals/corr/abs-2305-18039, , Figure 1). We do not recall
this notion here, but only the basic results about it:

  1. (1)

definability always implies recognisability (here and below, definability
refers to definability in cmso);

  2. (2)

if the class $\mathscr{C}$ has unbounded rankwidth, then recognisability is
not equivalent to definability;

  3. (3)

(conjectured) if the class $\mathscr{C}$ has bounded rankwidth, then
recognisability is equivalent to definability.

The third item would be true, assuming a conjecture implied by the main
conjecture of this paper. Putting the above observation together, we get the
following

######  Conjecture 5.4 (Implied by main conjecture).

A class $\mathscr{C}$ of structures has bounded rankwidth if and only if

$\displaystyle\forall L\subseteq\mathscr{C}\quad\text{$L$ is
recognisable}\Leftrightarrow\text{$L$ is definable.}$

#### Two sub-goals.

Given the importance of the main conjecture, it is worthwhile to split it into
sub-conjectures. Here is one possible split. In the following, a transduction
is called _rank-invariant_ if it is rank-decreasing in both directions. In
other words, the rank of a subset is asymptotically the same in the input and
output structures.

######  Conjecture 5.5 (Equivalent statement of main conjecture, see Fact 5.6
below).

Let $\mathscr{C}$ be a class of structures.

  1. (1)

if $\mathscr{C}$ has bounded rankwidth, then there is a surjective rank-
invariant tree-to-$\mathscr{C}$ transduction; and

  2. (2)

if a $\mathscr{C}$-to-tree transduction is rank-invariant, then it is sub-
definable.

The assumption that $\mathscr{C}$ has bounded rankwidth is not stated in item
2 above, but it is implicit: if a transduction with tree outputs is rank-
invariant, then its inputs have bounded rankwidth (courcelle1995logical, ). In
Appendix B we prove a special case of item 2, which corresponds to bounded
linear rankwidth.

######  Fact 5.6.

Conjectures 5.2 and 5.5 are equivalent.

###### Proof.

Let us first show how the two items in Conjecture 5.5 imply Conjecture 5.2.
Let $\beta$ be the rank-invariant transduction from item 1. By Theorem 4.10
this transduction is sub-definable in the tree-to-$\mathscr{C}$ direction, and
by item 2 it is sub-definable in the $\mathscr{C}$-to-tree direction.

We now show the converse implication. Assume Conjecture 5.2. If a transduction
is sub-definable in both directions, then it is rank-invariant by Corollary
3.6. Therefore, the main conjecture gives item 1 in Conjecture 5.5. Let us now
prove item 2. Let $\beta$ be the tree-to-$\mathscr{C}$ transduction from
Conjecture 5.2 that is sub-definable in both directions, and let $\alpha$ be a
rank-invariant $\mathscr{C}$-to-tree transduction. We want to show that
$\alpha$ is sub-definable. Consider the following diagram:

${\mathscr{C}}$treestrees$\scriptstyle{\alpha}$$\scriptstyle{\beta}$$\scriptstyle{\beta;\alpha}$

Since $\beta$ is sub-definable, it is rank-invariant, and therefore
$\beta;\alpha$ is rank-invariant. Since $\beta;\alpha$ inputs trees, it must
be sub-definable by Theorem 4.10. Finally, $\bar{\beta};\beta;\alpha$ is sub-
definable as a composition of the sub-definable transductions $\bar{\beta}$
and $\beta;\alpha$. The transduction $\alpha$ is a subset of this
transduction, since $\bar{\beta};\beta$ contains the identity on
$\mathscr{C}$, and therefore $\alpha$ is sub-definable. ∎

## References

  * [1] Stefan Arnborg, Jens Lagergren, and Detlef Seese.  Easy problems for tree-decomposable graphs.  Journal of Algorithms, 12(2):308–340, 1991.
  * [2] Mikołaj Bojańczyk.  Transducers with Origin Information.  In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 26–37. Springer, 2014\.
  * [3] Mikołaj Bojańczyk.  Languages recognized by finite semigroups, and their generalizations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic.  https://www.mimuw.edu.pl/~bojan/papers/algebra-26-aug-2020.pdf, 2020\.
  * [4] Mikołaj Bojańczyk.  The category of MSO transductions.  CoRR, abs/2305.18039, 2023.
  * [5] Mikołaj Bojańczyk, Martin Grohe, and Michał Pilipczuk.  Definable decompositions for graphs of bounded linear cliquewidth.  Logical Methods in Computer Science, Volume 17, Issue 1, January 2021.
  * [6] Mikołaj Bojańczyk and Michal Pilipczuk.  Definability equals recognizability for graphs of bounded treewidth.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 407–416. ACM, 2016.
  * [7] J. Richard Büchi.  Weak second-order arithmetic and finite automata.  Z. Math. Logik und Grundl. Math., 6:66–92, 1960.
  * [8] J. Richard Büchi.  On a decision method in restricted second order arithmetic.  In Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr .), pages 1–11. Stanford Univ. Press, Stanford, Calif., 1962\.
  * [9] Bruno Courcelle.  The monadic second-order logic of graphs. I. Recognizable sets of finite graphs.  Information and Computation, 85(1):12–75, March 1990.
  * [10] Bruno Courcelle.  The monadic second-order logic of graphs v: on closing the gap between definability and recognizability.  Theoretical Computer Science, 80(2):153 – 202, 1991.
  * [11] Bruno Courcelle and Joost Engelfriet.  A logical characterization of the sets of hypergraphs defined by hyperedge replacement grammars.  Mathematical Systems Theory, 28(6):515–552, 1995.
  * [12] Bruno Courcelle and Joost Engelfriet.  Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of Mathematics and Its Applications.  Cambridge University Press, 2012.
  * [13] Bruno Courcelle and Sang-il Oum.  Vertex-minors, monadic second-order logic, and a conjecture by seese.  Journal of Combinatorial Theory, Series B, 97(1):91–126, 2007.
  * [14] Calvin C. Elgot.  Decision problems of finite automata design and related arithmetics.  Trans. Amer. Math. Soc., 98:21–51, 1961.
  * [15] Joost Engelfriet.  A characterization of context-free nce graph languages by monadic second-order logic on trees.  In Hartmut Ehrig, Hans-Jörg Kreowski, and Grzegorz Rozenberg, editors, Graph Grammars and Their Application to Computer Science, pages 311–327, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg.
  * [16] Martin Grohe and Stephan Kreutzer.  Methods for algorithmic meta theorems.  Model Theoretic Methods in Finite Combinatorics, 558:181–206, 2011\.
  * [17] Sang-il Oum.  Rank-width and vertex-minors.  Journal of Combinatorial Theory, Series B, 95(1):79–100, 2005.
  * [18] Michael O. Rabin.  Decidability of Second-Order Theories and Automata on Infinite Trees.  Transactions of the American Mathematical Society, 141:1–35, 1969\.
  * [19] Detlef Seese.  The structure of the models of decidable monadic theories of graphs.  Annals of pure and applied logic, 53(2):169–195, 1991.
  * [20] Imre Simon.  Factorization forests of finite height.  Theoretical Computer Science, 72(1):65–94, 1990.
  * [21] James W. Thatcher and Jesse B. Wright.  Generalized finite automata theory with an application to a decision problem of second-order logic.  Mathematical systems theory, 2(1):57–81, 1968.
  * [22] Wolfgang Thomas.  Languages, automata, and logic.  In Handbook of formal languages, Vol. 3, pages 389–455. Springer, Berlin, 1997.
  * [23] Boris A. Trakhtenbrot.  The synthesis of logical nets whose operators are described in terms of one-place predicate calculus (russian).  Dokl. Akad. Nauk SSSR, 118(4):646–649, 1958.

##  Appendix A Ranks of bounded quantifier depth

We now prove Theorem 3.5. In the proof, it will be more convenient to use a
variant of logic and the type matrix uses only set variables and does not use
first-order variables. We begin by describing this variant.

Define a _monadic second-order structure_ to be a structure where all
relations take only set arguments. This means that a relation of arity $m$
describes an $m$-ary relation on subsets of the universe. (An example is a
hypergraph, in which the edge relation is a family of subsets of the universe,
or a matroid, which is a hypergraph subject to certain axioms. These two
examples have only unary relations on sets, but it turns out that relations of
higher arity do not make a big difference, see [4, Example 9].) For the
purposes of the proof of Theorem 3.5, we use the name _first-order structure_
for the usual kind of structures, where relations take only element arguments,
to distinguish them from monadic second-order structures. Every first-order
structure $\mathbb{A}$ can be converted into a monadic second-order structure,
called its _singleton lifting_ , as follows: replace every relation $R$ with a
relation of same arity (but taking set arguments) that is interpreted as

$\displaystyle\\{\ \ (\\{a_{1}\\},\ldots,\\{a_{n}\\})\ \
|\begin{tabular}[]{l}$\mathbb{A}\models
R(a_{1},\ldots,a_{n})$\end{tabular}\\}.$

The notion of types is extended to monadic second-order structures in the
usual way, by associating to a tuple of $m$ subsets in a given structure the
set of all mso formulas with $m$ free set-variables, of given quantifier
depth, that hold for this tuple. The following observation shows that a
structure is essentially the same as its singleton lifting.

######  Fact A.1.

For every quantifier depth $d$ and number of arguments $m$, the following
types are in one-to-one correspondence:

  1. (1)

$d$-type of a first-order structure $\mathbb{A}$ with distinguished elements
$a_{1},\ldots,a_{m}$;

  2. (2)

$d$-type of the singleton lifting of $\mathbb{A}$ with distinguished subsets
$\\{a_{1}\\},\ldots,\\{a_{m}\\}$.

The matrices defining the rank are adapted to monadic second-order structures
in the obvious way, defined as follows. Consider a monadic second-order
structure $\mathbb{A}$, a subset $X$ of its universe, a quantifier depth $d$
and a number of arguments $m$. Define the following matrix, which we call the
$d$-type matrix of arity $m$, for the subset $X$ in the structure
$\mathbb{A}$:

  1. (1)

rows are $m$-tuples $(X_{1},\ldots,X_{m})$ of subsets of $X$;

  2. (2)

columns are $m$-tuples $(Y_{1},\ldots,Y_{m})$ of subsets of
$\mathbb{A}\setminus X$;

  3. (3)

the value of the matrix in a row $(X_{1},\ldots,X_{m})$ and column
$(Y_{1},\ldots,Y_{m})$ is the monadic $d$-type of the tuple $X_{1}\cup
Y_{1},\ldots,X_{m}\cup Y_{m}$ in $\mathbb{A}$.

We denote this matrix by $M_{d,n}$, assuming that the structure $\mathbb{A}$
and subset $X$ are implicit from the context. The following lemma rephrases
Theorem 3.5 in terms of monadic second-order structures.

######  Lemma A.2.

Fix a class of monadic second-order structures, where $m$ is the maximal arity
of relations. For every quantifier depth $d\in\\{0,1,\ldots\\}$, the following
rank functions, each of which inputs a structure $\mathbb{A}$ with a
distinguished subset of elements $X$, are asymptotically equivalent:

  1. (1)

number of distinct rows in the matrix $M_{0,m}$;

  2. (2)

number of distinct rows in the matrix $M_{0,d+m}$;

  3. (3)

number of distinct rows in the matrix $M_{d,m}$.

By Fact A.1, the equivalence between items 1 and 3 in Lemma A.2 implies
Theorem 3.5. Therefore, it remains to prove the lemma.

We begin with the equivalence of the first two items.

######  Lemma A.3.

The rank functions in items 1 and 2 of Lemma A.2 are asymptotically
equivalent.

###### Proof.

Since $m$ is the maximal arity of relations in the vocabulary, a quantifier-
free type is uniquely determined by its projections onto $m$-tuples of
variables. ∎

We are left with showing the equivalence of the rank function in item 3 of
Lemma A.2. Clearly the matrix $M_{d,m}$ corresponding to item 3 stores more
information than the matrix $M_{0,m}$ corresponding to item 1, and therefore
the corresponding rank function can only be bigger. The following lemma shows
that it cannot be uncontrollably bigger, because it is bounded by a function
of the rank of the matrix $M_{0,d+m}$ corresponding to item 2.

######  Lemma A.4.

For every monadic second-order structure $\mathbb{A}$, every subset $X$ of its
universe, and every $d,m\in\\{0,1,\ldots\\}$, the number of distinct rows in
the matrix $M_{d+1,m}$ is at most

$\displaystyle 2^{\text{number of distinct rows in the matrix $M_{d,m+1}$}}.$

By applying this lemma $d$ times, we get the equivalence of items 2 and 3,
although the bound uses a tower of $d$ exponentials. (This is not particularly
surprising, since a tower of exponentials is the usual dependency of the
number of types on the quantifier depth.) Therefore, the lemma concludes the
proof of Theorem 3.5, and it only remains to prove it.

###### Proof of Lemma A.4.

This is a symbol-pushing proof. We begin by introducing some notation and
assigning types to the objects that will be used.

In the lemma, we are counting _distinct_ rows in a matrix, so we use the
following notation: a _row index_ is the name of a row, while a _row content_
is the sequence of values in the row, which is indexed by columns in the
matrix.In the matrix $M_{d+1,m}$, a row index is a choice of subsets
$X_{1},\ldots,X_{m}\subseteq X$, and the corresponding row content, which we
denote by

$\displaystyle M_{d,m}[(X_{1},\ldots,X_{m}),\\_]$

is a function of type

$\displaystyle\underbrace{(\mathsf{P}(\mathbb{A}\setminus
X))^{m}}_{\mathclap{\text{\scriptsize\begin{tabular}[]{c}columns of the
matrix\end{tabular} }}}\to\underbrace{\text{$(d+1)$-types with $m$
variables}}_{\mathclap{\text{\scriptsize\begin{tabular}[]{c}type of values in
the matrix\end{tabular} }}}.$

We want to estimate the number of distinct rows, i.e. the number of possible
row contents, in the matrix $M_{d+1,m}$, based on the corresponding number for
the matrix $M_{d,m+1}$. This is done in the following claim, which immediately
implies the lemma.

######  Claim A.5.

In the matrix $M_{d+1,m}$, the row contents

$\displaystyle M_{d+1,m}[(X_{1},\ldots,X_{m}),\\_]$

are uniquely determined by the following set of row contents

$\displaystyle\\{\ \ M_{d,m+1}[(X_{1},\ldots,X_{m},X_{m+1}),\\_]\ \
|\begin{tabular}[]{l}$X_{m+1}\subseteq X$\end{tabular}\\}.$

###### Proof.

This is a standard Ehrenfeucht-Fraïssé argument. Consider two rows in the
matrix $M_{d+1,m}$

$\displaystyle X_{1},\ldots,X_{m}\subseteq X$ $\displaystyle
X^{\prime}_{1},\ldots,X^{\prime}_{m}\subseteq X$

that agree on the information in the statement of the claim, which means that
the following two sets of row contents are the same

$\displaystyle\\{\ \ M_{d,m+1}[(X_{1},\ldots,X_{m},X_{m+1}),\\_]\ \
|\begin{tabular}[]{l}$X_{m+1}\subseteq X$\end{tabular}\\}$ $\displaystyle\\{\
\ M_{d,m+1}[(X^{\prime}_{1},\ldots,X^{\prime}_{m},X^{\prime}_{m+1}),\\_]\ \
|\begin{tabular}[]{l}$X^{\prime}_{m+1}\subseteq X$\end{tabular}\\}.$

We need to show that the row contents

$\displaystyle M_{d+1,m}[(X_{1},\ldots,X_{m}),\\_]$ $\displaystyle
M_{d+1,m}[(X^{\prime}_{1},\ldots,X^{\prime}_{m}),\\_]$

are equal. By unravelling the definition of the matrix $M_{d+1,m}$, this means
that for every column

$\displaystyle Y_{1},\ldots,Y_{m}\subseteq\mathbb{A}\setminus X,$

player Duplicator can win the $d+1$ round Ehrenfeucht-Fraisse game on the
structure $\mathbb{A}$ with the two sides being

$\displaystyle X_{1}\cup Y_{1},\ldots,X_{m}\cup Y_{m}$ $\displaystyle
X^{\prime}_{1}\cup Y_{1},\ldots,X^{\prime}_{m}\cup Y_{m}.$

Consider a move by player Spoiler in this game. By symmetry, we assume that
Spoiler plays in the first side, and he chooses a subset $X_{m+1}\cup
Y_{m+1}$. By the assumption on the sets of row contents in $M_{d,m+1}$ being
equal, there is some $X^{\prime}_{m}$ such that the following row contents are
equal

$\displaystyle M_{d,m+1}[(X_{1},\ldots,X_{m},X_{m+1}),\\_]$ $\displaystyle
M_{d,m+1}[(X^{\prime}_{1},\ldots,X^{\prime}_{m},X^{\prime}_{m+1}),\\_].$

This implies that the matrix $M_{d,m+1}$ has the same values in the entries
corresponding to

$\displaystyle X_{1}\cup Y_{1},\ldots,X_{m+1}\cup Y_{m+1}$ $\displaystyle
X^{\prime}_{1}\cup Y_{1},\ldots,X^{\prime}_{m+1}\cup Y_{m+1}$

and therefore player Duplicator can use $X^{\prime}_{m+1}\cup Y_{m+1}$ as her
response to win the game. ∎

This completes the proof of Theorem 3.5. ∎

##  Appendix B Bounded branching

Recall item 2 of Conjecture 5.5, which said that if a $\mathscr{C}$-to-tree
transduction is rank-invariant, then it is sub-definable. In this section, we
prove a special case of the conjecture, which is the most technically advanced
contribution of the paper. This result will work with structures that are not
necessarily graphs, i.e. we allow relations in the vocabulary that have arity
bigger than two, and therefore we cannot use the results from [5].

We begin by observing that the assumption on being rank-invariant cannot be
weakened to rank-decreasing.

###### Example B.1.

Here is a transduction that outputs trees, is rank-invariant, but is not sub-
definable. Consider the transduction which inputs a grid, and outputs all
possible trees over the universe of the input grid. Like every transduction
that inputs grids, this transduction is rank-decreasing. However, it is not
sub-definable, since the number of trees on a universe of size $n$ is bigger
than the number of possible outputs for a sub-definable transduction. This is
the because the former is $2^{\Theta(n\cdot\log n)}$ while the latter is
$2^{\Theta(n)}$.

Define a _minor_ of a tree to be a tree that is obtained by removing some
leaves, and restricting the family of subtrees to the smaller set of leaves.
The _branching_ of a tree is defined to be the largest $k$ such that the tree
contains, as a minor, the complete binary tree of height $k$. We will be
interested in classes of trees of bounded branching. An equivalent description
of bounded branching is that some tree is avoided as a minor (this is because
every tree is a minor of some complete binary tree).

The goal of this section is to prove the following special case of item 2 in
Conjecture 5.5, in which the outputs have bounded branching.

######  Theorem B.2.

Let $\mathscr{C}$ be a class of structures. If a $\mathscr{C}$-to-tree
transduction is rank-invariant, and has outputs of bounded branching, then it
is sub-definable.

Note that the transduction in the above theorem is also sub-definable in the
converse direction, by Theorem 4.10. The rest of this section is devoted to
proving Theorem B.2.

####  B.0.1. Partially ordered trees

In the proof of the above theorem, we will be working with a notion that is
equivalent to trees of bounded branching, namely partially ordered trees of
bounded height. These are trees where some, but not all, nodes are equipped
with a linear order on their children.

######  Definition B.3 (Partially ordered trees).

A _partially ordered tree_ is a tree together with the following extra
structure:

  1. (1)

a partition of the nodes into two kinds: ordered and unordered nodes;

  2. (2)

for each ordered node, a linear order on its children.

To represent partially ordered trees as logical structures, we rely on the
following notion. Define the _document order_ of a partially ordered tree to
be the following preorder on leaves: $x\leq y$ if either $x=y$, or otherwise
the closest common ancestor of $x$ and $y$ is an ordered node, and the child
containing $x$ is to the left of the child containing $y$. If the closest
common ancestor of the two leaves is an unordered node, then they are
incomparable in the document order. In particular, if a tree has only
unordered nodes, then every two nodes are incomparable. It is not hard to see
that a partially ordered tree is uniquely specified by the family of nodes and
its document order.

The following lemma shows that partially ordered trees of bounded height are
the same as trees of bounded branching.

######  Lemma B.4.

For every $k$ there is a transduction between:

  1. (1)

trees of branching $\leq k$; and

  2. (2)

partially ordered trees of height $\leq 2k$,

which is bijective and definable in both directions.

Thanks to Lemma B.4, an equivalent statement of Theorem B.2 is: if a
transduction that outputs partially ordered trees of bounded height is rank-
invariant, then it is sub-definable. We will prove this induction on the
height of the output trees, and in the induction step, we will show that the
local tree structure is sub-definable.

####  B.0.2. Local tree structure

We begin by formalising the concept of local tree structure in a partially
ordered tree.

######  Definition B.5.

Let $X$ be a node in a partially ordered tree.

  1. (1)

Define the _child partition_ to be the equivalence relation on $X$ which
identifies two elements if they are in the same child.

  2. (2)

Assume that $X$ is an ordered node. Define the _child preorder_ to be the
linear preorder on $X$ which is obtained by ordering the equivalence classes
of the child partition according to the order on children of $X$.

The child preorder is represented as a linear preorder, i.e. a relation that
is reflexive, transitive, and total (i.e. every two elements are related in at
least one direction). The following lemma will be used several times in this
section to show sub-definability for transductions that output partially
ordered trees.

######  Lemma B.6.

Let $\alpha$ be a transduction that outputs partially ordered trees of bounded
height. A sufficient condition for $\alpha$ being sub-definable is that the
following two transductions are sub-definable:

$\displaystyle\underbrace{\\{\ \ (\mathbb{A}|X,\sim)\ \
|\begin{tabular}[]{l}$X$ is an unordered node for some
$\mathbb{T}\in\alpha(\mathbb{A})$\\\ and $\sim$ is the corresponding child
partition\end{tabular}\\}}_{\mathclap{\text{\scriptsize\begin{tabular}[]{c}this
transduction is called the local unordered transduction of
$\alpha$\end{tabular} }}}$ $\displaystyle\underbrace{\\{\ \
(\mathbb{A}|X,\leq)\ \ |\begin{tabular}[]{l}$X$ is an ordered node for some
$\mathbb{T}\in\alpha(\mathbb{A})$\\\ and $\leq$ is the corresponding child
preorder\end{tabular}\\}}_{\mathclap{\text{\scriptsize\begin{tabular}[]{c}this
transduction is called the local unordered transduction of
$\alpha$\end{tabular} }}}.$

###### Proof.

Induction on the maximal height of the output trees. Define $\beta$ to be the
transduction

$\displaystyle\\{\ \ (\mathbb{A}|X,\mathbb{T}|X)\ \
|\begin{tabular}[]{l}$(\mathbb{A},\mathbb{T})\in\alpha$ and $X$ is a child
subtree in $\mathbb{T}$\end{tabular}\\}.$

To this transduction, we can apply the induction assumption, and therefore it
is sub-definable. The original transduction is then obtained from by combining
$\beta$ with the local transduction, in the special case where $X$ is the root
of the tree. ∎

In Sections B.1 and B.2 below, we will show that for every rank-invariant
transduction that outputs partially ordered trees, the two local transductions
from the above lemma are sub-definable. This will imply that if, furthermore,
the output trees have bounded height, then the transduction is sub-definable.
This will, in turn, imply Theorem B.2, due to the isomorphism between
partially ordered trees of bounded height and trees of bounded branching that
was stated in Lemma B.4.

###  B.1. Unordered local transduction

The goal of this section is to prove the following lemma.

######  Lemma B.7.

For every rank-invariant transduction that outputs partially ordered trees,
its local unordered transduction is sub-definable.

The rest of Section B.1 is devoted to proving the above lemma. The assumption
on rank-invariance cannot be relaxed to being rank-decreasing, for the same
reasons as in Example B.1. The proof of the lemma proceeds in two steps.
First, we show that the local unordered transduction satisfies a certain
technical condition, and then we show that every transduction with this
condition is sub-definable.

####  B.1.1. Unordered approximation

In this section, we define and prove the technical condition that will later
be used to prove sub-definability.

The general idea is that we can approximate the output equivalence relation
using logic in the input structure. What do we mean by approximating an
equivalence relation? Recall Example 3.9, in which we showed that in a
structure which is an equivalence relation, the rank of a subset is
approximately the same as the number of equivalence classes that are cut by
the subset. In the following lemma, we will show that we can define in logic
for every subset an approximation of the number of equivalence classes that
are cut by this subset. The lemma also contains an additional recognisability
condition; as far as we know the remainder of the proof could be improved so
that the recognisability condition is not needed.

######  Lemma B.8.

Let $\alpha$ be a rank-invariant transduction that outputs partially ordered
trees, and let $\beta$ be its local unordered transduction. Then $\beta$
satisfies the following condition, which we call _unordered approximation_.
There is a cmso formula $\varphi$ over the input vocabulary, a finite
commutative semigroup $S$ and some $k\in\\{1,2,\ldots\\}$ such that every pair
$(\mathbb{A},\sim)\in\beta$ satisfies all the following conditions:

  1. (1)

_Completeness._ If a subset of $\mathbb{A}$ cuts no equivalence classes, then
it satisfies $\varphi$;

  2. (2)

_Approximate soundness._ If a subset of $\mathbb{A}$ cuts at least $k$
equivalence classes, then it does not satisfy $\varphi$;

  3. (3)

_Recognisability._ Let $X_{1},\ldots,X_{n}$ be the equivalence class of
$\sim$. There is a function666In the type of the function $\lambda$ we use
disjoint union, since the empty subset appears in each of the powersets
$\mathsf{P}X_{1},\ldots,\mathsf{P}X_{n}$, and we want $\lambda$ to be able to
assign different values to the different instances of the empty subset.

$\displaystyle\lambda:\mathsf{P}X_{1}\uplus\cdots\uplus\mathsf{P}X_{n}\to S$

with the following property. Let $Y\subseteq\mathbb{A}$, and let
$s_{1},\ldots,s_{n}$ be the semigroup elements where $s_{i}$ is obtained by
applying $\lambda$ to the set $Y\cap X_{i}$. Then the product $s_{1}\cdots
s_{n}$ in the semigroup uniquely determines if the set $Y$ satisfies
$\varphi$. Observe that since the semigroup is commutative, the order of
arguments in the product is not important.

  4. (4)

The value of $\lambda$ determines if a subset is full or empty.

###### Proof.

Consider a pair $(\mathbb{A},\mathbb{T})\in\alpha$, and an unordered node $X$
in the tree $\mathbb{T}$. If a set $Y\subseteq X$ does not cut any children of
$X$, then its rank in $\mathbb{T}$ is bounded. This, together with the
assumption that $\alpha$ is rank-invariant, yields some constant
$\ell\in\\{1,2,\ldots\\}$, such that

  1. (a)

for every $(\mathbb{A},\mathbb{T})\in\alpha$, every unordered node $X$ of
$\mathbb{T}$ and every $Y\subseteq X$, if $Y$ does not cut any children of
$X$, then the rank of $Y$ in $\mathbb{A}|X$ is at most $\ell$ (Lemma 4.13).

Using again the assumption that the transduction $\alpha$ is rank-invariant,
we know that sets $Y\subseteq X$ which have rank at most $\ell$ in
$\mathbb{A}|X$ will have bounded rank in $\mathbb{T}|X$. A set of bounded rank
in a partially ordered tree can cut a bounded number of children of any given
node, and therefore there is some constant $k$ such that

  1. (b)

for every $(\mathbb{A},\mathbb{T})\in\alpha$, every unordered node $X$ of
$\mathbb{T}$ and every $Y\subseteq X$, if $Y$ has rank at most $\ell$ in
$\mathbb{A}|X$ then it cuts at most $k$ children of $X$.

Define $\varphi(Y)$ to be the formula which says that the set $Y$ has rank at
most $\ell$ in the structure $\mathbb{A}|X$. This is indeed a formula of mso,
even without counting, since an mso formula can count distinct rows in a type
matrix up to a given threshold. Conditions (a) and (b) give the completeness
and approximate soundness conditions from the lemma.

It remains to prove the recognisability condition in the lemma. Since the
transduction $\alpha$ is rank-invariant, it follows that its converse is rank-
decreasing. Since the converse inputs trees, it is sub-definable by Theorem
4.10. By pulling back the formula $\varphi$ along the converse, there is a
cmso formula

$\displaystyle\psi(Y,Z_{1},\ldots,Z_{n})$

over the vocabulary of partially ordered trees, such that for every pair
$(\mathbb{A},\mathbb{T})\in\alpha$ there is some choice of parameters
$Z_{1},\ldots,Z_{n}\subseteq\mathbb{T}$ such that

$\displaystyle\mathbb{A}\models\varphi(Y)\quad\text{iff}\quad\mathbb{T}\models\psi(Y,Z_{1},\ldots,Z_{n})$

holds for all subsets $Y\subseteq\mathbb{A}$. Let $d$ be the quantifier depth
of the formula $\psi$. By compositionality of mso on trees, we know that if
$X$ is a node of the tree $\mathbb{T}$ and $Y\subseteq X$, then whether the
right-hand side of the above equivalence holds depends only on the values

(2) $\displaystyle\text{$d$-type of $Y$ in
$(\mathbb{T},Z_{1},\ldots,Z_{n})|X_{i}$},$

where $X_{i}$ ranges over children of $X$. Furthermore, the dependence is
commutative, i.e. it is mediated by a homomorphism into a finite commutative
semigroup, namely the semigroup of $d$-types with respect to disjoint unions
of structures. This yields the commutative semigroup $S$ from the homogeneity
condition in the lemma, with the colouring $\lambda$ mapping a subset
$Y\subseteq X_{i}$ to the $d$-type from (2). ∎

####  B.1.2. Sub-definability using unordered approximation

We now show that the unordered approximation condition, as defined in Lemma
B.8, implies sub-definability. In the proof, we use a stronger version of this
condition, defined as follows. We say that a transduction has the _homogeneous
unordered approximation property_ if it satisfies the unordered approximation
property (see Lemma B.8), together with the following extra condition:

  1. (4)

Homogeneity. All the images are equal:

$\displaystyle\lambda(\mathsf{P}X_{1})=\cdots=\lambda(\mathsf{P}X_{n}).$

The following lemma shows that this stronger property is sufficient for sub-
definability.

######  Lemma B.9.

If a transduction has the homogeneous unordered approximation property, then
it is sub-definable.

###### Proof.

Let $\beta$ be a transduction with the homogeneous unordered approximation
property. Let the semigroup $S$, the threshold $k$ and the formula $\varphi$
be as in this property.

Consider a pair $(\mathbb{A},\sim)\in\beta$, let $X_{1},\ldots,X_{n}$ be the
equivalence classes of $\sim$, and let

$\displaystyle\lambda:\mathsf{P}X_{1}\uplus\cdots\uplus\mathsf{P}X_{n}\to S$

be the function from the unordered approximation property. For each class
$X_{i}$, we will be especially interested in two values produced by the
function $\lambda$: the _empty value_ , which is produced for the empty set
$\emptyset\subseteq X_{i}$ and the _full value_ , which is produced for the
full subset $X_{i}\subseteq X_{i}$.

######  Claim B.10.

Without loss of generality, we can assume that all classes have the same empty
value, all classes have the same full value, and these two values are
idempotent.

###### Proof.

Without loss of generality, we can assume that the colouring $\lambda$ in the
recognisability condition also keeps track of whether a set is full or empty,
which is an idempotent property. (In fact, the proof of Lemma B.8 already
ensures this, since $\lambda$ returns the mso type of sufficiently high
quantifier depth, and such a type will tell us if a set is empty or full, as
long as the quantifier depth is at least one.) From the homogeneity condition,
we know that $\lambda$ has the same image on the powerset of every class, and
hence all full values (respectively, all empty values) must be the same. ∎

We say that a set $Y\subseteq\mathbb{A}$ is a _seed_ if it satisfies all the
following conditions:

  1. (1)

$Y$ satisfies the formula $\varphi$;

  2. (2)

$Y$ is full in at least one equivalence classes;

  3. (3)

$Y$ is empty in at least one equivalence classes.

Note that as long as there are at least two classes, there is a seed: simply
take any set satisfying (2) and (3) that does not cut any class, then it
satisfies (1) by the completeness property.

Choose a seed $Y_{0}$ that cuts a maximal number of equivalence classes. Note
that $Y_{0}$ cuts at most $k$ classes by approximate soundness. Fix an
arbitrary class for which $Y_{0}$ is full, and an arbitrary class for which
$Y_{0}$ is empty, then define a _special equivalence_ class to be either these
two fixed classes, or any class that is cut by $Y_{0}$, as in the following
figure.

The main observation is in the following claim, which shows that the
equivalence classes can be determined by looking at sets that are similar to
the seed $Y_{0}$.

######  Claim B.11.

Assume that there are at least $2$ equivalence classes. Consider two elements
of the universe that are not in any special class. Then they are in different
classes if and only if they can be separated by some seed that agrees with
$Y_{0}$ on the special classes.

###### Proof.

By maximality, if a seed agrees with $Y_{0}$ on the special classes, then it
cannot cut any class that is not special. Therefore, such a seed cannot
separate two elements in the same class.

We now prove the converse implication. As explained above, if a seed agrees
with $Y_{0}$ on the special classes, then it is full or empty on every non-
special class. Since the values of the full and empty set are idempotent, and
the semigroup is commutative, the set which agrees with $Y_{0}$ on the special
classes, is full on the class containing one of the elements, and empty
elsewhere, is a seed separating the two elements. ∎

We are now ready to prove that the transduction is sub-definable. The case
where there is a single class can be explicitly guessed by the transduction.
Otherwise, the transduction can guess the seed and the special equivalence
classes, and then use the condition in the above claim to check which elements
are in the same equivalence class. ∎

####  B.1.3. Ensuring homogeneity

In Lemma B.8, we have shown that the unordered local transduction has the
unordered approximation property, and in Lemma B.9 we have shown that the
stronger homogeneous version of this property is sufficient for sub-
definability. We finish the proof by bridging the gap between these two
properties. The idea is that every transduction with the unordered
approximation property can be refined to ensure the homogeneous version.

This refinement will be relatively straightforward in the present unordered
case, but it will be more involved (using factorisation forests) in the
ordered case. To cover both cases, we present below a general definition of
what we mean by refining a transduction.

######  Definition B.12 (Refinement on trees).

A partial tree $\mathbb{S}$ is called _finer_ than a partial tree $\mathbb{T}$
if

  1. (1)

the two trees have the same universe, i.e. leaves;

  2. (2)

the two trees have the same document preorder;

  3. (3)

every node of $\mathbb{S}$ is also a node of $\mathbb{T}$.

A transduction $\beta$ is _refined by_ a transduction $\gamma$ if both
transductions output partially ordered trees, and for every input structure
$\mathbb{A}$, every output tree in $\beta(\mathbb{A})$ is refined by some
output tree in $\gamma(\mathbb{A})$.

We have now all the definitions in place that are needed to complete the proof
of Lemma B.7.

###### Proof of Lemma B.7.

Let $\beta$ be a transduction as in the assumptions of the lemma, i.e. this is
the local unordered transduction of some rank-invariant transduction that
outputs partially ordered trees. We want to show that $\beta$ is sub-
definable.

By Lemma B.8, $\beta$ has the unordered approximation property. We can view of
$\beta$ as a transduction that outputs trees, since an equivalence relation
can be seen as a special case of a partially ordered tree, which has height
two, as in the following picture:

It is this view that we use when talking about a refinement of an equivalence
relation, or a transduction that outputs equivalence relations.

######  Claim B.13.

Let $\beta$ be a transduction that outputs equivalence relations, and has the
unordered approximation property. There is a transduction $\gamma$ that
refines $\beta$, has outputs of bounded height, and such that the local
unordered transduction of $\gamma$ has the homogeneous unordered approximation
property.

###### Proof.

Group the equivalence classes into a bounded number of groups, with two
classes being together in a group when they have the same image of the
function $\lambda$. This grouping can be seen as tree of height three, in
which the root has a bounded number of children, since the semigroup is fixed.
For every group, its children satisfy the homogeneity condition. ∎

The proof of the above claim is very straightforward. The reason why we phrase
the claim in terms of refinements is that we want to underline the
similarities with the ordered case in the next section, where the analogue of
Claim B.13 will be more advanced.

Consider the transduction $\gamma$ from Claim B.13. This transduction has
outputs of bounded height. Its local unordered transduction is sub-definable
by the claim, and its local ordered transduction is sub-definable for vacuous
reasons: all output trees of $\gamma$ use only unordered nodes, since the same
is true for $\beta$. Therefore, $\gamma$ is sub-definable thanks to Lemma B.6.
Therefore, $\beta$ is also sub-definable, since it can be obtained from
$\gamma$ by forgetting the extra levels with the groups of equivalence
classes. ∎

###  B.2. The ordered local transduction

In this section, we prove the ordered analogue of Lemma B.7, stated below.

######  Lemma B.14.

For every rank-invariant transduction that outputs partially ordered trees,
its local ordered transduction is sub-definable.

The proof follows the same structure as in Section B.1.

####  B.2.1. Ordered approximation

We begin with the first step, in which we show that the local ordered
transduction has a certain approximation property. In the unordered case,
where the outputs were equivalence relations, the approximation property
counted the number of equivalence classes that were cut. In the ordered case,
we will be counting blocks, as explained below.

Consider a linear preorder $\leq$. In the following, a _class_ of this
preorder is defined to be an equivalence class of the accompanying equivalence
relation. An _interval_ in the preorder $\leq$ is defined to be any subset
which has the property that if $x$ and $y$ are in the interval, then the same
is true for any element $z$ with $x\leq z\leq y$. In particular, an interval
cannot cut any class. For a subset $Y$ in a linear preorder, define a _block_
to be an interval that has one of the following three kinds:

  1. (1)

a maximal inclusion-wise interval contained in $Y$;

  2. (2)

a maximal inclusion-wise interval disjoint with $Y$;

  3. (3)

a class that is cut by $Y$.

We will use the name “full block”, “empty block” and “cut block” for the three
kinds, respectively. Here is a picture:

Observe that the blocks partition the equivalence classes induced by the
preorder.

The following lemma, whose straightforward proof is left to the reader, shows
that the number of blocks is approximately equal to the rank of a subset.

######  Lemma B.15.

In the class of linear preorders, the rank of a subset is asymptotically
equivalent to the number of blocks.

We are now ready to state the ordered version of the approximation property.
The proof of the following lemma is the same as in the unordered version.

######  Lemma B.16.

Let $\alpha$ be a rank-invariant transduction that outputs partially ordered
trees, and let $\beta$ be its local ordered transduction. Then $\beta$
satisfies the following condition, which we call _ordered approximation_.
There is a cmso formula $\varphi$ over the input vocabulary, a finite (not
necessarily commutative) semigroup $S$ and some $k\in\\{1,2,\ldots\\}$ such
that every pair $(\mathbb{A},\leq)\in\beta$ satisfies all the following
conditions:

  1. (1)

_Completeness._ If a subset of $\mathbb{A}$ is an interval, then it satisfies
$\varphi$;

  2. (2)

_Approximate soundness._ If a subset of $\mathbb{A}$ has at least $k$ blocks,
then it does not satisfy $\varphi$;

  3. (3)

_Recognisability._ Let $X_{1},\ldots,X_{n}$ be the equivalence classes of
$\leq$, listed according to the order. There is a function

$\displaystyle\lambda:\mathsf{P}X_{1}\uplus\cdots\uplus\mathsf{P}X_{n}\to S$

with the following property. Let $Y\subseteq\mathbb{A}$, and let
$s_{1},\ldots,s_{n}$ be the semigroup elements where $s_{i}$ is obtained by
applying $\lambda$ to the set $Y\cap X_{i}$. Then the product $s_{1}\cdots
s_{n}$ in the semigroup uniquely determines if the set $Y$ satisfies
$\varphi$.

####  B.2.2. Sub-definability using ordered approximation

We now show how the ordered variant of the approximation condition can be used
to prove sub-definability. As in the unordered variant, we define a
homogeneous strengthening of the approximation property.

We say that a transduction which outputs linear preorders has the _homogeneous
ordered approximation property_ if it satisfies the ordered approximation
property (see Lemma B.16), together with the following extra condition:

  1. (4)

Homogeneity. All the images are equal:

$\displaystyle\lambda(\mathsf{P}X_{1})=\cdots=\lambda(\mathsf{P}X_{n}),$

and furthermore the above image is an idempotent in the powerset semigroup
$\mathsf{P}S$.

Later, in Section B.2.3, we will use the Factorisation Forest Theorem to
ensure the above strengthening. The following lemma shows how it can be used
to prove sub-definability.

######  Lemma B.17.

If a transduction has the homogeneous ordered approximation property, then it
is sub-definable.

###### Proof.

Let the formula $\varphi$, the semigroup $S$ and the constant $k$ be as in the
ordered approximation property.

Consider a pair $(\mathbb{A},\leq)$ in the transduction, with the classes
being $X_{1},\ldots,X_{n}$, listed according to the order, and let $\lambda$
be the function from the ordered approximation property. Define the full and
empty values for each class in the same way as in the unordered case. Using
the same argument as in the unordered case, see Claim B.10, we can assume that
all the full values are the same, all the empty values are the same, and these
two values are idempotents.

Similarly to the unordered case, the crucial notion will be that of _seed_.
The ordered version of seed is defined just as before: it is a subset
$Y\subseteq\mathbb{A}$ that satisfies $\varphi$, is full in at least one
class, and is empty in at least one class. If a set is a seed, then it has at
most $k$ blocks, like any set that satisfies $\varphi$, by the approximate
soundness condition.

Define a _long block_ to be a block that has at least two classes. Define a
_maximal seed_ to be one that has a maximal number of blocks that are full or
empty among all seeds.

######  Claim B.18.

Assume that there are at least two classes. One can choose a maximal seed
$Y_{0}$ so that it has exactly two long blocks, one of them full, one of them
empty, and between these two blocks all other blocks are cut blocks, as in the
following picture:

###### Proof.

Blocks that are full or empty can be stretched or compressed without affecting
the image under $\lambda$, thanks to the homogeneity assumption and the fact
that the full and empty values are idempotent. Pick a seed $Y_{0}$ and pick
two blocks, one of them full, one of them empty, such that there are only cut-
blocks between them. Then stretch them until all other full or empty blocks
are reduced to size one. ∎

Consider the seed $Y_{0}$ from the above claim. By symmetry, we assume from
now on that the left block is full, and the right long block is empty. Define
the _special classes_ to be all the following classes: up to and including the
first class in the left long block, and symmetrically, from the last class in
the right long block until the end. Here is a picture:

Since the number of special classes is at most the number of blocks, there is
a bounded number of special classes.

Define a _good seed_ to be one that agrees with $Y_{0}$ on the special
classes. By maximality, a good seed has at most two long blocks, which are
separated by several cut blocks (we call these cut blocks the _island_), as in
the following picture:

Furthermore, the island can be moved around at will, with the two long blocks
stretching to accommodate it, by the assumption on homogeneity. Since the
island has at most $k$ classes, we get the following claim.

######  Claim B.19.

Consider two elements $x$ and $y$ that are in non-special classes, and which
are separated by at least $k$ classes. Then $x<y$ if and only if there is some
good seed $Y$ that contains $x$ but not $y$.

In the claim above, we use the assumption that the two elements are separated
by at least $k$ classes. If we do not know the order, then it is difficult to
check this assumption. To work around this problem, we will work with a
stronger condition, which can be checked by a transduction. This condition
will use modulo counting, as described below. Define the _index_ of an element
of the universe to be the number of its class in the order of equivalence
classes. The index belongs to $\\{1,\ldots,n\\}$, where $n$ is the number of
classes. A sufficient condition for having distance at least $d$ is that the
indices differ by $d$ modulo $2d$. Therefore, a corollary of Claim B.19 is the
following claim.

######  Claim B.20.

Let $d\geq k$. Consider two elements $x$ and $y$ that are in non-special
classes, and whose indices differ by $d$ modulo $2d$. Then $x<y$ if and only
if there is some good seed $Y$ that contains $x$ but not $y$.

In Claims B.18–B.20 we were working with a fixed pair $(\mathbb{A},\leq)$, and
the notions of seed, special class, good seed, and colour were relative to
that pair. We now put together the observations so far, with the pair
$(\mathbb{A},\leq)$ no longer being fixed, to show that the relation from the
previous claim can be produced as outputs by a sub-definable transduction.

######  Claim B.21.

Let $d\geq k$. There is a sub-definable transduction $\gamma$, such that for
every $(\mathbb{A},\leq)\in\beta$, one of the outputs in $\gamma(\mathbb{A})$
is the binary relation

$\displaystyle\\{\ \ (x,y)\in\mathbb{A}^{2}\ \ |\begin{tabular}[]{l}$x<y$ and
the indices differ by $d$ modulo $2d$\end{tabular}\\}.$

###### Proof.

The seed $Y_{0}$ and the special classes can be guessed by the transduction.
The remaining notions are definable in mso. ∎

From the relation in the output of the above transduction, we can recover the
$d$-fold successor relation defined by

$\displaystyle\text{index of $x$}+d=\text{index of $y$}.$

This is because $y$ is the $d$-fold successor of $x$ if and only if the pair
$(x,y)$ belongs to the relation produced in Claim B.21, and there is no $z$
such that both $(x,z)$ and $(z,y)$ are in this relation. Once we have the
$d$-fold successor and $(d+1)$-fold successor, we can get the $1$-fold
successor, i.e. the usual notion of successor. From the successor, we get the
order by transitivity, thus finishing the proof of the lemma. ∎

####  B.2.3. Ensuring homogeneity

We now complete the proof of Lemma B.14, by bridging the gap between the
ordered approximation property in the conclusion of Lemma B.16 and the
homogeneous variant in the assumption of Lemma B.17. The proof is the same as
in Section B.1.3, except that the refinement step is more involved. (A linear
preorder is seen as a partially ordered tree of height two, in the same way as
for equivalence relations, except that the root is ordered.) We only state the
refinement step, which is given in Claim B.22, and which is the ordered
version of Claim B.13.

######  Claim B.22.

Let $\beta$ be a transduction that outputs linear preorders, and has the
unordered approximation property. There is a transduction $\gamma$ that
refines $\beta$, has outputs of bounded height, and such that the local
ordered transduction of $\gamma$ has the homogeneous ordered approximation
property.

###### Proof.

An application of the Factorisation Forest Theorem of Imre Simon [20, Theorem
6.1]. ∎