# Uniformisation of Regular Relations in First-Order Logic with Two Variables

Nathan Lhote, Vincent Michielini, Michal Skrzypczak

► To cite this version:

Nathan Lhote, Vincent Michielini, Michal Skrzypczak. Uniformisation of Regular Relations in First-Order Logic with Two Variables. LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallinn, Estonia. pp.1-13, 10.1145/3661814.3662114. hal-05406575

HAL Id: hal-05406575

https://hal.science/hal-05406575v1

Submitted on 10 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Uniformisation of Regular Relations
in First-Order Logic with Two Variables

Nathan Lhote*

nathan.lhote@lis-lab.fr

Laboratoire d'Informatique et
Systèmes,

Aix-Marseille Université

Marseille, France

Vincent Michielini†

vincent.michielini@mimuw.edu.pl

Institute of Informatics,
University of Warsaw

Warsaw, Poland

Michał Skrzypczak‡

mskrzypczak@mimuw.edu.pl

Institute of Informatics,
University of Warsaw

Warsaw, Poland

## ABSTRACT

A uniformisation of a binary relation is a functional relation contained in it, with the same domain. The uniformisation problem asks whether such a uniformisation can be defined in a given formalism.

We solve this problem in the context of regular relations over finite words, for the fragment $FO^2[<]$ of First-Order Logic with two variables: we provide an algorithm that decides if a given regular relation over finite words admits a uniformisation definable in $FO^2[<]$.

The paper provides a new representation of languages definable in $FO^2[<]$, which can be used for the decidability of other problems involving this formalism, e.g. the problem of separability of two regular languages by a language definable in $FO^2[<]$.

## CCS CONCEPTS

* Theory of computation → Automata over infinite objects; Logic and verification; Formalisms.

## KEYWORDS

Uniformisation Question, Two-Variable Fragment, Synthesis

**ACM Reference Format:**

Nathan Lhote, Vincent Michielini, and Michał Skrzypczak. 2024. Uniformisation of Regular Relations in First-Order Logic with Two Variables. In *39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24)*, July 8–11, 2024, Tallinn, Estonia. ACM, New York, NY, USA, 13 pages. https://doi.org/10.1145/3661814.3662114

# 1 INTRODUCTION

## 1.1 MSO and uniformisation problems

The importance of the class of regular languages in Computer Science can be explained by both its robustness and its expressiveness. Among the variety of equivalent definitions, regular languages

can be characterised as those that are definable in Monadic Second-Order Logic (MSO). This characterisation can be considered over various structures, such as finite words, infinite words (also called $\omega$-words), finite and infinite trees, etc.

A particularly important result about regular languages is Rabin's tree theorem [12, Theorem 1.1], stating that the MSO theory of the infinite binary tree is decidable. This theorem is the core of a large variety of other decidability results.

The pivoting idea behind Rabin's tree theorem is to reduce satisfiability of MSO to non-emptiness of a certain model of automata. This whole construction can be seen as a variant of quantifier elimination for MSO. From this perspective, it is natural to ask to what extent one can define the involved Skolem functions within MSO. Rabin expressed a variant of this question as "Rabin's Uniformisation Problem", as explained below.

A uniformisation of a binary relation $R \subseteq X \times Y$ is a partial function from $X$ to $Y$ assigning to every $x$ from the domain of $R$ a single $y \in Y$ such that the pair $(x, y)$ belongs to $R$. More intuitively, a uniformisation selects a function from a relation. Rabin's Uniformisation Problem asks if every relation definable over MSO over infinite trees admits uniformisation definable in MSO as well. The problem was answered in the negative by Gurevich and Shelah [8, Corollary 2] using the method of forcing. Later, an automata-based construction was also given [3, Theorem 1], [4, Theorem 3.1].

At the same time, it is known that for simpler structures, like finite words, $\omega$-words, or finite trees, the answer to the uniformisation problem is positive: every relation definable in MSO admits a uniformisation definable in MSO [13, 16]. This naturally leads to the question whether the same holds for weaker formalisms. The question was studied in [9] for fragments of First-Order Logic (FO) over finite words. The cited paper provides examples showing that all of the natural fragments of FO are too weak to uniformise all of their own relations.

Still, certain relations admit uniformisations in the considered weaker formalisms. This raises the following problem:

**PROBLEM 1.1.** For a fixed fragment of MSO (or FO in our case), provide an effective algorithm deciding if a given regular relation $R$ admits a uniformisation definable in the fragment.

Since definability of a uniformisation does not imply definability of the relation, the input to the above problem can be an arbitrary relation definable in MSO, not only one definable in the considered formalism.

<figure><img src="image_2.png" /></figure>

<footnote>* Author supported by the French government "Investissements d'Avenir" program integrated to France 2030, Throught the QuaSy research grant ANR-23-CE48-0008-01</footnote>

<footnote>† Author supported by the ERC grant INFSYS, agreement no. 950398.</footnote>

<footnote>‡ Author supported by the National Science Centre, Poland (grant no. 2021/41/B/ ST6/03914).</footnote>
## 1.2 The main result

In this work we approach Problem 1.1. Our structures are pairs of finite words of the same length, encoded as words over a product alphabet (one might consider words of differing lengths at a cost of some padding at the end, but it wouldn't add much expressive power). We input a relation $R$ given as a regular language and we want to effectively characterise when $R$ admits a uniformisation definable in a fixed formalism.

We solve this problem for $FO^2[<]$, i.e. First-Order Logic with linear order, where only two variables $x$ and $y$ are allowed in the syntax (typically, one can express things like “the position $x$ is somewhere before the position $y$”, but not “the position $x$ is just before the position $y$”, since this would require a third variable). The main reason we consider this particular fragment is because of its very nice properties. Indeed, the class of languages definable in $FO^2[<]$ has been characterised in many different ways (see e.g. [18] and [15]). After the full MSO and FO logics, it is arguably the most studied and understood class of regular languages.

Our solution to Problem 1.1 is effective in the sense that if a uniformisation exists, then our algorithm can construct it. Together with a result from a PhD thesis [10], it is the only known answer to Problem 1.1 in the case of finite words. The cited PhD thesis solves Problem 1.1 for the very weak fragment of FO, namely $FO[ ]$, see [10, Theorem 2.32]. The fragment $FO[ ]$ only allows to count letters e.g. “there are exactly 5 occurrences of the letter $a$”, “there are at least 3 letters distinct from $b$, etc.”

The only other known solution to Problem 1.1 was given in [7, Main Theorem 1] in the case of bi-infinite words (i.e. words over $\mathbb{Z}$) and uniformisations definable in full MSO.

## 1.3 Uniformisation and synthesis

Uniformisation problems are closely related to synthesis and the Church synthesis problem in particular (see [17] for a survey on the matter). In synthesis, one wants to uniformise a relation given as a *specification* by a function given by a *program*. In the Church synthesis problem, the specification is a regular relation given in MSO, while the program is a sequential function given by a Mealy machine. Since the seminal solution given by [2], many other variants have been considered with different classes of specifications and programs.

The class $FO^2[<]$ has been characterised in terms of simple programs, for instance *turtle languages* [19] (sometimes called rankers) which are programs of the form “*go to the first a to the right; then go to the first b to the left; then to the first c to the left*”. Another formalism equivalent to $FO^2[<]$ is that of deterministic partially ordered 2-way automata [15], which as the name suggests cannot go back to a state visited in the past.

Thus, our result can be seen as a synthesis result with MSO specifications and programs given by either of the above models.

## 1.4 Structure of the article

The whole article is dedicated to the proof of our main theorem. It is divided into different sections, as follows.

Section 2 sums up the technical background we rely on.

In Section 3, we recall a known result, stating that $FO^2[<]$ can be characterised, in particular, in terms of certain languages called

*unambiguous monomials*. Inspired from this characterisation, we introduce a particular subclass of monomials, namely the class of *splits*. These splits are less expressive than unambiguous monomials, but have the property of finitely partitioning the set of all words in a nicely structured way, which will prove useful in the remainder of the proof.

In Section 4, we propose a generalisation of these splits, by inductively defining what we call *split trees*. Each split tree defines a language of finite words. Split trees form the ground base of our proof, as we show in Section 5 the crucial split theorem. This result proposes a new characterisation of $FO^2[<]:$ a language is in this class if and only if it can be described as a union of finitely many split trees.

Using this characterisation, we can finally prove our main theorem: we show that for every regular relation $R$ over finite words, we can define an MSO formula $\Psi_R$, over the $\omega$-branching tree, that directly expresses the possibility to uniformise $R$ in $FO^2[<]$. Since the MSO theory of this $\omega$-branching tree is decidable, we deduce a procedure for our problem.

We conclude the paper with a discussion on the possibilities to extend our results to other formalisms, and argue that our techniques can be used to solve other problems that involve the class $FO^2[<]$.

The proofs omitted due to space limitations can be found in the full version of the paper, available on arXiv.

# 2 TECHNICAL BACKGROUND

## 2.1 Words and logic

An *alphabet* $\mathcal{A}$ is any finite set, its elements are called *letters*. A subset $A_0 \subseteq \mathcal{A}$ is a *subalphabet* of $\mathcal{A}$. A *word* over $\mathcal{A}$ is any function $w$ from some set $\{0, \dots, n-1\}$ to $\mathcal{A}$, where the natural number $n$ is called the *length* of $w$, and is denoted by $|w|$. We often write $w$ as the finite sequence of its letters: $w = a_0 \cdots a_{n-1}$, where $a_i = w(i)$ occurs at the *position* $i$ of $w$. We also say that the *position* $i$ is labelled by $a_i$. The *concatenation* of two words $w_1 = a_0 \cdots a_{p-1}$ and $w_2 = b_0 \cdots b_{q-1}$ is the word $a_0 \cdots a_{p-1}b_0 \cdots b_{q-1}$, denoted by $w_1 \cdot w_2$. The word $v$ is called an *infix* of $u$ if there exist words $v_0, v_1$ such that $u = v_0 \cdot v \cdot v_1$. It is a *prefix* of $u$ (resp. a *suffix* of $u$) if moreover $v_1 = \epsilon$ (resp. $v_0 = \epsilon$).

The set of all words over $\mathcal{A}$ is written $A^*$, and its subsets are called *languages*. There is a unique word $\epsilon$ of length 0 which is called the *null word*. In the literature, it is more often called the *empty word*, but in this paper we prefer to use the former terminology in order to avoid any possible confusion between the empty language $\emptyset$ and the language composed of this null word $\{\epsilon\}$ (which is therefore not empty). The concatenation generalises to languages of words: if $K$ and $L$ are two languages of words over $\mathcal{A}$, then $K \cdot L$, the concatenation of $K$ and $L$, is the language of all words of the shape $u \cdot v$, with $u \in K$ and $v \in L$.

We give a brief introduction to *Monadic Second-Order Logic* (MSO) over finite words. The signature is composed of the linear order $<$ between two positions of a word, of the equality $=$ between two positions, and of the letter tests of individual positions ($a(x)$ means that the position $x$ of the word is labelled by the letter $a$). We also consider the membership relation $\in$ between a position $x$ of a word and a set $X$ of positions of a word. Formulae of MSO are
obtained from these *atoms* via Boolean combinations ($\wedge$ stands for the conjunction, $\vee$ for the disjunction, $\neg$ for the negation), quantifications over positions ($\exists x. \varphi$ stands for the existence of a position $x$ such that $\varphi$ holds, while $\forall x. \varphi$ states that $\varphi$ holds for every choice of the position $x$) as well as quantifications over subsets of positions (called *monadic quantifiers* and always written using upper-case letters: $\exists X, \forall X$).

By MSO$[<, A]$ we denote the class of formulae os MSO when the alphabet $A$ is considered; and by MSO$[<]$ we denote the union of all these classes, over all alphabets; this convention will be kept for the other formalism defined in the paper. By $\mathcal{L}(\varphi)$ we denote the language *defined by* $\varphi$, i.e.. the set of words that satisfy the formula $\varphi$. The notion of a language of words being *definable* in MSO$[<]$ generalises to any other formalism. Finally, a language definable in MSO$[<]$ is called *regular*.

First-Order Logic (FO$[<]$) is the fragment of MSO where quantifiers over positions are allowed ($\exists x, \forall x$), but quantifiers over sets of positions ($\exists X, \forall X$) are not. In this paper we will focus on one particular syntactic fragment of FO$[<]: FO$^2[<]$, the fragment in which only two first-order variables are allowed – typically $x$ and $y$. It shall be kept in mind that the variables can be repeated though; thus a formula such as $\exists x. a(x) \wedge \exists y. x<y \wedge b(y) \wedge \exists x. y<x \wedge c(x)$ belongs to our fragment. A complete characterisation of the languages definable in FO$^2[<]$ will be provided in the next section. As an example, the language $\{a, b, c\}^* \cdot a \cdot b \cdot \{a, b, c\}^*$ of words over $\{a, b, c\}$ that contain somewhere the letter $a$ immediately followed by the letter $b$, is definable in FO$[<]$ but not in FO$^2[<]:$ one would need a third variable in order to express the successor relation between said occurrences of $a$ and $b$ (see [6, Example 4]).

First-Order and Monadic Second-Order Logics can be used on many structures other than finite words. In particular, later in the paper, we will rely on Rabin's tree theorem, stating decidability of MSO over infinite trees. We will come back to this in the appropriate sections.

## 2.2 Relations and uniformisations over words

Let $A$ and $B$ be two alphabets. For the sake of readability, for $a \in A$ and $b \in B$ we will write the pair $\langle a, b \rangle$ as $\begin{pmatrix} a \\ b \end{pmatrix}$. Similarly, $\begin{pmatrix} A \\ B \end{pmatrix}$ denotes the product alphabet, i.e. the set of all such pairs $\{(\begin{smallmatrix} a \\ b \end{smallmatrix}) \mid a \in A \text{ and } b \in B\}$.

Any word $p$ over a product alphabet $\begin{pmatrix} A \\ B \end{pmatrix}$ can be identified with a pair $\langle w, \sigma \rangle$, with $w \in A^*$ and $\sigma \in B^*$, both having the same length as $p$, and such that for all positions $i$ of $p$, $p(i) = \begin{pmatrix} w(i) \\ \sigma(i) \end{pmatrix}$. We will write $\begin{pmatrix} w \\ \sigma \end{pmatrix}$ for such a word $p$. This way, any language $R \subseteq \begin{pmatrix} A \\ B \end{pmatrix}^*$ over a product alphabet induces a binary relation between $A^*$ and $B^*$ which contains $\langle w, \sigma \rangle \in A^* \times B^*$ if and only if $\begin{pmatrix} w \\ \sigma \end{pmatrix} \in R$. Note that a relation given this way implicitly preserves the lengths of the words. Treating relations as languages, it makes sense to speak about relations of words that are regular, or that are definable in a certain formalism such as FO$[<]$ of FO$^2[<]$.

If $L \subseteq A^*$ and $K \subseteq B^*$ then by $\langle L \rangle$ we denote the set of words $\begin{pmatrix} w \\ \sigma \end{pmatrix} \in \begin{pmatrix} A \\ B \end{pmatrix}^*$ such that $w \in L$ and $\sigma \in K$ and both have the same length.

Let $R \subseteq \begin{pmatrix} A \\ B \end{pmatrix}^*$ be a binary relation between words over $A$ and words over $B$. We define its *projection* onto $A^*$, denoted by $\text{proj}(R)$, as the language of words $w$ over $A$ such that $\begin{pmatrix} w \\ \sigma \end{pmatrix} \in R$ for some

$\sigma \in B^*$. We say that $R$ is *functional* if for every $w \in \text{proj}(R)$ there exists exactly one $\sigma \in B^*$ such that $\begin{pmatrix} w \\ \sigma \end{pmatrix} \in R$.

A first thing to notice is that the projection of a regular relation is also regular, and moreover it can be computed:

**FACT 2.1.** *The projection of a regular relation of finite words is also regular. Moreover there exists an algorithm that inputs a regular relation $R \subseteq \begin{pmatrix} A \\ B \end{pmatrix}^*$ and outputs its projection onto $A^*$.* □

This fact is folklore, it is most easily seen by simulating projection using monadic quantifiers of MSO.

This paper is mostly focused on decidability, so it does not matter if the relation $R$ of the above statement is given as an MSO$[<, \begin{pmatrix} A \\ B \end{pmatrix}]$ formula or as another model (e.g. a finite automaton, a finite monoid...), which is why we do not specify it. We will keep that convention for the other algorithms we refer to in the paper.

A *uniformisation* of a binary relation $R \subseteq \begin{pmatrix} A \\ B \end{pmatrix}^*$ is a functional binary relation $F$ included in $R$ sharing the same projection onto $A^*$. Intuitively, for every $w \in A^*$, $F$ selects a unique word $\sigma$ such that $\begin{pmatrix} w \\ \sigma \end{pmatrix} \in R$, whenever there exists one.

MSO has the property of providing uniformisations for its own relations, as it is stated in the following proposition. This result is mostly considered as folklore in the literature, yet a proof of it can be found for example in [10, Theorem 1.48].

**PROPOSITION 2.2.** *Every regular relation of finite words admits a uniformisation that is also regular. Moreover, there exists an algorithm that inputs a regular relation $R$ over finite words, and outputs a regular uniformisation $F$ of it.* □

This property of providing uniformisation is not shared by FO$[<]$, nor by its most natural fragments, like FO$^2[<]$ or FO$[$, see [9]. Hence, being a relation definable in FO$^2[<]$ is not a sufficient condition in order to admit a uniformisation definable in FO$^2[<]$ as well.

As it occurs, it is not a necessary condition either: consider the relation $R_{\text{even}} \subseteq \begin{pmatrix} \{a\} \\ \{0,1\} \end{pmatrix}^*$, consisting of the pairs of words over $\begin{pmatrix} w \\ \sigma \end{pmatrix}$ over the product alphabet $\begin{pmatrix} \{a\} \\ \{0,1\} \end{pmatrix}$ such that $\sigma$ has an even number of occurrences of the letter 1. This language is regular, but not definable in FO$^2[<]$, nor even in full First-Order Logic (parity is a classic limitation of FO$[<]$, see e.g. [14]), yet it admits an actually very simple uniformisation, clearly definable in FO$^2[<]:$ the relation $F_{\text{zero}} \subseteq \begin{pmatrix} \{a\} \\ \{0,1\} \end{pmatrix}^*$ consisting of pairs of words with no occurrences of the letter 1 in their second coordinate.

This illustrates the difficulty of characterising the relations uniformisable in FO$^2[<]$.

# 3 UNAMBIGUOUS MONOMIALS

This section introduces some of the key notions of the article, namely monomials, labellings, and splits. Moreover, we show how they relate to the logic FO$^2[<]$.

## 3.1 Monomials

A complete survey of the expressiveness of FO$^2[<]$ can be found in [19]. Among all the known characterisations, we cite the following: FO$^2[<]$ corresponds to *unambiguous polynomials*, a notion that we define below.
Intuitively, a *monomial* should correspond to a language of the shape $A_0^* \cdot a_0 \cdot A_1^* \cdot a_1 \cdots A_{n-1}^* \cdot a_{n-1} \cdot A_n^*$, where each $a_i$ is a letter of the considered alphabet $\mathcal{A}$, and each $A_i$ is a subalphabet of it. However, since we will need to operate on monomials as primitive objects, we need to define them syntactically. Thus, given an alphabet $\mathcal{A}$ we fix a *labelling set* (formally nothing more than another alphabet)

$$ \mathbb{L}_{\mathcal{A}} = \{a \mid a \in \mathcal{A}\} \cup \{A_0^* \mid A_0 \subseteq \mathcal{A}\}, $$

which consists of all the letters from $\mathcal{A}$ as well as formal stars $A_0^*$ of all subalphabets $A_0$ of $\mathcal{A}$. Then, a monomial $M$ over $\mathcal{A}$ is a finite word over $\mathbb{L}_{\mathcal{A}}$ of the shape

$$ M = A_0^* \cdot a_0 \cdot A_1^* \cdot a_1 \cdots A_{n-1}^* \cdot a_{n-1} \cdot A_n^* \in (\mathbb{L}_{\mathcal{A}})^*. $$

Note that the length of $M$ equals $2n+1$ (it is always an odd natural number). For every $i<n$, we say that the letter $a_i$ is a distinguished letter in the monomial $M$.

Each monomial $M$ has its language, obtained by treating $M$ as a regular expression. More formally, we say that $w$ is in the language of $M$ (simply written $w \in M$) if $w$ has a decomposition with respect to $M$, i.e.

$$ w = w_0 \cdot a_0 \cdot w_1 \cdot a_1 \cdots w_{n-1} \cdot a_{n-1} \cdot w_n, $$

with $w_i \in A_i^*$ for every $i \le n$ (note that if $A_i = \emptyset$ then necessarily $w_i = \epsilon$). Treating monomials as languages, it makes sense to say that $M \subseteq M'$, that $M$ is functional (when the considered alphabet is a product alphabet), etc.

The reason we formally define monomials as words is that two different monomials may lead to the same language, for instance the languages of $\{a\}^* \cdot a \cdot \emptyset^*$ and of $\emptyset^* \cdot a \cdot \{a\}^*$ coincide.

Every monomial is non-empty as a language, the unique word of minimal length that belongs to it is exactly the word of distinguished letters $a_0 \cdots a_{n-1}$ (if $n=0$ then this is the null word).

A monomial $M$ is called *unambiguous* if the decompositions it induces are unique, meaning that for all sequences of pairs of words $(w_i, w'_i)_{i \le n}$ with $w_i, w'_i \in A_i^*$ for $i \le n$ such that

$$ w_0 \cdot a_0 \cdots w_{n-1} \cdot a_{n-1} \cdot w_n = w'_0 \cdot a_0 \cdots w'_{n-1} \cdot a_{n-1} \cdot w'_n, $$

we necessarily have $w_i = w'_i$ for every $i \le n$.

**FACT 3.1.** If $M'$ is a monomial which is an infinx (as a word) of an unambiguous monomial $M$ then $M'$ is also unambiguous. $\square$

A polynomial is a finite sequence $(M_i)_{i < I}$ of monomials, the language of such a polynomial is the union of the languages of $M_i$ for $i < I$. Such a polynomial is unambiguous if every $M_i$ is unambiguous itself. One might require the monomials to be pairwise disjoint here, but as we will see later in the construction, it does not matter.

The following result states the link between unambiguous polynomials and the logic FO²[<]:

**THEOREM 3.2 (BASED ON [19]).** Let $L \subseteq A^*$ be a language of finite words over an alphabet $\mathcal{A}$. The following conditions are equivalent:

A) $L$ is definable in FO²[<, A],

B) $L$ is the language of an unambiguous polynomial.

Moreover, given a regular language $L$ over $\mathcal{A}$, it is decidable if $L$ is definable in FO²[<, A]. If it is, then a representation of $L$ as an unambiguous polynomial can be effectively constructed.

**PROOF.** The characterisation stated in [19] shows that $A$ is equivalent to

$B^*)$ $L$ is the language of an unambiguous polynomial, whose monomials are pairwise disjoint as languages.

For the sake of simplicity, we will work with representations as in B). The implication $B^*) \Rightarrow B$) is obvious. The implication $B) \Rightarrow A$) follows from the closure of FO²[<, A] under alternative (i.e. union) and the fact that each unambiguous monomial is expressible in FO²[<, A], as shown by the implication $B^*) \Rightarrow A$). $\square$

If $M = C_0^* \cdot c_0 \cdot C_1^* \cdots C_{n-1}^* \cdot c_{n-1} \cdot C_n^*$ is a monomial over a product alphabet $(\mathbb{A}_B)^{\dagger}$, then its projection onto $A^*$ (denoted by $\text{proj}(M)$) is the monomial $A_0^* \cdot a_0 \cdot A_1^* \cdots A_{n-1} \cdot a_{n-1} \cdot A_n^*$, where every $A_i$ is the projection $\text{proj}(C_i)$ of the subalphabet $C_i$ onto $\mathcal{A}$ (meaning the set of letters $a \in \mathcal{A}$ such that $(a^b) \in C_i$ for some $b \in \mathbb{B}$), and similarly $a_i$ is the projection $\text{proj}(c_i)$ of the letter $c_i$ onto $\mathcal{A}$ (meaning that there exists $b_i \in \mathbb{B}$ such that $c_i = (b_i^a)$).

**FACT 3.3.** The language of $\text{proj}(M)$ is the projection of the language of $M$ onto $A^*$, so no confusion between syntax and semantics can arise here. $\square$

For the rest of this article, we will use the letter $M$ for monomials over such a product alphabet $(\mathbb{A}_B)$ and the letter $P$ for monomials over $\mathcal{A}$, typically projections of the former.

## 3.2 Labellings

Recall that $M \subseteq (\mathbb{A}_B)^*$ is functional if for every $w \in \text{proj}(M)$, there exists a unique $\sigma \in \mathbb{B}^*$ such that $(w^\sigma) \in M$. Similarly, we say that a subalphabet $C \subseteq (\mathbb{A}_B)$ is functional if for every letter $a \in \mathcal{A}$ there is at most one letter $b \in \mathbb{B}$ such that $(b^a) \in C$. Such an alphabet in fact encodes a partial function from $A^*$ to $\mathbb{B}^*$, as expressed by the following fact:

**FACT 3.4.** Let $C \subseteq (\mathbb{A}_B)$. The language $C^* \subseteq (\mathbb{A}_B)^*$ is functional (as a relation) if and only if $C$ is functional (as a subalphabet). $\square$

A B-labelling (or just a labelling) of a monomial

$$ P = A_0^* \cdot a_0 \cdot A_1^* \cdots A_{n-1}^* \cdot a_{n-1} \cdot A_n^* $$

over $\mathcal{A}$ is a monomial

$$ M = C_0^* \cdot c_0 \cdot C_1^* \cdots C_{n-1}^* \cdot c_{n-1} \cdot C_n^* $$

over the product alphabet $(\mathbb{A}_B)$ such that $\text{proj}(M) = P$ and for every $i \le n$, the subalphabet $C_i$ is functional.

**FACT 3.5.** Assume that $C \subseteq (\mathbb{A}_B)$ is a functional alphabet with $\text{proj}(C) = \mathcal{A}$ and $P$ is a monomial over $\mathcal{A}$. Then there exists a unique B-labelling $M$ of $P$ such that (treated as languages) $M \subseteq C^*$.

Moreover, this B-labelling $M$ satisfies $M = (P^B) \cap C^*$. $\square$

**PROOF.** Assume that

$$ P = A_0^* \cdot a_0 \cdot A_1^* \cdots A_{n-1}^* \cdot a_{n-1} \cdot A_n^* $$

and let

$$ M = C_0^* \cdot (a_0^b) \cdot C_1^* \cdots C_{n-1}^* \cdot (b_{n-1}^{a_{n-1}}) \cdot C_n^* $$

<footnote>†Here, $M$ is seen as a word over the labelling set $L(\mathbb{A}_B)$, defined in the same way as $L_A$.</footnote>
where $C_i = (\begin{smallmatrix} A_i \\ B \end{smallmatrix}) \cap C_i$ for $i \le n$ and for $i < n$ the letter $b_i$ is the unique letter such that $(\begin{smallmatrix} a_i \\ b_i \end{smallmatrix}) \in C$. This definition guarantees that $M \subseteq C^*$.

Uniqueness of $M$ is clear, as there is no other choice for the subalphabets and letters. The inclusion $M \subseteq (\begin{smallmatrix} P \\ B^* \end{smallmatrix}) \cap C^*$ follows directly from the definition. For the other inclusion take $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in (\begin{smallmatrix} P \\ B^* \end{smallmatrix}) \cap C^*$. Thus, $w \in P$ and Fact 3.4 implies that $\sigma$ is uniquely determined by $C$. Thus, any decomposition of $w$ with respect to $P$ also gives a decomposition of $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix})$ with respect to $M$, witnessing that $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in M$. $\square$

The following proposition, although technically simple, gives an important connection between the syntactic notion of a $\mathbb{B}$-labelling and the semantic property of being a functional relation.

**PROPOSITION 3.6.** Let $M$ be a monomial over a product alphabet $(\begin{smallmatrix} A \\ B \end{smallmatrix})$ and let $P = \text{proj}(M)$. The following conditions are equivalent:

(1) $M$ is functional and unambiguous,

(2) $M$ is a $\mathbb{B}$-labelling of $P$ and $P$ is unambiguous.

Both directions of the equivalence follow directly from the definitions and from Fact 3.4.

**EXAMPLE 3.7.** Let us illustrate Proposition 3.6 with the monomial $P = \{a\}^* \cdot a \cdot \{a\}^*$.

It is clearly ambiguous (i.e. it is not unambiguous). Therefore, the proposition tells us that any labelling of $P$ is either ambiguous as well, or not functional.

The monomials $M_1 = \{(\begin{smallmatrix} a \\ 0 \end{smallmatrix})\}^* \cdot (\begin{smallmatrix} a \\ 0 \end{smallmatrix}) \cdot \{(\begin{smallmatrix} a \\ 0 \end{smallmatrix})\}^*$ and $M_2 = \{(\begin{smallmatrix} a \\ 0 \end{smallmatrix})\}^* \cdot (\begin{smallmatrix} a \\ 1 \end{smallmatrix}) \cdot \{(\begin{smallmatrix} a \\ 0 \end{smallmatrix})\}^*$ are instances of such $\{0, 1\}$-labellings of $P$. Observe that the former is functional, but ambiguous; while the latter is unambiguous, but not functional. $\square$

**COROLLARY 3.8.** The projection of a functional relation definable in $\text{FO}^2[<, (\begin{smallmatrix} A \\ B \end{smallmatrix})]$ is also definable in $\text{FO}^2[<, A]$.

**PROOF.** Theorem 3.2 implies that a functional relation $F$ definable in $\text{FO}^2[<, (\begin{smallmatrix} A \\ B \end{smallmatrix})]$ is a finite union of unambiguous monomials. Each of these monomials must necessarily be functional. Proposition 3.6 implies that the projection of $F$ is a finite union of unambiguous monomials. Using again Theorem 3.2 we know that the projection of $F$ is definable in $\text{FO}^2[<, A]$. $\square$

The assumption that $F$ is functional is necessary here. For instance take $A = \{a, b, c\}$ and $B = \{0, 1\}$ and consider the monomial

$$M = (\begin{smallmatrix} a,b,c \\ 0 \end{smallmatrix})^* \cdot (\begin{smallmatrix} a \\ 0 \end{smallmatrix}) \cdot \theta^* \cdot (\begin{smallmatrix} b \\ 1 \end{smallmatrix}) \cdot (\begin{smallmatrix} a,b,c \\ 1 \end{smallmatrix})^*,$$

over $(\begin{smallmatrix} A \\ B \end{smallmatrix})$. It is easy to see that $M$ is unambiguous and therefore has a language definable in $\text{FO}^2[<]$. However, $M$ is not functional and the projection of $M$ onto $A$ is $\{a, b, c\}^* \cdot a \cdot b \cdot \{a, b, c\}^*$, which is not definable in $\text{FO}^2[<]$, as noted in Section 2.

## 3.3 Splits

The notion of unambiguous monomials, although simple to phrase, turns out to be too complex for our purposes. More precisely, being unambiguous is not a regular property of monomials (treated as words over a labelling set $\mathbb{L}_A$), as expressed by the following remark.

**REMARK 3.9.** Consider the alphabet $A = \{a, \#\}$. Let $U \subseteq (\mathbb{L}_A)^*$ be the set of all unambiguous monomials over $A$. The language $U$ is not regular.

**PROOF.** Take $m, n > 0$ and let $P_{m,n}$ be the monomial

$$\{a\}^* \cdot a \cdot \{\#\}^* \cdot a^{\circ m} \cdot \theta^* \cdot \# \cdot \theta^* \cdot a^{\circ n} \cdot \{\#\}^* \cdot a \cdot \{a\}^*,$$

where $a^{\circ k}$ stands for the word $a \cdot \theta^* \cdot a \cdots \theta^* \cdot a$ with exactly $k$ occurrences of $a$.

We will now show that the monomial $P_{m,n}$ is unambiguous if and only if $m \neq n$. Consider the monomial $P_{m,n}$ for some $m, n > 0$. Observe that the only words $w$ which potentially admit two distinct decompositions are those which contain exactly two occurrences of $\#$, separated by some non-null block of occurrences of $a$, i.e.

$$w = a \cdots a \cdot \# \cdot a \cdots a \cdot \# \cdot a \cdots a. \atop \qquad k \text{ times}$$

However, if $m \neq n$ then at most one decomposition fits, depending on whether $k = m$ or $k = n$. On the other hand, assume that $m = n$ and consider the word

$$u = a \cdot a \cdots a \cdot \# \cdot a \cdots a \cdot \# \cdot a \cdots a \cdot a. \atop \qquad n \text{ times} \qquad n \text{ times} \qquad n \text{ times}$$

This word admits two distinct decompositions with respect to $P_{n,n}$.

Note that the language $\{P_{m,n} | m, n > 0\} \subseteq (\mathbb{L}_A)^*$ is regular. Therefore, if $U$ were regular, then $\{P_{m,n} | m, n > 0\} \setminus U = \{P_{n,n} | n > 0\}$ would be as well. A contradiction easily follows from the well-known Pumping Lemma, the language $\{P_{n,n} | n > 0\}$ is analogous to the language $\{a^n b^n | n > 0\} \subseteq \{a, b\}^*$. $\square$

On the other hand, one can show that given a fixed regular language $L \subseteq A^*$, the set of monomials $P$ over $A$ such that $P \subseteq L$ is a regular language over $\mathbb{L}_A$.

The impossibility to speak about unambiguous monomials in $\text{MSO}[<]$ is the reason why, in Section 4, we represent them via trees, which have a richer structure. Before doing this, we introduce the two crucial notions of splits and 2-words. The splits can be seen as the equivalence classes of the first level of the congruence from [18, Section 3].

Intuitively, two words will be equivalent if they are equal when applying the operation that only keeps the first and last occurrences of each letter. For instance, applying this operation to both $v_1$ and $v_2$ we obtain the same word $u$:

$$v_1 = a \cdot c \cdot a \cdot b \cdot b \cdot a,$$

$$v_2 = a \cdot c \cdot b \cdot b \cdot b \cdot a \cdot a,$$

$$u = a \cdot c \cdot b \cdot b \cdot a.$$

Hence, $v_1$ and $v_2$ are equivalent, with the equivalence class represented by $u$. Note that each letter can appear at most twice in a word $u$ obtained this way.

More formally, we define a 2-word as being any word in which every letter occurs at most twice. Given a 2-word $u = a_0 \cdots a_{n-1}$, the split induced from $u$ is the monomial

$$A_{0}^{*} \cdot a_{0} \cdot A_{1}^{*} \cdot a_{1} \cdots A_{n-1}^{*} \cdot a_{n-1} \cdot A_{n}^{*},$$

where, for every $j \le n$, the subalphabet $A_j$ is defined as the set of letters $a \in A$ such that $a_i = a = a_k$ for some $i, k$ such that $0 \le i < j \le k < n$. In other words, $a \in A_j$ if $a$ occurs twice as
a distinguished letter in the monomial: once before $A_j^*$ and once after. In particular, the extremal subalphabets $A_0$ and $A_n$ are always empty.

We denote by split($u$) the split induced from $u$. As an example, split($a \cdot c \cdot b \cdot b \cdot a$), the split of the example in the above paragraph, is the monomial

$$0^* \cdot a \cdot \{a\}^* \cdot c \cdot \{a\}^* \cdot b \cdot \{a, b\}^* \cdot b \cdot \{a\}^* \cdot a \cdot 0^*.$$

Notice that the null word $\epsilon$ is a 2-word and its induced split is $0^*$, whose language is $\{\epsilon\}$.

A monomial $P$ is a split if it is split($u$) for some 2-word $u$. In this case, similarly as for monomials, $u$ is the unique word of minimal length in $P$. Hence, the word $u$, from which the split is induced, is uniquely determined.

The convenience of working with splits derives from the fact that they are unambiguous, disjoint, and finitely partition the full language of all words over $\mathbb{A}$, as it is stated in the following two propositions.

**PROPOSITION 3.10.** All splits over $\mathbb{A}$ are unambiguous.

**PROOF.** Let

$$\text{split}(u) = A_0^* \cdot a_0 \cdot A_1^* \cdots a_{n-2} \cdot A_{n-1}^* \cdot a_{n-1} \cdot A_n^*$$

be some split over $\mathbb{A}$, $u = a_0 \cdot a_1 \cdots a_{n-1}$ being a 2-word. Let $w \in \text{split}(u)$ and consider two decompositions of it

$$w = w_0 \cdot a_0 \cdot w_1 \cdots a_{n-2} \cdot w_{n-1} \cdot a_{n-1}, \text{ and}$$

$$w = w'_0 \cdot a_0 \cdot w'_1 \cdots a_{n-2} \cdot w'_{n-1} \cdot a_{n-1},$$

where for every $j \le n$ we have $w_j, w'_j \in A_j^*$.

Let us suppose for the sake of contradiction that these two decompositions are distinct, and let $j \le n$ be the minimal index such that $w_j \ne w'_j$: this means that one of the two is a strict prefix of the other. Without loss of generality, we can assume that $w'_j$ is a strict prefix of $w_j$. Since $a_j$ is the letter following $w'_j$ in $w$, it must have an occurrence in $w_j$. Because $w_j \in A_j^*$, by definition there must be some $i < j$ such that $a_i = a_j$.

Since $a_j$ also follows $w_j$ in $w$, this letter necessarily has an occurrence somewhere in the word $w'_{j+1} \cdot a_{j+1} \cdots a_{n-2} \cdot w'_{n-1} \cdot a_{n-1} \cdot w'_n$, which implies that it occurs as some of the $a_k$'s, $j < k < n$. Hence, we obtain the equalities $a_i = a_j = a_k$ with $i < j < k$: this letter has at least three occurrences in $u = a_0 \cdots a_{n-1}$. This goes in contradiction with the assumption that $u$ is a 2-word. □

**PROPOSITION 3.11.** All splits over $\mathbb{A}$, treated as languages, finitely partition $\mathbb{A}^*$: they are all non-empty, pairwise disjoint, their union is the set of all words over $\mathbb{A}$, and finally, there are finitely many of them.

**PROOF.** Non-emptiness follows from the fact that every monomial has a non-empty language.

Intuitively, the disjointness of splits induced from distinct 2-words follows from the fact that a split can be interpreted as a maximal consistent conjunction of statements of the shape “the word contains no occurrence / exactly one occurrence / at least two occurrences of the letter $a$”, and of the shape “the first / last occurrence of $a$ is before / after the first / last occurrence of $b$”, and two distinct such conjunctions go in contradiction to each other.

Straightforwardly, every word $w$ over $\mathbb{A}$ belongs to some split, since it belongs to the one induced from the word obtained from $w$ by applying the operation which keeps only the first and the last occurrences of each letter.

Finally, the finite number of splits over $\mathbb{A}$ follows from the finite number of 2-words. Indeed, if $m$ is the cardinality of $\mathbb{A}$, then all 2-words over $\mathbb{A}$ have length not greater than $2m$. Therefore, the number of 2-words over $\mathbb{A}$ is bounded by $(m+1)^{2m}$.

Thus, splits over $\mathbb{A}$ finitely partition $\mathbb{A}^*$. □

If $A_0 \subseteq \mathbb{A}$ then every split over $A_0$ is also a split over $\mathbb{A}$. Thus, we obtain the following corollary.

**COROLLARY 3.12.** Take $A_0 \subseteq \mathbb{A}$. The language $A_0^* \subseteq \mathbb{A}^*$ is a finite pairwise disjoint union of splits over $\mathbb{A}$. □

# 4 TREES, MONOMIAL TREES, AND SPLIT TREES

Splits behave in a more rigid way than arbitrary unambiguous monomials. However, a single split is too weak to express sufficiently complex properties. In particular, a split can count occurrences of each letter up to at most 2, while an unambiguous monomial can require that there are exactly 7 such occurrences. To overcome these limitations, we allow to nest splits inside other splits. This is achieved by arranging such nested splits into a tree structure: a split tree.

This section is devoted to a definition of split trees. Then, we will show in Section 5 that functional relations definable in FO² can be syntactically represented as unions of labellings of split trees, which will prove itself as a crucial result for the characterisation of relations uniformisable in FO²[<].

## 4.1 Trees

In this paper, a tree labelled by some labelling set $\mathcal{L}$ is any function $t: \text{Nodes}(t) \to \mathcal{L}$ such that the set of nodes $\text{Nodes}(t) \subseteq \mathbb{N}^*$ is:

(1) a finite and non-empty set of words over natural numbers$^\dagger$,

(2) closed under prefixes: if $u \cdot v \in \text{Nodes}(t)$ then $u \in \text{Nodes}(t)$, for all words $u, v \in \mathbb{N}^*$,

(3) closed under smaller nodes: if $u \cdot j \in \text{Nodes}(t)$ then $u \cdot i \in \text{Nodes}(t)$, for $u \in \mathbb{N}^*$, and $i \le j \in \mathbb{N}$.

We denote the value of $t$ at a node $u \in \text{Nodes}(t)$ by $t(u) \in \mathcal{L}$ and call it the label of $t$ at $u$.

The lexicographic order over nodes of a tree is the linear order given by $u \le_{\text{lex}} u \cdot v$, and by $u \cdot i \cdot v \le_{\text{lex}} u \cdot j \cdot w$ for any $i \le j$. Finally, we denote by $u \le v$ the fact that the node $u$ is a prefix of the node $v$ (seen as words).

The root of a tree is the node $\epsilon$. A leaf of a tree $t$ is a node $u \in \text{Nodes}(t)$ such that $u \cdot 0 \notin \text{Nodes}(t)$. A node which is not a leaf is called internal. If $u \cdot i \in \text{Nodes}(t)$, then $u \cdot i$ is called the $i$-th child of $u$ in $t$.

If $t$ is a tree and $u \in \text{Nodes}(t)$ then $t \upharpoonright_u$ is the subtree of $t$ at $u$: its nodes are words $v$ such that $u \cdot v \in \text{Nodes}(t)$, and $t \upharpoonright_u(v) = t(u \cdot v)$.

<footnote>$^\dagger$Even though it is not finite, we allow ourselves to treat $\mathbb{N}$ as an alphabet here. For this reason, the notation $\mathbb{N}^*$ shall never be understood as the set of non-zero natural numbers, as we are used to see it in the literature. We can naturally make use of the notions of concatenations, prefixes, etc.</footnote>
The height of a node is defined inductively: a leaf is of height 0, and the height of an internal node is the maximal height of its children plus one. The height of a tree is the height of its root.

Let $t_0, \dots, t_{n-1}$ be trees, and let $\ell \in \mathbb{L}$. We denote by

$$t = \ell[t_0, \dots, t_{n-1}]$$

the tree $t$ defined by:

* Nodes($t$) = {$\epsilon$} $\sqcup$ $\sqcup_{i<n} i \cdot$ Nodes($t_i$);

* $t(\epsilon) = \ell$, and $t(i \cdot u) = t_i(u)$ for $i < n$ and $u \in$ Nodes($t_i$).

The above definition also makes sense for $n = 0$, i.e. $\ell[\quad]$ is a tree with only one node: the null word $\epsilon$, labelled by $\ell$. Note that each tree is obtained via such a composition in a unique way.

A tree $t_1$ is a prefix of $t_2$, denoted by $t_1 \subseteq_{\text{pref}} t_2$, if the following conditions hold:

* Nodes($t_1$) $\subseteq$ Nodes($t_2$),

* for all $u \in$ Nodes($t_1$) we have $t_1(u) = t_2(u)$,

* for every internal node $u$ of $t_1$ and for every $i \in \mathbb{N}$ we have $u \cdot i \in$ Nodes($t_1$) if and only if $u \cdot i \in$ Nodes($t_2$).

In other words, given a tree $t_2$, a prefix $t_1 \subseteq_{\text{pref}} t_2$ is obtained by turning certain internal nodes of $t_2$ into leaves of $t_1$ by removing their subtrees, and keeping all the remaining nodes unchanged.

Consider a tree $t$ and an internal node $u \in$ Nodes($t$). We say that the children of $u$ form the word $W = \ell_0 \cdots \ell_{n-1} \in \mathbb{L}^*$ in $t$ if $u$ has exactly $n$ children ($u \cdot 0, \dots, u \cdot (n-1)$) in $t$, and if $t(u \cdot i) = \ell_i$ for every $i < n$. Note that if $t_1 \subseteq_{\text{pref}} t_2$ and $u$ is an internal node of $t_1$ then the children of $u$ form the same word both in $t_1$ and $t_2$.

The yield of a tree $t$, denoted by $\text{yield}(t) \in \mathbb{L}^*$, is the word over the same set of labels $\mathbb{L}$, obtained by concatenating the labels of the leaves of $t$ in the lexicographical order. More precisely: if $t = \ell[\quad]$ is a tree consisting of its root only, then $\text{yield}(t) = \ell$; if $t = \ell[t_0, \dots, t_{n-1}]$, then

$$\text{yield}(t) = \text{yield}(t_0) \cdot \text{yield}(t_1) \cdots \text{yield}(t_{n-1}).$$

Notice that the yield does not depend on the labels of the internal nodes.

## 4.2 Monomial trees and split trees

A monomial tree over an alphabet $\mathcal{A}$ is a tree labelled by the set $\mathbb{L}_{\mathcal{A}} = \{a \mid a \in \mathcal{A}\} \sqcup \{A_0^* \mid A_0 \subseteq \mathcal{A}\}$ (the same set of labels we considered in the formal definition of monomials) such that the following two conditions hold:

(1) every node labelled by a letter $a \in \mathcal{A}$ or by the formal star $\emptyset^*$ of the empty subalphabet is necessarily a leaf;

(2) for every internal node $u$ labelled by $A_0^*$ for some non-empty subalphabet $A_0 \subseteq \mathcal{A}$, the children of $u$ form a word over $\mathbb{L}_{\mathcal{A}}$ which is a monomial over $A_0$.

Note that a monomial tree might also have leaves labelled by a formal star $A_0^*$ for some non-empty $A_0 \subseteq \mathcal{A}$.

Similarly, define a split tree over $\mathcal{A}$ as a monomial tree in which additionally the root is necessarily labelled by $A_0^*$ and the children of every internal node form a word which is a split.

**REMARK 4.1.** If $t_2$ is a monomial tree and $t_1 \subseteq_{\text{pref}} t_2$ then also $t_1$ is a monomial tree. The same holds for split trees over $\mathcal{A}$.

**LEMMA 4.2.** For every monomial tree $t$ over $\mathcal{A}$, the word $\text{yield}(t) \in \mathbb{L}_{\mathcal{A}}^*$ is a monomial over $\mathcal{A}$.

<figure><img src="image_3.png" /><figcaption>**Figure 1:** A split tree $t$ and a labelling $\lambda$ of it, not being a split tree.</figcaption></figure>

**PROOF.** The proof is by induction over the height of $t$, and relies on the following closure property of monomials: if, for every $i \le n$, $M_i$ is a monomial over $A_i \subseteq \mathcal{A}$, and, for every $i < n$, $a_i \in \mathcal{A}$ is a letter, then the concatenation $M_0 \cdot a_0 \cdot M_1 \cdots M_{n-1} \cdot a_{n-1} \cdot M_n$ is a monomial over $\mathcal{A}$. $\square$

As in the case of monomials, the yield of a monomial tree always contains some word. Also, if $t$ is a monomial tree such that its root is an internal node and the children of the root form a monomial $M$, then we have the inclusion $\text{yield}(t) \subseteq M$.

In general, the yield of a split tree might not be a split, but, due to Lemma 4.2, it is at least a monomial, as it is illustrated in the following example:

**EXAMPLE 4.3.** Figure 1 depicts a split tree $t$ over the alphabet $\mathcal{A} = \{a_0, a_1\}$. The monomial

$$P = \emptyset^* \cdot a_0 \cdot \{a_0\}^* \cdot a_0 \cdot \emptyset^*,$$

which is a split, is formed both by the children of the root $\epsilon$ and by the children of the node $2 \in \mathbb{N}^*$, labelled by $\{a_0\}^*$.

The yield of $t$ is the monomial

$$\text{yield}(t) = \emptyset^* \cdot a_0 \cdot \emptyset^* \cdot a_0 \cdot \{a_0\}^* \cdot a_0 \cdot \emptyset^* \cdot a_0 \cdot \emptyset^*,$$

which is not a split ($a_0 \cdot a_0 \cdot a_0 \cdot a_0$ is not a 2-word). $\square$

Yet, for trees of height 1, we clearly have a correspondence between splits and yields of split trees:

**FACT 4.4.** Consider a non-empty alphabet $\mathcal{A}$. Then the splits over $\mathcal{A}$ are exactly the yields of split trees of height 1 over $\mathcal{A}$ (all non-root nodes are leaves).

If $\mathcal{A} = \emptyset$, then the unique split over $\mathcal{A}$ is $\emptyset^*$. This split is the yield of the unique split tree $\emptyset^*[]$ over $\emptyset$, whose height is 0. $\square$

Let

$$P = A_0^* \cdot a_0 \cdot A_1^* \cdots A_{n-1}^* \cdot a_{n-1} \cdot A_n^*$$

be a split over $\mathcal{A}$, and let $t_0, \dots, t_n$ be split trees such that for every $i \le n$, the root of $t_i$ is labelled by $A_i^*$ (i.e. it is a split tree over $A_i$). Then the tree

$$A_i^*[t_0, a_0[, t_1, \dots, t_{n-1}, a_{n-1}[, t_n],$$

obtained by joining the trees $t_i$'s with single-node trees $a_i[\quad]$, is again a split tree. We call this tree the composition of $t_0, \dots, t_n$ under $P$.
**LEMMA 4.5.** If $t$ is a split tree then the monomial yield($t$) is unambiguous.

**PROOF.** The proof is by induction on the height of $t$. If $t$ is the tree reduced to its root $A^*[ ]$, then its yield is $A^*$, clearly unambiguous.

Now, suppose that $t$ has non-zero height. In that case $t$ is of the shape

$$A^*[t_0, a_0[, t_1, \dots, a_{n-2}[, t_{n-1}, a_{n-1}[, t_n],$$

where $u = a_0 \cdots a_{n-1}$ is a 2-word, and for every $i \le n$ the tree $t_i$ is a split tree over the alphabet $A_i$ induced from split($u$). By the inductive assumption we know that for $i \le n$ the monomial yield($t_i$) is unambiguous. If $w \in \text{yield}(t)$ then by unambiguity of split($u$) (see Proposition 3.10) there exists a unique sequence of words $(w_0)_{i \le n}$ such that $w_i \in \text{yield}(t_i) \subseteq A_i^*$ and

$$w = w_0 \cdot a_0 \cdot w_1 \cdot a_1 \cdots w_{n-1} \cdot a_{n-1} \cdot w_n.$$

For every $i \le n$, since yield($t_i$) is unambiguous, the word $w_i$ admits a unique decomposition w.r.t. the monomial yield($t_i$). Thus, $w$ has a unique decomposition w.r.t. the whole monomial yield($t$). □

In the following proposition, when writing yield($t_2$) $\subseteq$ yield($t_1$), we rely on the fact that the yield of a monomial tree is a monomial and each monomial induces a language of words over $A$. This proposition is the main result of this section, showing that split trees can be used to represent languages of words in a way consistent with the inclusion order.

**PROPOSITION 4.6.** Let $t_1$ and $t_2$ be two split trees over the same alphabet $A$. Then $t_1 \sqsubseteq_{\text{pref}} t_2$ if and only if yield($t_2$) $\subseteq$ yield($t_1$).

The proof of the proposition is made by induction on $t_2$, each inductive step relying on the fact that two distinct splits have disjoint non-empty languages, see Proposition 3.11. Thus, if yield($t_2$) $\subseteq$ yield($t_1$) and the root of $t_1$ is not a leaf then the children of the root in $t_1$ and in $t_2$ must form the same split, and we can inductively show inclusion for the subtrees below it.

## 4.3 Labellings of trees

From here, we will make a distinction between monomial trees over $A$ (written $t$) and monomial trees over a product alphabet $(\mathbb{A}/\mathbb{B})$ (written $\lambda)^{\dagger}$. Given a monomial tree $\lambda$ over $(\mathbb{A}/\mathbb{B})$, we define its projection $\text{proj}(\lambda)$ by applying the projection to each label of $\lambda$ separately: it is a monomial tree over $A$.

**FACT 4.7.** The operations of projection and yield commute, i.e.

$$\text{proj}(\text{yield}(\lambda)) = \text{yield}(\text{proj}(\lambda)).$$

□

Now, we generalise to monomial trees the notion of labellings of monomials we defined in Section 3. A monomial tree $\lambda$ over a product alphabet $(\mathbb{A}/\mathbb{B})$ is a $\mathbb{B}$-labelling of a monomial tree $t$ over $A$ if $\text{proj}(\lambda) = t$, every internal node of $\lambda$ is labelled by a label of the form $C^*$ with $C = (\mathbb{A}_0)$ (i.e. the second coordinate is the full alphabet $\mathbb{B}$), and every leaf of $\lambda$ is labelled by either a letter of the form $(a/b) \in (\mathbb{A}/\mathbb{B})$ or by the formal star $C^*$ of some functional alphabet $C \subseteq (\mathbb{A}/\mathbb{B})$.

Thus, the only freedom when defining a $\mathbb{B}$-labelling of a monomial tree $t$ is when choosing labels of the leaves of $t$, as summarised by the following fact.

**FACT 4.8.** Let $t$ be a monomial tree over $A$, with yield($t$) being a monomial $P$ over $A$. The operation $\lambda \mapsto \text{yield}(\lambda)$ is a bijection between $\mathbb{B}$-labellings $\lambda$ of $t$ and $\mathbb{B}$-labellings $M$ of $P$. □

If the monomial tree $t$ is moreover a split tree, then we naturally say that $\lambda$ is a $\mathbb{B}$-labelling of a split tree over $A$. Such labellings are the crucial objects used in our characterisation. As the following example shows, $\lambda$ is not necessarily a split tree itself.

**EXAMPLE 4.9.** The already mentioned Figure 1 depicts on the right side a $(\mathbb{B} = \{b_0, b_1, b_2\})$-labelling $\lambda$ of the split tree $t$. The children of the root of $\lambda$ form the word

$$M = \mathbf{0}^* \cdot \binom{a_0}{b_0} \cdot \binom{\{a_0\}}{\{b_0, b_1, b_2\}}^* \cdot \binom{a_0}{b_0} \cdot \mathbf{0}^*,$$

which is a monomial over $(\mathbb{A}/\mathbb{B})$, but not a split (the subalphabet in the middle is too big, in a split it should be $\{(\mathbb{A}_0)\}$). Hence, $\lambda$ is not a split tree over $(\mathbb{A}/\mathbb{B})$.

However, the monomial

$$\text{yield}(\lambda) =$$

$$\mathbf{0}^* \cdot \binom{a_0}{b_0} \cdot \mathbf{0}^* \cdot \binom{a_0}{b_1} \cdot \binom{\{a_0\}}{\{b_2\}}^* \cdot \binom{a_0}{b_1} \cdot \mathbf{0}^* \cdot \binom{a_0}{b_0} \cdot \mathbf{0}^*$$

is indeed a $\mathbb{B}$-labelling of yield($t$). □

# 5 SPLIT THEOREM

In this section, we show a strong link between unambiguous monomials and yields of split trees, stated in the following theorem:

**THEOREM 5.1 (SPLIT THEOREM).** As a language, any functional and unambiguous monomial over a product alphabet $(\mathbb{A}/\mathbb{B})$ is a finite union of yields of $\mathbb{B}$-labellings of split trees over $A$.

Our main characterisation of uniformisability will rely on this split theorem (see also [5]), but before proving it, let us observe the following one-dimensional variant:

**COROLLARY 5.2.** As a language, any unambiguous monomial over $A$ is a finite union of yields of split trees over $A$.

**PROOF.** It is enough to consider a single-letter alphabet $\mathbb{B} = \{b_0\}$ and apply Theorem 5.1 in a straightforward way. □

We believe that this particular corollary may be of a separate interest, and help in the comprehension of the logic FO$^2$[$<$]. Indeed, while unambiguous monomials do not form a regular language of words (see Remark 3.9), split trees do form a regular language of finite trees. For this reason, some problems related to languages of words definable in FO$^2$[$<$] may be solved via the theory of regular languages of trees, see the discussion in Section 7.

## 5.1 Factorising monomials

Let $N = \mathbb{D}_0^* \cdot d_0 \cdot \mathbb{D}_1^* \cdots \mathbb{D}_{m-1}^* \cdot d_{m-1} \cdot \mathbb{D}_m^*$ and $P = A_0^* \cdot a_0 \cdot A_1^* \cdots A_{n-1}^* \cdot a_{n-1} \cdot A_n^*$ be two monomials over an alphabet $A$. A decomposition of $N$ with respect to $P$ is a sequence of monomials $(N_i)_{i \le n}$ such that each $N_i$, for $i \le n$, is over the alphabet $A_i$, and moreover $N$ can be written as the concatenation $[N_0] \cdot a_0 \cdot [N_1] \cdots [N_{n-1}] \cdot a_{n-1} \cdot [N_n]$.

<footnote>$^{\dagger}$Here again, the considered labelling set is $L(\mathbb{A}/\mathbb{B})$.</footnote>
We usually represent a decomposition using the bracket notation as above. The width of such a decomposition is the maximal length of the monomials $N_i$. We say that P factors N if there exists any decomposition of N with respect to P.

FACT 5.3. If P factors N then $N \subseteq P$, as languages. □

LEMMA 5.4. If P is unambiguous then there is at most one decomposition of N with respect to P.

PROOF. Two distinct decompositions of N with respect to P would imply two distinct decompositions of the word $d_0 \cdot d_1 \cdots d_{m-1}$ with respect to P, which would violate unambiguity of P. □

Thus, for an unambiguous monomial P which factors N, we will speak about the (unique) decomposition of N with respect to P.

LEMMA 5.5. If M is a B-labelling of an unambiguous monomial P which factors some monomial N, then there exists a unique B-labelling M' of N such that (treated as languages) $M' \subseteq M$.

Moreover, this B-labelling M' satisfies

$$M' = M \cap (\mathbb{N}_{\mathbb{B}^*}).$$

This lemma is a rather straightforward application of Fact 3.5 to each of the monomials from a decomposition of N with respect to P.

## 5.2 Shrinking decompositions

The following lemma is the crucial inductive step in the proof of Theorem 5.1.

LEMMA 5.6. Assume that P is an unambiguous monomial over A and S is a split over A. Assume that the length of P is greater than 1, i.e. it has at least one distinguished letter. Then there exists a finite set of monomials U such that the union of their languages equals P ∩ S and moreover, if $N \in U$ then:

* P factors N,

* S factors N,

* the width of the decomposition of N with respect to S is strictly smaller than the length of P.

The main idea of the proof is to see a monomial $A_0^* \cdot a_0 \cdots a_{n-1} \cdot A_n^*$ as a linearly ordered automaton with states $\{0, \dots, n\}$, transitions of the form $(i, a_i, i+1)$ for $i < n$, and looping transitions $(i, a, i)$ for $a \in A_i$ with $i \le n$.

Thus, we get two such automata: A for P and B for S. Then, we apply the classical product construction to obtain a partially ordered automaton C recognising the language $P \cap S$. Unambiguity of P and S guarantees that all three automata A, B, and C are unambiguous (i.e. each word in the language admits a unique accepting run). Now, since C is partially ordered, we can represent its language as a finite union of languages of unambiguous linearly ordered automata, i.e. unambiguous monomials.

An example of these automata is depicted on Figure 2. The automaton A corresponds to the monomial $P = \{a\}^* \cdot a \cdot \{b, c\}^* \cdot a \cdot \{a, b\}^*$, while B corresponds to the split $S = \emptyset^* \cdot a \cdot \{a\}^* \cdot b \cdot \{a\}^* \cdot a \cdot \emptyset^*$. Note that the monomial P is ambiguous, which violates the assumptions of Lemma 5.6.

The middle part of Figure 2 depicts the product automaton C. Its states are pairs of states and transitions are synchronised pairs of

<figure><img src="image_4.png" /><figcaption>Figure 2: An illustration of two linearly ordered automata A, B together with their product (the automaton C in the proof). The boldfaced sequence of transitions forms one of the full sequences in C.</figcaption></figure>

transitions of the two automata. The language of C is the language $P \cap S$. This language can be represented as a union ranging over possible ways (called full sequences) of going from the initial to the final state of C. Note that there are six such full sequences here: we may visit the state (1, 0) or go directly to (1, 1), and then, from (1, 1) there are three ways of reaching (3, 2).

Each of these six full sequences provides a monomial which is factored by both P and S. Consider the full sequence which is boldfaced, it goes through both states (1, 0) and (1, 2). It provides the monomial:

$$N = \emptyset^* \cdot a \cdot \{a\}^* \cdot a \cdot \emptyset^* \cdot a \cdot \{a\}^* \cdot b \cdot \{a\}^* \cdot a \cdot \emptyset^*.$$

The induced decomposition of N with respect to S has the form:

$$N = [\emptyset^*] \cdot a \cdot [\{a\}^* \cdot a \cdot \emptyset^* \cdot a \cdot \{a\}^*] \cdot b \cdot [\{a\}^*] \cdot a \cdot [\emptyset^*].$$

Its width is 5 because of the second monomial, between a and b. This coincides with the length of P, contradicting the last item in the statement of Lemma 5.6 (remember that P is not unambiguous).

However, the monomial N witnesses the fact that all the distinguished letters (here only a) of P must appear in the respective second subalphabet {a} of S. Due to the definition of a split, this means that all these letters must appear both before and after this subalphabet in S (here this are the first and the last distinguished letter a in S). Thus, due to the nature of transitions of C, all these letters must belong to both the first and the last subalphabet of P (it is witnessed by the first and the last transition on the boldfaced full sequence). Thus, we get a contradiction with unambiguity of P due to the following simple fact.

FACT 5.7. Assume that $P = \mathbb{D}_0^* \cdot d_0 \cdot \mathbb{D}_1^* \cdots \mathbb{D}_{m-1}^* \cdot d_{m-1} \cdot \mathbb{D}_m^*$ is a monomial of length strictly greater than 1 such that

$$\mathbb{D} = \{d_0, \dots, d_{m-1}\}$$
is contained in both $D_0$ and $D_m$. Then $P$ is ambiguous (i.e. not unambiguous). □

PROOF. Put $w' = d_0 \cdot d_1 \cdots d_{m-1}$ and let $w = w' \cdot w'$. The inclusion $D \subseteq D_0 \cap D_m$ guarantees that $w' \in D_0^*$ and $w' \in D_m^*$. We know that $m > 0$ and therefore $w' \neq \epsilon$. The word $w$ has at least two distinct decompositions with respect to $P$:

$$ w = w' \cdot d_0 \cdot \epsilon \cdot d_1 \cdots \epsilon \cdot d_{m-1} \cdot \epsilon, \\ w = \epsilon \cdot d_0 \cdot \epsilon \cdot d_1 \cdots \epsilon \cdot d_{m-1} \cdot w', $$

which implies that $P$ cannot be unambiguous. □

## 5.3 Proof of the split theorem

Now, we move to a proof of the split theorem. The proof is inductive over the length of the monomial $M$. Recall that such a length is always an odd natural number.

We begin with the basic case, when the length of $M$ is 1. In that case, $M = C^*$, for some subalphabet $C \subseteq (\mathbb{A}/\mathbb{B})$ which, by Fact 3.4, is functional. Thus, the following claim proves the split theorem in this case.

CLAIM 5.8. If $C \subseteq (\mathbb{A}/\mathbb{B})$ is a functional subalphabet, then $C^*$ is a finite union of yields of B-labellings of split trees over $A$.

PROOF. Let us define $A_0$ as the projection of $C$ onto $A$. Apply Corollary 3.12 to write $A_0^*$ as a finite union $\cup_{i<i} P_i$ of splits over $A_0$.

Consider any of these splits $P_i$, for $i < I$. The fact that $C$ is functional allows us to find a unique $B$-labelling $M_i$ of $P_i$ such that $M_i \subseteq C^*$. This guarantees that $\cup_{i<i} M_i = C^*$.

At the same time, Fact 4.4 implies that there is a split tree $t_i$ such that $\text{yield}(t_i) = P_i$. We can then transfer the labelling $M_i$ from $P_i$ to $t_i$ by Fact 4.8 to obtain a $B$-labelling $\lambda_i$ of the split tree $t_i$. Thus, $\cup_{i<i} \text{yield}(\lambda_i)$ is a representation of $C^*$ as in the statement. □

We now move to the induction step. Assume that the thesis of Theorem 5.1 holds for every monomial of length at most $2n$ for some $n > 0$. Let $M$ be a functional unambiguous monomial over a product alphabet $(\mathbb{A}/\mathbb{B})$, of length $2n+1$, whose projection onto $A^*$ is $P$. From Proposition 3.6, $M$ is a $B$-labelling of $P$, which is unambiguous.

Consider a split $S$ over $A$. Our goal is to show that the language $M \cap (\mathbb{S}/\mathbb{B}^*)$ is a finite union of yields of $B$-labellings of split trees over $A$. This suffices to conclude the proof because it is enough to take the union over the finitely many possible splits $S$.

Apply Lemma 5.6 to $P$ and $S$ to get a set of monomials $\mathcal{U}$ such that $\cup_{N \in \mathcal{U}} N = P \cap S$.

Take any monomial $N \in \mathcal{U}$. Use the fact that $P$ factors $N$ to apply Fact 5.5, which gives a $B$-labelling $M'$ of $N$ such that the language of $M'$ is $M \cap (\mathbb{N}/\mathbb{B}^*)$. We will show that $M'$ is a finite union of yields of $B$-labellings of split trees over $A$. Again, taking union of these representations ranging over all $N \in \mathcal{U}$ will give us a representation of $M \cap (\mathbb{S}/\mathbb{B}^*)$ and thus conclude the proof.

We will now use the fact that $S$ factors $N$. Decompose $N$ with respect to $S$ and apply the same decomposition to $M'$:

$$ \begin{aligned} S &= A_0^* \cdot a_0 \cdot A_1^* \cdots A_{d-1}^* \cdot a_{d-1} \cdot A_d^*, \\ N &= [N_0] \cdot a_0 \cdot [N_1] \cdots [N_{d-1}] \cdot a_{d-1} \cdot [N_d], \\ M' &= [M'_0] \cdot c_0 \cdot [M'_1] \cdots [M'_{d-1}] \cdot c_{d-1} \cdot [M'_d], \end{aligned} $$

where the above decomposition of $M'$ satisfies that for every $i \le d$ the monomial $M'_i$ is a $B$-labelling of $N_i$ and for every $i < d$ the letter $a_i$ is the projection of the letter $c_i$.

Moreover, for $i \le d$, we know that $N_i$ is a monomial over $A_i$ and therefore $M'_i$ is a monomial over $(\mathbb{A}/\mathbb{B})$. Lemma 5.6 guarantees that for each $i \le d$ the monomial $N_i$ (and therefore also $M'_i$) has length strictly smaller than the length of $P$, i.e. $2n+1$.

The induction hypothesis of our proof of the split theorem tells us that for every $i \le d$, the language of the monomial $M'_i$ over $(\mathbb{A}/\mathbb{B})$ can be represented as a finite union of yields of $B$-labellings of split trees over $A_i$. Let us denote this set of labellings by $\mathcal{U}_i$.

For each $\vec{\lambda} = (\lambda_0, \dots, \lambda_d) \in \mathcal{U}_0 \times \dots \times \mathcal{U}_d$, define:

$$ \Lambda_{\vec{\lambda}} := (\mathbb{A}/\mathbb{B})^* [\lambda_0, c_0[ ], \lambda_1, c_1[ ], \dots, c_{d-2}[ ], \lambda_{d-1}, c_{d-1}[ ], \lambda_d[ ]]. $$

For each $i \le d$, let $t_i = \text{proj}(\lambda_i)$. Our assumptions guarantee that $t_i$ is a split tree over $A_i$. Notice that $\Lambda_{\vec{\lambda}}$ is a $B$-labelling of the tree

$$ T_i := A^* [t_0, a_0[ ], t_1, a_1[ ], \dots, a_{d-2}[ ], t_{d-1}, a_{d-1}[ ], t_d]. $$

The tree $T_i$ is the composition of $t_0, \dots, t_d$ under the split $S$, as defined in Subsection 4.2. Therefore, it is a split tree. This means that $\Lambda_{\vec{\lambda}}$ is a $B$-labelling of a split tree.

Finally, we notice that there are finitely many choices of such tuples $\vec{\lambda} \in \mathcal{U}_0 \times \dots \times \mathcal{U}_d$ and moreover, the yields of all the trees $\Lambda_{\vec{\lambda}}$ sum up to the language of the monomial $M'$. Thus, the proof of the split theorem is concluded.

## 5.4 Singleton trees

Our characterisation uses split trees not only to represent languages but also single words. This motivates the following definition: a monomial tree $t$ is singleton if its yield is singleton as a set (i.e. contains a single word).

FACT 5.9. A monomial tree $t$ is singleton if and only if all its leaves are labelled either by single letters or by $\emptyset^*$. □

The following lemma is an application of the split theorem.

LEMMA 5.10. For every word $w \in A^*$, there exists a split tree $t$ over $A$ such that $\text{yield}(t) = \{w\}$ (i.e. $t$ is a singleton tree).

Analogously, for every word $(w^\sigma) \in (\mathbb{A}/\mathbb{B})$ there exists a singleton $B$-labelling of a split tree over $A$ such that the yield of this labelling equals $\{(w^\sigma)\}$.

PROOF. Consider $w = a_0 \cdots a_{n-1}$ and take the monomial:

$$ P = \emptyset^* \cdot a_0 \cdot \emptyset^* \cdots \emptyset^* \cdot a_{n-1} \cdot \emptyset^*. $$

Clearly $P$ is unambiguous and its language is $\{w\}$. Apply Corollary 5.2 to represent $P$ as a finite union of yields of split trees. Take as $t$ any tree from this union. Since the yield of every split tree is non-empty as a language, $\text{yield}(t) = \{w\}$.

Now, given $(w^\sigma) \in (\mathbb{A}/\mathbb{B})$ with $(w^\sigma) = (a_0^{a_0} \cdots a_{b_0}^{a_{b_0-1}})$ we can apply Theorem 5.1 to the functional unambiguous monomial

$$ M = \emptyset^* \cdot (a_0^{a_0} \cdot \emptyset^* \cdots \emptyset^* \cdot (a_{b_0-1}^{a_{b_0-1}}) \cdot \emptyset^*. $$

In the same way as above, any of the obtained labellings must satisfy the thesis. □
Now, if we take a singleton split tree $t_1$ over $\mathcal{A}$ such that $\text{yield}(t_1) = \{w\}$, then Proposition 4.6 characterises the split trees $t_2$ such that $w \in \text{yield}(t_2)$ as precisely those such that $t_2 \subseteq_{\text{pref}} t_1$. We now prove a similar result for singleton labellings.

**LEMMA 5.11.** Let $\lambda_1$ be a singleton $\mathcal{B}$-labelling of a split tree over $\mathcal{A}$, whose yield consists of a single word $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})^*$. Let $\lambda_2$ be any $\mathcal{B}$-labelling of a split tree over $\mathcal{A}$.

Then $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in \text{yield}(\lambda_2)$ if and only if $\text{proj}(\lambda_2) \subseteq_{\text{pref}} \text{proj}(\lambda_1)$ and for every leaf $u$ of $\lambda_2$, the following two conditions hold:

* if $u$ is labelled by a letter $(\begin{smallmatrix} a \\ b \end{smallmatrix})$ in $\lambda_2$, then $u$ must be a leaf of $\lambda_1$ labelled by the same letter $(\begin{smallmatrix} a \\ b \end{smallmatrix})$,

* if $u$ is labelled by $\mathcal{C}^*$ in $\lambda_2$ for some functional alphabet $\mathcal{C} \subseteq (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})$, then for every leaf $u'$ $\supseteq u$ in $\lambda_1$ either $\lambda_1(u') = \emptyset^*$ or $\lambda_1(u')$ is of the form $(\begin{smallmatrix} a \\ b \end{smallmatrix})$ with $(\begin{smallmatrix} a \\ b \end{smallmatrix}) \in \mathcal{C}$.

**PROOF.** First assume that $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in \text{yield}(\lambda_2)$. This means in particular that $w \in \text{yield}(\text{proj}(\lambda_2))$, which implies that $\text{proj}(\lambda_2) \subseteq_{\text{pref}} \text{proj}(\lambda_1)$ by Proposition 4.6. Moreover, the leaves of $\lambda_2$ need to preserve the labelling as in $\lambda_1$, which implies the two above conditions.

Now assume that $\text{proj}(\lambda_2) \subseteq_{\text{pref}} \text{proj}(\lambda_1)$ and the two conditions above. Then it immediately gives us a decomposition of the monomial yield($\lambda'$) which witnesses that $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in \text{yield}(\lambda')$. $\square$

# 6 UNIFORMISING IN FO<sup>2</sup>

We can finally move to the proof of the main theorem.

**THEOREM 6.1.** There exists an algorithm that inputs a formula $\varphi$ in MSO$[<, (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})]$, $\mathcal{A}$ and $\mathcal{B}$ being any alphabets, and outputs a formula $\psi$ in FO<sup>2</sup>$[<, (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})]$ such that the relation $\mathcal{L}(\psi)$ uniformises the relation $\mathcal{L}(\varphi)$ if there exists one, and outputs NO in the opposite case.

The rest of this section is devoted to a proof of this theorem. Assume that $\varphi$ together with $\mathcal{A}$ and $\mathcal{B}$ are given. We begin by performing some preliminary computations.

We first apply Fact 2.1 to compute the projection $P = \text{proj}(R)$. This projection is again a regular language and we can apply Theorem 3.2 to check if it is definable in FO<sup>2</sup>$[<, \mathcal{A}]$. If it is not, then we terminate our procedure with output NO: indeed, if $R$ did admit a uniformisation $F$ definable in FO<sup>2</sup>$[<, (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})]$, then the projection of $R$ would be equal to that of $F$, definable in FO<sup>2</sup>$[<, \mathcal{A}]$ by Corollary 3.8.

For the rest of this section assume that $P$ is definable in FO<sup>2</sup>$[<, \mathcal{A}]$. In this case, we can reformulate the existence of a uniformisation in terms of labellings of split trees:

**LEMMA 6.2.** Under the above assumptions, the relation $R$ admits a uniformisation definable in FO<sup>2</sup>$[<, (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})]$ if and only if there exists a finite sequence $\vec{\lambda} = (\lambda_j)_{j<J}$ of $\mathcal{B}$-labellings of split trees over $\mathcal{A}$ such that:

(1) for every $j < J$ we have $\text{yield}(\lambda_j) \subseteq R$,

(2) for every word $w \in P$ there exists $j < J$ such that we have $w \in \text{yield}(\text{proj}(\lambda_j))$.

In the if direction, a formula $\psi(\vec{\lambda})$ defining such a uniformisation can be effectively computed based on $\vec{\lambda}$.

**PROOF.** First, assume that there exists a uniformisation $F$ of $R$ that is definable in FO<sup>2</sup>$[<, (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})]$. Theorem 3.2 means that $F$ is a finite union of unambiguous monomials over $(\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})$. Since $F$ is a

uniformisation, each of these monomials is functional. Thus, Theorem 5.1 applied to each of the monomials separately implies that $F$ can be written as a finite union of yields of $\mathcal{B}$-labellings of split trees over $\mathcal{A}$. Let $\lambda_0, \dots, \lambda_{J-1}$ be the sequence of these labellings.

Clearly, for every $j < J$ we have $\text{yield}(\lambda_j) \subseteq F \subseteq R$. Thus, the first item of the lemma holds. Now consider any word $w \in P$. Since $w \in \text{proj}(F)$, we know that there exists $j < J$ such that $w \in \text{proj}(\text{yield}(\lambda_j))$, which coincides with $\text{yield}(\text{proj}(\lambda_j))$ by Fact 4.7. Therefore, the sequence $(\lambda_j)_{j<J}$ satisfies the conditions of the lemma.

Now, we assume, conversely, that such a sequence $\vec{\lambda} = (\lambda_j)_{j<J}$ exists, and we construct a uniformisation $F$ of $R$ from it. Take $j < J$ and consider the monomials $M_j = \text{yield}(\lambda_j)$ and $P_j = \text{yield}(\text{proj}(\lambda_j))$. From Lemma 4.5, we know that $P_j$ is unambiguous. Since $M_j$ is a $\mathcal{B}$-labelling of $P_j$, Proposition 3.6 guarantees that $M_j$ is functional and unambiguous.

For each $j < J$ Theorem 3.2 applied to $M_j$ and $P_j$ gives us two formulae of FO<sup>2</sup>$[<]: a formula $\psi_{M,j}$ over $(\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})$ defining the language of $M_j$, and a formula $\psi_{P,j}$ over $\mathcal{A}$ defining the language of $P_j$. Let $\psi'_{P,j}$ be a variant of $\psi_{P,j}$ rewritten over the alphabet $(\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})$: whenever $\psi_{P,j}$ tests a letter $a \in \mathcal{A}$ then $\psi'_{P,j}$ checks a disjunction of all the letters $(\begin{smallmatrix} a \\ b \end{smallmatrix})$ for $b \in \mathcal{B}$. The point is simply to add a second coordinate: any pair $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix})$ satisfies $\psi'_{P,j}$ if and only if $w$ satisfies $\psi_{P,j}$, i.e. when $w \in P_j$.

Consider now the following formula

$$ \psi(\vec{\lambda}) := \bigvee_{j<j} \left( \psi_{M,j} \wedge \bigwedge_{j'<j} \neg \psi'_{P,j'} \right). $$

It is clear that $\psi(\vec{\lambda})$, as a Boolean combination of the previous formulae, is also a formula of FO<sup>2</sup>$[<, (\begin{smallmatrix} \mathcal{A} \\ \mathcal{B} \end{smallmatrix})]$. We claim that $F$, the language of $\psi(\vec{\lambda})$, is a uniformisation of $R$.

First, let $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in F$. Then $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in M_j$ for some $j < J$ and therefore $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in M_j = \text{yield}(\lambda_j) \subseteq R$. This means that $F \subseteq R$.

To see that $F$ is functional and of domain $P$, consider any word $w \in P$. Let $j_w < J$ be the minimal such that $w \in \text{yield}(\text{proj}(\lambda_{j_w})) = P_{j_w}$. By the construction of $\psi(\vec{\lambda})$, a word $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix})$ belongs to $F$ if and only if it belongs to $M_{j_w}$. Thus, by functionality of $M_{j_w}$ we know that there is precisely one word $\sigma$ such that $(\begin{smallmatrix} w \\ \sigma \end{smallmatrix}) \in F$. Therefore, $F$ is functional. Thus, we constructed a uniformisation of $R$. $\square$

Now, Theorem 3.2 and Corollary 5.2 tell us that we can write the language $P$ as a union of yields of split trees over $\mathcal{A}: P = \bigcup_{i \le I} \text{yield}(t_i^P)$.

Using these split trees, we can reformulate the above requirement in a statement $\Psi_R$ which is directly expressible in MSO over the $\omega$-branching tree. The $\omega$-branching tree consists of the infinite set $\mathbb{N}^*$ of finite words over $\mathbb{N}$, structured as a tree in a way similar to what we proposed in Section 4. The crucial point here is that it is decidable whether a given MSO formula over the $\omega$-branching tree is satisfied.
LEMMA 6.3. The relation $R$ admits a uniformisation definable in FO$^2$[<, ($\mathbb{A}_B$)] if and only if the following condition $\Psi_R$ holds:

$$ \Psi_R := \exists D \subseteq \mathbb{N}^* \cdot |D| < \infty \wedge \forall w \in A^* \cdot \left( \bigvee_{i < I} w \in \text{yield}(t_i^P) \right) \Rightarrow \quad (1) $$

$$ \exists \lambda \in \text{splits}(A \to \mathbb{B}), \text{Nodes}(\lambda) \subseteq D. $$

$$ (w \in \text{yield}(\text{proj}(\lambda))) \wedge \quad (2) $$

$$ \left( \forall (w'_{\sigma'}) \in (\mathbb{A}_B)^* \cdot (w'_{\sigma'}) \in \text{yield}(\lambda) \Rightarrow (w'_{\sigma'}) \in R \right) \quad (3) $$

where splits($A \to \mathbb{B}$) stands for the set of all $\mathbb{B}$-labellings of split trees over $A$.

For every fixed finite set $D \subseteq \mathbb{N}^*$ there is only finitely many labellings $\lambda$ such that $\text{Nodes}(\lambda) \subseteq D$. Therefore, the condition $\Psi_R$ is equivalent to the requirements of Lemma 6.2.

Thus, to conclude the proof of Theorem 6.1 it is enough to observe the following lemma.

LEMMA 6.4. Assume that we are given two alphabets $A$ and $B$, a regular relation $R \subseteq (\mathbb{A}_B)^*$, and the projection $P = \text{proj}(R)$ of $R$ represented as $P = \bigcup_{i < I} \text{yield}(t_i^P)$, for a finite sequence $(t_i^P)_{i < I}$ of split trees over $A$.

Then the condition $\Psi_R$ from Lemma 6.3 can be effectively decided. Moreover, if it holds, then a finite sequence $(\lambda_j)_{j < J}$ of $\mathbb{B}$-labellings of split trees over $A$ can be effectively constructed in such a way that this sequence satisfies the conditions of Lemma 6.2.

The proof of this lemma relies on the fact that the whole condition $\Psi_R$ can be expressed in Monadic Second-Order Logic over the $\omega$-branching tree $\mathbb{N}^*$. More precisely:

(1) MSO allows for quantification over subsets $D$ of the domain $\mathbb{N}^*$ and finiteness is definable over the $\omega$-branching tree;

(2) by quantifying over tuples of sets, we can simulate quantification over labellings of $\mathbb{N}^*$ by some labelling set $\mathcal{L}$, which allows us to quantify over e.g. finite trees;

(3) instead of quantifying over words $w \in A^*$ and $(w_\sigma) \in (\mathbb{A}_B)^*$ we can use Fact 5.9 and Lemma 5.10 to quantify over singleton split trees and singleton labellings of split trees;

(4) checking if $w \in \text{yield}(t)$ can be done using Proposition 4.6;

(5) checking if $(w_\sigma) \in \text{yield}(\lambda)$ can be done using Lemma 5.11;

(6) checking if $(w_\sigma) \in R$ can be done by interpreting the formula defining $R$ over the leaves of the singleton tree representing $(w_\sigma)$.

Note that the above lemma concludes the decidability part of the proof of Theorem 6.1 — it is enough to verify if the constructed formula of MSO holds. For the constructive part, we can apply again Lemma 6.4 to obtain a sequence $\tilde{\lambda} = (\lambda_j)_{j < J}$. Since it satisfies the conditions of Lemma 6.2, the formula $\psi(\tilde{\lambda})$ constructed there is a formula of FO$^2$[<, ($\mathbb{A}_B$)] which defines a uniformisation of $R$.

## Complexity

The proof of Theorem 6.1 given above is optimised for readability, thus we assume that both the input and output languages are represented as formulae of MSO[<, ($\mathbb{A}_B$)] and FO$^2$[<, ($\mathbb{A}_B$)] respectively. This approach does not give any reasonable computational complexity bounds on the claimed algorithm. However, one can work with more verbose representations of regular languages, like finite automata. Then, the characterisation given in Theorem 3.2 becomes elementary in the size of an automaton representing $L$. Finally, the fact that the quantifier alternation of the formula $\Psi_R$ from Lemma 6.3 does not depend on $R$, implies the following corollary:

COROLLARY 6.5. The algorithm provided in Theorem 6.1 is in fact elementary in the size of an automaton recognising the given regular language $R$.

## 7 CONCLUSIONS

This paper effectively characterises uniformisability of regular relations in the well-known fragment of FO$^2$[<]. In [10, Theorem 2.32] the author provides a similar result for the logic of FO with only letter predicates. Together with a characterisation of uniformisability in MSO over bi-infinite words [7], these are the only known characterisations of uniformisability.

The algorithms given in the paper are all of elementary$^{‡}$ (although high) complexity. This high complexity comes from the fact that, when dealing with uniformisations, one needs to merge together the syntactic (or algebraic) characterisation of the given class of languages, with the semantic (pointwise) condition of being a uniformisation.

We hope that the techniques presented above can be used to consider other logic fragments which interact with polynomials. Just to cite a few: the languages definable in linear temporal logic with only the “eventually” modality are characterised by deterministic polynomials (a condition stronger than unambiguous), while the class $\Sigma_2$[<] is known to be equivalent to (possibly ambiguous) polynomial languages (see e.g. [6]). This fragment $\Sigma_2$[<] sits at the level $1 + \frac{1}{2}$ of the Straubing-Thérien hierarchy, where each next non-integer level consists of Boolean combinations of languages in the current level. Since polynomials are involved in the definition, it may be that our techniques prove useful in approaching uniformisation problems for the further levels of the hierarchy.

Another property on which our approach crucially relies is the fact that FO$^2$[<] is closed under projections when restricted to functional relations (basically Proposition 3.6). One direction of research could be to try to solve the uniformisation problem for other formalisms sharing this property. However, such fragments cannot be very expressive, as already the fragment FO$^2$[S] (First-Order Logic with the successor relation and only two variables) can express accepting runs of deterministic automata, thus with projections of its functional relations we already get all of the regular languages.

The ultimate goal would be to decide a variant of Problem 1.1 for MSO over infinite trees. However, it seems to be out of reach for the moment: there exists a particular regular relation over infinite trees (namely choice over thin trees), whose (non)uniformisability in MSO is an open problem [1]. From this perspective, the provided

<footnote>†If $R$ is given by an automaton, then one can express existence of an appropriate accepting run.</footnote>

<footnote>‡If the input relation is given, e.g. as an automaton.</footnote>
results can be seen as preliminary steps in our understanding of Problem 1.1.

Moreover, we believe that the interest of this work goes beyond the problem of uniformisability. The point is that the split theorem provides a new perspective on the expressive power of FO²[<]: the split trees.

The latter result can be applied to a number of different questions. In particular, it directly entails a result from [11], where the authors solve the following separability problem: given two disjoint regular languages $L_1$ and $L_2$, is there a language $L$ definable in FO²[<] that separates $L_1$ from $L_2$, i.e. that contains $L_1$ but yet does not intersect with $L_2$? To see this entailment, one can write an analogue of the condition $\Psi_R$ from Lemma 6.3 as follows, where $L_1, L_2 \subseteq A^*$:

$$ \Psi_{L_1 \perp L_2} := \exists D \subseteq \mathbb{N}^*, |D| < \infty. \quad (4) $$

$$ \forall w \in L_1. \quad (5) $$

$$ \exists t \in \text{splits}(A), \text{Nodes}(t) \subseteq D. \quad (6) $$

$$ (\forall w' \in A^*. w' \in \text{yield}(t) \Rightarrow w' \notin L_2) \quad (7) $$

Indeed, suppose that $L$ is such a separator, definable in FO²[<]. By Corollary 5.2, $L$ is the yield of a finite union $\cup_{i<i} t_i$ of split trees. Since $L \cap L_2 = \emptyset$, no word $w \in t_i$ can belong to $L_2$, and, if we define $D$ as the union $\cup_{i<i} \text{Nodes}(t_i) \subseteq \mathbb{N}^*$, we get the above formula satisfied.

Reciprocally, if there exists a finite set $D \subseteq \mathbb{N}^*$ that makes $\Psi_{L_1 \perp L_2}$ hold, then we can define the separator $L$ to be the union of yields of split trees $t$ over $A$, with domains contained in $D$, that additional satisfy conditions (6) and (7).

We believe that the above technique can work for other, similar problems about FO²[<].

## REFERENCES

[1] Marcin Bilkowski and Michał Skrzypczak. 2013. Unambiguity and Uniformization Problems on Infinite Trees. In CSL (LIPIcs, Vol. 23). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 81–100. https://doi.org/10.4230/LIPIcs.CSL.2013.81

[2] Julius Richard Büchi and Lawrence H. Landweber. 1969. Solving Sequential Conditions by Finite State Strategies. Department of Computer Science Technical Reports 138, 88 (1969).

[3] Arnaud Carayol and Christof Löding. 2007. MSO on the Infinite Binary Tree: Choice and Order. In CSL. 161–176.

[4] Arnaud Carayol, Christof Löding, Damian Niwiński, and Igor Walukiewicz. 2010. Choice Functions and Well-Orderings over the Infinite Binary Tree. Central European Journal of Mathematics 8 (2010), 662–682.

[5] Jean-Claude Van Damme. 2013. The Epic Split. Youtube. https://www.youtube.com/watch?v=M7Flvfx5j10

[6] Volker Diekert, Paul Gastin, and Manfred Kufleitner. 2008. A Survey on Small Fragments of First-Order Logic over Finite Words. Int. J. Found. Comput. Sci. 19, 3 (2008), 513–548. https://doi.org/10.1142/S0129054108005802

[7] Grzegorz Fabiański, Michał Skrzypczak, and Szymon Toruńczyk. 2020. Uniformisations of Regular Relations over Bi-Infinite Words. In LICS. ACM, 384–396. https://doi.org/10.1145/3373718.3394782

[8] Yuri Gurevich and Saharon Shelah. 1983. Rabin's Uniformization Problem. J. Symb. Log. 48, 4 (1983), 1105–1119. https://doi.org/10.2307/2273673

[9] Vincent Michielini. 2018. Uniformization Problem for Variants of First Order Logic over Finite Words. In DLT (Lecture Notes in Computer Science, Vol. 11088). Springer, 516–528. https://doi.org/10.1007/978-3-319-98654-8_42

[10] Vincent Michielini. 2022. Uniformisation and Choice Questions for Regular Languages. Ph. D. Dissertation. University of Warsaw.

[11] Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. 2013. Separating Regular Languages by Piecewise Testable and Unambiguous Languages. In MFCS (Lecture Notes in Computer Science, Vol. 8087), Krishnendu Chatterjee and JiriSGall (Eds.). Springer, 729–740.

[12] Michael Oser Rabin. 1969. Decidability of Second-Order Theories and Automata on Infinite Trees. Trans. Amer. Math. Soc. 141 (1969), 1–35.

[13] Alexander Rabinovich and Amit Shomrat. 2008. Selection and Uniformization Problems in the Monadic Theory of Ordinals: A Survey. In Pillars of Computer Science. 571–588.

[14] Marcel-Paul Schützenberger. 1965. On finite monoids having only trivial subgroups. Information and Control 8, 2 (1965), 190–194.

[15] Thomas Schwentick, Denis Thérien, and Heribert Vollmer. 2001. Partially-Ordered Two-Way Automata: A New Characterization of DA. In Developments in Language Theory, 5th International Conference, DLT 2001, Vienna, Austria, July 16-21, 2001, Revised Papers (Lecture Notes in Computer Science, Vol. 2295), Werner Kuich, Grzegorz Rozenberg, and Arto Salomaa (Eds.). Springer, 239–250. https://doi.org/10.1007/540-46011-X_20

[16] Dirk Siefkes. 1975. The recursive sets in certain monadic second order fragments of arithmetic. Arch. Math. Logik 17, 1–2 (1975), 71–80.

[17] Wolfgang Thomas. 2009. Facets of Synthesis: Revisiting Church's Problem, Vol. 5504. 1–14. https://doi.org/10.1007/978-3-642-00596-1_1

[18] Denis Thérien and Thomas Wilke. 1998. Over Words, Two Variables Are as Powerful as One Quantifier Alternation. In Proceedings of the 30th Annual ACM Symposium on Theory of Computing. ACM, 234–240. https://doi.org/10.1145/276698.276749

[19] Philipp Weis and Neil Immerman. 2007. Structure Theorem and Strict Alternation Hierarchy for FO2 on Words. In Computer Science Logic. Springer Berlin Heidelberg, 343–357.