Loughborough University, Loughborough, United
Kingdom0000-0001-5088-0067Supported by EPSRC grant EP/T033762/1. Loughborough
University, Loughborough, United Kingdomhttps://orcid.org/0000-0002-3476-6739
Dominik D. Freydenberger and Sam M. Thompson [100]Theory of computation
Complexity theory and logic Conference version: [15].

###### Acknowledgements.

The authors would like to thank Justin Brackemann, and the anonymous reviewers
for all their helpful comments and suggestions. Dan Olteanu and Nils Vortmeier
2 25th International Conference on Database Theory (ICDT 2022) ICDT 2022 ICDT
2022 March 29–April 1, 2022 Edinburgh, UK 220 6

# Splitting Spanner Atoms:
A Tool for Acyclic Core Spanners

Dominik D. Freydenberger  Sam M. Thompson

###### Abstract

This paper investigates regex ${\mathsf{CQ}}$s with string equalities
($\mathsf{SERCQ}$s), a subclass of core spanners. As shown by Freydenberger,
Kimelfeld, and Peterfreund (PODS 2018), these queries are intractable, even if
restricted to acyclic queries. This previous result defines acyclicity by
treating regex formulas as atoms. In contrast to this, we propose an
alternative definition by converting $\mathsf{SERCQ}$s into
$\mathsf{FC\mathchar 45\relax CQ}$s – conjunctive queries in $\mathsf{FC}$, a
logic that is based on word equations. We introduce a way to decompose word
equations of unbounded arity into a conjunction of binary word equations. If
the result of the decomposition is acyclic, then evaluation and enumeration of
results become tractable. The main result of this work is an algorithm that
decides in polynomial time whether an $\mathsf{FC\mathchar 45\relax CQ}$ can
be decomposed into an acyclic $\mathsf{FC\mathchar 45\relax CQ}$. We also give
an efficient conversion from synchronized $\mathsf{SERCQ}$s to
$\mathsf{FC\mathchar 45\relax CQ}$s with regular constraints. As a
consequence, tractability results for acyclic relational ${\mathsf{CQ}}$s
directly translate to a large class of $\mathsf{SERCQ}$s.

###### keywords:

Document spanners, information extraction, conjunctive queries

##  1 Introduction

Document spanners were introduced by Fagin, Kimelfeld, Reiss, and Vansummeren
[7] as a formalization of AQL, an information extraction query language used
in IBM’s SystemT. Informally, they can be described in two steps. First, so-
called _extractors_ convert an input document, a word over a finite alphabet,
into relations of so-called _spans_. We assume the extractors to be _regex
formulas_ (as described in [7]), which are regular expressions with capture
variables. Consider the following example of a regex formula

$\gamma(x):=\Sigma^{*}\cdot
x\\{(\mathtt{EBDT})\lor(\mathtt{ICDT})\\}\cdot\Sigma^{*}.$

Given some input word, $\gamma(x)$ can be used to extract a unary relation of
spans such that each span represents a factor of the input word that is either
“$\mathtt{EBDT}$” or “$\mathtt{ICDT}$”.

The second step is that the extracted relations are combined using a
relational algebra. Classes of spanners can be defined by the choice of
relational operators. _Regular spanners_ allow for union $\mathrel{\cup}$,
projection $\pi$, and natural join $\bowtie$. Depending on how they are
represented, regular spanners have been shown to be efficient. For example, if
a regular spanner is given as a so-called vset-automaton, results can be
enumerated with constant delay after linear time preprocessing [9, 2].
However, if a regular spanner is given as a join of regex formulas, evaluation
is intractable – as shown in [13], evaluation for spanners of the form
$P:=\pi_{\emptyset}(\gamma_{1}\bowtie\gamma_{2}\cdots\bowtie\gamma_{n})$ is
$\mathsf{NP}$-complete, even if $P$ is acyclic.

_Core spanners_ extend regular spanners by allowing equality selection
$\zeta^{=}$, which checks whether two (potentially different) spans represent
the same factor of the input document. Even when core spanners are restricted
to queries of the form
$\pi_{\emptyset}\zeta^{=}_{x_{1},y_{1}}\cdots\zeta^{=}_{x_{m},y_{m}}\gamma$
for a single regex formula $\gamma$, the evaluation problem is
$\mathsf{NP}$-complete [11]. Therefore, both joins and equalities introduce
computational hardness.

Regex ${\mathsf{CQ}}$s can be understood as the spanner version of relational
${\mathsf{CQ}}$s, which are a central topic in database theory. In each case,
a conjunctive query is a projection over a join of atoms. Apart from the
setting, the key difference is that while the tables for relational
${\mathsf{CQ}}$s are usually part of the input, the tables for regex
${\mathsf{CQ}}$s are defined implicitly through the regex formulas. Hence,
while one could extract these tables and then perform a standard CQ over the
extractions, the number of tuples in the materialized relations may be
exponential. As a consequence, tractable restrictions on relational queries
(such as _acyclic ${\mathsf{CQ}}$s_) do not lead to tractable fragments of
regex ${\mathsf{CQ}}$s [13].

So-called $\mathsf{SERCQ}$s extend regex ${\mathsf{CQ}}$s by also allowing
string equality, thus allowing us to examine both previously discussed sources
of intractability. Consider the following $\mathsf{SERCQ}$

$P:=\pi_{x,y}\;\zeta^{=}_{x,x^{\prime}}\left(\gamma_{\mathsf{sen}}(z)\bowtie\gamma_{\mathsf{prod}}(x)\bowtie\gamma_{\mathsf{pos}}(y)\bowtie\gamma_{\mathsf{factors}}(x,x^{\prime},z)\bowtie\gamma_{\mathsf{factor}}(y,z)\right),$

where we assume $\gamma_{\mathsf{sen}}$ extracts sentences,
$\gamma_{\mathsf{prod}}$ extracts product names, $\gamma_{\mathsf{pos}}$
extracts positive sentiments (such as “enjoyed”), and
$\gamma_{\mathsf{factors}}(x,x^{\prime},z)$ and
$\gamma_{\mathsf{factor}}(y,z)$ ensure that $x$ and $x^{\prime}$ are
successive (but not necessarily consecutive) factors of $z$, and $y$ is a
factor of $z$ respectively. Therefore, $P$ extracts spans representing
products that are mentioned twice within a sentence, along with a positive
sentiment that appears in the same sentence.

Syntactic restrictions on conjunctive queries have been incredibly fruitful
for finding tractable fragments. A well known result of Yannakakis [25] is
that for _acyclic_ conjunctive queries, evaluation can be solved in polynomial
time. Further research on the complexity of acyclic conjunctive queries [16]
and the enumeration of results for acyclic conjunctive queries [3] has shown
the efficacy of this restriction. On the other hand, for document spanners,
such syntactic restrictions are yet to unlock tractable fragments.

To address this gap, we consider a different approach and represent
$\mathsf{SERCQ}$s as a conjunctive query fragment of the logic
$\mathsf{FC}[\mathsf{REG}]$, introduced by Freydenberger and Peterfreund [14].
This logic is based on word equations, regular constraints, and first-order
logic connectives. Consider the following $\mathsf{FC}[\mathsf{REG}]$
conjunctive query

$\varphi:=\mathsf{Ans}(x,y)\leftarrow(z\mathbin{\dot{=}}z_{2}\cdot x\cdot
z_{3}\cdot x\cdot z_{4})\land(z\mathbin{\dot{=}}z_{5}\cdot y\cdot
z_{6})\land(z\mathbin{\dot{\in}}\gamma_{\mathsf{sen}})\land(x\mathbin{\dot{\in}}\gamma_{\mathsf{prod}})\land(y\mathbin{\dot{\in}}\gamma_{\mathsf{pos}}).$

If $\gamma_{\mathsf{sen}}$ is a regular expression that accepts sentences,
$\gamma_{\mathsf{prod}}$ accepts a product name, and $\gamma_{\mathsf{pos}}$
accepts a positive sentiment, then $\varphi$ is “equivalent” to the previously
given $\mathsf{SERCQ}$. They are not equivalent in a strict sense – a key
difference being that $\mathsf{SERCQ}$s reason over spans, whereas
$\mathsf{FC[REG]\mathchar 45\relax CQ}$s reason over factors of the input
words. Reasoning over words does bring some advantages: For example, $\varphi$
simply uses relations of words (for example, $\gamma_{\mathsf{prod}}$) encoded
as a regular expression, and if we wanted to do something analogous for regex-
formulas, we would first have to extract the corresponding relation of spans.

When dealing with word equations, we run into an issue that we already
encountered for regex formulas: Their relations may contain an exponential
number of tuples. This is due to the unbounded arity of word equations.
However, an $\mathsf{FC}$ atom can be considered shorthand for a concatenation
term. For example, the word equation $y\mathbin{\dot{=}}x_{1}x_{2}x_{3}x_{4}$
can be represented as $y\mathbin{\dot{=}}f(f(x_{1},x_{2}),f(x_{3},x_{4}))$
where $f$ denotes binary concatenation. This then lends itself to the
“decomposition” of the word equation into a ${\mathsf{CQ}}$ consisting of
smaller word equations. We can express the above word equation as
$(y\mathbin{\dot{=}}z_{1}\cdot z_{2})\land(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{3}\cdot x_{4})$. For such a
_decomposition_ , the relations defined by each word equation can be stored in
linear space and we can enumerate them with constant delay. Thus, if the
resulting query is acyclic, then the tractability properties of acyclic
conjunctive queries directly translate to the $\mathsf{FC\mathchar 45\relax
CQ}$.

#### Contributions of this paper

The goal of this work is to bridge the gap between acyclic relational
${\mathsf{CQ}}$s and information extraction. To this end, we define
$\mathsf{FC[REG]\mathchar 45\relax CQ}$s, a conjunctive query fragment of
$\mathsf{FC}[\mathsf{REG}]$, and show show that any so-called synchronized
$\mathsf{SERCQ}$ can be converted into an equivalent $\mathsf{FC[REG]\mathchar
45\relax CQ}$ in polynomial time (Lemma 3.6).

We define the decomposition of an $\mathsf{FC\mathchar 45\relax CQ}$ into a
$2\mathsf{FC\mathchar 45\relax CQ}$, where $2\mathsf{FC\mathchar 45\relax CQ}$
denotes the set of $\mathsf{FC\mathchar 45\relax CQ}$s where the right-hand
side of each word equation is of at most length two. Our first main result is
a polynomial-time algorithm that decides whether a _pattern_ 111For the
purposes of this introduction, a pattern can be considered a single
$\mathsf{FC}$ atom. can be decomposed into an acyclic $2\mathsf{FC\mathchar
45\relax CQ}$ (Theorem 4.12).

Building on this, we give a polynomial-time algorithm that decomposes an
$\mathsf{FC\mathchar 45\relax CQ}$ into an acyclic $2\mathsf{FC\mathchar
45\relax CQ}$, or determines that this is not possible (Theorem 5.14). As soon
as we have an acyclic $2\mathsf{FC\mathchar 45\relax CQ}$, the upper bound
results for model checking and enumeration of results follow from previous
work on relational acyclic ${\mathsf{CQ}}$s [16, 3].

We mainly focus on $\mathsf{FC\mathchar 45\relax CQ}$s (i. e., no regular
constraints) due to the fact that we can add regular constraints for “free”.
This is because regular constraints are unary predicates, and therefore can be
easily incorporated into a join tree. Thus, our work defines a class of
$\mathsf{FC[REG]\mathchar 45\relax CQ}$s for which model checking can be
solved in polynomial time, and results can be enumerated with polynomial-delay
(both in terms of combined complexity).

Our approach offers a new research direction for tractable document spanners.
Most of the current literature approaches regular spanners by “compiling” the
spanner representation (regex formulas that are combined with projection,
union, and joins) into a single automaton, where the use of joins can lead to
a number of states that is exponential in the size of the original
representation. Instead, we look at decomposing $\mathsf{FC}$ conjunctive
queries into small and tractable components. This allows us to use the wealth
of research on relational algebra, while also allowing for the use of the
string equality selection operator.

#### Related Work

Regarding data complexity, Florenzano, Riveros, Vgarte, Vansummeren, and Vrgoc
[9] gave a constant-delay algorithm for enumerating the results of
deterministic vset-automata, after linear time preprocessing. Amarilli,
Bourhis, Mengal, and Niewerth [2] extended this result to non-deterministic
vset-automata. Regarding combined complexity, Freydenberger, Kimelfeld, and
Peterfreund [13] introduced regex ${\mathsf{CQ}}$s and proved that their
evaluation is $\mathsf{NP}$-complete (even for acyclic queries), and that
fixing the number of atoms and the number of string equalities in
$\mathsf{SERCQ}$s allows for polynomial-delay enumeration of results.
Freydenberger, Peterfreund, Kimelfeld, and Kröll [12] showed that non-
emptiness for a join of two sequential regex formulas is $\mathsf{NP}$-hard,
under schemaless semantics, even for a single character document. Connections
between the theory of concatenation and spanners have been considered in [11,
10, 14], which give many of the lower bound complexity results for core
spanners. Schmid and Schweikardt [24] examined a subclass of core spanners
called refl-spanners, which incorporate string equality directly into a
regular spanner. Peterfreund [22] considered extraction grammars, and gave an
algorithm for unambiguous extraction grammars that enumerates results with
constant-delay after quintic preprocessing.

##  2 Preliminaries

Let $\emptyset$ denote the _empty set_ , and for $n\geq 1$ let
$[n]:=\\{1,2,\dots,n\\}$. Given a set $S$, we use $|S|$ for the _cardinality_
of $S$. If $S$ is a subset of $T$ then we write $S\subseteq T$ and if $S\neq
T$ also holds, then $S\subset T$. We write $\mathcal{P}(S)$ for the powerset
of $S$. The difference of two sets $S$ and $T$ is denoted as $S\setminus T$.
If $\vec{x}$ is a tuple, we write $x\in\vec{x}$ to indicate that $x$ is a
component of $\vec{x}$. Let $A$ be an alphabet. We use $|w|$ to denote the
length of some word $w\in A^{*}$ and $\varepsilon$ to denote the _empty word_.
The number of occurrences of $a\in A$ within $w$ is $|w|_{a}$. We write
$u\cdot v$ or just $uv$ for the concatenation of words $u,v\in A^{*}$. If
$u=p\cdot v\cdot s$ for $p,s\in A^{*}$ then $v$ is a _factor_ of $u$, denoted
$v\sqsubseteq u$. If $u\neq v$ also holds, then $v\sqsubset u$. Let $\Sigma$
be an alphabet of _terminal symbols_ and let $\Xi$ be an infinite alphabet of
_variables_. We assume that $\Sigma\mathrel{\cap}\Xi=\emptyset$ and
$|\Sigma|\geq 2$.

If $T:=(V,E)$ is a tree, then a path between $x_{1}\in V$ and $x_{n}\in V$ is
the shortest sequence of edges from $x_{1}$ to $x_{n}$. If
$(\\{x_{1},x_{2}\\},\\{x_{2},x_{3}\\},\dots,\\{x_{n-1},x_{n}\\})$ is a path,
then we say a node $y$ _lies_ on this path if $y=x_{j}$ for some $j\in[n]$. We
call the number of edges on a path from $x_{1}$ to $x_{n}$ the _distance_
between $x_{1}$ and $x_{n}$.

#### Document Spanners

Given $w:=w_{1}\cdot w_{2}\cdots w_{n}$ where $w_{i}\in\Sigma$ for all
$i\in[n]$, a so-called _span_ of $w$ is an interval $[i,j\rangle$ where $1\leq
i\leq j\leq n+1$. A span $[i,j\rangle$ defines a factor
$w_{[i,j\rangle}:=w_{i}\cdot w_{i+1}\cdots w_{j-1}$ of $w$. Let $V\subset\Xi$,
where $V$ is finite, and let $w\in\Sigma^{*}$. A _$(V,w)$ -tuple_ is a
function $\mu$ that maps each $x\in V$ to a span $\mu(x)$ of $w$. A _spanner_
$P$, with variables $V$, is a function that maps every $w\in\Sigma^{*}$ to a
set $P(w)$ of $(V,w)$-tuples. By ${\mathsf{Vars}\left(P\right)}$, we denote
the set of variables of $P$.

Like [7], we use _regex formulas_ as the primary extractors. Regex formulas
are an extension of regular expressions with so-called _capture variables_.
More formally: $\emptyset$, $\varepsilon$, and $\mathtt{a}$ where
$\mathtt{a}\in\Sigma$ are all regex formulas, and if $\gamma_{1}$ and
$\gamma_{2}$ are regex formulas then so are $(\gamma_{1}\cdot\gamma_{2})$,
$(\gamma_{1}\lor\gamma_{2})$, $(\gamma_{1})^{*}$, and $x\\{\gamma_{1}\\}$
where $x\in\Xi$. We use $\Sigma$ as a shorthand for $\bigvee_{a\in\Sigma}a$.
We can omit the parentheses when the meaning is clear. A variable binding
$x\\{\gamma\\}$ matches the same words as $\gamma$ and assigns the
corresponding span of the input word to $x$. A regex formula is _functional_
if on every match, each variable is assigned exactly one span. We denote the
set of functional regex formulas by $\mathsf{RGX}$. For
$\gamma\in\mathsf{RGX}$, we use $\llbracket\gamma\rrbracket$ to define the
corresponding spanner as follows. Every match of $\gamma$ on $w$ defines
$\mu$, a $({\mathsf{Vars}\left(\gamma\right)},w)$-tuple, where for each
$x\in{\mathsf{Vars}\left(\gamma\right)}$, we have that $\mu(x)$ is the span
assigned to $x$. We use $\llbracket\gamma\rrbracket(w)$ to denote the set of
all such $({\mathsf{Vars}\left(\gamma\right)},w)$-tuples. See [7] for more
details.

We now define _synchronized $\mathsf{RGX}$-formulas_ (this follows the
definition by Freydenberger, Kimelfeld, Kröll, and Peterfreund in [12]). An
expression $\gamma\in\mathsf{RGX}$ is _synchronized_ if for all sub-
expressions of the form $(\gamma_{1}\lor\gamma_{2})$, no variable bindings
occur in $\gamma_{1}$ or $\gamma_{2}$. We denote the class of synchronized
$\mathsf{RGX}$-formulas by $\mathsf{RGX_{sync}}$.

The motivation for synchronized $\mathsf{RGX}$-formulas is that non-
synchronized formulas allow for “hidden” disjunctions within the atoms. This
goes (arguably) against the spirit of ${\mathsf{CQ}}$s and (as shown in [12])
leads to “un-${\mathsf{CQ}}$-like” behavior.

######  Example 2.1.

Consider the regex formula $\gamma:=\Sigma^{*}\cdot
x\\{\mathtt{a}\lor(\mathtt{b})^{*}\\}\cdot y\\{\Sigma^{*}\\}\cdot\Sigma^{*}$.
We have that $\llbracket\gamma\rrbracket(w)$ contains those $\mu$ such that
$\mu(x)$ is a factor of $w$ which is either an $\mathtt{a}$ or a sequence of
$\mathtt{b}$ symbols, and the span $\mu(y)$ occurs directly after $\mu(x)$.
Since $\gamma$ is functional, and for every sub-expression of the form
$(\gamma_{1}\lor\gamma_{2})$, we have that
${\mathsf{Vars}\left(\gamma_{1}\right)}={\mathsf{Vars}\left(\gamma_{2}\right)}=\emptyset$,
it follows that $\gamma$ is a _synchronized regex formula_.

Essentially, a synchronized regex formula is functional if no variable is
redeclared, and no variable is used inside of a Kleene star.

This is extended into a _relational algebra_ comprised of $\mathrel{\cup}$
(union), $\pi$ (projection), $\bowtie$ (natural join), and $\zeta^{=}$ (string
equality). Let $w\in\Sigma^{*}$, and let $P_{1}$ and $P_{2}$ be spanners. We
say $P_{1}$ and $P_{2}$ are _compatible_ if
${\mathsf{Vars}\left(P_{1}\right)}={\mathsf{Vars}\left(P_{2}\right)}$. If two
spanners $P_{1}$ an $P_{2}$ are compatible, then
$(P_{1}\mathrel{\cup}P_{2})(w):=P_{1}(w)\mathrel{\cup}P_{2}(w)$. For
$Y\subseteq{\mathsf{Vars}\left(P_{1}\right)}$, the _projection_
$\pi_{Y}P_{1}(w)$ is defined as the restriction of all $\mu\in P_{1}(w)$ to
the set of variables $Y$, and hence
${\mathsf{Vars}\left(\pi_{Y}P_{1}\right)}:=Y$.

The _natural join_ , $P_{1}\bowtie P_{2}$, is obtained by defining
${\mathsf{Vars}\left(P_{1}\bowtie
P_{2}\right)}:={\mathsf{Vars}\left(P_{1}\right)}\mathrel{\cup}{\mathsf{Vars}\left(P_{2}\right)}$,
and $(P_{1}\bowtie P_{2})(w)$ as the set of all
$({\mathsf{Vars}\left(P_{1}\right)}\mathrel{\cup}{\mathsf{Vars}\left(P_{2}\right)},w)$-tuples
for which there exists $\mu_{1}\in P_{1}(w)$ and $\mu_{2}\in P_{2}(w)$ such
that $\mu_{1}(x)=\mu_{2}(x)$ for all
$x\in{\mathsf{Vars}\left(P_{1}\right)}\mathrel{\cap}{\mathsf{Vars}\left(P_{2}\right)}$.
The _string equality operator_ $\zeta^{=}_{x_{1},x_{2}}P_{1}$ is defined by
$\zeta^{=}_{x_{1},x_{2}}P_{1}(w):=\\{\mu\in P_{1}(w)\mid
w_{\mu(x_{1})}=w_{\mu(x_{2})}\\}$, where
${\mathsf{Vars}\left(\zeta^{=}_{x_{1},x_{2}}P_{1}\right)}:={\mathsf{Vars}\left(P_{1}\right)}$.

Given a class of regex-formulas $C$ and a spanner algebra $\mathsf{O}$, we use
$C^{\mathsf{O}}$ to denote the set of spanner representations which can be
constructed by repeated combinations of operators from $\mathsf{O}$ with a
regex-formula from $C$. We write $\llbracket C^{\mathsf{O}}\rrbracket$ to
denote the closure of $\llbracket C\rrbracket$ under $\mathsf{O}$.

The class of _core spanners_ (introduced by Fagin, Kimelfeld, Reiss, and
Vansummeren [7]) is defined as
$\llbracket\mathsf{RGX}^{\mathsf{core}}\rrbracket$ where
$\mathsf{core}:=\\{\pi,\zeta^{=},\mathrel{\cup},\bowtie\\}$. The class of
_regex ${\mathsf{CQ}}$s with string equality_ ($\mathsf{SERCQ}$s) is defined
as expressions of the form:

$P:=\pi_{Y}\left(\zeta^{=}_{x_{1},y_{1}}\cdots\zeta^{=}_{x_{l},y_{l}}(\gamma_{1}\bowtie\cdots\bowtie\gamma_{k})\right),$

where $\gamma_{i}\in\mathsf{RGX}$ for all $i\in[k]$. We call an
$\mathsf{SERCQ}$ a _synchronized_ $\mathsf{SERCQ}$ if every regex formula is a
synchronized $\mathsf{RGX}$-formula.

######  Example 2.2.

Consider $P:=\zeta^{=}_{x_{1},x_{2}}\left(\gamma_{1}\bowtie\gamma_{2}\right)$
where $\gamma_{1}:=\Sigma^{*}\cdot
x_{1}\\{\Sigma^{+}\\}\cdot\mathtt{a}\cdot\Sigma^{*}$ and
$\gamma_{2}:=\Sigma^{*}\cdot
x_{2}\\{\Sigma^{+}\\}\cdot\mathtt{b}\cdot\Sigma^{*}$. Given $w\in\Sigma^{*}$,
we have that $\llbracket P\rrbracket(w)$ contains those $\mu$ such that the
factor $w_{\mu(x_{1})}$ is non-empty, and is immediately followed by the
symbol $\mathtt{a}$, the factor $w_{\mu(x_{2})}$ is immediately followed by
the symbol $\mathtt{b}$, and $w_{\mu(x_{1})}=w_{\mu(x_{2})}$. Since both
$\gamma_{1}$ and $\gamma_{2}$ are synchronized, $P$ is a synchronized
$\mathsf{SERCQ}$.

#### Computational Model and Complexity Measures

We use the _random access machine_ model with uniform cost measures, where the
size of each machine word is logarithmic in the size of the input. We
represent factors of a word $w\in\Sigma^{*}$ as spans of $w$. This allows us
to check whether $u=v$ for $u,v\sqsubseteq w$ in constant time after
preprocessing that takes linear time and space [17, 5] (see Proposition 4.1
for more details). The complexity results we state are in terms of _combined
complexity_. That is, both the query and the word are considered part of the
input. When considering the enumeration of results for a query executed on a
word, we say that we can enumerate results with _polynomial-delay_ if there
exists an algorithm which returns the first result in polynomial time, the
time between two consecutive results is polynomial, and the time between the
last result and terminating is polynomial.

##  3 Conjunctive Queries for FC

This section introduces $\mathsf{FC[REG]\mathchar 45\relax CQ}$s, a
conjunctive query fragment of $\mathsf{FC}$ with regular constraints. We give
some complexity results regarding $\mathsf{SERCQ}$s and show an efficient
conversion from synchronized $\mathsf{SERCQ}$s to $\mathsf{FC[REG]\mathchar
45\relax CQ}$s.

A pattern is a word $\alpha\in(\Sigma\cup\Xi)^{*}$, and a _word equation_ is a
pair $\eta:=(\alpha_{L},\alpha_{R})$ where
$\alpha_{L},\alpha_{R}\in(\Sigma\mathrel{\cup}\Xi)^{*}$ are patterns known as
the _left_ and _right_ side respectively. We usually write such $\eta$ as
$(\alpha_{L}\mathbin{\dot{=}}\alpha_{R})$. The length of a word equation,
denoted $|(\alpha_{L}\mathbin{\dot{=}}\alpha_{R})|$, is
$|\alpha_{L}|+|\alpha_{R}|$. A  _pattern substitution_ is a morphism
$\sigma\colon(\Sigma\cup\Xi)^{*}\rightarrow\Sigma^{*}$ such that
$\sigma(\mathtt{a})=\mathtt{a}$ holds for all $\mathtt{a}\in\Sigma$. Since
$\sigma$ is a morphism, we have
$\sigma(\alpha_{1}\cdot\alpha_{2})=\sigma(\alpha_{1})\cdot\sigma(\alpha_{2})$
for all $\alpha_{1},\alpha_{2}\in(\Sigma\cup\Xi)^{*}$.

A pattern substitution $\sigma$ is a _solution_ to a word equation
$(\alpha_{L}\mathbin{\dot{=}}\alpha_{R})$ if and only if
$\sigma(\alpha_{L})=\sigma(\alpha_{R})$. When applying a pattern substitution
$\sigma$ to a pattern $\alpha$, we assume that its domain
$\mathsf{dom}(\sigma)$ satisfies
$\mathsf{var}(\alpha)\subseteq\mathsf{dom}(\sigma)$. Freydenberger and
Peterfreund [14] introduced $\mathsf{FC}$ as a first-order logic that is based
on word equations. In the present paper, we do not consider the full logic
$\mathsf{FC}$. Instead, we introduce its conjunctive queries.

######  Definition 3.1.

An $\mathsf{FC\mathchar 45\relax CQ}$ is an $\mathsf{FC}$-formula of the form
$\varphi(\vec{x}):=\exists\vec{y}\colon\bigwedge_{i=1}^{n}\eta_{i}$, where
$\eta_{i}:=(x_{i}\mathbin{\dot{=}}\alpha_{i})$, $x_{i}\in\Xi$, and
$\alpha_{i}\in(\Sigma\mathrel{\cup}\Xi)^{*}$ for all $i\in[n]$. We use the
shorthand
$\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$ where
$\vec{x}$ is the tuple of free variables. We call $\mathsf{Ans}(\vec{x})$ the
_head_ of $\varphi$, and $\bigwedge_{i=1}^{n}\eta_{i}$ the _body_ of
$\varphi$.

We write $\varphi(\vec{x})$ to denote that $\vec{x}$ is the set of free
variables of $\varphi$. The set of all variables used in $\varphi$ is denoted
by $\mathsf{var}(\varphi)$. We distinguish a variable $\mathfrak{u}\in\Xi$,
called the _universe variable_ , that shall represent the input document $w$.
The universe variable is not considered a free variable, and we adopt the
convention that $\mathfrak{u}\notin\mathsf{var}(\varphi)$ for all $\varphi$
(even if $\mathfrak{u}$ occurs in $\varphi$). Next, we define the semantics
for $\mathsf{FC\mathchar 45\relax CQ}$s.

######  Definition 3.2.

For $\varphi\in\mathsf{FC\mathchar 45\relax CQ}$ and a pattern substitution
$\sigma$ with
$\mathsf{var}(\varphi)\mathrel{\cup}\\{\mathfrak{u}\\}\subseteq\mathsf{dom}(\sigma)$,
we define $\sigma\models\varphi$ as follows:
$\sigma\models(\alpha_{l}\mathbin{\dot{=}}\alpha_{R})$ if
$\sigma(\eta_{L})=\sigma(\eta_{R})$ and
$\sigma(x)\sqsubseteq\sigma(\mathfrak{u})$ for all
$x\in\mathsf{var}(\alpha_{L}\mathbin{\dot{=}}\alpha_{R})$. For
$\sigma\models\exists x\colon\varphi$ we have that $\sigma_{x\mapsto
u}\models\varphi$ holds for some $u\sqsubseteq\sigma(\mathfrak{u})$, where
$\sigma_{x\mapsto u}$ is defined as $\sigma_{x\mapsto u}(x):=u$ and
$\sigma_{x\mapsto u}(y):=\sigma(y)$ for all $y\in(\Sigma\cup\Xi)$ where $y\neq
x$. We use the canonical definition for conjunction.

Hence, for all $\sigma\models\varphi(\vec{x})$, the universe for variables in
$\mathsf{var}(\varphi)$ is the set of factors of $\sigma(\mathfrak{u})$. If
$\varphi(\vec{x})\in\mathsf{FC\mathchar 45\relax CQ}$ and $w\in\Sigma^{*}$,
then $\llbracket\varphi\rrbracket(w)$ denotes the set of all $\sigma(\vec{x})$
such that $\sigma\models\varphi$ and $\sigma(\mathfrak{u})=w$. When
determining $\llbracket\varphi\rrbracket(w)$ for a given $w$, we know that
$\mathfrak{u}$ represents $w$, and hence $\mathfrak{u}$ can be treated as a
constant (see [14] for more information on the role of the universe variable).
If $\varphi\in\mathsf{FC}$ is _Boolean_ (that is, it has no free variables),
$\llbracket\varphi\rrbracket(w)$ is either the empty set, or the set
containing the empty tuple, which we interpret as ${\mathsf{False}}$ and
${\mathsf{True}}$, respectively.

In [14], $\mathsf{FC}$ was extended to $\mathsf{FC}[\mathsf{REG}]$ by adding
_regular constraints_. This allows for atoms of the form
$(x\mathbin{\dot{\in}}\gamma)$, where $\gamma$ is a _regular expression_ ; and
$\sigma\models(x\mathbin{\dot{\in}}\gamma)$ if and only if
$\sigma(x)\in\mathcal{L}(\gamma)$ and
$\sigma(x)\sqsubseteq\sigma(\mathfrak{u})$. We extend $\mathsf{FC\mathchar
45\relax CQ}$ to $\mathsf{FC[REG]\mathchar 45\relax CQ}$ in the same way.

#### Complexity

We now define various decision problems for $\mathsf{FC\mathchar 45\relax CQ}$
and $\mathsf{FC[REG]\mathchar 45\relax CQ}$: The _non-emptiness problem_ is,
given $w\in\Sigma^{*}$ and $\varphi$, decide whether
$\llbracket\varphi\rrbracket(w)\neq\emptyset$. The _evaluation problem_ is,
given $\sigma$ and $\varphi$, decide whether $\sigma\models\varphi$. The
_model checking problem_ is the special case of non-emptiness and evaluation
that only considers Boolean queries, note that for Boolean queries
$\mathsf{Dom}(\sigma)=\\{\mathfrak{u}\\}$. Given $w\in\Sigma^{*}$ and
$\varphi$, the _enumeration problem_ is outputting all
$\llbracket\varphi\rrbracket(w)$. The _containment problem_ is, given
$\varphi$ and $\psi$, decide whether
$\llbracket\varphi\rrbracket(w)\subseteq\llbracket\psi\rrbracket(w)$ for all
$w\in\Sigma^{*}$. Previous results on patterns and $\mathsf{FC}$ (see [4, 6,
14]) directly imply the following.

######  Proposition 3.3.

For each of $\mathsf{FC\mathchar 45\relax CQ}$ and $\mathsf{FC[REG]\mathchar
45\relax CQ}$, the evaluation problem is $\mathsf{NP}$-complete, and the
containment problem is undecidable.

As discussed in [14], $\mathsf{FC}$ and $\mathsf{FC}[\mathsf{REG}]$ can be
evaluated analogously to relational first-order logic ($\mathsf{FO}$), by
materializing the tables that are defined by the atoms and then proceeding “as
usual”. Hence, bounding the width of a formula (the maximum number of free
variables in a subformula) bounds the size of the intermediate tables, and
thereby the complexity of evaluation. As the complexity of evaluating
$\mathsf{FC}$ and $\mathsf{FO}$ are the same ($\mathsf{PSPACE}$-complete in
general, $\mathsf{NP}$-complete for the existential-positive fragment), it is
no surprise that this correspondence also translates to conjunctive queries.
From Section 5 on, we further develop this connection by finding tractable
subclasses of $\mathsf{FC[REG]\mathchar 45\relax CQ}$.

As containment for ${\mathsf{CQ}}$s is decidable (although
$\mathsf{NP}$-complete), it can be used for query minimization (see Chapter 6
of [1]). But by Proposition 3.3, this does not apply to $\mathsf{FC\mathchar
45\relax CQ}$.

#### Document Spanners and FC-CQs

Our next goal is to establish a connection between $\mathsf{SERCQ}$s and
$\mathsf{FC[REG]\mathchar 45\relax CQ}$s. However, first we must overcome the
fact that $\mathsf{FC}$ reasons over strings, whereas spanners reason over
intervals of positions. We deal with this by defining the notion of an
$\mathsf{FC}$-formula _realizing_ a spanner, as described in [11, 10, 14].

######  Definition 3.4.

A pattern substitution $\sigma$ _expresses_ a $(V,w)$-tuple $\mu$, if for all
$x\in V$, we have that $\mathsf{Dom}(\sigma)=\\{x^{P},x^{C}\mid x\in V\\}$,
and $\sigma(x^{P})=w_{[1,i\rangle}$ and $\sigma(x^{C})=w_{[i,j\rangle}$ for
the span $\mu(x)=[i,j\rangle$. An $\mathsf{FC[REG]\mathchar 45\relax CQ}$
$\varphi$ _realizes_ a spanner $P$ if
$\mathsf{free}(\varphi)=\\{x^{P},x^{C}\mid
x\in{\mathsf{Vars}\left(P\right)}\\}$ and $\sigma\models\varphi$ for all
$w\in\Sigma^{*}$ where $\sigma(\mathfrak{u})=w$, if and only if $\sigma$
expresses some $\mu\in P(w)$.

Less formally, for each $\mu\in P(w)$, we have that $\mu(x)=[i,j\rangle$ is
uniquely represented by the prefix, $\sigma(x^{P})=w_{[1,i\rangle}$, and the
content, $\sigma(x^{C})=w_{[i,j\rangle}$.

######  Example 3.5.

Consider the following $\mathsf{FC[REG]\mathchar 45\relax CQ}$.

$\varphi:=\mathsf{Ans}(x_{1}^{P},x_{1}^{C},x_{2}^{P},x_{2}^{C})\leftarrow(\mathfrak{u}\mathbin{\dot{=}}x_{1}^{P}\cdot
x_{1}^{C}\cdot\mathtt{a}\cdot
s_{1})\land(\mathfrak{u}\mathbin{\dot{=}}x_{2}^{P}\cdot
x_{2}^{C}\cdot\mathtt{b}\cdot s_{2})\\\
\land(x_{1}^{C}\mathbin{\dot{=}}x_{2}^{C})\land(x_{1}^{C}\mathbin{\dot{\in}}\Sigma^{+})\land(x_{2}^{C}\mathbin{\dot{\in}}\Sigma^{+}).$

We can see that $\varphi$ realizes the $\mathsf{SERCQ}$ given in Example 2.2.

Recall that synchronized $\mathsf{SERCQ}$s consist of $\mathsf{RGX}$-formulas
that do not have variables within sub-expressions of the form
$(\gamma_{1}\lor\gamma_{2})$. As we observe in the following result, a
synchronized $\mathsf{SERCQ}$ can be efficiently translated into an equivalent
$\mathsf{FC[REG]\mathchar 45\relax CQ}$.

######  Lemma 3.6.

Given a synchronized $\mathsf{SERCQ}$ $P$, we can construct in polynomial time
an $\mathsf{FC[REG]\mathchar 45\relax CQ}$ that realizes $P$.

The proof of Lemma 3.6 follows from [14, 11, 10]. The converse of Lemma 3.6
follows directly from [14]. However, one would need to define how
$\mathsf{FC[REG]\mathchar 45\relax CQ}$-formulas can be realized by regex
formulas closed under spanner algebra (details on this can be found in [10,
14]). We omit such a result as it is not the focus on this work.

In this section, we have introduced $\mathsf{FC[REG]\mathchar 45\relax CQ}$s,
and shown an efficient conversion from synchronized $\mathsf{SERCQ}$s to
$\mathsf{FC[REG]\mathchar 45\relax CQ}$s. Therefore, while the present paper
mainly considers a tractable fragment of $\mathsf{FC[REG]\mathchar 45\relax
CQ}$, this tractability carries over to a subclass of $\mathsf{SERCQ}$s.

##  4 Acyclic Pattern Decomposition

This section examines decomposing terminal-free patterns (i. e., patterns
$\alpha\in\Xi^{+}$) into acyclic $2\mathsf{FC\mathchar 45\relax CQ}$s, where
$2\mathsf{FC\mathchar 45\relax CQ}$ denotes the set of $\mathsf{FC\mathchar
45\relax CQ}$s where each word equation has a right-hand side of at most
length two. Patterns are the basis for $\mathsf{FC\mathchar 45\relax CQ}$
atoms, and hence, this section gives us a foundation on which to investigate
the decomposition of $\mathsf{FC\mathchar 45\relax CQ}$s. We do not consider
regular constraints, or patterns with terminals. This is because regular
constraints are unary predicates, and therefore can be easily added to a join
tree; and terminals can be expressed through regular constraints. We use
$2\mathsf{FC\mathchar 45\relax CQ}$s for two reasons. Firstly, binary
concatenation is the most elementary form of concatenation, as it cannot be
decomposed into further (non-trivial) concatenations. Secondly, this ensures
that each word equation has very low width, and therefore we can store the
tables in linear space and enumerate them with constant delay – as shown in
the following.

######  Proposition 4.1.

Given $w\in\Sigma^{*}$, we can construct a data structure in linear time that,
for $x,y,z\in\Xi$, allow us to enumerate $\llbracket x\mathbin{\dot{=}}y\cdot
z\rrbracket(w)$ with constant-delay, and to decide in constant time if
$\sigma\in\llbracket x\mathbin{\dot{=}}y\cdot z\rrbracket(w)$ holds.

Although the cardinality of $\llbracket x\mathbin{\dot{=}}y\cdot
z\rrbracket(w)$ is cubic in $|w|$, Proposition 4.1 allows us to represent this
relation in linear space. As we can query such relations in constant time,
they behave “nicer” than relations in relational algebra. Furthermore, after
materializing the relations defined by each atom of an $2\mathsf{FC\mathchar
45\relax CQ}$, Proposition 4.1 allows us to treat the $2\mathsf{FC\mathchar
45\relax CQ}$ as a relational conjunctive query. We now introduce a way to
_decompose_ a pattern into a conjunction of word equations where the right
hand side of each atom is at most length two. We start by looking at a
canonical way to decompose terminal-free patterns.

Let $\alpha\in\Xi^{+}$ be a terminal-free pattern. To decompose $\alpha$,
first we factorize $\alpha$ so that it can be written using only binary
concatenation We define $\mathsf{BPat}$, the set of all _well-bracketed
patterns_ , recursively as follows:

######  Definition 4.2.

$x\in\mathsf{BPat}$ for all $x\in\Xi$, and if
$\tilde{\alpha},\tilde{\beta}\in\mathsf{BPat}$, then
$(\tilde{\alpha}\cdot\tilde{\beta})\in\mathsf{BPat}$.222For convenience, we
tend use $\tilde{\alpha}$ to denote a bracketing of the pattern
$\alpha\in\Xi^{+}$.

We extend the notion of a factor to a _sub-bracketing_. We write
$\tilde{\alpha}\sqsubseteq\tilde{\beta}$ if $\tilde{\alpha}$ is a factor of
$\tilde{\beta}$ and $\tilde{\alpha},\tilde{\beta}\in\mathsf{BPat}$. Let
$\alpha\in\Xi^{+}$, by $\mathsf{BPat}(\alpha)$ we denote the set of all
bracketings which correspond to the pattern $\alpha$ (i. e., if we remove the
brackets, then the resulting pattern is $\alpha$). Every
$\tilde{\alpha}\in\mathsf{BPat}(\alpha)$ can be converted into an equivalent
formula $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ using the
following.

######  Definition 4.3.

While there exists $\tilde{\beta}\sqsubseteq\tilde{\alpha}$ where
$\tilde{\beta}=(x\cdot y)$ for some $x,y\in\Xi$, we replace every occurrence
of $\tilde{\beta}$ in $\tilde{\alpha}$ with a new, unique variable
$z\in\Xi\setminus\mathsf{var}(\alpha)$ and add the word equation
$(z\mathbin{\dot{=}}x\cdot y)$ to $\Psi_{\tilde{\alpha}}$. When
$\tilde{\alpha}=\tilde{\beta}$, we have that $z=\mathfrak{u}$.

Therefore, up to renaming of variables, every $\tilde{\alpha}\in\mathsf{BPat}$
has a corresponding formula $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar
45\relax CQ}$. We call $\Psi_{\tilde{\alpha}}$ the _decomposition_ of
$\tilde{\alpha}$. The decomposition can be thought of as a logic formula
expressing a _straight-line program_ of the pattern (see [20] for a survey on
algorithms for SLPs). We now give an example of _decomposing_ a bracketing.

######  Example 4.4.

Let $\alpha:=x_{1}x_{2}x_{1}x_{1}x_{2}$ and let
$\tilde{\alpha}\in\mathsf{BPat}(\alpha)$ be defined as follows:

$\tilde{\alpha}:=(((x_{1}\cdot x_{2})\cdot x_{1})\cdot(x_{1}\cdot x_{2})).$

We now list $\tilde{\alpha}$ after every sub-bracketing is replaced with a
variable. We also give the corresponding word equation that is added to
$\Psi_{\tilde{\alpha}}$.

$\displaystyle((\underline{(x_{1}\cdot x_{2})}\cdot
x_{1})\cdot\underline{(x_{1}\cdot x_{2})})$ $\displaystyle
z_{1}\mathbin{\dot{=}}x_{1}\cdot x_{2}$ $\displaystyle(\underline{(z_{1}\cdot
x_{1})}\cdot z_{1})$ $\displaystyle z_{2}\mathbin{\dot{=}}z_{1}\cdot x_{1}$
$\displaystyle\underline{(z_{3}\cdot z_{1})}$
$\displaystyle\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot z_{1}$

Therefore, we get the decomposition $\Psi_{\tilde{\alpha}}\in
2\mathsf{FC\mathchar 45\relax CQ}$, which is defined as

$\Psi_{\tilde{\alpha}}:=\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}z_{2}\cdot z_{1}).$

Notice that every sub-bracketing of $\tilde{\alpha}$ has a corresponding word
equation in $\Psi_{\tilde{\alpha}}$.

The decomposition of $\tilde{\alpha}$ is somewhat similar to the _Tseytin
transformations_ , see [23], which transforms a propositional logic formula
into a formula in _Tseytin normal form_.

Our next focus is to study which patterns can be decomposed into an _acyclic_
$2\mathsf{FC\mathchar 45\relax CQ}$.

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

A _join tree_ for $\Psi\in 2\mathsf{FC\mathchar 45\relax CQ}$ with body
$\bigwedge_{i=1}^{n}\chi_{i}$ is an undirected tree $T:=(V,E)$, where
$V:=\\{\chi_{i}\mid i\in[n]\\}$, and for all $\chi_{i},\chi_{j}\in V$, if
$x\in\mathsf{var}(\chi_{i})$ and $x\in\mathsf{var}(\chi_{j})$, then $x$
appears in all nodes that lie on the path between $\chi_{i}$ and $\chi_{j}$ in
$T$.

Note that we use $\chi$ (with indices) to denote atoms of a
$2\mathsf{FC\mathchar 45\relax CQ}$ to distinguish them from word equations
with arbitrarily large right-hand sides – which we denote by $\eta$ (with
indices). We call $\Psi\in 2\mathsf{FC\mathchar 45\relax CQ}$ _acyclic_ if
there exists a join tree for $\Psi$. Otherwise, we call $\Psi$ _cyclic_.

######  Definition 4.6 (Acyclic Patterns).

If $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ is a
decomposition of $\tilde{\alpha}\in\mathsf{BPat}$ and $\Psi_{\tilde{\alpha}}$
is acyclic, then we call $\tilde{\alpha}$ _acyclic_. If
$\Psi_{\tilde{\alpha}}$ is cyclic, then we call $\tilde{\alpha}$ _cyclic_. If
there exists $\tilde{\alpha}\in\mathsf{BPat}(\alpha)$ which is acyclic, then
we say that $\alpha$ is _acyclic_. Otherwise, $\alpha$ is _cyclic_.

When determining whether a decomposition $\Psi_{\tilde{\alpha}}\in
2\mathsf{FC\mathchar 45\relax CQ}$ is acyclic, we treat each word equation
(atom) of $\Psi_{\tilde{\alpha}}$ as a single relational symbol. We also
consider $\mathfrak{u}$ to be a constant symbol, since
$\sigma(\mathfrak{u})=w$ always holds. This raises the question as to whether
every pattern has an acyclic decomposition. The answers is no, as the
following result shows.

######  Proposition 4.7.

$x_{1}x_{2}x_{1}x_{3}x_{1}$ is a cyclic pattern, and $x_{1}x_{2}x_{3}x_{1}$ is
an acyclic pattern that has a cyclic bracketing.

This leads to the following question: _Can we decide whether a pattern is
acyclic in polynomial time?_ Given a pattern $\alpha\in\Xi^{+}$, we have that
$|\mathsf{BPat}(\alpha)|=C_{|\alpha|-1}$, where $C_{i}$ is the $i^{th}$
_Catalan number_ , see [21]. As the Catalan numbers grow exponentially, a
straightforward enumeration of bracketings to finding an acyclic bracketing is
not enough.

If $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ is a
decomposition of $\tilde{\alpha}\in\mathsf{BPat}(\alpha)$, then we call the
variable $x\in\Xi$ which represents the whole pattern the _root variable_. If
$x$ is the root variable, then the atom $(x\mathbin{\dot{=}}y\cdot z)$ for
some $y,z\in\Xi$, is called the _root atom_. So far, the root variable has
always been $\mathfrak{u}$. In Section 5, different root variables will be
considered.

Let $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ be the
decomposition of $\tilde{\alpha}\in\mathsf{BPat}(\alpha)$, where
$\alpha\in\Xi^{+}$. We define the _concatenation tree_ of
$\Psi_{\tilde{\alpha}}$ as a rooted, undirected, binary tree
$\mathcal{T}:=(\mathcal{V},\mathcal{E},<,\Gamma,\tau,v_{r})$, where
$\mathcal{V}$ is a set of nodes and $\mathcal{E}$ is a set of undirected
edges. If $v$ and $v^{\prime}$ have a shared parent node, then we use
$v<v^{\prime}$ to denote that $v$ is the left child and $v^{\prime}$ is the
right child of their shared parent. We also have
$\Gamma:=\mathsf{var}(\Psi_{\tilde{\alpha}})$ and the function
$\tau\colon\mathcal{V}\rightarrow\Gamma$ that _labels_ nodes from the
concatenation tree with variables from $\mathsf{var}(\Psi_{\tilde{\alpha}})$.
We use $v_{r}$ to denote the root of $\mathcal{T}$. The _concatenation tree_
of $\Psi_{\tilde{\alpha}}$ is defined as follows.

######  Definition 4.8.

Let
$\Psi_{\tilde{\alpha}}:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}(z_{i}\mathbin{\dot{=}}x_{i}\cdot
x_{i}^{\prime})$ be a decomposition of
$\tilde{\alpha}\in\mathsf{BPat}(\alpha)$. We carry out the construction of a
concatenation tree in two steps. First, we build a tree recursively. If
$v\in\mathcal{V}$ is labeled with $z_{i}$ for $i\in[n]$, then there exists a
left and right child of $v$ that are labeled with $x_{i}$ and $x_{i}^{\prime}$
respectively.

In the second step, we prune the result of the above construction to remove
redundancies. For each set of _non-leaf nodes_ that share a common label, we
define an ordering $\ll$. If $\tau(v_{i})=\tau(v_{j})$ and the distance from
the root of $\mathcal{T}$ to $v_{j}$ is strictly less than the distance from
the root to $v_{i}$, then $v_{j}\ll v_{i}$. If $\tau(v_{i})=\tau(v_{j})$ and
the distance from $v_{r}$ to $v_{i}$ and $v_{j}$ is equal, then $v_{j}\ll
v_{i}$ if and only if $v_{j}$ appears to the _right_ of $v_{i}$. For each set
of non-leaf nodes that share a common label, all nodes other than the
$\ll$-maximum node are called _redundant_. All descendants of redundant nodes
are removed.

Concatenation trees for $2\mathsf{FC\mathchar 45\relax CQ}$s can be understood
as a variation of _derivation trees_ for straight-line programs [20]. While
the pruning may seem somewhat unnatural, the concatenation tree of a
decomposition is a useful tool that we shall use in Lemma 4.11 to characterize
acyclic bracketings.

Due to the pruning procedure, every non-leaf node represents a unique sub-
bracketing. For every node $v$ with left child $v_{l}$ and right child
$v_{r}$, we define
$\mathsf{atom}(v):=(\tau(v)\mathbin{\dot{=}}\tau(v_{l})\cdot\tau(v_{r}))$.
Note that for any two non-leaf nodes $v,v^{\prime}\in\mathcal{V}$ where $v\neq
v^{\prime}$, we have that $\mathsf{atom}(v)\neq\mathsf{atom}(v^{\prime})$. We
call $v\in\mathcal{V}$ an $x$-parent if one of the child nodes of $v$ is
labeled $x$. If $v$ is an $x$-parent, then $\mathsf{atom}(v)$ must contain the
variable $x$.

######  Definition 4.9.

Let $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ be the
decomposition of $\tilde{\alpha}\in\mathsf{BPat}$ and let $\mathcal{T}$ be the
concatenation tree for $\Psi_{\tilde{\alpha}}$. For some
$x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$, we say that $\Psi_{\tilde{\alpha}}$
is _$x$ -localized_ if all nodes that exist on the path between any two
$x$-parents in $\mathcal{T}$ are also $x$-parents.

Since there is exactly one concatenation tree for a decomposition
$\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ of
$\tilde{\alpha}\in\mathsf{BPat}$, we can say $\Psi_{\tilde{\alpha}}$ is
$x$-localized without referring to the concatenation tree of
$\Psi_{\tilde{\alpha}}$.

######  Example 4.10.

Consider the pattern $\alpha:=x_{1}x_{2}x_{1}x_{2}$ and the following two
bracketings:

$\tilde{\alpha}_{1}:=((x_{1}\cdot x_{2})\cdot(x_{1}\cdot x_{2}))\text{ and
}\tilde{\alpha}_{2}:=(((x_{1}\cdot x_{2})\cdot x_{1})\cdot x_{2}).$

The bracketing $\tilde{\alpha}_{1}$ is decomposed into
$\Psi_{1}:=\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(\mathfrak{u}\mathbin{\dot{=}}z_{1}\cdot z_{1})$ and
$\tilde{\alpha}_{2}$ is decomposed into
$\Psi_{2}:=\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}z_{2}\cdot x_{2})$. The concatenation
trees for $\Psi_{1}$ and $\Psi_{2}$ are given in Figure 1. The label for each
node is given in parentheses next to the corresponding node. We can see that
$\mathsf{atom}(v_{2})=(z_{1}\mathbin{\dot{=}}x_{1}\cdot x_{2})$. It follows
that $\Psi_{2}$ is $x_{1}$-localized, but $\Psi_{2}$ is not $x_{2}$-localized.
Observe that $v_{3}\ll v_{2}$, since $v_{2}$ appears to the left of $v_{3}$.
Therefore, $v_{3}$ does not have any descendants, since it is a _redundant
node_.

$v_{1}\;(\mathfrak{u})$$v_{3}\;(z_{1})$$v_{2}\;(z_{1})$$v_{4}\;(x_{1})$$v_{5}\;(x_{2})$

$v_{6}\;(\mathfrak{u})$$v_{8}\;(x_{2})$$v_{7}\;(z_{2})$$v_{9}\;(z_{1})$$v_{10}\;(x_{1})$$v_{11}\;(x_{1})$$v_{12}\;(x_{2})$

Figure 1: Concatenation trees for the decompositions of $((x_{1}\cdot
x_{2})\cdot(x_{1}\cdot x_{2}))$ and $(((x_{1}\cdot x_{2})\cdot x_{1})\cdot
x_{2})$. This figure is used to illustrate Example 4.10.

Utilizing concatenation trees for the decomposition $\Psi_{\tilde{\alpha}}$ of
$\tilde{\alpha}\in\mathsf{BPat}(\alpha)$, and the notion of
$\Psi_{\tilde{\alpha}}$ being $x$-localized for
$x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$, we are now able to state sufficient
and necessary conditions for $\alpha\in\Xi^{+}$ to be acyclic.

######  Lemma 4.11.

The decomposition $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$
of $\tilde{\alpha}\in\mathsf{BPat}(\alpha)$ is acyclic if and only if
$\Psi_{\tilde{\alpha}}$ is $x$-localized for every
$x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$.

The proof of the if-direction is rather straightforward: Take the
concatenation tree of $\Psi_{\tilde{\alpha}}$, replace each non-leaf node
$v\in\mathcal{V}$ with $\mathsf{atom}(v)$, then remove all leaf nodes from the
concatenation tree of $\Psi_{\tilde{\alpha}}$. This gives us a join tree for
$\Psi_{\tilde{\alpha}}$. The only-if direction for Lemma 4.11 is somewhat more
technical. This is because we need to prove this direction for the most
general join tree of $\Psi_{\tilde{\alpha}}$. We prove this by contradiction,
showing that there does not exist a valid label for certain non-leaf nodes of
the concatenation tree if $\Psi_{\tilde{\alpha}}$ is not $x$-localized for
some variable $x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$.

Refering back to Example 4.10, we see that $\Psi_{2}$ is not $x_{2}$-localized
and therefore $\Psi_{2}$ is cyclic, whereas we have that $\Psi_{1}$ is
$x$-localized for all $x\in\mathsf{var}(\Psi_{1})$ and hence $\Psi_{1}$ is
acyclic.

######  Theorem 4.12.

Whether $\alpha\in\Xi^{+}$ is acyclic can be decided in time
$\mathcal{O}(|\alpha|^{7})$.

We prove Theorem 4.12 by giving a bottom-up algorithm that continuously adds
larger acyclic subpatterns of $\alpha$ to a set. To determine whether
concatenating two acyclic subpatterns results in a larger acyclic subpattern,
we also keep an edge relation and check whether $x$ is localized, see Lemma
4.11. We terminate the algorithm when the edge relation has reached a fixed-
point. In the proof of Theorem 4.12, we also show that if $\alpha$ is acyclic,
then we can construct a concatenation tree for a decomposition for
$\tilde{\alpha}\in\mathsf{BPat}(\alpha)$ in $\mathcal{O}(|\alpha|^{7})$ time.

##  5 Acyclic FC-CQs

In this section, we generalize from decomposing patterns to decomposing
$\mathsf{FC\mathchar 45\relax CQ}$s. The main result of this section is a
polynomial-time algorithm to determine whether an $\mathsf{FC\mathchar
45\relax CQ}$ can be decomposed into an acyclic $2\mathsf{FC\mathchar 45\relax
CQ}$. We do this to find a notion of acyclicity for $\mathsf{FC\mathchar
45\relax CQ}$s such that the resulting fragment is tractable.

Decomposing a word equation $(x\mathbin{\dot{=}}\alpha)$ where $x\in\Xi$ and
$\alpha\in(\Xi\setminus\\{x\\})^{+}$ is analogous to decomposing $\alpha$, but
whereas $\mathfrak{u}$ is the root variable when decomposing a pattern, we use
$x$ as the root variable when decomposing $(x\mathbin{\dot{=}}\alpha)$.

If every atom of $\varphi\in\mathsf{FC\mathchar 45\relax CQ}$ is acyclic, then
$\varphi$ does not necessarily have tractable model checking. If this were the
case, then any decomposition $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar
45\relax CQ}$ of some $\tilde{\alpha}\in\mathsf{BPat}$ would have tractable
model checking (because every word equation of the form
$z\mathbin{\dot{=}}x\cdot y$ is acyclic). This would imply that the membership
problem for patterns can be solved in polynomial time, which contradicts [6],
unless $\mathsf{P}=\mathsf{NP}$. Furthermore, if we define
$\varphi\in\mathsf{FC\mathchar 45\relax CQ}$ to be acyclic if there exists a
join tree for $\varphi$ where every word equation is an atom, then model
checking for $\varphi$ is not tractable. To show this, consider
$\varphi:=\mathsf{Ans}()\leftarrow(\mathfrak{u}\mathbin{\dot{=}}\alpha)$.
Model checking for $\varphi$ is equivalent to the membership problem for
$\alpha$, which is $\mathsf{NP}$-complete [6]. Therefore, we require a more
refined notion of acyclicity for $\mathsf{FC\mathchar 45\relax CQ}$s.

In Section 4, we studied the decomposition of terminal-free patterns. If
$\varphi$ is an $\mathsf{FC\mathchar 45\relax CQ}$ with the body
$\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$, then the right-
hand side of some $\eta_{i}$ may not be terminal-free. Therefore, before
defining the decomposition of $\mathsf{FC[REG]\mathchar 45\relax CQ}$s, we
define a way to _normalize_ $\mathsf{FC[REG]\mathchar 45\relax CQ}$s in order
to better utilize the techniques of Section 4.

######  Definition 5.1.

We call an $\mathsf{FC\mathchar 45\relax CQ}$ with body
$\bigwedge_{i=1}^{n}(x_{i}\mathbin{\dot{=}}\alpha_{i})$ _normalized_ if for
all $i,j\in[n]$, we have $\alpha_{i}\in\Xi^{+}$,
$x_{i}\notin\mathsf{var}(\alpha_{i})$,
$\mathfrak{u}\notin\mathsf{var}(\alpha_{i})$, and $\alpha_{i}=\alpha_{j}$ if
and only if $i=j$.

An $\mathsf{FC[REG]\mathchar 45\relax CQ}$ with body
$\bigwedge_{i=1}^{n}(x_{i}\mathbin{\dot{=}}\alpha_{i})\land\bigwedge_{j=1}^{m}(y_{j}\mathbin{\dot{\in}}\gamma)$
is _normalized_ if the subformula
$\bigwedge_{i=1}^{n}(x_{i}\mathbin{\dot{=}}\alpha_{i})$ is normalized.

Since we are interested in polynomial time algorithms, the following lemma
allows us to assume that all $\mathsf{FC\mathchar 45\relax CQ}$s are
normalized without affecting any claims about complexity.

######  Lemma 5.2.

Given $\varphi\in\mathsf{FC[REG]\mathchar 45\relax CQ}$, we can construct an
equivalent, normalized $\mathsf{FC[REG]\mathchar 45\relax CQ}$ in time
$\mathcal{O}(|\varphi|^{2})$.

To prove Lemma 5.2 we use a simple re-writing procedure. We replace every
terminal factor in our formula with a new variable, and use a regular
constraint to determine which terminal word that variable represents. If
$\sigma$ is a morphism that satisfies $(x\mathbin{\dot{=}}\alpha)$ for some
$\alpha\in\Xi$, then $|\sigma(x)|=|\sigma(\alpha)|$. Therefore, if
$x\in\alpha$, then
$|\sigma(x)|=|\sigma(\alpha_{1})|+|\sigma(x)|+|\sigma(\alpha_{2})|$ where
$\alpha=\alpha_{1}\cdot x\cdot\alpha_{2}$. We can then determine that
$\sigma(\alpha_{1})\cdot\sigma(\alpha_{2})=\varepsilon$. Hence,
$x\mathbin{\dot{=}}\alpha$ can be replaced with
$(x\mathbin{\dot{=}}y)\land\bigwedge_{z\in\mathsf{var}(\alpha_{1}\cdot\alpha_{2})}(z\mathbin{\dot{\in}}\varepsilon)$
where $y$ is a new and unique variable. An analogous method is used if
$\mathfrak{u}\in\mathsf{var}(\alpha)$.

######  Example 5.3.

We define an $\mathsf{FC[REG]\mathchar 45\relax CQ}$ along with an equivalent
normalized $\mathsf{FC[REG]\mathchar 45\relax CQ}$:

$\displaystyle\varphi:=$
$\displaystyle\mathsf{Ans}(\vec{x})\leftarrow(x_{1}\mathbin{\dot{=}}x_{2}\cdot\mathfrak{u}\cdot
x_{2})\land(x_{4}\mathbin{\dot{=}}x_{4})\land(x_{3}\mathbin{\dot{=}}\mathtt{aab}),$
$\displaystyle\varphi^{\prime}:=$
$\displaystyle\mathsf{Ans}(\vec{x})\leftarrow(\mathfrak{u}\mathbin{\dot{=}}x_{1})\land(x_{2}\mathbin{\dot{\in}}\varepsilon)\land(x_{4}\mathbin{\dot{=}}z_{2})\land(x_{3}\mathbin{\dot{=}}z_{1})\land(z_{1}\mathbin{\dot{\in}}\mathtt{aab}).$

We now generalize the process of decomposing patterns to decomposing
$\mathsf{FC\mathchar 45\relax CQ}$s. For every $\mathsf{FC\mathchar 45\relax
CQ}$ $\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$, we
say that a $2\mathsf{FC\mathchar 45\relax CQ}$
$\Psi_{\varphi}:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\Psi_{i}$
is a _decomposition_ of $\varphi$ if every $\Psi_{i}$ is a decomposition of
$\eta_{i}$ and, for all $i,j\in[n]$ with $i\neq j$, the sets of introduced
variables for $\Psi_{i}$ and $\Psi_{j}$ are disjoint.

######  Example 5.4.

Let $\varphi\in\mathsf{FC\mathchar 45\relax CQ}$ be defined as follows:

$\varphi:=\mathsf{Ans}(\vec{x})\leftarrow(x_{1}\mathbin{\dot{=}}y_{1}\cdot
y_{2}\cdot y_{3})\land(x_{2}\mathbin{\dot{=}}y_{2}\cdot y_{3}\cdot y_{3}\cdot
y_{4}).$

We now consider the following decompositions for each word equation of
$\varphi$:

$\Psi_{1}:=(x_{1}\mathbin{\dot{=}}y_{1}\cdot
z_{1})\land(z_{1}\mathbin{\dot{=}}y_{2}\cdot y_{3}),\text{ and
}\Psi_{2}:=(x_{2}\mathbin{\dot{=}}z_{2}\cdot
y_{4})\land(z_{2}\mathbin{\dot{=}}z_{3}\cdot
y_{3})\land(z_{3}\mathbin{\dot{=}}y_{2}\cdot y_{3}).$

Therefore,
$\Psi_{\varphi}:=\mathsf{Ans}(\vec{x})\leftarrow\Psi_{1}\land\Psi_{2}$ is a
decomposition of $\varphi$.

######  Definition 5.5 (Acyclic $\mathsf{FC\mathchar 45\relax CQ}$s).

If $\Psi_{\varphi}\in 2\mathsf{FC\mathchar 45\relax CQ}$ is a decomposition of
$\varphi\in\mathsf{FC\mathchar 45\relax CQ}$, we say that $\Psi_{\varphi}$ is
_acyclic_ if there exists a join tree for $\Psi_{\varphi}$. Otherwise,
$\Psi_{\varphi}$ is _cyclic_. If there exists an acyclic decomposition of
$\varphi$, then we say that $\varphi$ is _acyclic_. Otherwise, $\varphi$ is
_cyclic_.

Recall that, since $\mathfrak{u}$ is always mapped to $w$, we can consider
$\mathfrak{u}$ a constant symbol. Therefore, if $T:=(V,E)$ is a join tree for
some decomposition of $\varphi$, then there can exist two nodes that both
contain $\mathfrak{u}$, yet it is not necessary for all nodes on the path
between these two nodes to also contain $\mathfrak{u}$. Referring back to
Example 5.4, we can see that $\varphi$ is acyclic by executing the GYO
algorithm on the decomposition (see Chapter 6 of [1] for more information on
acyclic joins). Our next focus is to study which $\mathsf{FC\mathchar 45\relax
CQ}$s are acyclic, and which are not.

######  Lemma 5.6.

If $\Psi_{\varphi}\in 2\mathsf{FC\mathchar 45\relax CQ}$ is a decomposition of
$\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$, and we
have a join tree $T:=(V,E)$ for $\Psi_{\varphi}$, then we can partition $T$
into $T^{1},T^{2},\dots T^{n}$ such that for each $i\in[n]$, we have that
$T^{i}$ is a join tree for a decomposition of $\eta_{i}$.

To prove Lemma 5.6, we consider a join tree $T:=(V,E)$ for the acyclic
decomposition $\Psi_{\varphi}\in 2\mathsf{FC\mathchar 45\relax CQ}$ of
$\varphi\in\mathsf{FC\mathchar 45\relax CQ}$, along with the induced subgraph
of $T$ on the set of atoms for a decomposition of a single atom of $\varphi$.
We show that this subgraph is connected, and since the introduced variables
are disjoint for separate atoms of $\varphi$, this forms a partition on $T$.

Let $\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$ be a
normalized $\mathsf{FC\mathchar 45\relax CQ}$. A join tree $T:=(V,E)$ for
$\varphi$ where $V=\\{\eta_{i}\mid i\in[n]\\}$ is called a _weak join tree_.
If there exists a weak join tree for $\varphi$, then we say that $\varphi$ is
_weakly acyclic_. Otherwise, $\varphi$ is _weakly cyclic_. Clearly weak
acyclicity is not sufficient for tractability, as discussed at the start of
the current section.

######  Example 5.7.

Consider the following normalized $\mathsf{FC\mathchar 45\relax CQ}$:

$\varphi:=\mathsf{Ans}(\vec{x})\leftarrow(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot
x_{2}\cdot x_{1}\cdot x_{3}\cdot x_{1})\land(x_{1}\mathbin{\dot{=}}x_{4}\cdot
x_{5}\cdot x_{5})\land(x_{6}\mathbin{\dot{=}}x_{7}\cdot x_{7}\cdot x_{7}).$

Using the GYO algorithm, we can see that $\varphi$ is weakly acyclic.

Let $\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$ be
an $\mathsf{FC\mathchar 45\relax CQ}$, and let $\Psi_{\varphi}$ be an acyclic
decomposition of $\varphi$. If $T:=(V,E)$ is a join tree of $\Psi_{\varphi}$,
then for each $i\in[n]$, we use $T^{i}:=(V^{i},E^{i})$ to denote the subtree
of $T$ that is a join tree for the decomposition of $\eta_{i}$. We know that
$T^{i}$ and $T^{j}$ are disjoint for all $i,j\in[n]$ where $i\neq j$, see
Lemma 5.6.

######  Lemma 5.8.

Let $\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$ be a
normalized $\mathsf{FC\mathchar 45\relax CQ}$. If any of the following
conditions holds, then $\varphi$ is cyclic:

  1. 1.

$\varphi$ is weakly cyclic,

  2. 2.

$\eta_{i}$ is cyclic for any $i\in[n]$,

  3. 3.

$|\mathsf{var}(\eta_{i})\mathrel{\cap}\mathsf{var}(\eta_{j})|>3$ for any
$i,j\in[n]$ where $i\neq j$, or

  4. 4.

$|\mathsf{var}(\eta_{i})\mathrel{\cap}\mathsf{var}(\eta_{j})|=3$, and
$|\eta_{i}|>3$ or $|\eta_{j}|>3$ for any $i,j\in[n]$ where $i\neq j$.

Condition 1 can be proven by simply replacing $T^{i}$ with a single node
$\eta_{i}$ for all $i\in[n]$. Condition 2 follows directly from Lemma 5.6.
Conditions 3 and 4 can be proven by a contradiction: Consider the shortest
path from any atom of the decomposition of $\eta_{i}$ to any atom of the
decomposition of $\eta_{j}$. Since the end points of these paths cannot
contain all the variables that $\eta_{i}$ and $\eta_{j}$ share, it follows
that $T:=(V,E)$ is not a join tree.

While Conditions 3 and 4 might seem strict, we can pre-factor common
subpatterns. For example, the conjunction
$(x_{1}\mathbin{\dot{=}}\alpha_{1}\cdot\alpha_{2}\cdot\alpha_{3})\land(x_{2}\mathbin{\dot{=}}\alpha_{4}\cdot\alpha_{2}\cdot\alpha_{5})$,
where $\alpha_{i}\in\Xi^{+}$ for $i\in[5]$, can be written as
$(x_{1}\mathbin{\dot{=}}\alpha_{1}\cdot
z\cdot\alpha_{3})\land(x_{2}\mathbin{\dot{=}}\alpha_{4}\cdot
z\cdot\alpha_{5})\land(z\mathbin{\dot{=}}\alpha_{2})$ where $z\in\Xi$ is a new
variable. We illustrate this further in the following example.

######  Example 5.9.

Consider the following $\mathsf{FC\mathchar 45\relax CQ}$:

$\varphi:=\mathsf{Ans}()\leftarrow(x_{1}\mathbin{\dot{=}}y_{1}\cdot y_{2}\cdot
y_{3}\cdot y_{4}\cdot y_{5})\land(x_{2}\mathbin{\dot{=}}y_{6}\cdot y_{2}\cdot
y_{3}\cdot y_{4}\cdot y_{5}).$

Using Lemma 5.8, we can see that $\varphi$ is cyclic. However, since the
right-hand side of the two word equations share a common subpattern, we can
rewrite $\varphi$ as

$\varphi^{\prime}:=\mathsf{Ans}()\leftarrow(x_{1}\mathbin{\dot{=}}y_{1}\cdot
z)\land(x_{2}\mathbin{\dot{=}}y_{6}\cdot z)\land(z\mathbin{\dot{=}}y_{2}\cdot
y_{3}\cdot y_{4}\cdot y_{5}).$

One could alter our definition of $\mathsf{FC\mathchar 45\relax CQ}$
decomposition so that if two atoms share a bracketing, then the bracketing is
replaced with the same variable (analogously to how decompositions are defined
on patterns). The authors believe it is likely that such a definition of
$\mathsf{FC\mathchar 45\relax CQ}$ decomposition is equivalent to our
definition of $\mathsf{FC\mathchar 45\relax CQ}$ decomposition after
“factoring out” common subpatterns between atoms.

Our next consideration is how the structure of a join tree for a decomposition
of an acyclic query $\varphi\in\mathsf{FC[REG]\mathchar 45\relax CQ}$ relates
to the structure of a weak join tree for $\varphi$.

######  Definition 5.10 (Skeleton Tree).

Let $\Psi_{\varphi}\in 2\mathsf{FC\mathchar 45\relax CQ}$ be an acyclic
decomposition of the query
$\varphi:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{n}\eta_{i}$, and let
$T:=(V,E)$ be a join tree for $\Psi_{\varphi}$. We say that a weak join tree
$T_{w}:=(V_{w},E_{w})$ is the _skeleton tree_ of $T$ if there exists an edge
in $E$ from a node in $V^{i}$ to a node in $V^{j}$ if and only if
$\\{\eta_{i},\eta_{j}\\}\in E_{w}$.

In the proof of Lemma 5.8 (Condition 1), we show that every join tree for a
decomposition has a corresponding skeleton tree. We shall leverage the fact
that every join tree of a decomposition of an acyclic
$\mathsf{FC[REG]\mathchar 45\relax CQ}$ has a skeleton tree in the algorithm
given in the proof of Theorem 5.14.

######  Example 5.11.

We define $\varphi\in\mathsf{FC\mathchar 45\relax CQ}$ and a decomposition
$\Psi_{\varphi}$ as follows:

$\displaystyle\varphi$
$\displaystyle:=\mathsf{Ans}(\vec{x})\leftarrow(x_{1}\mathbin{\dot{=}}x_{2}\cdot
x_{3}\cdot x_{2})\land(x_{2}\mathbin{\dot{=}}x_{4}\cdot x_{4}\cdot x_{5}),$
$\displaystyle\Psi_{\varphi}$
$\displaystyle:=\mathsf{Ans}(\vec{x})\leftarrow(x_{1}\mathbin{\dot{=}}x_{2}\cdot
z_{1})\land(z_{1}\mathbin{\dot{=}}x_{3}\cdot
x_{2})\land(x_{2}\mathbin{\dot{=}}z_{2}\cdot
x_{5})\land(z_{2}\mathbin{\dot{=}}x_{4}\cdot x_{4}).$

The skeleton tree along with the join tree of $\Psi_{\varphi}$ are given in
Figure 2.

$x_{1}\mathbin{\dot{=}}x_{2}\cdot z_{1}$$z_{1}\mathbin{\dot{=}}x_{3}\cdot
x_{2}$$x_{2}\mathbin{\dot{=}}z_{2}\cdot
x_{5}$$z_{2}\mathbin{\dot{=}}x_{4}\cdot x_{4}$

$x_{1}\mathbin{\dot{=}}x_{2}\cdot x_{3}\cdot
x_{2}$$x_{2}\mathbin{\dot{=}}x_{4}\cdot x_{4}\cdot x_{5}$

Figure 2:  The join tree (left) and the skeleton tree of the join tree (right)
for Example 5.11.

One might assume that some skeleton trees are more “desirable” than others in
terms of using it for finding an acyclic decomposition of an
$\mathsf{FC[REG]\mathchar 45\relax CQ}$. However, as we observe next, any
skeleton tree is sufficient.

######  Lemma 5.12.

Let $\Psi_{\varphi}\in 2\mathsf{FC\mathchar 45\relax CQ}$ be a decomposition
of $\varphi\in\mathsf{FC\mathchar 45\relax CQ}$. If $\Psi_{\varphi}$ is
acyclic, then any weak join tree can be used as the skeleton tree.

Given a weak join tree of an acyclic query $\varphi$, the proof of Lemma 5.12
transforms the join tree of $\Psi_{\varphi}$ so that the resulting join tree
has the given weak join tree as its skeleton tree. Thus, we can use any weak
join tree as a “template” for the eventual join tree of the decomposition
(under the assumption that the query is acyclic).

While Lemma 5.8 and Lemma 5.12 give some insights and necessary conditions for
deciding whether $\varphi\in\mathsf{FC\mathchar 45\relax CQ}$ is acyclic,
these conditions are not sufficient. We therefore give the following lemma
which is needed in the proof of Theorem 5.14 to find an acyclic decomposition
of $\varphi$.

######  Lemma 5.13.

Given a normalized $\mathsf{FC\mathchar 45\relax CQ}$ of the form
$\varphi:=\mathsf{Ans}(\vec{x})\leftarrow(z\mathbin{\dot{=}}\alpha)$ and a set
$C\subseteq\\{\\{x,y\\}\mid x,y\in\mathsf{var}(z\mathbin{\dot{=}}\alpha)\text{
and }x\neq y\\}$, we can decide whether there is an acyclic decomposition
$\Psi\in 2\mathsf{FC\mathchar 45\relax CQ}$ of $\varphi$ such that for every
$\\{x,y\\}\in C$, there is an atom of $\Psi$ that contains both $x$ and $y$ in
time $\mathcal{O}(|\alpha|^{7})$.

We prove Lemma 5.13 using a variant of the algorithm given in the proof of
Theorem 4.12. The purposes of Lemma 5.13 should become clearer after giving
the following necessary and sufficient criteria for an
$\mathsf{FC[REG]\mathchar 45\relax CQ}$ to be acyclic: Let
$\varphi:=\bigwedge_{i=1}^{m}(x_{i}\mathbin{\dot{=}}\alpha_{i})\land\bigwedge_{j=1}^{n}(y_{j}\mathbin{\dot{\in}}\gamma_{j})$
be a normalized $\mathsf{FC[REG]\mathchar 45\relax CQ}$. Then, there exists an
acyclic decomposition $\Psi\in 2\mathsf{FC[REG]\mathchar 45\relax CQ}$ of
$\varphi$ if and only if the following conditions hold:

  1. 1.

$\varphi$ is weakly acyclic,

  2. 2.

for all $i\in[m]$ the pattern $\alpha_{i}$ is acyclic, and

  3. 3.

for every $i\in[m]$, there is a decomposition $\Psi_{i}$ of
$x_{i}\mathbin{\dot{=}}\alpha_{i}$ such that for all $j\in[m]\setminus\\{i\\}$
there is a decomposition $\Psi_{j}$ of $x_{j}\mathbin{\dot{=}}\alpha_{j}$
where there exists an atom $\chi_{i}$ of $\Psi_{i}$ and an atom $\chi_{j}$ of
$\Psi_{j}$ that satisfies
$\mathsf{var}(\chi_{i})\mathrel{\cap}\mathsf{var}(\chi_{j})=\mathsf{var}(x_{i}\mathbin{\dot{=}}\alpha_{i})\mathrel{\cap}\mathsf{var}(x_{j}\mathbin{\dot{=}}\alpha_{j})$.

We are now ready to give the main result of the paper.

######  Theorem 5.14.

Whether $\varphi\in\mathsf{FC[REG]\mathchar 45\relax CQ}$ is acyclic can be
decided in time $\mathcal{O}(|\varphi|^{8})$.

To prove Theorem 5.14, we first check whether $\varphi\in\mathsf{FC\mathchar
45\relax CQ}$ has any of the conditions from Lemma 5.8. If so, then we know
that $\varphi$ is cyclic. Then, we construct a weak join tree for $\varphi$.
If there is an edge $\\{\eta_{i},\eta_{j}\\}$ of the weak join tree such that
$\eta_{i}$ and $\eta_{j}$ share exactly two variables, then we use Lemma 5.13
to decompose $\eta_{i}$ and $\eta_{j}$ such that there is an atom of the
decomposition (of $\eta_{i}$ and $\eta_{j}$), which contains the variables
that $\eta_{i}$ and $\eta_{j}$ share. In the full proof, we show that if such
decompositions do not exist, then $\varphi$ is cyclic. For all other atoms of
$\varphi$ we can use any decomposition. The resulting acyclic decomposition is
the conjunction of the decompositions of each atom. The proof of Theorem 5.14
also shows that if $\varphi$ is acyclic, an acyclic decomposition can be
constructed in polynomial time.

######  Example 5.15.

We revisit the $\mathsf{FC[REG]\mathchar 45\relax CQ}$ that was given in the
introduction:

$\varphi:=\mathsf{Ans}(x,y)\leftarrow(z\mathbin{\dot{=}}z_{2}\cdot x\cdot
z_{3}\cdot x\cdot z_{4})\land(z\mathbin{\dot{=}}z_{5}\cdot y\cdot
z_{6})\land(z\mathbin{\dot{\in}}\gamma_{\mathsf{sen}})\land(x\mathbin{\dot{\in}}\gamma_{\mathsf{prod}})\land(y\mathbin{\dot{\in}}\gamma_{\mathsf{pos}}).$

We can see this is acyclic by considering the following decomposition:

$\Psi:=\mathsf{Ans}(x,y)\leftarrow(y_{1}\mathbin{\dot{=}}x\cdot
z_{3})\land(y_{2}\mathbin{\dot{=}}y_{1}\cdot
x)\land(y_{3}\mathbin{\dot{=}}z_{2}\cdot
y_{2})\land(z\mathbin{\dot{=}}y_{3}\cdot z_{4})\\\
\land(y_{4}\mathbin{\dot{=}}z_{5}\cdot y)\land(z\mathbin{\dot{=}}y_{4}\cdot
z_{6})\land(z\mathbin{\dot{\in}}\gamma_{\mathsf{sen}})\land(x\mathbin{\dot{\in}}\gamma_{\mathsf{prod}})\land(y\mathbin{\dot{\in}}\gamma_{\mathsf{pos}}).$

Due to the small width of the tables that each word equation of the form
$(x\mathbin{\dot{=}}y\cdot z)$ produces, we conclude the following:

######  Proposition 5.16.

If $\Psi\in 2\mathsf{FC[REG]\mathchar 45\relax CQ}$ is acyclic, then:

  1. 1.

Given $w\in\Sigma^{*}$, the model checking problem can be solved in time
$\mathcal{O}(|\Psi|^{2}|w|^{3})$.

  2. 2.

Given $w\in\Sigma^{*}$, we can enumerate $\llbracket\Psi\rrbracket(w)$ with
$\mathcal{O}(|\Psi|^{2}|w|^{3})$ delay.

For $\mathsf{FC[REG]\mathchar 45\relax CQ}$s, we first find an acyclic
decomposition $\Psi_{\varphi}\in 2\mathsf{FC[REG]\mathchar 45\relax CQ}$ of
$\varphi$ in $\mathcal{O}(|\varphi|^{7})$. Then, the upper bound for model
checking follows from [16]. Polynomial-delay enumeration follows from [3],
where it was proven that given an acyclic (relational) conjunctive query
$\psi$ and a database $D$, we can enumerate $\psi(D)$ with
$\mathcal{O}(|\psi||D|)$ delay. Our “database” is of size
$\mathcal{O}(|\varphi|\cdot|w|^{3})$ as each atom of the form
$(z\mathbin{\dot{=}}x\cdot y)$ defines a relation of size
$\mathcal{O}(|w|^{3})$.

Considering techniques from [3], it may seem that the results of an acyclic
$\mathsf{FC[REG]\mathchar 45\relax CQ}$ without projections can be enumerated
with constant-delay after polynomial time preprocessing. However this is not
the case. New variables, that are not free, are introduced in the
decomposition of $\varphi$ and therefore the resulting
$2\mathsf{FC[REG]\mathchar 45\relax CQ}$ may not be free-connex, which is
required for the results of a ${\mathsf{CQ}}$ to be enumerated with constant-
delay [3].

#### From FC[REG]-CQs to SERCQs

Combining Lemma 3.6 and Proposition 5.16 gives us a class of $\mathsf{SERCQ}$s
for which model checking can be solved in polynomial-time, and we can
enumerate results with polynomial-delay. The hardness of deciding semantic
acyclicity (whether a given $\mathsf{SERCQ}$ can be realized by an acyclic
$\mathsf{FC[REG]\mathchar 45\relax CQ}$) remains open. The authors believe
that semantic acyclicity for $\mathsf{SERCQ}$s is undecidable, partly due to
the fact that various minimization problems are undecidable for $\mathsf{FC}$
[11, 14]. For now, all we have are sufficient critiera for a $\mathsf{SERCQ}$
to be realized by an acyclic $\mathsf{FC[REG]\mathchar 45\relax CQ}$.

######  Definition 5.17.

We say that a query of the form
$P:=\pi_{Y}\bigl{(}\zeta^{=}_{x_{1},y_{1}}\cdots\zeta^{=}_{x_{k},y_{k}}(\gamma_{1}\bowtie\cdots\bowtie\gamma_{n})\bigr{)}$
is _pseudo-acyclic_ if for every $i\in[n]$, we have that
$\gamma_{i}:=\beta_{i_{1}}\cdot x_{i}\\{\beta_{i_{2}}\\}\cdot\beta_{i_{3}}$
where $x_{i}\in\Xi$, and where $\beta_{i_{1}}$, $\beta_{i_{2}}$, and
$\beta_{i_{3}}$ are regular expressions.

We now show that Definition 5.17 gives sufficient criteria for an
$\mathsf{SERCQ}$ to be realized by an acyclic $\mathsf{FC[REG]\mathchar
45\relax CQ}$.

######  Proposition 5.18.

Given a pseudo-acyclic $\mathsf{SERCQ}$ $query$, we can construct in
polynomial time an acyclic $\mathsf{FC[REG]\mathchar 45\relax CQ}$ that
realizes $P$.

Freydenberger et al. [13] proved that fixing the number of atoms and the
number of string equalities in a $\mathsf{SERCQ}$ allows for polynomial-delay
enumeration of results. In contrast to this, Proposition 5.18 allows an
unbounded number of joins and string equality selection operators. However, in
order to have this tractability result, the expressive power of each regex
formula is restricted to only allow one variable. While Proposition 5.18 gives
sufficient criteria for a $\mathsf{SERCQ}$ to be represented by an acyclic
$\mathsf{FC[REG]\mathchar 45\relax CQ}$, many other such classes of
$\mathsf{SERCQ}$s likely exist. Research into finding large classes of
$\mathsf{SERCQ}$s that map to acyclic $\mathsf{FC[REG]\mathchar 45\relax CQ}$s
seems like a promising direction for future work.

##  6 A Note on k-ary Decompositions

We now generalize the notion of pattern decomposition so that the length of
the right-hand side of the resulting formula is less than or equal to some
$k\geq 2$. While the binary decompositions might be considered the natural
case, we show that generalizing to higher arities increases the expressive
power of acyclic patterns. By $k\mathsf{FC\mathchar 45\relax CQ}$ we denote
the set of $\mathsf{FC\mathchar 45\relax CQ}$ formulas that have a right-hand
side of at most length $k$. We write $\mathsf{BPat}_{k}$ for the set of
$k$-ary bracketed patterns over $\Xi$. We define $\mathsf{BPat}_{k}$ formally
using the following recursive definition: For all $x\in\Xi$ we have that
$x\in\mathsf{BPat}_{k}$, and if
$\alpha_{1},\alpha_{2},\dots,\alpha_{i}\in\mathsf{BPat}_{k}$ where $i\leq k$,
then
$(\tilde{\alpha}_{1}\cdot\tilde{\alpha}_{2}\cdots\tilde{\alpha}_{i})\in\mathsf{BPat}_{k}$.
We write $\tilde{\alpha}\in\mathsf{BPat}_{k}(\alpha)$ for some
$\alpha\in\Xi^{+}$ if the underlying, unbracketed pattern of $\tilde{\alpha}$
is $\alpha$. We can convert $\tilde{\alpha}\in\mathsf{BPat}_{k}$ into an
equivalent $k\mathsf{FC\mathchar 45\relax CQ}$ analogously to the binary case,
see Definition 4.3.

######  Example 6.1.

Consider the following $4$-ary bracketing:

$\tilde{\alpha}:=(((x_{1}\cdot x_{2}\cdot x_{3})\cdot(x_{4}\cdot x_{2}\cdot
x_{4})\cdot(x_{1}\cdot x_{2})\cdot(x_{5}\cdot x_{5}))\cdot x_{2}).$

As with the $2$-ary case, we decompose $\tilde{\alpha}$ to get the following
$4\mathsf{FC\mathchar 45\relax CQ}$:

$\Psi_{\tilde{\alpha}}:=\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{5}\cdot
x_{5})\land(z_{3}\mathbin{\dot{=}}x_{4}\cdot x_{2}\cdot x_{4})\\\
\land(z_{4}\mathbin{\dot{=}}x_{1}\cdot x_{2}\cdot
x_{3})\land(z_{5}\mathbin{\dot{=}}z_{4}\cdot z_{3}\cdot z_{1}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}z_{5}\cdot x_{2}).$

The definition of $k$-ary concatenation tree for a decomposition
$\Psi_{\tilde{\alpha}}\in k\mathsf{FC\mathchar 45\relax CQ}$ of
$\tilde{\alpha}\in\mathsf{BPat}_{k}$ follows analogously to the concatenation
trees for $2$-ary decompositions, see Definition 4.8. The concatenation tree
of the decomposition $\Psi_{\tilde{\alpha}}\in k\mathsf{FC\mathchar 45\relax
CQ}$ is a rooted, labeled, undirected tree
$\mathcal{T}:=(\mathcal{V},\mathcal{E},<,\Gamma,\tau,v_{r})$, where
$\mathcal{V}$ is the set of nodes, the relation $\mathcal{E}$ is the edge
relation, and $<$ is used to denote the order of children of a node (from left
to right). We have that $\Gamma:=\mathsf{var}(\Psi_{\tilde{\alpha}})$ is the
alphabet of labels and $\tau\colon\mathcal{V}\rightarrow\Gamma$ is the
labeling function. The semantics of a $k$-ary concatenation tree are defined
by considering the natural generalization of Definition 4.8. We say that
$\Psi_{\tilde{\alpha}}$ is _$x$ -localized_ if all nodes which exist on a path
between two $x$-parents (of $\mathcal{T}$) are also $x$-parents.

######  Proposition 6.2.

There exists $\tilde{\alpha}\in\mathsf{BPat}_{3}$ such that the decomposition
$\Psi\in 3\mathsf{FC\mathchar 45\relax CQ}$ of $\tilde{\alpha}$ is acyclic,
but there exists $x\in\mathsf{var}(\Psi)$ such that $\Psi$ is not
$x$-localized.

######  Proof 6.3.

Consider $\tilde{\alpha}:=((x_{3}\cdot x_{3})\cdot((x_{3}\cdot x_{3})\cdot
x_{2})\cdot(x_{1}\cdot((x_{3}\cdot x_{3})\cdot x_{2})))$. The bracketing
$\tilde{\alpha}$ is decomposed into $\Psi_{\tilde{\alpha}}\in
3\mathsf{FC\mathchar 45\relax CQ}$, which is defined as

$\Psi_{\tilde{\alpha}}:=\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{3}\cdot
x_{3})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{2})\land(z_{3}\mathbin{\dot{=}}x_{1}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}z_{1}\cdot z_{2}\cdot z_{3}).$

The formula $\Psi_{\tilde{\alpha}}$ can be verified to be acyclic. However,
$\Psi_{\tilde{\alpha}}$ is not $z_{1}$-localized.

In this section, we have briefly examined $k$-ary decompositions, and have
shown that there exists $\tilde{\alpha}\in\mathsf{BPat}_{3}$ such that the
decomposition $\Psi\in 3\mathsf{FC\mathchar 45\relax CQ}$ of $\tilde{\alpha}$
is acyclic, but $\Psi$ is not $x$-localized for some $x\in\mathsf{var}(\Psi)$.
The authors note that the if-direction in the proof of Lemma 4.11 implies that
$x$-locality for all variables is a sufficient criterion for a $k$-ary
decomposition to be acyclic. A systematic study into $k$-ary acyclic
decompositions may yield more expressive spanners, and could be useful for
pattern languages, which have been linked to $\mathsf{FC}$-formulas with
bounded width [14]. However, more general approaches such as bounded treewidth
for binary decompositions appear to be a more promising direction for future
work. Furthermore, the membership problem for a pattern $\alpha$ parameterized
by $|\alpha|$ is $\mathsf{W}[1]$-hard [8]. Since every pattern is trivially
$|\alpha|$-ary acyclic, the authors believe it to be likely that the
parameterized problem of model checking for $k$-ary acyclic decompositions is
$\mathsf{W}[1]$-hard.

##  7 Conclusions

Freydenberger and Peterfreund [14] introduced $\mathsf{FC}[\mathsf{REG}]$ as a
logic for querying and model checking words that behaves similar to relational
$\mathsf{FO}$. The present paper develops this connection further by providing
a polynomial-time algorithm that either decomposes an
$\mathsf{FC[REG]\mathchar 45\relax CQ}$ into an acyclic
$2\mathsf{FC[REG]\mathchar 45\relax CQ}$, or determines that this is not
possible. These acyclic $2\mathsf{FC[REG]\mathchar 45\relax CQ}$ formulas
allow for polynomial-time model checking, and their results can be enumerated
with polynomial-delay. Consequently, the present paper establishes a notion of
tractable acyclicity for $\mathsf{FC\mathchar 45\relax CQ}$s. Due to the close
connections between $\mathsf{FC}[\mathsf{REG}]$ and core spanners, this
provides us with a large class of tractable $\mathsf{SERCQ}$s.

But this is only the first step in the study of tractable $\mathsf{SERCQ}$s
and $\mathsf{FC[REG]\mathchar 45\relax CQ}$s. It seems likely that more
efficient algorithms for model checking and enumeration can be found by
utilizing string algorithms rather than materializing the relations for each
atom.

Another future direction for research is the consideration of other structural
parameters, like treewidth. A systematic study of the decomposition of
$\mathsf{FC\mathchar 45\relax CQ}$s into $2\mathsf{FC\mathchar 45\relax CQ}$s
of bounded treewidth would likely yield a large class of $\mathsf{FC\mathchar
45\relax CQ}$s with polynomial-time model checking. As a consequence, one
could define a suitable notion of treewidth for core spanners. Determining the
exact class of $\mathsf{FC\mathchar 45\relax CQ}$s with polynomial-time model
checking is likely a hard problem. This is because such a result would solve
the open problem in formal languages of determining exactly what patterns have
polynomial-time membership.

## References

  * [1] Serge Abiteboul, Richard Hull, and Victor Vianu.  Foundations of databases, volume 8.  Addison-Wesley Reading, 1995.
  * [2] Antoine Amarilli, Pierre Bourhis, Stefan Mengel, and Matthias Niewerth.  Constant-delay enumeration for nondeterministic document spanners.  ACM SIGMOD Record, 49(1):25–32, 2020.
  * [3] Guillaume Bagan, Arnaud Durand, and Etienne Grandjean.  On acyclic conjunctive queries and constant delay enumeration.  In Proceedings of CSL 2007, pages 208–222, 2007.
  * [4] Joachim Bremer and Dominik D. Freydenberger.  Inclusion problems for patterns with a bounded number of variables.  Information and Computation, 220:15–43, 2012.
  * [5] Stefan Burkhardt, Juha Kärkkäinen, and Peter Sanders.  Linear work suffix array construction.  Journal of the ACM, 53(6):918–936, 2006.
  * [6] Andrzej Ehrenfreucht and Grzegorz Rozenberg.  Finding a homomorphism between two words is NP-complete.  Information Processing Letters, 9(2):86–88, 1979.
  * [7] Ronald Fagin, Benny Kimelfeld, Frederick Reiss, and Stijn Vansummeren.  Document spanners: A formal approach to information extraction.  Journal of the ACM, 62(2):12, 2015.
  * [8] Henning Fernau, Markus L Schmid, and Yngve Villanger.  On the parameterised complexity of string morphism problems.  Theory of Computing Systems, 59:24–51, 2016.
  * [9] Fernando Florenzano, Cristian Riveros, Martín Ugarte, Stijn Vansummeren, and Domagoj Vrgoc.  Constant delay algorithms for regular document spanners.  In Proceedings of PODS 2018, pages 165–177, 2018.
  * [10] Dominik D. Freydenberger.  A logic for document spanners.  Theory of Computing Systems, 63(7):1679–1754, 2019.
  * [11] Dominik D. Freydenberger and Mario Holldack.  Document spanners: From expressive power to decision problems.  Theory of Computing Systems, 62(4):854–898, 2018.
  * [12] Dominik D. Freydenberger, Benny Kimelfeld, Markus Kröll, and Liat Peterfreund.  Complexity bounds for relational algebra over document spanners.  In Proceedings of PODS 2019, pages 320–334, 2019.
  * [13] Dominik D. Freydenberger, Benny Kimelfeld, and Liat Peterfreund.  Joining extractions of regular expressions.  In Proceedings of PODS 2018, pages 137–149, 2018.
  * [14] Dominik D. Freydenberger and Liat Peterfreund.  The theory of concatenation over finite models.  In Proceedings of ICALP 2021, pages 130:1–130:17, 2021.
  * [15] Dominik D. Freydenberger and Sam M. Thompson.  Splitting spanner atoms: A tool for acyclic core spanners.  In Proceedings of ICDT 2022, pages 6:1–6:18, 2022.
  * [16] Georg Gottlob, Nicola Leone, and Francesco Scarcello.  The complexity of acyclic conjunctive queries.  Journal of the ACM, 48(3):431–498, 2001.
  * [17] Dan Gusfield.  Algorithms on Strings, Trees, and Sequences – Computer Science and Computational Biology.  Cambridge University Press, 1997.
  * [18] Dan Gusfield and Jens Stoye.  Linear time algorithms for finding and representing all the tandem repeats in a string.  Journal of Computer and System Sciences, 69(4):525–546, 2004.
  * [19] Tao Jiang and Bala Ravikumar.  A note on the space complexity of some decision problems for finite automata.  Information Processing Letters, 40(1):25–31, 1991.
  * [20] Markus Lohrey.  Algorithmics on SLP-compressed strings: A survey.  Groups-Complexity-Cryptology, 4(2):241–299, 2012.
  * [21] Gloria Olive.  Catalan numbers revisited.  Journal of mathematical analysis and applications, 111(1):201–235, 1985.
  * [22] Liat Peterfreund.  Grammars for document spanners.  In Proceedings of ICDT 2021, pages 7:1–7:18, 2021.
  * [23] Steven David Prestwich.  CNF encodings.  Handbook of satisfiability, 185:75–97, 2009.
  * [24] Markus L. Schmid and Nicole Schweikardt.  A purely regular approach to non-regular core spanners.  In Proceedings of ICDT 2021, pages 4:1–4:19, 2021.
  * [25] Mihalis Yannakakis.  Algorithms for acyclic database schemes.  In Proceedings of VLDB 1981, pages 82–94, 1981.

##  Appendix A Proof of 3.3

See 3.3

######  Proof A.1.

The upper bound for evaluation follows immediately from the matching upper
bound for the existential-positive fragment of $\mathsf{FC}$ with regular
constraints (see [14]).

Lower bound for evaluation follows from the fact that, given
$\alpha\in\Xi^{*}$ and $w\in\Sigma^{*}$, deciding whether there is a morphism
$\sigma\colon\Xi^{*}\to\Sigma^{*}$ with $\sigma(\alpha)=w$ is
$\mathsf{NP}$-complete (see Ehrenfeucht and Rozenberg [6]). Hence, even model-
checking $\mathsf{FC\mathchar 45\relax CQ}$s of the form
$\mathsf{Ans}()\leftarrow(\mathfrak{u}\mathbin{\dot{=}}\alpha)$ is
$\mathsf{NP}$-hard.

The undecidability follows from the undecidability of the inclusion problem
for pattern languages (see Bremer and Freydenberger [4]): Given
$\alpha,\beta\in(\Xi\cup\Sigma)^{*}$, does every pattern substitution $\sigma$
have a pattern substitution $\tau$ with $\sigma(\alpha)=\tau(\beta)$? Hence,
containment is undecidable even if restricted to comparing
$\mathsf{FC\mathchar 45\relax CQ}$s of the form
$\mathsf{Ans}()\leftarrow(\mathfrak{u}\mathbin{\dot{=}}\alpha)$ and
$\mathsf{Ans}()\leftarrow(\mathfrak{u}\mathbin{\dot{=}}\beta)$ with
$\alpha,\beta\in(\Xi\cup\Sigma)^{*}$.

##  Appendix B Proof of 3.6

Before proving Lemma 3.6, we first define a _parse trees_ for
$\gamma\in\mathsf{RGX_{sync}}$. Note that we assume $\gamma$ is well-
bracketed. That is, each subexpression of $\gamma$ is of the form $a$,
$\emptyset$, $\varepsilon$, $(\gamma_{1})^{*}$, $(\gamma_{1}\cdot\gamma_{2})$,
$(\gamma_{1}\lor\gamma_{2})$, or $x\\{\gamma_{1}\\}$ for $a\in\Sigma$ and
$\gamma_{1},\gamma_{2},\in\mathsf{RGX_{sync}}$. If
$\gamma\in\mathsf{RGX_{sync}}$ is not well-bracketed, then we can assume any
valid bracketing for $\gamma$.

######  Definition B.1.

Let $\gamma\in\mathsf{RGX_{sync}}$. A _parse tree_ for $\gamma$ is a rooted,
direct tree $T_{\gamma}$. Each node of $T_{\gamma}$ is a subexpression of
$\gamma$. The root of $T_{\gamma}$ is $\gamma$. For each node $v$ of
$T_{\gamma}$, the following rules must hold.

  1. 1.

If $v$ is $(\gamma_{1}\cdot\gamma_{1})$ where
${\mathsf{Vars}\left(\gamma_{1}\right)}\neq\emptyset$ or
${\mathsf{Vars}\left(\gamma_{2}\right)}\neq\emptyset$, then $v$ has a left
child $\gamma_{1}$, and a right child $\gamma_{2}$,

  2. 2.

if $v$ is $x\\{\gamma^{\prime}\\}$, then $v$ has $\gamma^{\prime}$ as a single
child, and

  3. 3.

if $v$ is any other subexpression, then $v$ is a leaf node.

The parse tree for $\gamma$ that we define is specific for our use, and is
different to the standard definition of $\gamma$-parse trees which are used to
define the semantics for regex-formulas, see [7]. The proof of the following
proposition follows from [11, 10, 14], however we include this proof for
completeness sake.

See 3.6

######  Proof B.2.

Let
$P:=\pi_{Y}\left(\zeta^{=}_{x_{1},y_{1}}\cdots\zeta^{=}_{x_{m},y_{m}}(\gamma_{1}\bowtie\cdots\bowtie\gamma_{k})\right)$
be a synchronized $\mathsf{SERCQ}$. We realize $P$ using the following
$\mathsf{FC[REG]\mathchar 45\relax CQ}$:

$\varphi_{P}:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{m}(x_{i}^{C}\mathbin{\dot{=}}y_{i}^{C})\land\bigwedge_{i=1}^{k}\varphi_{\gamma_{i}},$

where $\vec{x}$ contains $x^{P}$ and $x^{C}$ for all $x\in Y$. Furthermore,
for each $i\in[k]$, we define $\varphi_{\gamma_{i}}$ as follows: Take the
parse tree $T_{\gamma_{i}}$ for $\gamma_{i}$ and associate every node $n$ of
$T_{\gamma_{i}}$ with a variable $v_{n}$ as follows:

  * •

If $n$ is the root, let $v_{n}:=\mathfrak{u}$ and disregard the following
cases.

  * •

If $n$ is a variable binding $x\\{\cdot\\}$, let $v_{n}:=x^{C}$.

  * •

Otherwise – that is, if $n$ is a concatenation or a regular expression – let
$v_{n}:=z_{n}$, where $z_{n}$ is a new variable that is unique to $n$.

The construction shall ensure that, when matching $\gamma_{i}$ against a word
$w$, each variable $v_{n}$ contains the part of $w$ that matches against the
subexpression of the node $n$. To this end, for every node $n$, we also define
an atom $A_{n}$ as follows:

  * •

If $n$ is a concatenation with left child $l$ and right child $r$, then
$A_{n}$ is the word equation $(v_{n}\mathbin{\dot{=}}v_{l}\cdot v_{r})$.

  * •

If $n$ is a variable binding, let $A_{n}$ be the word equation
$(v_{n}\mathbin{\dot{=}}v_{c})$, where $c$ is the child of $n$.

  * •

If $n$ is a regular expression $\gamma^{\prime}$, then $A_{n}$ is the regular
constraint $(v_{n}\mathbin{\dot{\in}}\gamma^{\prime})$.

We add all these atoms $A_{n}$ to $\varphi_{\gamma_{i}}$. Up to this point, we
have that every $\sigma\in\llbracket\varphi_{\gamma_{i}}\rrbracket(w)$ encodes
the contents of the spans of some $\mu\in\llbracket\gamma_{i}\rrbracket(w)$.
The only part that is missing in the construction are the prefix variables.

Recall that for every node $n$ in the parse tree $T(\gamma_{i})$, we defined a
variable $v_{n}$ that represent the part of $w$ that matches against the
subexpression of $n$. To obtain the corresponding prefix, we define a function
$\mathsf{p}$ that maps each node $n$ to a pattern $\mathsf{p}(n)\in\Xi^{*}$ as
follows. Given a node $n$, we look for the lowest node above $n$ that is a
concatenation and has $n$ as right child or descendant of its left child. If
no such node exists – that is, if no node above $n$ is a concatenation, or
every concatenation above $n$ has $n$ as descendant on the left side – define
$\mathsf{p}(n):=\varepsilon$. If such a node exists, we denote it by $m$ and
its left child by $l$ and define $\mathsf{p}(n):=\mathsf{p}(m)\cdot v_{l}$. In
other words, $\mathsf{p}(n)$ is the concatenation of all $v_{l}$ that belongs
to nodes that refer a part of $w$ that is to the left of the part that belongs
to $n$.

Hence, to get the values for prefix variables, we take each node $n$ that is a
variable binding $x\\{\cdot\\}$ and add the word equation
$(x^{P}\mathbin{\dot{=}}\mathsf{p}(n))$ to $\varphi_{\gamma_{i}}$.

#### Complexity

First, we build the parse tree $T_{\gamma_{i}}$ which can be constructed in
time polynomial in the size of $\gamma_{i}$. Then, we mark each node of
$T_{\gamma_{i}}$ with a variable and add a word equation or regular constraint
to $\varphi_{\gamma_{i}}$, which takes polynomial time. To ensure the spanner
$\gamma_{i}$ represents is correctly realized, we add an extra word equation
for the prefix variable – this clearly takes polynomial time. There are
linearly many regex formulas in $P$, we can construct $\varphi_{\gamma_{i}}$
for all $i\in[k]$ in polynomial time. The final step of computing
$\varphi_{P}$ takes polynomial time – we consider each string equality and add
the corresponding word equation, and consider each variable in the projection
and add the corresponding variables to the head of the query. Therefore, the
overall complexity is polynomial in the size of $P$.

##  Appendix C Proof of 4.1

See 4.1

######  Proof C.1.

The two main concepts that are used for the data structures are the _LCP data
structure_ (from “least common prefix”, see e. g. [5]), and the _suffix tree_
(see e. g. part II of [17]), which can both be constructed from $w$ in time
$\mathcal{O}(|w|)$.

Evaluation The LCP data structure (for $w$) takes two indices $1\leq i,j\leq
w$ and returns in constant time $\mathsf{LCP}(i,j)$, the length of the longest
common prefix of the two suffixes $w_{[i,|w|+1\rangle}$ and
$w_{[j,|w|+1\rangle}$. Recall that we mentioned in Section 2 (when clarifying
the complexity assumptions) that we represent factors of $w$ as a pair of
indices. To be precise, we can express each $u\sqsubseteq w$ as a span
$[i,j\rangle$ with $1\leq i\leq j\leq|w|+1$. We use this to decide
$\sigma\in\llbracket x\mathbin{\dot{=}}y\cdot z\rrbracket(w)$ in constant time
as follows: Let $[i,j\rangle$, $[i_{1},j_{1}\rangle$, and
$[i_{2},j_{2}\rangle$ be the representations of $\sigma(x)$, $\sigma(y)$, and
$\sigma(z)$, respectively. In other words, $\sigma(x)=w_{[i,j\rangle}$,
$\sigma(y)=w_{[i_{1},j_{1}\rangle}$, and $\sigma(z)=w_{[i_{2},j_{2}\rangle}$.
For our convenience, let $\ell:=|\sigma(x)|$, $\ell_{1}:=|\sigma(y)|$, and
$\ell_{2}:=|\sigma(z)|$.

We have $\sigma(x)=\sigma(y)\cdot\sigma(z)$ if and only if the following
conditions are met:

  * •

$|\sigma(x)|=|\sigma(y)|+|\sigma(z)|$, that is, $\ell=\ell_{1}+\ell_{2}$,

  * •

$\sigma(y)=\sigma(x)_{[1,1+\ell_{1}\rangle}$, and

  * •

$\sigma(z)=\sigma(x)_{[1+\ell_{1},\ell+1\rangle}$.

These are (respectively) equivalent to the following conditions:

  * •

$(j-i)=(j_{1}-i_{1})+(j_{2}-i_{2})$,

  * •

$\mathsf{LCP}(i,i_{1})\geq(j_{1}-i_{1})$, and

  * •

$\mathsf{LCP}(i+(j_{1}-i_{1}),i_{2})\geq(j_{2}-i_{2})$,

due to $\ell=j-i$, $\ell_{1}=j_{1}-i_{1}$, and $\ell_{2}=j_{2}-i_{2}$. The
arithmetic operations can be performed in constant time due to our choice of
computation model, and the LCP data structure can also be queried in constant
time.

Enumeration of all factors Apart from some trivial special cases, the
enumeration relies on enumerating all factors of $w$ with constant delay. This
is a straightforward application of a _suffix tree_ (although the authors
assume that this has been shown before, they were not able to locate a
reference). We give a brief introduction to suffix trees, with just the level
of detail that is required for our purposes. More information can be found
(for example) in [17] (chapters 5 to 7).

The suffix tree $T(w)$ of $w$ is a rooted directed tree with $|w|$ leaves that
are labeled with numbers from 1 to $n$. With the exception of the root, each
internal node has at least two children, and each edge is labeled with a
nonempty factor of $w$. No two edges from the same nodes are labeled with
factors that start with the same letter. Most importantly, for any leaf with
label $i$, the word that is obtained by concatenating the edge labels along
the path from the root to that leaf is exactly $w_{[i,n+1\rangle}$ – that is,
the suffix of $w$ that starts at position $i$.

To ensure that a suffix tree for $w$ exists, we assume that the last letter of
$w$ is a special character $\mathdollar$ that does not occur otherwise (that
is, in a strict sense, we construct the suffix tree of $w\mathdollar$). Figure
3 shows an example suffix tree, which we also use as a running example. While
storing the edge labels explicitly would take quadratic space, recall that we
represent factors of $w$ as spans (this allows us to keep the size of $T(w)$
linear in $|w|$).

6241357$\mathdollar$$\mathtt{paya}\mathdollar$$\mathtt{ya}\mathdollar$$\mathtt{paya}\mathdollar$$\mathtt{ya}\mathdollar$$\mathtt{a}$$\mathtt{pa}$$\mathtt{ya}\mathdollar$$\mathdollar$
Figure 3: The suffix tree that we construct for the word $w:=\mathtt{papaya}$.
From left to right, the leaves correspond to the suffixes $\varepsilon$,
$\mathtt{a}$, $\mathtt{apaya}$, $\mathtt{aya}$, $\mathtt{papaya}$,
$\mathtt{paya}$, and $\mathtt{ya}$. To enumerate the factors of $w$, we use
the nodes 2, 4, 1, 3, 5. In the enumeration of factors, the leaf $2$ generates
(in this order) $\varepsilon$, $\mathtt{a}$, $\mathtt{ap}$, $\mathtt{apa}$,
$\mathtt{apay}$, and $\mathtt{apaya}$; while $4$ only generates $\mathtt{ay}$
and $\mathtt{aya}$. Although this leaf corresponds to $\mathtt{aya}$, we skip
the prefix $\mathtt{a}$, due to $\mathsf{LCP}(2,4)=1$. As
$\mathsf{LCP}(4,1)=0$, we have that $1$ outputs $\mathtt{p}$,
$\mathtt{pa}$,…$\mathtt{papaya}$; and $3$ only $\mathtt{pay}$ and
$\mathtt{paya}$. Finally, from $5$, we get $\mathtt{y}$ and $\mathtt{ya}$.

The suffix tree can be constructed in time $\mathcal{O}(|w|)$ (see e. g. [17,
5]). Note that we can ensure that the children of each node are ordered
lexicographically. To allow us enumerating all factors, we traverse the suffix
tree depth-first during the preprocessing and create a list
$L=i_{1},\ldots,i_{k}$ of those leaves for which the incoming edge is labeled
with more than just $\mathdollar$ (see Figure 3). For the actual enumeration,
we iterate over this list and use the leaves to output factors as follows:

  * •

$i_{1}$ generates $\varepsilon$ and $w_{[i_{1},i_{1}+1\rangle}$ to
$w_{[i_{1},n+1\rangle}$ (where we assume that $w_{[n,n+1\rangle}$ is the last
letter of $w$, not $\mathdollar$), and

  * •

for $1\leq j<k$, every $i_{j+1}$ generates
$w_{[i_{j+1},i_{j+1}+\mathsf{LCP}(i_{j},i_{j+1})+1\rangle}$ to
$w_{[i_{j+1},n+1\rangle}$.

That is, we use the suffix tree to enumerate all suffixes; and for each
suffix, we enumerate all of its prefixes (apart from those that were already
enumerated, which we spot skip by using $\mathsf{LCP}$, see “Evaluation”
above). As the list $L$ was derived directly from the tree, all leaves that
have a common parent (which means that they longest common prefix is not
$\varepsilon$) are grouped together as a block. By using $\mathsf{LCP}$, we
ensure that no factor is output twice. This is also why $L$ does not include
leaves where the incoming edge is labeled $\mathdollar$; factors that could be
obtained from these words are handled by other leaves. As the children of each
inner node are ordered lexicographically, the construction also ensures that
the factors of $w$ are output in lexicographic order. See Figure 3 for an
example.

The list $L$ can be created in linear time during the preprocessing. Each of
the steps during the enumeration – iterating over $L$, calling $\mathsf{LCP}$,
and moving the indices – takes only constant time. As the factors are returned
as spans, we can conclude constant delay.

Enumeration of all solutions To enumerate all $\sigma\in\llbracket
x\mathbin{\dot{=}}y\cdot z\rrbracket(w)$, we need to consider various cases
that depend on the three variables. The “standard” case is that the variables
$x,y,z$ are pairwise distinct, and none of them is $\mathfrak{u}$. Then all we
need to do is enumerate all $u\sqsubseteq w$ (as described above). For each of
these, we enumerate all ways of splitting $u$ into $v_{1},v_{2}$ with
$u=v_{1}\cdot v_{2}$, by enumerating the lengths of $v_{1}$ from 0 to $|u|$.
In each case, we define $\sigma(x):=u$, $\sigma(y):=u_{1}$, and
$\sigma(z):=u_{2}$ (and, of course, $\sigma(\mathfrak{u}):=w$).

Regarding special cases, we first discuss those where at least one variable is
$\mathfrak{u}$:

  * •

If $y=\mathfrak{u}$, the only solution is $\sigma(x):=\sigma(y)=w$ and
$\sigma(z):=\varepsilon$. This is well-defined – unless $z=\mathfrak{u}$ and
$w\neq\varepsilon$. In this case, we have $\llbracket x\mathbin{\dot{=}}y\cdot
z\rrbracket(w)=\emptyset$. This can be identified during the preprocessing.

  * •

If $z=\mathfrak{u}$, we proceed as in the previous case.

  * •

If $x=\mathfrak{u}$ and $y,z\neq\mathfrak{u}$, we distinguish two cases:

    * –

If $y\neq z$, we set $\sigma(\mathfrak{u}):=w$, and generate all possible
$\sigma(y)$ and $\sigma(z)$ by enumerating all ways of splitting $w$ (as in
the standard case).

    * –

If $y=z$, we check if the first and second half of $w$ are identical (using
$\mathsf{LCP}$ and arithmetic, we can perform this check in constant time
during the preprocessing). If this is the case, we can define the only
$\sigma$ in $\llbracket\mathfrak{u}\mathbin{\dot{=}}y\cdot y\rrbracket(w)$
accordingly. Otherwise, the set is empty.

Now we can assume that none of the three variables is $\mathfrak{u}$, which
leaves only cases where at least two are identical.

  * •

If $x=y=z$, the only $\sigma$ with $\sigma\in\llbracket
x\mathbin{\dot{=}}y\cdot z\rrbracket(w)$ has $\sigma(x)=\varepsilon$.

  * •

If $x=y\neq z$, we can assume $\sigma(z)=\varepsilon$, and can choose any
factor of $w$ for $\sigma(x)$. Hence, we enumerate all factors of $w$. The
case for $x=z\neq y$ is analogous.

  * •

If $x\neq y=z$, we enumerate all $u\sqsubseteq w$ that are squares (i. e.,
that can be written as $u=vv$ for some $v\sqsubseteq w$. Enumerating all these
squares with constant delay is possible with additional preprocessing on the
suffix tree, see Gusfield and Stoye[18].

Hence, we can set up the data structures for each of these cases during the
preprocessing. Given a word equation $x\mathbin{\dot{=}}y\cdot z$, we can then
pick the appropriate enumeration algorithm that allows us to enumerate
$\llbracket x\mathbin{\dot{=}}y\cdot z\rrbracket(w)$ with constant delay.

This construction also applies to equations of the form
$x\mathbin{\dot{=}}y_{1}\cdots y_{k}$ with $k>2$, assuming that $x$ and all
$y_{i}$ are pairwise distinct (this proceeds as the “standard case”).

##  Appendix D Proof of 4.7

Before proving Proposition 4.7, we give the version of the GYO algorithm that
we work with to decide the decomposition
$\Psi_{\tilde{\alpha}}:=\mathsf{Ans}(\vec{x})\leftarrow\bigwedge_{i=1}^{m}\chi_{i}$
of $\tilde{\alpha}\in\mathsf{BPat}(\alpha)$ is acyclic333We use variant of
$\chi$ to denote atoms of some decomposition. (see Chapter 6 of [1] for more
information on acyclic joins). We remind the reader that $\mathfrak{u}$ is
considered a constant symbol (not a variable) since $\sigma(\mathfrak{u})$ is
always our input document, $w\in\Sigma^{*}$.

  1. 1.

Let $E:=\emptyset$ and $V:=\\{\chi_{i}\mid i\in[m]\\}$.

  2. 2.

Define all nodes of $V$ and all variables in
$\mathsf{var}(\Psi_{\tilde{\alpha}})$ as _unmarked_.

  3. 3.

Repeat the following until nothing changes:

    1. (a)

If there exists unmarked nodes $\chi_{i}$ and $\chi_{j}$ with $i\neq j$ such
that $\mathsf{var}(\chi_{i})\subseteq\mathsf{var}(\chi_{j})$, then:

      1. i.

Mark $\chi_{i}$ and add the edge $\\{\chi_{i},\chi_{j}\\}$ to $E$.

    2. (b)

Mark all $x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$ that occurs in exactly one
unmarked node.

  4. 4.

If there exists exactly one unmarked node, then return $T:=(V,E)$.

  5. 5.

Otherwise, return “$\tilde{\alpha}$ is cyclic”.

See 4.7

######  Proof D.1.

We prove this Proposition in two parts.

Part 1. There exists a cyclic pattern: Let
$\alpha:=x_{1}x_{2}x_{1}x_{3}x_{1}$. We prove that $\alpha$ is cyclic by
enumerating every possible bracketing
$\tilde{\alpha}\in\mathsf{BPat}(\alpha)$, and then show that the decomposition
of each bracketing is cyclic. To show a formula is cyclic, we can use the GYO
algorithm.

After the GYO algorithm has been executed on a $2\mathsf{FC\mathchar 45\relax
CQ}$, we have a set of unmarked nodes, and each unmarked node contains
unmarked variables. We represent each unmarked node as a set containing its
unmarked variables. The set of unmarked nodes for $\Psi_{\tilde{\alpha}_{i}}$
after the GYO algorithm has been executed is denoted by $\mathcal{H}_{i}$.
Therefore, the formula $\Psi_{\tilde{\alpha}_{i}}$ is acyclic if and only if
$|\mathcal{H}_{i}|=1$. We now consider all the bracketings, the corresponding
decompositions, and the set $\mathcal{H}_{i}$ for each
$\tilde{\alpha}_{i}\in\mathsf{BPat}(\alpha)$:

  * •

$\tilde{\alpha}_{1}:=((x_{1}\cdot(x_{2}\cdot(x_{1}\cdot(x_{3}\cdot x_{1})))))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{1}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{3}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}x_{1}\cdot
z_{1})\land(z_{3}\mathbin{\dot{=}}x_{2}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{1}:=$
$\displaystyle\\{\\{z_{2},x_{1}\\},\\{z_{3},z_{2}\\},\\{x_{1},z_{3}\\}\\}.$

  * •

$\tilde{\alpha}_{2}:=(x_{1}\cdot(x_{2}\cdot((x_{1}\cdot x_{3})\cdot x_{1})))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{2}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{3})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{1})\land(z_{3}\mathbin{\dot{=}}x_{2}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{2}:=$
$\displaystyle\\{\\{z_{2},x_{1}\\},\\{z_{3},z_{2}\\},\\{x_{1},z_{3}\\}\\}.$

  * •

$\tilde{\alpha}_{3}:=((x_{1}\cdot x_{2})\cdot(x_{1}\cdot(x_{3}\cdot x_{1})))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{3}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{3}\cdot
x_{1})\land(z_{3}\mathbin{\dot{=}}x_{1}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}z_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{3}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},x_{1}\\},\\{z_{3},z_{1},z_{2}\\},\\{x_{1},z_{3}\\}\\}.$

  * •

$\tilde{\alpha}_{4}:=(x_{1}\cdot((x_{2}\cdot x_{1})\cdot(x_{3}\cdot x_{1})))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{4}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{3}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}x_{2}\cdot
x_{1})\land(z_{3}\mathbin{\dot{=}}z_{1}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{4}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},z_{1}\\},\\{z_{2},x_{1}\\}\\}.$

  * •

$\tilde{\alpha}_{5}:=(x_{1}\cdot((x_{2}\cdot(x_{1}\cdot x_{3}))\cdot x_{1}))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{5}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{3})\land(z_{2}\mathbin{\dot{=}}x_{2}\cdot
z_{1})\land(z_{3}\mathbin{\dot{=}}z_{2}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{5}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},z_{1}\\},\\{z_{2},x_{1}\\}\\}.$

  * •

$\tilde{\alpha}_{6}:=(x_{1}\cdot(((x_{2}\cdot x_{1})\cdot x_{3})\cdot x_{1}))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{6}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{2}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{3})\land(z_{3}\mathbin{\dot{=}}z_{2}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{6}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{3},z_{2},x_{1}\\},\\{z_{1},z_{3}\\}\\}.$

  * •

$\tilde{\alpha}_{7}:=((x_{1}\cdot x_{2})\cdot((x_{1}\cdot x_{3})\cdot x_{1}))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{7}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{1}\cdot
x_{3})\land(z_{3}\mathbin{\dot{=}}z_{2}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}z_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{7}:=$
$\displaystyle\\{\\{z_{2},x_{1}\\},\\{z_{3},x_{1}\\},\\{z_{3},z_{2}\\}\\}.$

  * •

$\tilde{\alpha}_{8}:=(x_{1}\cdot(x_{2}\cdot x_{1}))\cdot(x_{3}\cdot x_{1}))$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{8}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{2}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}x_{3}\cdot
x_{1})\land(z_{3}\mathbin{\dot{=}}x_{1}\cdot
z_{1})\land(\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot z_{2}),$
$\displaystyle\mathcal{H}_{8}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},z_{1}\\},\\{z_{2},x_{1}\\}\\}.$

  * •

$\tilde{\alpha}_{9}:=(x_{1}\cdot(x_{2}\cdot(x_{3}\cdot x_{1})))\cdot x_{1})$
which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{9}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{3}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}x_{2}\cdot
z_{1})\land(z_{3}\mathbin{\dot{=}}z_{2}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}x_{1}\cdot z_{3}),$
$\displaystyle\mathcal{H}_{9}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},z_{1}\\},\\{x_{1},z_{2}\\}\\}.$

  * •

$\tilde{\alpha}_{10}:=((x_{1}\cdot((x_{2}\cdot x_{1})\cdot x_{3}))\cdot
x_{1})$ which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{10}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{2}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{3})\land(z_{3}\mathbin{\dot{=}}x_{1}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot x_{1}),$
$\displaystyle\mathcal{H}_{10}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},x_{1}\\},\\{z_{3},z_{1},z_{2}\\},\\{z_{3},x_{1}\\}\\}.$

  * •

$\tilde{\alpha}_{11}:=(((x_{1}\cdot x_{2})\cdot(x_{1}\cdot x_{3}))\cdot
x_{1})$ which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{11}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{1}\cdot
x_{3})\land(z_{3}\mathbin{\dot{=}}z_{1}\cdot
z_{2})\land(\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot x_{1}),$
$\displaystyle\mathcal{H}_{11}:=$
$\displaystyle\\{\\{z_{1},x_{1}\\},\\{z_{2},x_{1}\\},\\{z_{3},z_{1},z_{2}\\},\\{z_{3},x_{1}\\}\\}.$

  * •

$\tilde{\alpha}_{12}:=(((x_{1}\cdot x_{2})\cdot x_{1})\cdot(x_{3}\cdot
x_{1}))$ which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{12}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{3}\cdot
x_{1})\land(z_{3}\mathbin{\dot{=}}z_{1}\cdot
x_{1})\land(\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot z_{2}),$
$\displaystyle\mathcal{H}_{12}:=$
$\displaystyle\\{\\{z_{2},x_{1}\\},\\{z_{3},x_{1}\\},\\{z_{3},z_{2}\\}\\}.$

  * •

$\tilde{\alpha}_{13}:=(((x_{1}\cdot(x_{2}\cdot x_{1}))\cdot x_{3})\cdot
x_{1})$ which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{13}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{2}\cdot
x_{1})\land(z_{2}\mathbin{\dot{=}}x_{1}\cdot
z_{1})\land(z_{3}\mathbin{\dot{=}}z_{2}\cdot
x_{3})\land(\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot x_{1}),$
$\displaystyle\mathcal{H}_{13}:=$
$\displaystyle\\{\\{z_{2},x_{1}\\},\\{z_{3},z_{2}\\},\\{z_{3},x_{1}\\}\\}.$

  * •

$\tilde{\alpha}_{14}:=((((x_{1}\cdot x_{2})\cdot x_{1})\cdot x_{3})\cdot
x_{1})$ which decomposes into

$\displaystyle\Psi_{\tilde{\alpha}_{14}}:=$
$\displaystyle\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}z_{1}\cdot
x_{1})\land(z_{3}\mathbin{\dot{=}}z_{2}\cdot
x_{3})\land(\mathfrak{u}\mathbin{\dot{=}}z_{3}\cdot x_{1}),$
$\displaystyle\mathcal{H}_{14}:=$
$\displaystyle\\{\\{z_{2},x_{1}\\},\\{z_{3},z_{2}\\},\\{z_{3},x_{1}\\}\\}.$

For every $\tilde{\alpha}_{i}\in\mathsf{BPat}(\alpha)$, we have that
$|\mathcal{H}_{i}|>1$. We can conclude that $\alpha$ is cyclic.

Part 2: There exists an acyclic pattern which has a cyclic bracketing. Let
$\alpha:=x_{1}x_{2}x_{3}x_{1}$, let
$\tilde{\alpha}_{1}:=((x_{1}\cdot(x_{2}\cdot x_{3}))\cdot x_{1})$, and let
$\tilde{\alpha}_{2}:=((x_{1}\cdot x_{2})\cdot(x_{3}\cdot x_{1}))$. The
decomposition of $\tilde{\alpha}_{1}$ is
$\Psi_{\tilde{\alpha}_{1}}:=\mathsf{Ans}()\leftarrow(z_{1}\mathbin{\dot{=}}x_{2}\cdot
x_{3})\land(z_{2}\mathbin{\dot{=}}x_{1}\cdot
z_{1})\land(\mathfrak{u}\mathbin{\dot{=}}z_{2}\cdot x_{1})$. Executing the GYO
algorithm on $\Psi_{\tilde{\alpha}_{1}}$ shows it to be acyclic.

The decomposition of $\tilde{\alpha}_{2}$ is
$\Psi_{\tilde{\alpha}_{2}}:=\mathsf{Ans}()\leftarrow(\mathfrak{u}\mathbin{\dot{=}}z_{1}\cdot
z_{2})\land(z_{1}\mathbin{\dot{=}}x_{1}\cdot
x_{2})\land(z_{2}\mathbin{\dot{=}}x_{3}\cdot x_{1})$. Performing the GYO
algorithm on $\Psi_{\tilde{\alpha}_{1}}$ will show it to be cyclic. Therefore,
we have proven that not all bracketings of an acyclic pattern is an acyclic
bracketing.

##  Appendix E Proof of 4.11

We first prove a useful lemma that makes the actual proof of Lemma 4.11 more
readable.

######  Lemma E.1.

If $T:=(V,E)$ is an undirected tree where $V:=[n]$, then every node that lies
on the path from $i$ to $j$, for $i,j\in[n]$ where $i<j$, must exist on a path
from $k$ to $k+1$ for some $k\in\\{i,i+1,\dots,j-1\\}$.

######  Proof E.2.

Let $T:=(V,E)$ be an undirected tree where $V:=[n]$. For any
$k,k^{\prime}\in[n]$, let $p_{k\rightarrow k^{\prime}}$ be the path from $k$
to $k^{\prime}$ in $T$. The path $p_{i\rightarrow j}$ can be constructed by
considering the sequence of edges $p_{i\rightarrow i+1}\cdot p_{i+1\rightarrow
i+2}\cdots p_{j-1\rightarrow j}$, then removing all edges which appear more
than once from this sequence. Since this defines a path from $i$ and $j$, and
there can only be one path between any two nodes in a tree, the stated lemma
holds.

Lemma E.1 can clearly be generalized to trees with any vertex set, $V$, by
considering some bijection from the vertices of the tree to $[n]$ where
$|V|=n$.

If $\eta:=(x\mathbin{\dot{=}}y\cdot z)$ is an atom of the acyclic
decomposition $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$,
then the right-hand side of $\eta$ can be reversed, i. e.
$\eta:=(x\mathbin{\dot{=}}z\cdot y)$, and $\Psi_{\tilde{\alpha}}$ remains
acyclic. Therefore, in the following proof, when the right-hand side of an
atom is ambiguous, we can assume one without loss of generality.

### Actual Proof of 4.11.

See 4.11

######  Proof E.3.

Let $\Psi_{\tilde{\alpha}}\in 2\mathsf{FC\mathchar 45\relax CQ}$ be a
decomposition of $\tilde{\alpha}\in\mathsf{BPat}$ and let
$\mathcal{T}:=(\mathcal{V},\mathcal{E},<,\Gamma,\tau,v_{r})$ be the
concatenation tree for $\Psi_{\tilde{\alpha}}$.

If-direction. If $\Psi_{\tilde{\alpha}}$ is $x$-localized for all
$x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$, then we can construct a join tree
for $\Psi_{\tilde{\alpha}}$ by augmenting the concatenation tree: First
replace all non-leaf nodes $v\in\mathcal{V}$ with $\mathsf{atom}(v)$. Then
remove all leaf nodes. By the definition of the concatenation tree, every atom
of $\Psi_{\tilde{\alpha}}$ is a node in the supposed join tree. Also due to
the definition of a concatenation tree, if $v$ is an $x$-parent, then $x$
occurs in $\mathsf{atom}(v)$. Because $\Psi_{\tilde{\alpha}}$ is $x$-localized
for all $x\in\mathsf{var}(\Psi_{\tilde{\alpha}})$, it follows that if two
nodes in the supposed join tree contain the variable $x$, then all nodes which
exist on the path between these two nodes also contains an $x$. Hence, the
resulting tree is a valid join tree for $\Psi_{\tilde{\alpha}}$.

Only if-direction. Let $v_{0},v_{n}\in\mathcal{V}$ be two $x$-parents such
that the distance between $v_{0}$ and $v_{n}$ in the concatenation tree
$\mathcal{T}$ is $n>1$. Let $v_{1},v_{2},\dots v_{n-1}\in\mathcal{V}$ be the
nodes on the path between $v_{0}$ and $v_{n}$ in $\mathcal{T}$ where $v_{i}$
is not an $x$-parent for all $i\in[n-1]$, hence $\Psi_{\tilde{\alpha}}$ is not
$x$-localized. For readability, we assume that $\tau(v_{i})=z_{i}$ for all
$i\in\\{0,1,\dots,n\\}$. Because the concatenation tree is pruned,
$\mathsf{atom}(v_{i})=\mathsf{atom}(v_{j})$ if and only if $i=j$, for
$i,j\in\\{0,1,\dots,n\\}$. Furthermore, if $\tau(v)=z_{i}$ where $v$ is a non-
leaf node, then $v=v_{i}$ because two different non-leaf nodes cannot share a
label. Figure 4 illustrates a subtree of $\mathcal{T}$. The variable that
labels each node is given next to the node in parentheses.

$v_{k}\;(z_{k})$$v_{k+1}\;(z_{k+1})$$v_{k-1}\;(z_{k-1})$$\vdots$$\vdots$$v_{0}\;(z_{0})$$v_{n}\;(z_{n})$$\vdots$$\vdots$$v\;(x)$$v^{\prime}\;(x)$$\vdots$$\vdots$
Figure 4:  The concatenation tree, $\mathcal{T}$, we use for the only if-
direction in the proof of Lemma 4.11.

For sake of a contradiction, assume there exists a join tree $T:=(V,E)$ for
$\Psi_{\tilde{\alpha}}$. Nodes in the join tree are the atoms of
$\Psi_{\tilde{\alpha}}$ and therefore any element of $V$ can be uniquely
determined by $\mathsf{atom}(v)$ where $v\in\mathcal{V}$ is a non-leaf node in
the concatenation tree. We remind the reader that
$\mathsf{atom}(v)=(z\mathbin{\dot{=}}x\cdot x^{\prime})$ if $v$ is labeled $z$
and the left and right children of $v$ are labeled $x$ and $x^{\prime}$
respectively. To improve readability, we use (variants of) $v$ for nodes of
the concatenation tree, and we use $\mathsf{atom}(v)$ for nodes of the join
tree where $v$ is some non-leaf node of the concatenation tree.

We relax the factor notation to variables in
$\mathsf{var}(\Psi_{\tilde{\alpha}})$. We write $z\sqsubset z^{\prime}$, where
$z,z^{\prime}\in\mathsf{var}(\Psi_{\tilde{\alpha}})$, if there exists
$v,v^{\prime}\in\mathcal{V}$ where $v^{\prime}$ which is an ancestor of $v$ in
the concatenation tree, and $\tau(v^{\prime})=z^{\prime}$ and $\tau(v)=z$. We
do this because the pattern that $z$ represents is a factor of the pattern
$z^{\prime}$ represents.

Let $p_{i\rightarrow j}$ be the path in the join tree, $T$, from
$\mathsf{atom}(v_{i})$ to $\mathsf{atom}(v_{j})$ for any
$i,j\in\\{0,1,\dots,n\\}$. The atom $\mathsf{atom}(v_{1})$ cannot exist on the
path $p_{0\rightarrow n}$ because $\mathsf{atom}(v_{0})$ and
$\mathsf{atom}(v_{n})$ contain the variable $x$, but $\mathsf{atom}(v_{1})$
does not contain the variable $x$. We therefore consider some non-leaf node
$v_{1}^{\prime}\in\mathcal{V}$ of the concatenation tree such that
$\mathsf{atom}(v_{1}^{\prime})$ is the atom on the path $p_{0\rightarrow n}$
which is closest (with regards to distance) to $\mathsf{atom}(v_{1})$. See
Figure 5 for a diagram to illustrate $\mathsf{atom}(v_{1}^{\prime})$. We know
that $\mathsf{atom}(v_{1}^{\prime})$ has a variable $x$ since it lies on the
path $p_{0\rightarrow n}$.

We now prove that $\mathsf{atom}(v_{1}^{\prime})$ contains some variable
$z_{i}$ where $i\in[n]$. Since $\mathsf{atom}(v_{1}^{\prime})$ is the node
closest to $\mathsf{atom}(v_{1})$ on the path $p_{0\rightarrow n}$, we have
that $\mathsf{atom}(v_{1}^{\prime})$ must also exist on the path
$p_{1\rightarrow n}$ (see Figure 5). Therefore, because of Lemma E.1,
$\mathsf{atom}(v_{1}^{\prime})$ must exist on some path $p_{j\rightarrow j+1}$
for some $j\in[n-1]$. Since $\mathsf{atom}(v_{j})$ and
$\mathsf{atom}(v_{j+1})$ share the variable $z_{j}$ or $z_{j+1}$ (depending on
whether $v_{j}$ or $v_{j+1}$ is the parent) for all $j\in[n-1]$, it follows
that $\mathsf{atom}(v_{1}^{\prime})$ must contain the variable $z_{i}$ for
some $i\in[n]$.

$\mathsf{atom}(v_{0})$…$\mathsf{atom}(v_{1}^{\prime})$$\vdots$$\mathsf{atom}(v_{1})$…$\mathsf{atom}(v_{n})$
Figure 5:  A figure to illustrate paths $p_{0\rightarrow 1}$ and
$p_{0\rightarrow n}$.

Case 1: $v_{n}$ is an ancestor of $v_{0}$ in $\mathcal{T}$.

Since $v_{n}$ is an ancestor of $v_{0}$, we know that $v_{i}$ is an ancestor
of $v_{0}$ (and hence $x\sqsubset z_{0}\sqsubset z_{i}$) for all $i\in[n]$.
Furthermore, it follows that $v_{1}$ is a $z_{0}$-parent and therefore
$\mathsf{atom}(v_{1})=(z_{1}\mathbin{\dot{=}}z_{0}\cdot z^{\prime})$ for some
$z^{\prime}\in\Xi$. Since $\mathsf{atom}(v_{1}^{\prime})$ lies on the path
$p_{0\rightarrow 1}$, it follows that $\mathsf{atom}(v_{1}^{\prime})$ contains
the variable $z_{0}$. One of the variables of $\mathsf{atom}(v_{1}^{\prime})$
must be the label of $v_{1}^{\prime}$, we therefore consider all the possible
labels for $v_{1}^{\prime}$ and show a contradiction for each.

  * •

$\tau(v_{1}^{\prime})=x$. This implies that, without loss of generality,
$\mathsf{atom}(v_{1}^{\prime})=(x\mathbin{\dot{=}}z_{0}\cdot z_{i})$ and
therefore $z_{0}\sqsubset x$. We know that $x\sqsubset z_{0}$ since $v_{0}$ is
an $x$-parent. Therefore, $z_{0}\sqsubset z_{0}$ which we know cannot hold and
hence $\tau(v_{1}^{\prime})=x$ cannot hold.

  * •

$\tau(v_{1}^{\prime})=z_{i}$ where $i\in[n]$. We split this case into two
parts:

    * –

$\tau(v_{1}^{\prime})=z_{i}$ where $i\in[n-1]$. This implies that
$\mathsf{atom}(v_{1}^{\prime})=\mathsf{atom}(v_{i})$. The word equation
$\mathsf{atom}(v_{i})$ does not contain an $x$. Since we know that
$\mathsf{atom}(v_{1}^{\prime})$ contains the variable $x$, we can conclude
that $\tau(v_{1}^{\prime})=z_{i}$ where $i\in[n-1]$ cannot hold.

    * –

$\tau(v_{1}^{\prime})=z_{n}$. This implies that
$\mathsf{atom}(v_{1}^{\prime})=\mathsf{atom}(v_{n})$ and therefore, without
loss of generality, $\mathsf{atom}(v_{n})=(z_{n}\mathbin{\dot{=}}x\cdot
z_{0})$. However, since we are in the case that $v_{n}$ is an ancestor of
$v_{0}$, it follows that $v_{n}$ is a parent of $v_{0}$ (since a node labeled
$x$ or $z_{0}$ cannot be an ancestor of $v_{0}$). Therefore
$\Psi_{\tilde{\alpha}}$ is $x$-localized, and hence
$\tau(v_{1}^{\prime})=z_{n}$ cannot hold.

  * •

$\tau(v_{1}^{\prime})=z_{0}$. This implies that
$\mathsf{atom}(v_{1}^{\prime})=\mathsf{atom}(v_{0})$. Therefore, without loss
of generality, $\mathsf{atom}(v_{0})=(z_{0}\mathbin{\dot{=}}x\cdot z_{i})$. We
also know that $z_{0}\sqsubset z_{i}$ since $v_{i}$ is an ancestor of $v_{0}$.
Therefore, $z_{0}\sqsubset z_{i}\sqsubset z_{0}$, which we know cannot hold.
Thus, $\tau(v_{1}^{\prime})=z_{0}$ cannot hold.

We have proven that, for the case where $v_{n}$ is an ancestor of $v_{0}$ in
the concatenation tree, there does not exist a valid label for
$v_{1}^{\prime}$. Hence we have reached a contradiction and therefore our
assumption $\Psi_{\tilde{\alpha}}$ is acyclic cannot hold.

Case 2: $v_{0}$ is an ancestor of $v_{n}$ in $\mathcal{T}$.

The case where $v_{0}$ is an ancestor of $v_{n}$ is trivially identical to
Case 1 by considering the closest node to $\mathsf{atom}(v_{n-1})$ on the path
$p_{n\rightarrow 0}$. We have therefore omitted the proof.

Case 3: $v_{n}$ is not an ancestor of $v_{0}$ in $\mathcal{T}$, and $v_{0}$ is
not an ancestor of $v_{n}$ in $\mathcal{T}$.

Let $k\in[n-1]$ such that $v_{k}\in\mathcal{V}$ is the lowest common ancestor
of $v_{0}$ and $v_{n}$ in $\mathcal{T}$. We remind the reader that
$\mathsf{atom}(v_{1}^{\prime})$ has the variables $x$, and $z_{i}$ for some
$i\in[n]$ because $\mathsf{atom}(v_{1}^{\prime})$ lies on the paths
$p_{0\rightarrow n}$ and $p_{1\rightarrow n}$. We also have that
$\mathsf{atom}(v_{1})=(z_{1}\mathbin{\dot{=}}z_{0}\cdot z^{\prime})$ for some
$z^{\prime}\in\Xi$, because for this case, $v_{1}$ must be a parent of
$v_{0}$, otherwise $v_{0}$ would be an ancestor of $v_{n}$. Therefore, since
$\mathsf{atom}(v_{0})$ and $\mathsf{atom}(v_{1})$ share the variable $z_{0}$,
we know that $\mathsf{atom}(v_{1}^{\prime})$ also contains a $z_{0}$ – because
$\mathsf{atom}(v_{1}^{\prime})$ lies on the path $p_{0\rightarrow 1}$. We now
consider each label for $v_{1}^{\prime}$ and show a contradiction for each
case.

Case 3.1: $\tau(v_{1}^{\prime})=x$. Without loss of generality,
$\mathsf{atom}(v_{1}^{\prime})=(x\mathbin{\dot{=}}z_{0}\cdot z_{i})$ which
implies that $x\sqsubset z_{0}$ and $z_{0}\sqsubset x$. This is a
contradiction and hence $\tau(v_{1}^{\prime})=x$ cannot hold.

Case 3.2: $\tau(v_{1}^{\prime})=z_{i}$ where $i\in[n-1]$. This implies
$\mathsf{atom}(v_{1}^{\prime})=\mathsf{atom}(v_{i})$, but
$\mathsf{atom}(v_{i})$ cannot have the variable $x$. This is a contradiction
and hence $\tau(v_{1}^{\prime})=z_{i}$ where $i\in[n-1]$ cannot hold.

Case 3.3: $\tau(v_{1}^{\prime})=z_{n}$. This implies that
$\mathsf{atom}(v_{1}^{\prime})=\mathsf{atom}(v_{n})$ and therefore without
loss of generality, we know that
$\mathsf{atom}(v_{n})=(z_{n}\mathbin{\dot{=}}z_{0}\cdot x)$, because
$\mathsf{atom}(v_{1}^{\prime})$ must contain the variable $z_{0}$ and $x$. For
this case, we first prove that $k\geq 2$ where $v_{k}$ is the lowest common
ancestor of $v_{0}$ and $v_{n}$. For sake of contradiction, assume $k=1$. It
follows that the distance from $v_{k}$ to $v_{0}$ is one and the distance from
$v_{k}$ to $v_{n}$ is greater than or equal to one. Hence, the distance from
$v_{k}$ to the children of $v_{n}$ is greater than or equal to two. Since
$v_{n}$ is a $z_{0}$ parent, and the children of $v_{n}$ are further from the
root than $v_{0}$, we know that $v_{0}$ must be redundant. If this is the
case, $v_{0}$ would have no children due to the pruning procedure used when
defining a concatenation tree. Therefore, $v_{0}$ would not be an $x$-parent
which we know cannot hold (we have chosen $v_{0}$ _because_ it is an
$x$-parent). Therefore, $k=1$ cannot hold and we can conclude $k\geq 2$.

We now consider $\mathsf{atom}(v_{k})$. We know that
$\mathsf{atom}(v_{k})=(z_{k}\mathbin{\dot{=}}z_{k-1}\cdot z_{k+1})$ and since
we have proven that $k\geq 2$, it follows that $z_{k-1}\neq z_{0}$. Since both
$\mathsf{atom}(v_{1})$ and $\mathsf{atom}(v_{n})$ contain the variable
$z_{0}$, we know that $\mathsf{atom}(v_{k})$ cannot exist on the path
$p_{1\rightarrow n}$. Hence, we consider some non-leaf node
$v_{k}^{\prime}\in\mathcal{V}$ such that $\mathsf{atom}(v_{k}^{\prime})$ lies
on the path $p_{1\rightarrow n}$ and $\mathsf{atom}(v_{k}^{\prime})$ is the
node on $p_{1\rightarrow n}$ which is closest node (with regards to distance)
to $\mathsf{atom}(v_{k})$. We illustrate a subtree of such a join tree in
Figure 6.

We now prove that $\mathsf{atom}(v_{k}^{\prime})$ must contain some variable
$z_{j}\in\Xi$, where $j\in[k-1]$. We know that $\mathsf{atom}(v_{k}^{\prime})$
lies on the path $p_{1\rightarrow k}$, therefore, because of Lemma E.1,
$\mathsf{atom}(v_{k}^{\prime})$ must lies on the path $p_{i\rightarrow i+1}$
for some $i\in[k-1]$. Since each atom which lies on the path $p_{i\rightarrow
i+1}$ must contain the variable $z_{i}$, it follows that
$\mathsf{atom}(v_{k}^{\prime})$ contains the variable $z_{j}$ for some
$j\in[k-1]$. Figure 4 illustrates why all nodes on the path $p_{i\rightarrow
i+1}$ for $i\in[k-1]$ must contain the variable $z_{i}$ (because $v_{i+1}$ is
a parent of $v_{i}$ for $i\in[k-1]$).

We now show that $\mathsf{atom}(v_{k}^{\prime})$ must also contain the
variable $z_{l}\in\Xi$ for some $l\in\\{k+1,\dots,n\\}$. We know that
$\mathsf{atom}(v_{k}^{\prime})$ lies on the path $p_{k\rightarrow n}$,
therefore, because of Lemma E.1, $\mathsf{atom}(v_{k}^{\prime})$ must lies on
the path $p_{i\rightarrow i+1}$ for some $i\in\\{k,\dots,n-1\\}$. Since each
atom which lies on the path $p_{i\rightarrow i+1}$ must contain the variable
$z_{i+1}$ for $i\in\\{k,\dots,n-1\\}$, it follows that
$\mathsf{atom}(v_{k}^{\prime})$ contains the variable $z_{l}$ for some
$l\in\\{k+1,\dots,n\\}$. Next, we consider the possible labels of
$v_{k}^{\prime}$.

$(z_{0}\mathbin{\dot{=}}x\cdot
z_{0}^{\prime})$$\vdots$$(z_{n}\mathbin{\dot{=}}x\cdot
z_{0})$…$\mathsf{atom}(v_{k}^{\prime})$…$(z_{1}\mathbin{\dot{=}}z_{0}\cdot
z^{\prime})$$\vdots$$(z_{k}\mathbin{\dot{=}}z_{k-1}\cdot z_{k+1})$ Figure 6:
A subtree of a join tree with nodes $\mathsf{atom}(v_{0})$,
$\mathsf{atom}(v_{n})$, $\mathsf{atom}(v_{k})$,
$\mathsf{atom}(v_{k}^{\prime})$ and $\mathsf{atom}(v_{1})$. This figure is
used to illustrate Case 3.3.

  * •

$\tau(v_{k}^{\prime})=z_{0}$. This implies
$\mathsf{atom}(v_{k}^{\prime})=\mathsf{atom}(v_{0})$. We can therefore state,
without loss of generality, that
$\mathsf{atom}(v_{0})=(z_{0}\mathbin{\dot{=}}z_{j}\cdot z_{l})$. However, if
this is the case then $x$ is not a variable of $\mathsf{atom}(v_{0})$. Hence,
$\tau(v_{k}^{\prime})=z_{0}$ cannot hold.

  * •

$\tau(v_{k}^{\prime})=z_{j}$ where $j\in[k-1]$. This implies that, without
loss of generality,
$\mathsf{atom}(v_{k}^{\prime})=(z_{j}\mathbin{\dot{=}}z_{0}\cdot z_{l})$. If
this is the case then $j=1$ must hold, since this is the only value for $j$
such that $(z_{j}\mathbin{\dot{=}}z_{0}\cdot z_{l})$ can hold. We can
therefore say that $\mathsf{atom}(v_{k}^{\prime})=\mathsf{atom}(v_{1})$. For
all nodes $v\in\mathcal{V}$, let $D(v)$ be the distance from the root of
$\mathcal{T}$ to $v$. Since $v_{l}$ cannot be a redundant node, it follows
that $D(v_{1})+1\leq D(v_{l})$. This implies that $D(v_{k})+k-1+1\leq
D(v_{k})+l-k$ and hence, $k\leq\frac{l}{2}$. Because
$\mathsf{atom}(v_{n})=(z_{n}\mathbin{\dot{=}}z_{0}\cdot x)$ and $v_{0}$ is not
redundant, we can also say that $D(v_{n})+1\leq D(v_{0})$ and hence,
$D(v_{k})+n-k+1\leq D(v_{k})+k$ and therefore $n+1\leq 2k$. Consequently,
$\frac{n+1}{2}\leq k\leq\frac{l}{2}$ and hence, $n+1\leq l$. This is a
contradiction since $l\in\\{k+1,\dots,n\\}$. This proves that
$\tau(v_{k})=z_{j}$ cannot hold.

  * •

$\tau(v_{k}^{\prime})=z_{l}$ for $l\in\\{k+1,\dots,n\\}$. We split this case
into two parts:

    * –

$\tau(v_{k}^{\prime})=z_{n}$. This implies that
$\mathsf{atom}(v_{k}^{\prime})=\mathsf{atom}(v_{n})$. We remind the reader
that $\mathsf{atom}(v_{n})=(z_{n}\mathbin{\dot{=}}z_{0}\cdot x)$. Therefore,
$\mathsf{atom}(v_{n})$ does not contain the variable $z_{j}$ for $j\in[k-1]$,
yet we know that $\mathsf{atom}(v_{k}^{\prime})$ does contain the variable
$z_{j}$. Consequently, $\tau(v_{k}^{\prime})=z_{n}$ cannot hold.

    * –

$\tau(v_{k}^{\prime})=z_{l}$ where $l\in\\{k+1,\dots,n-1\\}$. This implies
that, without loss of generality,
$\mathsf{atom}(v_{k}^{\prime})=(z_{l}\mathbin{\dot{=}}z_{0}\cdot z_{j})$. This
cannot hold since if $k<l<n$, then $\mathsf{atom}(v_{l})$ contains the
variable $z_{l+1}$. However, $\mathsf{atom}(v_{k}^{\prime})$ does not contain
the variable $z_{l+1}$.

Consequently, we have proven that if $\tau(v_{1}^{\prime})=z_{n}$, then there
does not exist a valid label for the non-leaf node $v_{k}^{\prime}$, where
$\mathsf{atom}(v_{k}^{\prime})$ is the closest node to $\mathsf{atom}(v_{k})$
on the path $p_{1\rightarrow n}$. Therefore $\tau(v_{1}^{\prime})=z_{n}$
cannot hold.

Case 3.4: $\tau(v_{1}^{\prime})=z_{0}$. This implies that
$\mathsf{atom}(v_{1}^{\prime})=\mathsf{atom}(v_{0})$. Without loss of
generality, $\mathsf{atom}(v_{0})=(z_{0}\mathbin{\dot{=}}x\cdot z_{i})$. We
can see that $k<i\leq n$, since if $1\leq i\leq k$ then $z_{i}\sqsubset
z_{0}\sqsubset z_{i}$ which cannot hold. We now claim that $n>2$ must hold.
For sake of contradiction, assume $n=2$. Since we know that $v_{k}$ is the
lowest common ancestor of $v_{0}$ and $v_{n}$, it follows that $k=1$. It also
follows that $i=n$ since $k<i\leq n$. The distance from $v_{k}$ to $v_{n}$ is
one and the distance from $v_{k}$ to the children of $v_{0}$ is two. Since
$v_{0}$ has a child with the label $z_{n}$, it follows that $v_{n}$ is a
redundant node, and hence it is not an $x$-parent. We know this cannot hold
and hence $n=2$ cannot hold. Therefore, we have proven that $n>2$.

We now consider $\mathsf{atom}(v_{n-1}^{\prime})$ which is the atom of the
path $p_{n\rightarrow 0}$ which is closest to $\mathsf{atom}(v_{n-1})$. Since
$n>2$, it follows that $v_{n-1}\neq v_{1}$. The nodes $v_{0}$ and $v_{n}$ are
arbitrary and therefore $v_{0}$ and $v_{n}$ can be thought of as being
symmetric. Thus, it must hold that
$\mathsf{atom}(v_{n-1}^{\prime})=(z_{n}\mathbin{\dot{=}}x\cdot z_{j})$ where
$0\leq j<k$ (in the same way that
$\mathsf{atom}(v_{1}^{\prime})=(z_{0}\mathbin{\dot{=}}x\cdot z_{i})$ where