# The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations

Marius Bozga, Lucas Bueri, Radu Iosif, Florian Zuleger

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

## To cite this version:

Marius Bozga, Lucas Bueri, Radu Iosif, Florian Zuleger. The Treewidth Boundedness Problem for an Inductive Separation Logic of Relations. 2023. hal-04264291v2

HAL Id: hal-04264291

https://hal.science/hal-04264291v2

Preprint submitted on 23 May 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
THE TREEWIDTH BOUNDEDNESS PROBLEM FOR AN INDUCTIVE
SEPARATION LOGIC OF RELATIONS

MARIUS BOZGA ⚙️ª, LUCAS BUERI ⚙️ª, RADU IOSIF ⚙️ª, AND FLORIAN ZULEGER ⚙️ᵇ

ABSTRACT. The treewidth boundedness problem for a logic asks for the existence of an upper bound on the treewidth of the models of a given formula in that logic. This problem is found to be undecidable for first order logic. We consider a generalization of Separation Logic over relational signatures, interpreted over standard relational structures, and describe an algorithm that decides the treewidth boundedness problem for this logic. Furthermore, our algorithm can give an estimate of the bound of the models of a given formula, in case there is a finite such bound.

# 1. INTRODUCTION

The treewidth of a graph is a positive integer measuring, informally speaking, how far a graph is from a tree. For instance, trees have treewidth one, series-parallel graphs (i.e., circuits with one input and one output that can be either cascaded or overlaid) have treewidth two, whereas $k \times k$ square grids have treewidth $k$, for any $k \ge 1$. The treewidth parameter is a cornerstone of algorithmic tractability. For instance, many NP-complete graph problems such as Hamiltonicity and 3-Colorability become polynomial-time, when restricted to inputs whose treewidth is bounded by a constant (see, e.g., [FG06, Chapter 11] for a survey of classical treewidth-parameterized tractable problems).

Structures are interpretations of relation symbols that define the standard semantics of first and second order logic [vD94]. They provide a unifying framework for reasoning about a multitude of graph types e.g., graphs with multiple edges, labeled graphs, colored graphs, hypergraphs, etc. The notion of treewidth is straightforwardly generalized from graphs to structures. In this context, bounding the treewidth by a constant sets the frontier between the decidability and undecidability of monadic second order (MSO) logical theories. A result of Courcelle [Cou90] proves that MSO is decidable over bounded treewidth structures, by reduction to the emptiness problem of tree automata. A dual result of Seese [See91] proves that each class of structures with a decidable MSO theory necessarily has bounded treewidth. Since MSO is the yardstick of graph specification logics [CE12], these results show that *treewidth bounded* classes of structures are tantamount to the existence of decision procedures for important classes of properties, in those areas of computing where graphs are relevant such as, e.g., static analysis [JM82], databases [ABS00] and concurrency [DNM08].

Key words and phrases: Model Theory, Treewidth, Separation Logic.

<footnote>ª Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France</footnote>

<footnote>ᵇ Institute of Logic and Computation, Technische Universität Wien, Austria</footnote>
This paper considers the *treewidth boundedness problem*, which asks for the existence of a bound on the treewidths of the models of a formula given in input. We show that for first-order logic (and implicitly **MSO**) the problem is already undecidable. This negative result for classical logics motivates our focus on *substructural logics* that have, in addition to boolean conjunction, a conjunction-like connective, for which Gentzen's natural deduction rules of weakening and contraction do not hold. We prove the decidability of this problem for a generalization of Separation Logic to relational signatures, interpreted over structures.

Separation Logic (SL) [IO01, Rey02, CGG02] is a first order substructural logic with a *separating conjunction* * that decomposes structures. For reasons related to its applications to the deductive verification of pointer-manipulating programs, the models of SL are finite partial functions, called heaps. In SL, the separating conjunction stands for the union of heaps with disjoint domains.

When combined with *inductive definitions* [Acz77], SL gives concise descriptions of the recursive data structures (singly- and doubly-linked lists, trees, etc.) used in imperative programming (e.g., C, C++, Java, etc.). The shape of these structures can be described using only existentially quantified separating conjunctions of (dis-)equalities and points-to atoms. This subset of SL is referred to as the *symbolic heap* fragment.

SL is a powerful tool for reasoning about low-level pointer updates. It allows to describe actions *locally*, i.e., only with respect to the resources (e.g., memory cells, network nodes) involved, while framing out the part of the state that is irrelevant for the action. This principle of describing mutations, known as *local reasoning* [COY07], is at the heart of scalable compositional proof techniques for pointer programs [CDOY11, CDNQ12, DPJ08, BCO06].

The *Separation Logic of Relations* (SLR) is the generalization of SL to relational signatures, interpreted over structures. This logic has been first considered for relational databases and object-oriented languages [KR04]. Here the separating conjunction splits the interpretation of each relation symbol from the signature into disjoint parts. For instance, the formula $r(x_1, \dots, x_n)$ describes a structure in which all relations are empty and $r$ consists of a single tuple of values $x_1, \dots, x_n$, whereas $r(x_1, \dots, x_n) * r(y_1, \dots, y_n)$ says that $r$ consists of two distinct tuples, i.e., the values of $x_i$ and $y_i$ differ for at least one index $1 \le i \le n$. Moreover, when encoding graphs by structures, SLR allows to specify edges that have no connected vertices, isolated vertices, or both. The same style of composition is found in other spatial logics interpreted over graphs, such as the GL logic of Cardelli et al [CGG02].

Our motivation for studying the models of SLR arose from recent work on deductive verification of self-adapting distributed systems, where Hoare-style local reasoning is applied to write correctness proofs for systems with dynamically reconfigurable network architectures [ABIK22, BBI22a, BBI22b]. The assertion language of these proofs is SLR, with unary relation symbols used to model nodes (processes) of the network and relation symbols of arity two or more used to model links (communication channels) between nodes. Just as user-defined inductive predicates are used in SL to describe data structures (lists, trees, etc.), SLR inductive predicates are used to describe common architectural styles (e.g., pipelines, rings, stars, etc.) that ensure correct and optimal behavior of many distributed applications.

The decidability result from this paper defines the class of SLR formulæ whose models are treewidth bounded and provides a reasonable estimate on the bound, in case one exists. On one hand, this algorithm answers the question *does the set of structures defined by a given system of inductive definitions have a decidable MSO theory?* If this is the case, problems such as, e.g., Hamiltonicity, k-Colorability, Planarity, etc. are decidable on this set of structures. Another application is the decidability of the *entailment problem* $[[\phi]]_{\Delta} \subseteq [[\psi]]_{\Delta}$
asking if each model of a formula $\phi$ is also a model of another formula $\psi$, when the predicate
symbols in $\phi$ and $\psi$ are interpreted by a set of inductive definitions $\Delta$. In principle, the
decidability of this problem depends on (i) $\phi$ having only treewidth bounded models, for
a computable upper bound, and (ii) both $\phi$ and $\psi$ being MSO-definable [IRS13]. The
algorithm described in the paper provides a key ingredient for defining fragments of SLR
with a decidable entailment problem, which is tantamount to automating proof generation
in Hoare logic [BBI22a, BBI22b].

1.1. **Related work.** One of the first fragments of SL with a decidable entailment problem relied on an ad-hoc translation into equivalent MSO formulæ, together with a static guarantee of treewidth boundedness, called *establishment* [IRS13]. More recently, the entailment problem in this fragment of SL has been the focus of an impressive body of work [CHO<sup>+</sup>11, KZ20, EIP21a, EIP21b, LL23]. In particular, the *establishment problem* "is a given set of inductive definitions established" has been found to be co-NP-complete [JKM<sup>+</sup>17]. Moreover, lifting the establishment condition leads to the undecidability of entailments, as showed in [EIP22]. The establishment problem can, in fact, be seen as the precursor of the treewidth boundedness problem studied in the present paper.

The treewidth parameter showed also in a recent comparison between the expressivity of SLR with inductive definitions and that of MSO [IZ23]. When restricting the interpretation of the logics to treewidth bounded graphs, SLR strictly subsumes MSO, i.e., for each MSO formula $\phi$ and integer $k \ge 1$, there exists a formula $\psi$ of SLR that defines the models of $\phi$ of treewidth at most $k$. Moreover, the logics are incomparable for classes of graphs of unbounded treewidth.

1.2. **Motivating examples.** We introduce the reader to SLR and the treewidth boundedness problem by means of examples. Figure 1 (a) shows a chain, defined by an unfolding of the inductive predicate $A(x_1, x_2)$. The chain starts at $x_1$ and ends at $x_2$. The elements of the chain are labeled by a unary relation symbol $a$ and the neighbours are linked by a binary relation $r$. Each unfolding of the inductive definition $A(x_1, x_2) \leftarrow \exists y. a(x_1) * r(x_1, y) * A(y, x_2)$ instantiates the existential quantifier to an element distinct from the existing ones. This is because every instantiation of an existential quantifier is placed into a set labeled by $a$ and the semantics of the separating conjunction requires that these sets must be disjoint in each decomposition of a model of $a(x_1) * r(x_1, y) * A(y, x_2)$ into models of $a(x_1) * r(x_1, y)$ and $A(y, x_2)$. Then, each model of $\exists x_1 \exists x_2. A(x_1, x_2)$ is a possibly cyclic chain, because nothing is enforced on $x_2$, which can be mapped back to a previous instantiation of $y$. Hence each model of this sentence has treewidth two at most.

Figure 1 (b) shows a family of models for a slightly modified definition of the chain
from Figure 1 (a), given by the recursive rule $A(x_1, x_2) \leftarrow \exists y. r(x_1, y) * A(y, x_2)$, where the
instantiations of the existential quantifiers are not placed into any particular set. In this
case, one can fold a sufficiently large chain onto itself and creating a square grid, by using
the same element of the structure more than once to instantiate a quantifier. Then, the
sentence $\exists x_1 \exists x_2. A(x_1, x_2)$ has an infinite set of models containing larger and larger square
grid minors, thus having unbounded treewidth.

Since placing every quantifier instance into the same set guarantees treewidth boundedness, as in, e.g., Figure 1 (a), a natural question that arises is what happens when these instances are placed into two (not necessarily disjoint) sets? The inductive definition of the
predicate A in Figure 1 (c) creates an unbounded number of disconnected r-edges whose endpoints are arbitrarily labeled with a and b, respectively. In this case, one can instantiate a a-labeled (resp. b-labeled) variable with a new element or a previous b (resp. a) element and build chains (or sets of disconnected chains), of treewidth two at most two. Again, this is because a simple cycle with more than two elements has treewidth two.

<figure><img src="image_3.png" /><figcaption>Figure 1: Examples of bounded and unbounded treewidth models</figcaption></figure>

Let us now consider three unary relation symbols a, b and c and three types of disconnected r-edges (according to the labels of their endpoints) created by three recursive definitions of Figure 1 (d), namely a-b, b-c and a-c edges. In this case, the sentence A(), where A is a predicate symbol of zero arity, has models with unboundedly large square grid minors, obtained by “glueing” these edges (i.e., instantiating several quantifiers with the same element from different sets). The glued pairs are connected with dotted lines in Figure 1 (d). Hence, these structures form a set of unbounded treewidth.

These examples highlight the main ideas behind an algorithm that decides the existence of a bound on the treewidths of the models of a given formula, with predicates interpreted by set of inductive definitions. First, one needs to identify the definitions that can iterate any number of times producing building blocks of unboundedly large grids (modulo edge contractions). Second, these structures must connect elements from different sets, e.g., a, b or c in Figure 1. A complication is that these sets can be defined not only by monadic relation symbols, but also by n-ary relation atoms where all but one variable have the same values for any occurrence. For instance, the variable $x_2$ in Figure 1 (a) has the same value in an arbitrarily long unfolding of $A(x_1, x_2)$ and we could have written $r(x_1, x_2)$ instead of $a(x_1)$ in the first rule, with the same effect, while avoid using ‘a’ altogether. Last, the interplay between the connectivity and labeling of the building blocks is important. For instance, in Figure 1 (d), the building blocks of the grid are structures consisting of six elements,
that connect three ‘a’ with three ‘b’ elements. In fact, as we shall prove, a necessary and sufficient condition for treewidth-boundedness is that any two such “iterable” substructures that connect at least three elements must also place these elements in at least one common set (e.g., a, b or c in our example).

## 2. THE SEPARATION LOGIC OF RELATIONS

This section defines formally the Separation Logic of Relations (SLR) and its corresponding treewidth boundedness problem. It also introduces most of the technical notions used throughout the paper.

Let $\mathbb{N}$ be the set of positive integers, zero included and $N_+ \stackrel{\text{def}}{=} \mathbb{N} \setminus \{0\}$. Given integers $i$ and $j$, we write $[i..j]$ for the set $\{i, i+1, \dots, j\}$, assumed to be empty if $i > j$. For a set $A$, we denote by $\text{pow}(A)$ its powerset. The cardinality of a finite set $A$ is $\text{card}(A)$. By writing $S = S_1 \uplus S_2$, we mean that $S_1$ and $S_2$ partition $S$, i.e., that $S = S_1 \cup S_2$ and $S_1 \cap S_2 = \emptyset$.

Multisets are denoted as $\{[a, b, \dots]\}$ and all set operations (union, intersection, etc.) are used with multisets as well. In particular, a binary operation involving a set and a multiset implicitly lifts the set to a multiset and returns a multiset. The multi-powerset (i.e., the set of multisets) of $A$ is denoted as $\text{mpow}(A)$.

For a binary relation $R \subseteq A \times A$, we denote by $R^*$ its reflexive and transitive closure and by $R^-=\text{the smallest equivalence relation that contains } R$, i.e., the closure of $R^*$ by symmetry. For a set $S \subseteq A$, we denote by $R|_S$ the relation obtained by removing from $R$ all pairs with an element not in $S$. A binary relation $R \subseteq A \times B$ is an *A-B matching* iff $\{a, b\} \cap \{a', b'\} = \emptyset$, for all distinct pairs $(a, b)$, $(a', b') \in R$.

### 2.1. Structures.
Let $\mathbb{R}$ be a finite and fixed set of relation symbols, of arities $\#r \ge 1$, for all $r \in \mathbb{R}$. A relation symbol of arity one (resp. two) is called *unary* (resp. *binary*).

A structure is a pair $S = (U, \sigma)$, where $U$ is an infinite set called the *universe* and $\sigma: \mathbb{R} \to \text{pow}(U^+)$ is an *interpretation* mapping each relation symbol $r$ into a *finite* subset of $U^{\#r}$. We consider only structures with finite interpretations, because the logic under consideration (defined below) can only describe sets of finite structures. The *support* $\text{supp}(\sigma) = \{u_i \mid \langle u_1, \dots, u_{\#r} \rangle \in \sigma(r), i \in [1..\#r]\}$ of an interpretation is the (necessarily finite) set of elements that occur in a tuple from the interpretation of a relation symbol. The support of a structure is the support of its interpretation.

Two structures $(U_1, \sigma_1)$ and $(U_2, \sigma_2)$ are *locally disjoint* iff $\sigma_1(r) \cap \sigma_2(r) = \emptyset$, for all $r \in \mathbb{R}$ and *disjoint* iff $\text{supp}(\sigma_1) \cap \text{supp}(\sigma_2) = \emptyset$. Two structures are *isomorphic* iff they differ only by a renaming of their elements (see, e.g., [EF95, Section A3] for a formal definition of isomorphism between structures).

We consider the *composition* as a partial binary operation between structures, defined as pointwise disjoint union of the interpretations of relation symbols:

**Definition 2.1.** The composition of two locally disjoint structures $(U_1, \sigma_1)$ and $(U_2, \sigma_2)$ is $(U_1, \sigma_1) \bullet (U_2, \sigma_2) \stackrel{\text{def}}{=} (U_1 \cup U_2, \sigma_1 \uplus \sigma_2)$, where $(\sigma_1 \uplus \sigma_2)(r) \stackrel{\text{def}}{=} \sigma_1(r) \uplus \sigma_2(r)$, for all $r \in \mathbb{R}$. The composition is undefined if $(U_1, \sigma_1)$ and $(U_2, \sigma_2)$ are not locally disjoint.

For example, Figure 2 shows the composition of two structures $S_1$ and $S_2$, whose interpretations are represented as hyper-graphs with edges denoting tuples from the interpretation of relation symbols a, b and c, of arities 3, 2 and 2, respectively. Note that $S_1$ and $S_2$ are locally
disjoint but not disjoint, for instance the elements $u_2$ and $u_3$ are present in the support of both structures.

<figure><img src="image_4.png" /><figcaption>Figure 2: Composition of structures</figcaption></figure>

**2.2. Treewidth.** A graph is a pair $G = (\mathcal{N}, \mathcal{E})$, such that $\mathcal{N}$ is a finite set of *nodes* and $\mathcal{E} \subseteq \mathcal{N} \times \mathcal{N}$ is a set of *edges*. A (simple) *path* in $G$ is a sequence of (pairwise distinct) nodes $v_1, \dots, v_n$, such that $(v_i, v_{i+1}) \in \mathcal{E}$, for all $i \in [1..n-1]$. We say that $v_1, \dots, v_n$ is an *undirected path* if $\{(v_i, v_{i+1}) \mid i \in [1..n-1] \mid v_i \neq v_{i+1}\}$ is a set of nodes $S \subseteq \mathcal{N}$ is *connected in G* iff between any two nodes in $S$ there is an undirected path in $G$ that involves only nodes from $S$. A graph $G$ is *connected* iff $\mathcal{N}$ is connected in $G$.

Given a set $\Omega$ of labels, a $\Omega$-labeled unranked tree is a tuple $T = (\mathcal{N}, \mathcal{E}, r, \lambda)$, where $(\mathcal{N}, \mathcal{E})$ is a graph, $r \in \mathcal{N}$ is a designated node called the *root*, such that there exists a unique simple path from $r$ to any other node $n \in \mathcal{N} \setminus \{r\}$ and no path from $r$ to $n$ in $(\mathcal{N}, \mathcal{E})$. The mapping $\lambda: \mathcal{N} \to \Omega$ associates each node of the tree a label from $\Omega$.

**Definition 2.2.** A tree decomposition of a structure $S = (U, \sigma)$ is a pow$(U)$-labeled unranked tree $T = (\mathcal{N}, \mathcal{E}, r, \lambda)$, such that the following hold:

(1) for each relation symbol $r \in \mathbb{R}$ and each tuple $(u_1, \dots, u_{\#r}) \in \sigma(r)$ there exists a node $n \in \mathcal{N}$, such that $\{u_1, \dots, u_{\#r}\} \subseteq \lambda(n)$,

(2) for each element $u \in \text{supp}(\sigma)$, the set of nodes $\{n \in \mathcal{N} \mid u \in \lambda(n)\}$ is nonempty and connected in $(\mathcal{N}, \mathcal{E})$.

The *width* of the tree decomposition is $\text{wd}(T) \stackrel{\text{def}}{=} \max_{n \in \mathcal{N}} \text{card}(\lambda(n)) - 1$. The *treewidth* of the structure $\sigma$ is $\text{tw}(\sigma) \stackrel{\text{def}}{=} \min\{\text{wd}(T) \mid T$ is a tree decomposition of $\sigma\}$.

Note that, since we consider only structures with finite support, tree decompositions are finite trees with finite sets as labels, hence the treewidth of a structure is a well-defined integer. A set of structures is *treewidth-bounded* iff the set of corresponding treewidths is finite and *treewidth-unbounded* otherwise. We assume basic acquaintance with the notions of *grid* and *minor*. It is known that a set of structures having infinitely many minors isomorphic to some $n \times n$ grid is *treewidth-unbounded* [Bod98].

**2.3. Separation Logic of Relations.** The *Separation Logic of Relations* (SLR) uses a set of variables $\mathbb{V} = \{x, y, \dots\}$ and a set of predicates $\mathbb{P} = \{\text{A}, \text{B}, \dots\}$ with given arities $\#\text{A} \ge 0$. A predicate of zero arity is called *nullary*.

The formulæ of SLR are defined by the syntax in Figure 3 (a). A variable is *free* if it does not occur within the scope of an existential quantifier and $\text{fv}(\phi)$ denotes the set of free variables of $\phi$. A sentence is a formula with no free variables. For a formula $\phi$, we denote by
$\phi^\exists$ the sentence obtained by existentially quantifying its free variables. A formula without quantifiers is called *quantifier-free*.

Instead of the standard boolean conjunction, SLR has a *separating conjunction* $\cdot$. The formulæ $x \neq y$ and $A(x_1, \dots, x_{\#A})$ are called *disequalities* and *predicate atoms*, respectively. To alleviate notation, we denote by $A$ the predicate atom $A()$, whenever $A$ is nullary. A formula without predicate atoms is called *predicate-free*. A qpf formula is both quantifier- and predicate-free.

<figure><img src="image_5.png" /><figcaption>Figure 3: The syntax (a) and semantics (b) of the Separation Logic of Relations</figcaption></figure>

**Definition 2.3.** A set of inductive definitions (SID) is a finite set $\Delta$ of rules of the form $A(x_1, \dots, x_{\#A}) \leftarrow \phi$, where $x_1, \dots, x_{\#A}$ are pairwise distinct variables, called *parameters*, such that $fv(\phi) \subseteq \{x_1, \dots, x_{\#A}\}$.

The semantics of SLR is given by the satisfaction relation $(U, \sigma) \models_{\Delta}^{\mathfrak{s}} \phi$ between structures and formulæ, parameterized by a store $\mathfrak{s}$ and a SID $\Delta$. We write $\mathfrak{s}[x \leftarrow u]$ for the store that maps $x$ into $u$ and agrees with $\mathfrak{s}$ on all variables other than $x$. By $[x_1/y_1, \dots, x_n/y_n]$ we denote the substitution that replaces each free variable $x_i$ by $y_i$ in a formula $\phi$. The result of applying the substitution $[x_1/y_1, \dots, x_n/y_n]$ to the formula $\phi$ is denoted as $\phi[x_1/y_1, \dots, x_n/y_n]$, where, by convention, the existentially quantified variables from $\phi$ are renamed to avoid clashes with $y_1, \dots, y_n$. Then $\models_{\Delta}^{\mathfrak{s}}$ is the least relation that satisfies the constraints in Figure 3 (b).

Note that the interpretation of equalities and relation atoms differs in SLR from first-order logic, namely $x = y$ requires that the structure is empty and $r(x_1, \dots, x_{\#r})$ denotes the structure in which all relations symbols are interpreted by empty sets, except for $r$, which contains the tuple of store values of $x_1, \dots, x_{\#r}$ only. Moreover, every structure $(U, \sigma)$, such that $(U, \sigma) \models_{\Delta}^{\mathfrak{s}} \phi$, interprets each relation symbol as a finite set of tuples, defined by a finite least fixpoint iteration over the rules from $\Delta$. The assumption that each structure has an infinite universe excludes the cases in which a formula becomes unsatisfiable because there are not enough elements to instantiate the quantifiers introduced by the unfolding of the rules, thus simplifying the definitions.

If $\phi$ is a sentence (resp. a predicate-free formula), we omit the store $\mathfrak{s}$ (resp. the SID $\Delta$) from $S \models_{\Delta}^{\mathfrak{s}} \phi$. For a SLR sentence $\phi$, let $[[\phi]]_{\Delta}^{\text{def}} = \{S \mid S \models_{\Delta}^{\mathfrak{s}} \phi\}$ be the set of $\Delta$-models of $\phi$. If $\phi$ is, moreover, predicate-free we say that $\phi$ is *satisfiable* iff $[[\phi]] \neq \emptyset$.
For a qpf formula $\phi$, we write $x \approx_{\phi} y$ (resp. $x \not\approx_{\phi} y$) iff $x = y$ is (resp. is not) a logical consequence of $\phi$, i.e., $s(x) = s(y)$ for each store $s$ and structure $S$, such that $S \models^{\mathfrak{s}} \phi$. Note that $x \not\approx_{\phi} y$ is the negation of $x \approx_{\phi} y$, which is different from that $x \neq y$ is implied by $\phi$. We define several quantitative measures relative to SIDs:

**Definition 2.4.** Let $\Delta$ be a SID. We denote by:

▷ $\maxVars(\Delta)$ the maximum number of variables that occur, either free or existentially quantified, in a rule from $\Delta$,

▷ $\maxRelAtoms(\Delta)$ the maximum number of relation atoms that occur in a rule from $\Delta$,

▷ $\maxPredAtoms(\Delta)$ the maximum number of predicates that occur in a rule from $\Delta$,

▷ $\maxRelArity(\Delta)$ the maximum arity of relation symbols occurring in $\Delta$,

▷ $\text{predNo}(\Delta)$ the number of predicate symbols occurring in $\Delta$,

▷ $\text{relNo}(\Delta)$ the number of relation symbols occurring in $\Delta$.

**2.4. Simplifying assumptions.** In the rest of this paper, we simplify the technical development by two assumptions, that lose no generality. The first assumption is that no equalities occur in the given SID (Lemma 2.6).

**Definition 2.5.** A formula is *equality-free* iff it contains no equalities nor predicate atoms in which the same variable occurs twice. A rule $A(x_1, \dots, x_n) \leftarrow \phi$ is equality-free iff $\phi$ is equality-free. A SID is equality-free iff it consists of equality-free rules.

**Lemma 2.6.** *Given a SID $\Delta$, one can build an equality-free SID $\Delta'$, such that $[A]_{\Delta} = [A]_{\Delta'}$, for each nullary predicate $A$. Moreover, all quantitative measures (Definition 2.4) of $\Delta'$ are the same as for $\Delta$, except for $\text{predNo}(\Delta') \le \text{predNo}(\Delta) \cdot \maxVars(\Delta)^{\maxVars(\Delta)}$.*

*Proof.* See [IZ23, Lemma 9]. The construction of $\Delta'$ considers predicates $A_{I_1, \dots, I_n}$, where $A$ is a predicate symbol that occurs in $\Delta$ and $I_1 \uplus \dots \uplus I_n = [1..\#A]$ is a partition. Since the number of partitions of $[1..\#A]$ is asymptotically bounded by $\#A^{\#A} \le \maxVars(\Delta)^{\maxVars(\Delta)}$, we obtain the bound on $\text{predNo}(\Delta')$. $\square$

The following notion of *unfolding* is used to define several technical notions and state the second simplifying assumption. Let $\phi$ and $\psi$ be formulæ and $\Delta$ be a SID. We denote by $\phi \Rightarrow_{\Delta} \psi$ the fact that $\psi$ is obtained by replacing a predicate atom $A(y_1, \dots, y_n)$ in $\phi$ by a formula $\rho[x_1/y_1, \dots, x_n/y_n]$, where $A(x_1, \dots, x_n) \leftarrow \rho$ is a rule from $\Delta$. A $\Delta$-*unfolding* is a sequence of formulæ $\phi_1 \Rightarrow_{\Delta} \dots \Rightarrow_{\Delta} \phi_n$. The $\Delta$-unfolding is *complete* if the last formula is predicate-free. The following statement is a direct consequence of the semantics of SLR:

**Proposition 2.7.** *Let $\phi$ be a sentence, $\Delta$ a SID and $S$ a structure. Then $S \in [\phi]_{\Delta}$ iff $S \models^{\mathfrak{s}} \psi$, for a store $s$ and complete $\Delta$-unfolding $\phi \Rightarrow_{\Delta}^* \exists x_1 \dots \exists x_n \psi$, where $\psi$ is a qpf formula.*

*Proof.* “$\Leftarrow$” By induction on the definition of the satisfaction relation $\models^{\mathfrak{s}}_{\Delta}$. “$\Rightarrow$” By induction on the length of the $\Delta$-unfolding. $\square$

The second assumption is that any $\Delta$-unfolding of a nullary predicate by the given SID yields a predicate-free formula that is satisfiable. Again, this assumption loses no generality (Lemma 2.9).

**Definition 2.8.** A SID $\Delta$ is *all-satisfiable* for a nullary predicate $A$ iff each predicate-free formula $\phi$ which is the outcome of a complete $\Delta$-unfolding $A \Rightarrow_{\Delta}^{*} \phi$ is satisfiable.
**Lemma 2.9.** Given a SID $\Delta$ and a nullary predicate $A$, one can build a SID $\bar{\Delta}$ all-satisfiable for $A$, such that $[[A]]_{\bar{\Delta}} = [[A]]_{\bar{\Delta}}$. Moreover, all quantitative measures (Definition 2.4) of $\Delta'$ are the same as for $\Delta$, except for $\text{predNo}(\bar{\Delta}) \le \text{predNo}(\Delta) \cdot \text{relNo}(\Delta) \cdot \text{maxVars}(\Delta)^{\text{maxRelArity}(\Delta)}$.

*Proof.* For space reasons, this proof is given in subsection A.1. $\square$

## 2.5. The treewidth boundedness problem.
We are ready to state the main problem addressed in this paper. Before, we state two technical lemmas that state several relations between qpf formulæ and the upper bounds on the treewidth of their models:

**Lemma 2.10.** Let $\phi, \psi$ be qpf formulæ, $x_0, x_1, x_2, \ldots, x_k$ variables and $\mathbf{r}$ a relation symbol of arity $k$. Then, the following hold:

(1) $\text{tw}([[(\phi * \mathbf{r})^{\exists}]]_{\bar{\Delta}}) \le \text{tw}([\phi^{\exists}])$,

(2) $\text{tw}([\phi^{\exists}]) - 1 \le \text{tw}([[(\phi * \mathbf{r})^{\exists}]]_{\bar{\Delta}})$ if $\phi * \mathbf{r} \ne x_0$ satisfiable,

(3) $\text{tw}([\phi^{\exists}]) - 1 \le \text{tw}([[(\phi * \mathbf{r})^{\exists}]]_{\bar{\Delta}})$ if $\phi * \mathbf{r}(x_1, \ldots, x_k) \text{ satisfiable.}$

(4) $\text{tw}([[(\phi * \psi)^{\exists}]]_{\bar{\Delta}}) \le \text{tw}([\phi^{\exists}]) + \text{card}(\text{fv}(\psi))$ if $\psi$ contains only relation atoms.

*Proof.* For space reasons, this proof is given in subsection A.2. $\square$

**Lemma 2.11.** Let $\phi$ and $\psi$ be qpf formulæ and $F \stackrel{\text{def}}{=} \text{fv}(\phi) \cap \text{fv}(\psi)$, such that $\phi * \psi$ is satisfiable and $x \not\approx_{\phi} y$, for all $x, y \in F$. Let $\eta \stackrel{\text{def}}{=} \mathbf{r}_{x,y \in F}$, $x \approx_{\psi y} y = y$. Then, $\text{tw}([[(\phi * \eta)^{\exists}]]_{\bar{\Delta}}) \le \text{tw}([[(\phi * \psi)^{\exists}]]_{\bar{\Delta}}) + \text{card}(F)$.

*Proof.* For space reasons, this proof is given in subsection A.3. $\square$

The main result of this paper is a decidability proof for the following decision problem:

**Definition 2.12.** The TWB<sup>SLR</sup> problem asks whether the set $[[\phi]]_{\bar{\Delta}}$ is treewidth-bounded, for an SID $\Delta$ and SLR sentence $\phi$ given as input.

This result is tightened by a proof of the undecidability of the treewidth-boundedness problem for first-order logic (section 5), that further improves our understanding of the relation between the expressivity of classical and substructural logics. The decidability proof proceeds in two steps. First, we show the decidability of the problem for sentences of the form $A$, where $A$ is a nullary predicate symbol, and a class of SIDs having a particular property, called *expandability*, defined below (section 3). Second, we show how to reduce the treewidth-boundedness problem for arbitrary sentences and SIDs to the problem for nullary predicate atoms and expandable SIDs (section 4).

# 3. EXPANDABLE SETS OF INDUCTIVE DEFINITIONS

This section introduces the formal definitions of canonical models and expandable SIDs, needed for the first part of the proof of decidability of the TWB<sup>SLR</sup> problem. The main result of this section is that the treewidth boundedness problem is decidable for the sets of models of a nullary predicate defined by an expandable SID.

For simplicity, in the rest of this paper we shall represent sentences $\phi$ by nullary predicate atoms $A$. This loses no generality since $[[\phi]]_{\bar{\Delta}} = [[A]]_{\bar{\Delta} \cup \{A \leftrightarrow \phi\}}$ provided that $A$ is not defined by any other rule in $\Delta$. In the rest of this section we fix an arbitrary SID $\Delta$ and nullary predicate $A$.
**3.1. Canonical models.** Intuitively, a $\Delta$-model of A is *canonical* if it can be defined using a store that matches only those variables that are equated in the outcome of the complete $\Delta$-unfolding of A that “produced” the model, in the sense of Proposition 2.7. A *rich canonical model* records, moreover, the disequalities introduced during the unfolding.

**Definition 3.1.** A store $\mathfrak{s}$ is *canonical for* $\phi$ iff $\mathfrak{s}(x) = \mathfrak{s}(y)$ only if $x \approx_{\phi} y$, for all $x, y \in \text{fv}(\phi)$. A rich canonical $\Delta$-model of a sentence $\phi$ is a pair $(S, \mathfrak{d})$, where $S = (U, \sigma)$ is a structure and $\mathfrak{d} \subseteq U \times U$ is a symmetric relation, such that there exists a complete $\Delta$-unfolding $\phi \Rightarrow_{\Delta}^{*} \exists x_1 \dots \exists x_n \psi$, where $\psi$ is qpf, and a store $\mathfrak{s}$ canonical for $\psi$, such that $S \models^{\mathfrak{s}} \psi$ and $\mathfrak{d}(u, v)$ iff there exist variables $x \in \mathfrak{s}^{-1}(u)$, $y \in \mathfrak{s}^{-1}(v)$ and the disequality $x \neq y$ occurs in $\psi$. We denote by $[[\phi]]_{\Delta}^{\prime}$ the set of rich canonical $\Delta$-models of $\phi$ and $[[\phi]]_{\Delta}^{\text{def}} = \{S \mid (S, \mathfrak{d}) \in [[\phi]]_{\Delta}^{\prime}\}$ the set of canonical $\Delta$-models of $\phi$. If $\phi$ is predicate-free, we write $[[\phi]]^{\text{c}}$ (resp. $[[\phi]]^{\prime}$) instead of $[[\phi]]_{\Delta}^{\text{c}}$ (resp. $[[\phi]]_{\Delta}^{\prime}$).

A store $\mathfrak{s}$ is *injective* over a set of variables $x_1, \dots, x_n$ iff $\mathfrak{s}(x_i) = \mathfrak{s}(x_j)$ implies $i = j$, for all $i, j \in [1..n]$. Note that the canonical $\Delta$-models of an equality free SID $\Delta$ can be defined considering injective, instead of canonical stores. Nevertheless, this more general definition of canonical models using canonical stores will become useful later on, when predicate-free formulæ with equalities will be considered.

Canonical models are important for two reasons. First, their treewidth is bounded:

**Lemma 3.2.** $\text{tw}(S) \leq \max\text{Vars}(\Delta) - 1$, for any $S \in [[\mathfrak{A}]]_{\Delta}^{\text{c}}$.

*Proof.* Let $S = (U, \sigma) \in [[\mathfrak{A}]]_{\Delta}^{\text{c}}$ be a canonical $\Delta$-model of A. We define a tree decomposition $T = (\mathcal{N}, \mathcal{E}, r, \lambda)$ of S as follows. The graph of T is any derivation tree of $\Delta$ whose outcome is S. This is a tree labeled with rules from $\Delta$, whose parent-child relation is defined as follows: if $n$ is a node labeled with a rule $\rho$, for each predicate atom $B(z_1, \dots, z_{\#B})$ that occurs in $\rho$, there is exactly one child $m$ of $n$ whose label is a rule that defines B. The bag $\lambda(n)$ contains exactly those elements that are the store values of the variables occurring free or bound in $\rho$. We check that $T$ is a tree decomposition of S by proving the two points of Definition 2.2:

(1) each tuple $(u_1, \dots, u_{\#r}) \in \sigma(r)$ occurs in S because of a relation atom $r(z_1, \dots, z_{\#r})$ that occurs in the label of a node $n$ from the parse tree. Then $u_1, \dots, u_{\#r} \in \lambda(n)$, by the definition of T.

(2) let $n, m \in \mathcal{N}$ be nodes of $T$ and $u \in \lambda(n) \cap \lambda(m)$ be an element. Then the label of each node on the path between $n$ and $m$ in the parse tree contains a variable whose store value is $u$, hence the set $\{p \in \mathcal{N} \mid u \in \lambda(p)\}$ is non-empty and connected in $T$. $\square$

Second, any model is obtained via an *internal fusion* of a rich canonical model. The internal fusion is a unary operation that takes as input a structure and outputs a set of structures obtained by joining certain elements from its support. This operation is formally defined as quotienting with respect to certain equivalence relations:

**Definition 3.3.** Let $S = (U, \sigma)$ be a structure and $\approx \subseteq U \times U$ be an equivalence relation, where $[u]_{\approx}$ is the equivalence class of $u \in U$. The quotient $S_{/\approx} = (U_{/\approx}, \sigma_{/\approx})$ is $U_{/\approx}^{\text{def}} = \{[u]_{\approx} \mid u \in U\}$ and $\sigma_{/\approx}(r) \stackrel{\text{def}}{=} \{\langle[u_1]_{\approx}, \dots, [u_{\#r}]_{\approx}\rangle \mid \langle u_1, \dots, u_{\#r} \rangle \in \sigma(r)\}$, for all $r \in \mathbb{R}$.

For example, Figure 4 (a) shows the outcome of quotienting a structure with respect to an equivalence relation, whose equivalence classes are encircled with dashed lines.

A fusion operation glues elements without losing tuples from the interpretation of a relation symbol. For this reason, we consider only equivalence relations that are *compatible* with a given structure and define internal fusion as the following unary operation:
**Definition 3.4.** An equivalence relation $\approx \subseteq U \times U$ is compatible with a structure $S = (U, \sigma)$ iff for all $r \in \mathbb{R}$ and any two tuples $(u_1, \dots, u_{\#r})$, $(v_1, \dots, v_{\#r}) \in \sigma(r)$, there exists $i \in [1..\#r]$ such that $u_i \not\approx v_i$. An internal fusion of $S$ is a structure isomorphic to $S_{/\approx}$, for an equivalence relation $\approx$ compatible with $S$. Let $\text{IF}(S)$ be the set of internal fusions of $S$ and $\text{IF}(S) \stackrel{\text{def}}{=} \bigcup_{S \in S} \text{IF}(S)$, for a set $S$ of structures.

For example, Figure 4 (b) shows a possible internal fusion of a structure. Note that the equivalence relation from Figure 4 (a) is not compatible with the structure and cannot be used in a fusion.

<figure><img src="image_6.png" /><figcaption>Figure 4: Quotient (a) and internal fusion (b)</figcaption></figure>

For technical reasons, we introduce also the internal fusion of a rich canonical model, as quotienting with respect to an equivalence relation that does not violate the disequality relation:

**Definition 3.5.** An equivalence relation $\approx \subseteq U \times U$ is compatible with a rich canonical model $(S, \mathfrak{d})$ iff it is compatible with $S = (U, \sigma)$ and $\mathfrak{d}(u, v)$ only if $u \not\approx v$. We denote by $\widetilde{\text{IF}}(S, \mathfrak{d})$ the set of structures isomorphic to $S_{/\approx}$, where $\approx$ is some equivalence relation compatible with $(S, \mathfrak{d})$.

The following lemma relates the sets of models, canonical and rich canonical models of a sentence, via the two types of internal fusion:

**Lemma 3.6.** $[[A]]_{\Delta} = \widetilde{\text{IF}}([[[A]]'_{\Delta}) \subseteq \text{IF}([[[A]]^{c}_{\Delta})}$.

*Proof.* It is sufficient to prove $[[A]]_{\Delta} = \widetilde{\text{IF}}([[[A]]'_{\Delta})$, since $\widetilde{\text{IF}}([[[A]]'_{\Delta}) \subseteq \text{IF}([[[A]]^{c}_{\Delta})$ is immediate, by Definition 3.5, because any equivalence relation that is compatible with a rich canonical $\Delta$-model $(S, \mathfrak{d})$ is also compatible with the canonical $\Delta$-model $S$.

“$\subseteq$” Let $S \in [[A]]_{\Delta}$ be a structure. By Proposition 2.7, we have $S \models \exists y_1 \dots \exists y_m \cdot \psi$, where $\psi$ is a qpf formula, such that $\text{fv}(\psi) = \{y_1, \dots, y_m\}$ and $A \Rightarrow^*_{\Delta} \exists y_1 \dots \exists y_m \cdot \psi$ is a complete $\Delta$-unfolding. Then there exists a store $\mathfrak{s}$, such that $S \models^s \psi$. Let $\bar{S} = (\bar{U}, \bar{\sigma})$ be a structure and $\bar{\mathfrak{s}}$ be an injective store over $y_1, \dots, y_m$. Since $\Delta$ is equality-free, there are no equality atoms in $\psi$, hence such a structure and injective store exist. We consider $\approx \subseteq \bar{U} \times \bar{U}$ to be the least equivalence relation such that $\bar{\mathfrak{s}}(y_i) \approx \bar{\mathfrak{s}}(y_j) \iff \mathfrak{s}(y_i) = \mathfrak{s}(y_j)$, for all $1 \le i < j \le m$. To prove that $\approx$ is compatible with $\bar{S}$, consider two tuples $(\bar{\mathfrak{s}}(z_1), \dots, \bar{\mathfrak{s}}(z_{\#r}))$, $(\bar{\mathfrak{s}}(z'_1), \dots, \bar{\mathfrak{s}}(z'_{\#r})) \in \bar{\sigma}(r)$, for some $r \in \mathbb{R}$ and suppose, for a contradiction, that $\bar{\mathfrak{s}}(z_i) \approx \bar{\mathfrak{s}}(z'_i)$, for all $i \in [1..\#r]$. Then $r(z_1, \dots, z_{\#r}) * r(z'_1, \dots, z'_{\#r})$ is a subformula of $\psi$, modulo a reordering of atoms. By the definition of $\approx$, we have $\mathfrak{s}(z_i) = \mathfrak{s}(z'_i)$, for all $i \in [1..\#r]$, in contradiction with $S \models^s \psi$ and the semantics of the separating conjunction. Since $\bar{S} \models^s \psi$ and $\bar{\mathfrak{s}}$ is injective over $y_1, \dots, y_m$,
we obtain that $\bar{s}|_{\{y_1, \dots, y_m\}}$ is a bijection between $\{y_1, \dots, y_m\}$ and $\text{supp}(\bar{\sigma})$ hence $\bar{s}^{-1}(u)$ is a singleton, for each $u \in \text{supp}(\bar{\sigma})$. Let $\mathfrak{d} \subseteq \bar{U} \times \bar{U}$ be the relation defined as $\mathfrak{d}(u, v)$ iff the disequality $\bar{s}^{-1}(u) \neq \bar{s}^{-1}(u)$ occurs in $\psi$. Then $\approx$ is compatible with $(\bar{S}, \mathfrak{d}) \in [[\mathfrak{A}]']_{\Delta}$ hence $\bar{S}_{/\approx} \in \tilde{\text{IF}}([\mathfrak{A}]']_{\Delta})$. Finally, the mapping $h : \text{supp}(\bar{\sigma}) \to \text{supp}(\bar{\sigma})$ defined as $h(\bar{s}(y_i)) \stackrel{\text{def}}{=} [\bar{s}(y_i)]_{/\approx}$, for all $i \in [1..m]$ is shown to be an isomorphism between $\mathfrak{S}$ and $\bar{S}_{/\approx}$, leading to $\mathfrak{S} \in \tilde{\text{IF}}([\mathfrak{A}]']_{\Delta})$, by the fact that the set $\tilde{\text{IF}}([\mathfrak{A}]']_{\Delta})$ is closed under isomorphism (Definition 3.5).

“$\supseteq$” Let $\mathfrak{S} \in \tilde{\text{IF}}([\mathfrak{A}]']_{\Delta})$ be a structure. Then there exists a rich canonical $\Delta$-model $(\bar{S}, \mathfrak{d}) \in [[\mathfrak{A}]']_{\Delta}$, where $\bar{S} = (\bar{U}, \bar{\sigma})$ and an equivalence relation $\approx \subseteq \bar{U} \times \bar{U}$ such that $\approx$ is compatible with $(\bar{S}, \mathfrak{d})$ and $\mathfrak{S}$ is isomorphic to $\bar{S}_{/\approx}$. Since $(\bar{S}, \mathfrak{d}) \in [[\mathfrak{A}]']_{\Delta}$, there exists a complete $\Delta$-unfolding $\mathfrak{A} \Rightarrow_{\Delta}^{*} \exists y_1 \dots \exists y_m \cdot \psi$, such that $\psi$ is qpf and a store $\bar{s}$, injective over $y_1, \dots, y_m$, such that $\bar{S} \models^{\bar{s}} \psi$ and $\mathfrak{d}(\bar{s}(z), \bar{s}(z'))$ for each disequality $z \neq z'$ from $\psi$. Let $\bar{s}$ be the store defined as $\bar{s}(y_i) = [\bar{s}(y_i)]_{/\approx}$, for all $i \in [1..m]$. We prove $\bar{S}_{/\approx} \models^{\bar{s}} \psi$ by induction on the structure of $\psi$, considering the following cases:

▷ $\psi = y_i \neq y_j$: because $\approx$ is compatible with $(\bar{S}, \mathfrak{d})$, we have $[\bar{s}(y_i)]_{/\approx} \neq [\bar{s}(y_j)]_{/\approx}$, hence $\bar{s}(y_i) \neq \bar{s}(y_j)$.

▷ $\psi = r(y_{i_1}, \dots, y_{i_{\#r}})$: because $\bar{S} \models^{\bar{s}} r(y_{i_1}, \dots, y_{i_{\#r}})$, we have $\bar{\sigma}(r) = \{\langle \bar{s}(y_{i_1}), \dots, \bar{s}(y_{i_{\#r}}) \rangle\}$ and $\bar{\sigma}_{/\approx}(r) = \{\langle [\bar{s}(y_{i_1})]_{/\approx}, \dots, [\bar{s}(y_{i_{\#r}})]_{/\approx} \rangle\}$, by Definition 3.3.

▷ $\psi = \psi_1 * \psi_2$: because $\bar{S} \models^{\bar{s}} \psi_1 * \psi_2$, there exist locally disjoint structures $\bar{S}_1 \bullet \bar{S}_2 = \bar{S}$, such that $\bar{S}_i \models^{\bar{s}} \psi_i$, for $i = 1, 2$. Since $\approx$ is compatible with $\mathfrak{S}$, the structures $\bar{S}_{1/\approx}$ and $\bar{S}_{2/\approx}$ are locally disjoint, by Definition 3.4. Then their composition is defined and we have $\bar{S}_{/\approx} = \bar{S}_{1/\approx} \bullet \bar{S}_{2/\approx}$. By the inductive hypothesis, we have $\bar{S}_{i/\approx} \models^{\bar{\sigma}} \psi_i$, for $i = 1, 2$, thus $\bar{S}_{/\approx} \models^{\bar{\sigma}} \psi_1 * \psi_2$.

Hence $\bar{S}_{/\approx} \in [[\mathfrak{A}]']_{\Delta}$ and $\mathfrak{S} \in [[\mathfrak{A}]']_{\Delta}$ follows, since the set $[[\mathfrak{A}]']_{\Delta}$ is closed under isomorphism, see, e.g., [IZ23, Proposition 7] for a proof. $\square$

**3.2. Expandable sets of inductive definitions.** We introduce the notion of *expandable* SID, a key ingredient of our proof of decidability for the TWB<sup>SLR</sup> problem. A structure is a *substructure* of another if the former is obtained from the latter by removing elements from its support:

**Definition 3.7.** Let $S_i = (U_i, \sigma_i)$ be structures, for $i = 1, 2$. $S_1$ is included in $S_2$ iff $U_1 \subseteq U_2$ and $\sigma_1(r) \subseteq \sigma_2(r)$, for all $r \in \mathbb{R}$. $S_1$ is a substructure of $S_2$, denoted $S_1 \sqsubseteq S_2$, iff $S_1 \subseteq S_2$ and $\sigma_1(r) = \{\langle u_1, \dots, u_{\#r} \rangle \in \sigma_2(r) \mid u_1, \dots, u_{\#r} \in \text{supp}(\sigma_1)\}$, for all $r \in \mathbb{R}$.

A SID is *expandable* if any set of canonical models of a sentence are all substructures of the same canonical model of that sentence, that can be, moreover, placed “sufficiently far away” one from another.

**Definition 3.8.** A SID $\Gamma$ is *expandable* for a nullary predicate $A$ iff for each sequence of pairwise disjoint canonical models $S_1 = (U_1, \sigma_1), \dots, S_n = (U_n, \sigma_n) \in [[\mathfrak{A}]']_{\Gamma}$, there exists a rich canonical model $(\mathfrak{S}, \mathfrak{d}) \in [[\mathfrak{A}]']_{\Gamma}$, where $\mathfrak{S} = (\mathfrak{U}, \mathfrak{\sigma})$, such that:

(1) $S_1 \bullet \dots \bullet S_n \sqsubseteq S$,

(2) $\mathfrak{d}(u, v)$ holds for no $u \in \text{supp}(\sigma_i)$ and $v \in \text{supp}(\sigma_j)$, where $1 \le i < j \le n$, and

(3) for no relation symbol $r \in \mathbb{R}$ and tuples $(u_1, \dots, u_{\#r})$, $(v_1, \dots, v_{\#r}) \in \sigma(r)$ there exist $1 \le i < j \le n$, such that $\{u_1, \dots, u_{\#r}\} \cap \text{supp}(\sigma_i) \neq \emptyset$, $\{v_1, \dots, v_{\#r}\} \cap \text{supp}(\sigma_j) \neq \emptyset$ and $\{u_1, \dots, u_{\#r}\} \cap \{v_1, \dots, v_{\#r}\} \neq \emptyset$.
**Example 3.9.** The SID $\Delta$ from Figure 5 is expandable for $A$, because any choice of pairwise disjoint canonical models of $A$ (here $S_1, S_2$ and $S_3$) can be embedded in a canonical model of $A$, such that there are no pairs, in the interpretation of the binary relation symbol $e$, that stretch from one such model to another (the pairs not entirely inside the support of either $S_1, S_2$ or $S_3$ are depicted in dashed lines).

<figure><img src="image_7.png" /><figcaption>Figure 5: An expandable SID</figcaption></figure>

**Example 3.10.** (continued from Example 3.9) Consider the SID $\Delta'$ obtained from $\Delta$ by changing its last rule into $B(x_1) \leftarrow \text{emp. } \Delta'$ is not expandable for $A$, because the canonical models of $A$ are acyclic chains of elements, whose neighbours are related by $e$, such that all but the last element is labeled by $a$. Then, two such structures $S_1$ and $S_2$ cannot be embedded in a third structure $S$ as substructures, because of the last non-labeled element of $S_1$ that occurs in the middle of $S$ and must be labeled by $a$. This violates the definition of substructures (see Definition 3.7), in which the labeling of an element is the same in a substructure and in its enclosing structure.

The *external fusion* is a binary operation that glues elements from disjoint structures:

**Definition 3.11.** An *external fusion* of the structures $S_1 = (U_1, \sigma_1)$ and $S_2 = (U_2, \sigma_2)$ is a structure isomorphic to $(S'_1 \bullet S'_2)_{\approx}$, where $S'_i = (U'_i, \sigma'_i)$ are disjoint isomorphic copies of $S_i$ and $\approx \subseteq U'_1 \times U'_2$ is the smallest equivalence relation containing a nonempty $\text{supp}(\sigma'_1)$-supp($\sigma'_2$) matching that is compatible with $S'_1 \bullet S'_2$. Let $\text{EF}(S_1, S_2)$ be the set of external fusions of $S_1$ and $S_2$. For a set of structures $S$, let $\text{EF}^*(S)$ (resp. $\text{IEF}^*(S)$) be the closure of $S$ under taking external (resp. both internal and external) fusions.

For example, Figure 6 shows the external fusion of two disjoint structures via a matching relation (the equivalence classes of the matching relation are encircled with dashed lines). Note that the conditions (2) and (3) of Definition 3.8 ensure that the external fusion of these substructures is not hindered by their position inside the larger structure. For instance, any matching relation between the supports of the substructures $S_1, S_2$ and $S_3$ from Figure 5 can be used to define an external fusion of these structures. This is because there are no pairs, from the interpretation of the $e$ relation symbol in $S$, that have an element in common and the other non-common elements in the support of two different substructures. If such pairs existed, the non-common elements could not be fused by an equivalence relation compatible with $S_i \bullet S_j$, for any $1 \le i < j \le 3$.

The following lemma proves one direction of the equivalence between the treewidth boundedness of $[[A]]_\Delta$ and that of the set of structures obtained by applying both internal and external fusion to the canonical models from $[[A]]_\Delta^c$.

**Lemma 3.12.** Let $\Delta$ be an expandable SID for a nullary predicate $A$. Then, (1) $\text{IEF}^*([A]^c_\Delta)$ is treewidth-bounded only if (2) $[[A]]_\Delta$ is treewidth-bounded only if (3) $\text{EF}^*([A]^c_\Delta)$ is treewidth-bounded.
<figure><img src="image_8.png" /><figcaption>Figure 6: External fusion</figcaption></figure>

Proof. “(1) ⇒ (2)” IF([[A]]<sub>Δ</sub><sup>c</sup>) ⊆ IEF<sup>*</sup>([[A]]<sub>Δ</sub><sup>c</sup>) holds trivially, by Definition 3.11, leading to [[A]]<sub>Δ</sub> ⊆ IEF<sup>*</sup>([[A]]<sub>Δ</sub><sup>c</sup>), by Lemma 3.6. “(2) ⇒ (3)” Let S = (U, σ) ∈ EF<sup>*</sup>([[A]]<sub>Δ</sub><sup>c</sup>) be a structure. It is sufficient to prove that S ⊆ S' for another structure S' ∈ [[A]]<sub>Δ</sub>, because tw(S) ≤ tw(S'), in this case. Then there exist pairwise disjoint structures S<sub>1</sub> = (U<sub>1</sub>, σ<sub>1</sub>), ..., S<sub>n</sub> = (U<sub>n</sub>, σ<sub>n</sub>) ∈ [[A]]<sub>Δ</sub><sup>c</sup> and an equivalence relation ≈ ⊆ (∪<sub>i=1</sub><sup>n</sup> U<sub>i</sub>) × (∪<sub>i=1</sub><sup>n</sup> U<sub>i</sub>), that is compatible with S<sub>1</sub> • ... • S<sub>n</sub>, matches only elements from different structures and is not the identity, such that S is isomorphic to (S<sub>1</sub> • ... • S<sub>n</sub>)<sub>/≈</sub>. By Definition 3.8, there exists a rich canonical model (S'', δ) ∈ [[A]]<sub>Δ</sub><sup>r</sup>, such that (1) S ⊆ S'', (2) δ(u, v) holds for no u ∈ supp(σ<sub>i</sub>) and v ∈ supp(σ<sub>j</sub>), where 1 ≤ i < j ≤ n, and (3) for no relation symbol r ∈ ℝ and tuples ⟨u<sub>1</sub>, ..., u<sub>#r</sub>⟩, ⟨v<sub>1</sub>, ..., v<sub>#r</sub>⟩ ∈ σ(r), there exist 1 ≤ i < j ≤ n, such that {u<sub>1</sub>, ..., u<sub>#r</sub>}∩supp(σ<sub>i</sub>) ≠ ∅, {v<sub>1</sub>, ..., v<sub>#r</sub>}∩supp(σ<sub>j</sub>) ≠ ∅ and {u<sub>1</sub>, ..., u<sub>#r</sub>}∩{v<sub>1</sub>, ..., v<sub>#r</sub>} ≠ ∅. By the last two conditions, ≈ is compatible with (S'', δ), leading to S''<sub>/≈</sub> ∈ ⋄IF([[A]]<sub>Δ</sub><sup>r</sup>) = [[A]]<sub>Δ</sub> by Lemma 3.6. We conclude by taking S' = S''<sub>/≈</sub>. □

The missing direction $EF^*(([A]^c_\Delta) \Rightarrow IEF^*([A]^c_\Delta))$, that allows to establish the equivalence of the three points of Lemma 3.12, requires the introduction of further technical notions. The proof of the main result of this section relies on an algorithm for the treewidth boundedness of sets $EF^*([A]^c_\Delta)$, obtained by external fusion of disjoint canonical $\Delta$-models of $A$. By the equivalence of the treewidth boundedness of the sets $[A]^c_\Delta$ and $EF^*([A]^c_\Delta)$ (Lemma 3.12 and Lemma 3.26), this is also an algorithm for the TWB$^{SLR}$ problem for expandable SIDs.

**3.3. Color schemes.** Intuitively, the color of an element from the support of a structure is the set of relation symbols labeling solely that element. For the given set $\mathbb{R}$ of relation symbols, we define the set of colors as $\mathbb{C} \stackrel{\text{def}}{=} \text{pow}(\mathbb{R})$. The elements of a structure are labeled with colors as follows:

**Definition 3.13.** The coloring of a structure $S = (U, \sigma)$ is the mapping $C_S : U \to \mathbb{C}$ defined as $C_S(u) \stackrel{\text{def}}{=} \{r \in \mathbb{R} \mid \langle u, \dots, u \rangle \in \sigma(r)\}$.

Moreover, we define an abstraction of structures as finite multisets of colors:

**Definition 3.14.** The multiset color abstraction $S^\sharp \in \text{mpow}(\mathbb{C})$ of a structure $S = (U, \sigma)$ is $S^\sharp \stackrel{\text{def}}{=} \{C_S(u) \mid u \in \text{supp}(\sigma)\}$. For an integer $k \ge 0$, the $k$-multiset color abstraction $S^{\sharp k} \subseteq \text{mpow}(\mathbb{C})$ is $S^{\sharp k} \stackrel{\text{def}}{=} \{M \subseteq S^\sharp \mid \text{card}(M) \le k\}$. These abstractions are lifted to sets $S$ of structures, yielding the sets of multisets $S^\sharp \stackrel{\text{def}}{=} \{S^\sharp \mid S \in S\}$ and $S^{\sharp k} \stackrel{\text{def}}{=} \bigcup_{S \in S} S^{\sharp k}$.

Colors are organized in *RGB color schemes*, defined below:

**Definition 3.15.** A partition $(\mathbb{C}^{\text{red}}, \mathbb{C}^{\text{green}}, \mathbb{C}^{\text{blue}})$ of $\mathbb{C}$ is an *RGB-color scheme* iff:

(1) $C_1 \cap C_2 \neq \emptyset$, for all $C_1, C_2 \in \mathbb{C}^{\text{blue}}$,

(2) $C_1 \cap C_2 \neq \emptyset$, for all $C_1 \in \mathbb{C}^{\text{green}}$ and $C_2 \in \mathbb{C}^{\text{blue}}$,

(3) for all $C_1 \in \mathbb{C}^{\text{red}}$ there exists $C_2 \in \mathbb{C}^{\text{blue}}$ such that $C_1 \cap C_2 = \emptyset$.
Note that an RGB-color scheme is fully specified by the set $C^{blue}$. Indeed, any color not in $C^{blue}$ is unambiguously placed within $C^{red}$ or $C^{green}$, depending on whether it is disjoint from some color in $C^{blue}$. For example, Figure 7 shows several RGB-color schemes for the relational signature $\mathbb{R} = \{a, b, c\}$.

<figure><img src="image_9.png" /><figcaption>Figure 7: Examples of RGB color schemes</figcaption></figure>

Because a fusion operation only joins element with disjoint colors, blue elements can only be joined with red elements, green elements can be joined with green or red elements, whereas red elements can be joined with elements of any other color, provided that they are disjoint subsets of $\mathbb{R}$. Moreover, a fusion operation can always join a pair of elements with disjoint colors:

**Lemma 3.16.** Let $S_1 = (U_1, \sigma_1)$ and $S_2 = (U_2, \sigma_2)$ be disjoint structures. Let $u_1 \in \text{supp}(\sigma_1)$, $u_2 \in \text{supp}(\sigma_2)$ be elements such that $C_{S_1}(u_1) \cap C_{S_2}(u_2) = \emptyset$. Then, the equivalence relation on $U_1 \cup U_2$ generated by $(u_1, u_2)$ is compatible with $S_1 \bullet S_2$.

*Proof.* We denote by $\approx$ the relation $\{(u_1, u_2)\}^= = \text{in the following. Let } r \in \mathbb{R}\text{ be a relation and let } \langle u_{1,1}, u_{1,2}, \dots, u_{1,r} \rangle \in \sigma_1(r), \langle u_{2,2}, u_{2,2}, \dots, u_{2,r} \rangle \in \sigma_2(r) \text{ be distinct tuples. If for some index } i \in [1..r] \text{ either } u_{1,i} \neq u_1 \text{ or } u_{2,i} \neq u_2 \text{ then } u_{1,i} \not\approx u_{2,i}, \text{ by the definition of } \approx$. Otherwise, if for all indices } i \in [1..r] \text{ both } u_{1,i} = u_1 \text{ and } u_{2,i} = u_2 \text{ then } r \in C_{S_1}(u_1) \text{ and } r \in C_{S_2}(u_2). This implies } C_{S_1}(u_1) \cap C_{S_2}(u_2) \neq \emptyset \text{ and contradicts the hypothesis about the choice of } u_1, u_2. Therefore, no tuples from } S_1 \text{ and } S_2 \text{ respectively are merged by the fusion. Finally, it is also an easy check that no tuples from } S_1 \text{ (resp. } S_2) \text{ are merged, because when restricted to } S_1 \text{ (resp. } S_2) \text{ the equivalence } \approx \text{ becomes the identity.}$ $\square$

The first ingredient of a decidable condition, equivalent to the treewidth boundedness of a set $\text{EF}^*([A]^c_\Delta)$, is conformance with an RGB color scheme, defined below:

**Definition 3.17.** A set $S$ of structures conforms to $(C^{red}, C^{green}, C^{blue})$ if and only if:

(1) for all structures $S = (U, \sigma) \in S$, if $C_S(u) \in C^{red}$, for some element $u \in \text{supp}(\sigma)$, then $C_S(u') \in C^{blue}$, for all other elements $u' \in \text{supp}(\sigma) \setminus \{u\}$, and

(2) $S^\# \cap C^{green} \subseteq [C, C | C \in C^{green}]$, for all structures $S \in \text{EF}^*(S)$.

Moreover, a structure $S \in S$ is said to be of either type:

▷ R if $S^\# \in \text{mpow}(C^{blue} \cup C^{red})$ and $\text{card}(S^\# \cap C^{red}) = 1$,

▷ G if $S^\# \in \text{mpow}(C^{blue} \cup C^{green})$ and $\text{card}(S^\# \cap C^{green}) > 0$, and

▷ B if $S^\# \in \text{mpow}(C^{blue})$.

Conformance to some RGB color scheme is the key to bounding the treewidth of the sets of structures obtained by external fusion of a treewidth bounded set of structures.
An equivalence relation $\approx$ is said to be generated by a set of pairs $(u_1, v_1), \dots, (u_k, v_k)$ if it is the least equivalence relation, such that $u_i \approx v_i$, for all $i \in [1..k]$. Furthermore, we say that $\approx$ is $k$-generated if $k$ is the minimal cardinality of a set of pairs that generates $\approx$.

**Lemma 3.18.** Let $S$ be a treewidth bounded set of structures conforming to an RGB color scheme. Then, for any structure $S \in \mathbf{EF}^*(S)$, the following hold:

(1) $S$ is of type either R, G or B,

(2) if $S = (S_1 \bullet S_2)_{\approx}$ for some $S_1, S_2 \in \mathbf{EF}^*(S)$ then exactly one of the following hold:

(a) $\approx$ is 1-generated, or

(b) $\approx$ is 2-generated and either (i) $S_1, S_2$ are of type R, or (ii) $S_1, S_2$ are of type G and $\mathrm{card}(S_1^{\#} \cap \mathbb{C}^{\mathrm{green}}) = \mathrm{card}(S_2^{\#} \cap \mathbb{C}^{\mathrm{green}}) = 2$

(3) $\mathrm{tw}(S) \le \mathrm{tw}(S) + 1$.

*Proof.* (1) By induction on the derivation of $S \in \mathbf{EF}^*(S)$ from $S$. Table 1 summarizes the possible types of $\mathbf{EF}(S_1, S_2)$ on structures $S_1$ and $S_2$ of types R, G or B, respectively.

<table><caption>Table 1: The types of structures obtained by external fusion ($\perp$ means none)</caption><thead><tr><th>EF(S<sub>1</sub>, S<sub>2</sub>)</th><th>S<sub>2</sub> of R type</th><th>S<sub>2</sub> of G type</th><th>S<sub>2</sub> of B type</th></tr></thead><tbody><tr><td>S<sub>1</sub> of R type</td><td>R, G, B</td><td>G, B</td><td>B</td></tr><tr><td>S<sub>1</sub> of G type</td><td>G, B</td><td>G, B</td><td>⊥</td></tr><tr><td>S<sub>1</sub> of B type</td><td>B</td><td>⊥</td><td>⊥</td></tr></tbody></table>

(2) We distinguish two cases:

▷ $S_1$ is of type R: If $S_2$ is of type B or G then $S_1$ and $S_2$ can be fused only by equivalences $\approx$ generated by a single pair, that contains the element from the support of $S_1$ with color in $\mathbb{C}^{\mathrm{red}}$, thus matching the case (1) from the statement. Else, if $S_2$ is of type R then $S_1$ and $S_2$ can be fused by equivalences generated by at most two pairs, each containing an element with color from $\mathbb{C}^{\mathrm{red}}$, from either $S_1$ or $S_2$, thus matching the case (2(b)i) from the statement.

▷ $S_1, S_2$ are both of type G: By contradiction, assume they can be fused by an equivalence $\approx$ generated by three pairs of elements $(u_{1i}, u_{2i})_{i=1,2,3}$. Let $G_{1i} = C_{S_1}(u_{1i})$, $G_{2i} = C_{S_2}(u_{2i})$ be the colors from $\mathbb{C}^{\mathrm{green}}$ of the matching elements in the two structures, for $i = 1, 2, 3$. Then, we can construct structures using $S_1$ and $S_2$ where any of these colors repeat strictly more than twice, henceforth, contradicting the conformance property to the RGB color scheme. The principle of the construction is depicted in Figure 8. Finally, note that the construction depicted in Figure 8 fuse actually only pairs of colors $(G_{1i}, G_{2i})$ for $i = 1, 2$. Henceforth, the conformance property is also contradicted if $S_1$ and $S_2$ can be fused by a 2-generated equivalence relation $\approx$, such that the support of either $S_1$ or $S_2$ contains more than three elements with colors in $\mathbb{C}^{\mathrm{green}}$.

(3) The previous point shows that, under the hypotheses of the lemma, every structure in $\mathbf{EF}^*(S)$ is constructed by external fusion with matchings generated by one or two pairs of elements. This result can be actually refined, i.e., we can consider only external fusions where the 1-generated matchings are applied before the 2-generated matchings. That is, assume $S = ((S_1 \bullet S_2)_{\approx_2} \bullet S_3)_{\approx_1}$ where $\approx_1, \approx_2$ are 1-, resp. 2-generated and $S_1, S_2, S_3 \in \mathbf{EF}^*(S)$. Without loss of generality, assume moreover, $\approx_1$ is matching some element
<figure><img src="image_10.png" /><figcaption>Figure 8: External fusion of G structures by 3-generated matchings</figcaption></figure>

of $S_3$ with an element of $S_1$ (the other case is symmetric). Then, we can find 1-, resp. 2-generated matchings $\approx_1', \approx_2'$ such that $S = ((S_1 \bullet S_3)_{\approx_1'} \bullet S_2)_{\approx_2'}$. That is, first fuse $S_1$ and $S_3$ by a single matching pair, then fuse the result with $S_2$ by two matching pairs. Therefore, we can w.l.o.g. assume in the following that $\mathrm{EF}^*(S) = \mathrm{EF}_2^*(\mathrm{EF}_1^*(S))$, where $\mathrm{EF}_k^*$ denotes the external fusion using only $k$-generated matchings.

Given a tree decomposition $T$ for a structure $S = (U, \sigma)$ and an equivalence relation $\approx \subseteq U \times U$, we denote by $T_{/\approx}$ the tree decomposition of the quotient structure $S_{/\approx}$, obtained by the relabeling of elements $u$ in the bags of $T$ by their representatives $[u]_{\approx}$. We prove the following facts:

**Fact 3.19.** $\mathrm{tw}(\mathrm{EF}_1^*(S)) \le \mathrm{tw}(S)$.

*Proof.* By induction on the derivation of $S \in \mathrm{EF}_1^*(S)$ from $S$.

**Base case:** Immediate, as for any $S \in S$ we have $\mathrm{tw}(S) \le \mathrm{tw}(S)$.

**Induction step:** Consider $S = (S_1 \bullet S_2)_{/\approx}$ where $\approx = \{(u_1, u_2)\}^=$. Let $T_1, T_2$ be tree decompositions of respectively $S_1, S_2$ such that $\mathrm{wd}(T_1), \mathrm{wd}(T_2) \le \mathrm{tw}(S)$. We first build a tree decomposition $T_{12}$ of $S_1 \bullet S_2$ by

* $\triangleright$ transforming $T_2$ into $T_2'$ by reversing edges such that a node $n_2$ containing $u_2$ in $T_2$ becomes the root of $T_2'$ and

* $\triangleright$ linking the root of $T_2'$ to a node $n_1$ of $T_1$ containing $u_1$.

This ensures that $T_{12}/\approx$ is a valid tree decomposition for $S$, and moreover $\mathrm{wd}(T_{12}/\approx) = \mathrm{wd}(T_{12}) = \max(\mathrm{wd}(T_1), \mathrm{wd}(T_2)) \le \mathrm{tw}(S)$. $\square$

**Fact 3.20.** Let $S = (U, \sigma) \in \mathrm{EF}_2^*(\mathrm{EF}_1^*(S))$ be a structure. Then, one of the following holds:

(A) $\mathrm{tw}(S) \le \mathrm{tw}(S)$,

(B) $S$ is of type B, $\mathrm{tw}(S) \le \mathrm{tw}(S) + 1$,

(C) $S$ is of type G and there exists $T = (\mathcal{N}, \mathcal{E}, r, \lambda)$ a tree decomposition of $S$ such that $\mathrm{wd}(T) \le \mathrm{tw}(S) + 1$ and $C_S(u) \in \mathbb{C}^{\text{green}}$ implies $u \in \lambda(r)$, for all $u \in \mathrm{supp}(\sigma)$.

*Proof.* By induction on the derivation of $S \in \mathrm{EF}_2^*(\mathrm{EF}_1^*(S))$ from $\mathrm{EF}_1^*(S)$.

**Base case:** Immediate, as we already shown $\mathrm{tw}(S) \le \mathrm{tw}(S)$, that is, (A) for any $S \in \mathrm{EF}_1^*(S)$.

**Induction step:** Consider $S = (S_1 \bullet S_2)_{/\approx}$ where $\approx = \{(u_{11}, u_{21}), (u_{12}, u_{22})\}^=$. Since $\approx$ is 2-generated, we know from the previous point (2) that either:

* $S_1, S_2$ are of type R: From the induction hypothesis on $S_1$ and $S_2$ it follows that both must satisfy (A), hence $\mathrm{tw}(S_1) \le \mathrm{tw}(S)$, $\mathrm{tw}(S_2) \le \mathrm{tw}(S)$ respectively. We are therefore in the situation of composing two structures of type R by a 2-generated matching, hence obtaining the structure S of type B. Without loss of generality consider $C_{S_1}(u_{11}) \in \mathbb{C}^{\mathrm{red}}$,
$C_{S_1}(u_{12}) \in \mathbb{C}^{blue}$, $C_{S_2}(u_{21}) \in \mathbb{C}^{blue}$, $C_{S_2}(u_{22}) \in \mathbb{C}^{red}$. Let $T_1, T_2$ be tree decompositions of $S_1, S_2$ respectively. First, we construct a tree decomposition $T_{12}$ for $S_1 \bullet S_2$ as follows:

- construct $T'_1$ from $T_1$ by propagating the element $u_{11}$ to all the nodes,

- construct $T'_2$ from $T_2$ by propagating the element $u_{22}$ to all the nodes and then reverting the edges such that a node $n_2$ containing the element $u_{21}$ becomes the root,

- link the root node of $T'_2$ to a node $n_1$ of $T'_1$ containing the element $u_{12}$.

This ensures that $T_{12/\approx}$ is a valid tree decomposition for $S$, and moreover $\mathrm{wd}(T_{12/\approx}) = \mathrm{wd}(T_{12}) = \max(\mathrm{wd}(T'_1), \mathrm{wd}(T'_2)) = \max(\mathrm{wd}(T_1) + 1, \mathrm{wd}(T_2) + 1) \le \mathrm{tw}(S) + 1$. This completes the proof that $S$ satisfies condition (B).

▷ $S_1, S_2$ are of type $G$ and $\mathrm{card}(S_1^{\#} \cap \mathbb{C}^{green}) = \mathrm{card}(S_2^{\#} \cap \mathbb{C}^{green}) = 2$: First, let us observe that the structure $S$ is either of type $B$ or $G$. According to the induction hypothesis, we consider the following two cases:

- both $S_1$ and $S_2$ satisfy the condition (C), namely there exist the tree decompositions $T_1, T_2$ of width at most $\mathrm{tw}(S) + 1$ such that moreover all the elements with colors in $\mathbb{C}^{green}$ are located at their root nodes. Then, we can construct a tree decomposition $T_{12}$ for $S_1 \bullet S_2$ by simply linking the root of $T_2$ as a child to the root of $T_1$. We obtain that $T_{12/\approx}$ is a valid decomposition for $S$ and satisfies $\mathrm{wd}(T_{12/\approx}) = \mathrm{wd}(T_{12}) = \max(\mathrm{wd}(T_1), \mathrm{wd}(T_2)) \le \mathrm{tw}(S) + 1$. Moreover, if $S$ is of type $G$ observe that all the elements with colors in $\mathbb{C}^{green}$ are located at the root node of $T_{12/\approx}$. Therefore, in any case, the structure $S$ satisfies either (B) or (C).

- either one or both of $S_1$ or $S_2$ satisfy the condition (A). Without loss of generality consider $\mathrm{tw}(S_1) \le \mathrm{tw}(S)$. We know however that $S_1$ satisfies $\mathrm{card}(S_1^{\#} \cap \mathbb{C}^{green}) = 2$, that is, it has exactly two elements with colors in $\mathbb{C}^{green}$. But then, we can show that $S_1$ satisfies the condition (C) as well. That is, consider a tree decomposition $T_1$ for $S_1$ such that $\mathrm{wd}(T_1) \le \mathrm{tw}(S)$. Let $u_{11}, u_{12}$ be the two elements with colors in $\mathbb{C}^{green}$. We can build a tree decomposition $T'_1$ fulfilling (C) by first propagating the element $u_{11}$ to all the nodes of $T_1$ and then reverting the edges such that some node containing the element $u_{12}$ becomes the root. Obviously, $\mathrm{wd}(T'_1) = \mathrm{wd}(T_1) + 1 \le \mathrm{tw}(S) + 1$ and all the elements with color in $\mathbb{C}^{green}$ are located at the root node. We can proceed similarly with $S_2$. Then, the proof is completed as in the first case. $\square$

This completes the proof of the point (3) from the statement. $\square$

Moreover, conformance with RGB schemes allow us to infer a bound on the set obtained by applying external fusion to a treewidth bounded set of structures:

**Lemma 3.21.** Let $S$ be a treewidth bounded set of structures, that conforms to an RGB color scheme. Then, we have $\mathrm{tw}(\mathrm{IF}(\mathrm{EF}^*(S))) \le \mathrm{tw}(S) + 1$.

*Proof.* $\mathrm{EF}^*(S)$ is treewidth bounded as a direct consequence of Lemma 3.18, that establishes the bounds for every type of structure from $\mathrm{EF}^*(S)$. Moreover, $\mathrm{IF}(\mathrm{EF}^*(S))$ is treewidth-bounded because, using the tree decompositions $T$ constructed for structures $S$ in $\mathrm{EF}^*(S)$ one obtains tree decomposition $T'$ and treewidth bounds for any structures $S' = S/\approx$ obtained by internal fusion, as follows:

▷ if $S$ is of type $R$ then by internal fusion one glues the unique element $u_1$ with color in $\mathbb{C}^{red}$ to some other element in the structure. We know, from the inductive property used in the proof of Lemma 3.18 (3) that if $S$ is of type $R$ then it must satisfies condition (A) of Fact 3.20 that is, $\mathrm{tw}(S) \le \mathrm{tw}(S)$. Therefore, one can construct $T'$ from $T$ by
replicating $u_1$ in all nodes and then $T'_{/\approx}$ is a valid tree decomposition for $S'$. Obviously $\mathrm{wd}(T') \le \mathrm{wd}(T) + 1 \le \mathrm{tw}(S) + 1$.

▷ if $S$ is of type $G$ then by internal fusion one glue elements with color in $C^{green}$. As before, using the same inductive property, we know that $S$ satisfies either condition (A) or (C) of Fact 3.20. If $S$ satisfies condition (C), as all elements that could be glued are already present in the root node, $T_{/\approx}$ is a valid tree decomposition for $S'$. Obviously, the treewidth bound remains unchanged, that is, at most $\mathrm{tw}(S) + 1$. If $S$ satisfies condition (A) and two of its nodes $u_1, u_2$ with colors in $C^{green}$ can be fused, then two copies of $S$, respectively $S'$, $S''$ can also be fused via the two-pair matching $(u'_1, u''_2)$, $(u''_1, u'_2)$. Henceforth, $u_1$ and $u_2$ must be the unique elements with colors in $C^{green}$, otherwise contradicting the point (2) of Lemma 3.18. But then, from the tree decomposition $T$ of $S$ such that $\mathrm{wd}(T) \le \mathrm{tw}(S)$ we can construct the tree decomposition $T'$ be simply propagating $u_2$ to all other nodes in $T$ and hence, preserving the bound of $\mathrm{tw}(S) + 1$.

▷ if $S$ is of type $B$ then no non-trivial internal fusion exists, and obviously, the treewidth bound remains unchanged. $\square$

**3.4. Connected structures.** We shall check conformance with RGB schemes for sets of maximally connected structures, defined below:

**Definition 3.22.** A path from $u$ to $v$ in a structure $S = (U, \sigma)$ is a finite sequence of tuples:

$$ \langle u_{1,1}, \dots, u_{1,n_1} \rangle \in \sigma(r_1), \dots, \langle u_{k,1}, \dots, u_{k,n_k} \rangle \in \sigma(r_k), \text{ for some } r_1, \dots, r_k \in \mathbb{R} $$

where $u \in \{u_{1,1}, \dots, u_{1,n_1}\}, v \in \{u_{k,1}, \dots, u_{k,n_k}\}$ and $\{u_{i,1}, \dots, u_{i,n_i}\} \cap \{u_{i+1,1}, \dots, u_{i+1,n_{i+1}}\} \ne \emptyset$, for all $i \in [1..k-1]$. The structure $S$ is connected iff there exists a path from $u$ to $v$, for all $u, v \in \mathrm{supp}(\sigma)$.

**Definition 3.23.** A structure $S_1$ is a maximal connected substructure of another structure $S_2$, denoted $S_1 \sqsubseteq^{mc} S_2$, iff (i) $S_1 \sqsubseteq S_2$ (see Definition 3.7), (ii) $S_1$ is connected, and (iii) for any connected substructure $S'_1 \sqsubseteq S_2$, we have $S_1 \sqsubseteq S'_1$ only if $S_1 = S'_1$. For a structure $S$ we denote by $\mathbf{split}(S) \stackrel{\mathrm{def}}{=} \{S' | S' \sqsubseteq^{mc} S\}$ the set of maximally connected substructures, lifted to sets of structures $S$ as $\mathbf{split}(S) \stackrel{\mathrm{def}}{=} \cup_{S \in \mathcal{S}} \mathbf{split}(S)$.

Note that $\mathrm{tw}(S) = \mathrm{tw}(\mathbf{split}(S))$ for any set of structures $S$. The next lemma shows that both internal and external fusions preserve maximally connected substructures:

**Lemma 3.24.** For each set $S$ of structures, the following hold:

(1) $\mathrm{split}(\mathrm{EF}^*(S)) = \mathrm{EF}^*(\mathrm{split}(S))$, and

(2) $\mathrm{split}(\mathrm{IEF}^*(S)) = \mathrm{IEF}^*(\mathrm{split}(S))$.

*Proof.* For space reasons, this proof is given in subsection B.1. $\square$

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

The core of our algorithm is a decidable equivalent condition for the treewidth boundedness of a set obtained by applying external fusion to a set of connected structures. This condition is that, in any of the structures produced by external fusion, there is no way of connecting six elements $u_1, v_1, w_1$ and $u_2, v_2, w_2$, labeled with non-disjoint colors $C_1$ and $C_2$, respectively. Assume that this condition is violated by some structures $S_1$ and $S_2$ with elements $u_1, v_1, w_1$ and $u_2, v_2, w_2$, such that $C_1 \cap C_2 = \emptyset$. In this case, Figure 9 depicts the construction of a structure with an $n \times n$ square grid minor, of treewidth at least $n$, for any $n \ge 1$. Intuitively, $C_1 \cap C_2 = \emptyset$ allows to glue the elements $u_1$ with $u_2$, $v_1$ with $v_2$ and $w_1$ with $w_2$, respectively.
**Lemma 3.25.** The following are equivalent, for any treewidth-bounded set $S$ of structures:

(1) $\mathrm{EF}^*(S)$ is treewidth bounded,

(2) $\{C_1, C_1, C_1\}, \{C_2, C_2, C_2\} \in (\mathrm{EF}^*(\mathrm{split}(S)))^{\#3}$ implies $C_1 \cap C_2 \neq \emptyset$, for all $C_1, C_2 \in \mathbb{C}$,

(3) $\mathrm{split}(S)$ conforms to some RGB color scheme.

*Proof.* "(1) ⇒ (2)" If $\mathrm{EF}^*(S)$ is treewidth-bounded then $\mathrm{split}(\mathrm{EF}^*(S))$ is treewidth-bounded. Using Lemma 3.24 the later set is equal to $\mathrm{EF}^*(\mathrm{split}(S))$ and henceforth treewidth bounded as well. By contradiction, assume that (2) does not hold. Then, there exist colors $C_1, C_2 \in \mathbb{C}$, connected structures $S_1, S_2 \in \mathrm{EF}^*(\mathrm{split}(S))$ such that $\{C_1, C_1, C_1\} \in S_1^\#$, $\{C_2, C_2, C_2\} \in S_2^\#$ and moreover $C_1 \cap C_2 = \emptyset$. We shall use $S_1$ and $S_2$ to build infinitely many connected structures containing arbitrarily large square grid minors. First, construct the connected structure $S_{12} \in \mathrm{EF}^*(\mathrm{split}(S))$ by fusing one pair $(u_1, u_2)$ with colors $C_1, C_2$. Let $v_1, w_1$ resp. $v_2, w_2$ be the remaining distinct elements of $S_{12}$ with color $C_1, C_2$ from respectively $S_1, S_2$. For arbitrarily positive $n$, consider $n \times n$ disjoint copies $(S_{12}^{i,j})_{i,j=1,n}$ of $S_{12}$. Let $\approx^{1,j}$ be $\{(v_1^{1,j}, v_2^{1,j-1})\} = \approx^{i,1}$ be $\{(w_2^{i,1}, w_1^{i-1,1})\} = \approx^{i,j}$ be $\{(v_1^{i,j}, v_2^{i,j-1}), (w_2^{i,j}, w_1^{i-1,j})\} = \approx^{i,j}$ for all $i, j = 2, n$. Second, construct the grid-like connected structure $X^{n,n} \in \mathrm{EF}^*(\mathrm{split}(S))$:

$$X^{n,n} = (...((S_{12}^{1,1} \bullet S_{12}^{1,2})_{\approx^{1,2}} \bullet S_{12}^{2,1})_{\approx^{2,1}} \bullet ... \bullet S_{12}^{i,j})_{\approx^{i,j}} \bullet ... \bullet S_{12}^{n,n})_{\approx^{n,n}}$$

where structures $S_{12}^{i,j}$ are added to the fusion in increasing order of $i + j$. The construction is illustrated in Figure 9. We can show that $X^{n,n}$ contains an $n \times n$ square grid minor. Finally, as $n$ can be taken arbitrarily large, we conclude that $\mathrm{EF}^*(\mathrm{split}(S))$ contains structures with arbitrarily large square grid minors, it is not treewidth-bounded, contradicting (1).

<figure><img src="image_12.png" /><figcaption>Figure 9: The principle of grid construction</figcaption></figure>

“(2) ⇒ (3)” We define a RGB color scheme by selecting:

$$\mathbb{C}^{\mathrm{blue}} = \{C \in \mathbb{C} \mid \{C, C, C\} \in (\mathrm{EF}^*(\mathrm{split}(S)))^{\#3}\}$$

Since (2) holds, this is a valid definition for $\mathbb{C}^{\mathrm{blue}}$, which induces a partitioning of the remaining colors into $\mathbb{C}^{\mathrm{green}}$ and $\mathbb{C}^{\mathrm{red}}$. We show that $\mathrm{split}(S)$ is conforming to this RGB partitioning, by checking the two points of Definition 3.17:

(1) Let $S \in \mathrm{split}(S)$ and prove that for any two colors $C_1, C_2 \in \mathbb{C}$, if $\{C_1, C_2\} \subseteq S^\#$ and $C_1 \in \mathbb{C}^{\mathrm{red}}$ then $C_2 \in \mathbb{C}^{\mathrm{blue}}$. Since $C_1 \in \mathbb{C}^{\mathrm{red}}$, there must exists a color $C'_1 \in \mathbb{C}^{\mathrm{blue}}$, such that $C_1 \cap C'_1 = \emptyset$, by Definition 3.15. By the definition of $\mathbb{C}^{\mathrm{blue}}$ in our RGB-color
scheme, this further implies $\{\mathcal{C}'_1, \mathcal{C}'_1, \mathcal{C}'_1\} \in (\mathrm{EF}^*(\mathrm{split}(S)))^{\#3}$. Henceforth, there exists a structure $S' \in \mathrm{EF}^*(\mathrm{split}(S))$ such that $\{\mathcal{C}'_1, \mathcal{C}'_1, \mathcal{C}'_1\} \subseteq S'^{\#}$. We can now use $S'$ and three disjoint copies of $S$ to build a new structure $S''$ by gluing progressively, each one of the three elements of color $\mathcal{C}'_1$ in $S'$ to the element of color $\mathcal{C}_1$ of $S$. Then, by construction, the structure $S''$ will also contain three elements of color $\mathcal{C}_2$, one from each disjoint copy of $S$. Therefore, $\{\mathcal{C}_2, \mathcal{C}_2, \mathcal{C}_2\} \in S''^{\#}$ and because $S'' \in \mathrm{EF}^*(\mathrm{split}(S))$ this implies $\{\mathcal{C}_2, \mathcal{C}_2, \mathcal{C}_2\} \in (\mathrm{EF}^*(\mathrm{split}(S)))^{\#3}$ and therefore $\mathcal{C}_2 \in \mathbb{C}^{\mathrm{blue}}$.

(2) By contradiction, let $S \in \mathrm{EF}^*(\mathrm{split}(S))$ be such that $S^\# \sqcap \mathbb{C}^{\mathrm{green}} \not\subseteq \{\mathcal{C}, \mathcal{C} \mid \mathcal{C} \in \mathbb{C}^{\mathrm{green}}\}$. Then there exists $C' \in (S^\# \sqcap \mathbb{C}^{\mathrm{green}}) \setminus \{\mathcal{C}, \mathcal{C} \mid \mathcal{C} \in \mathbb{C}^{\mathrm{green}}\}$, i.e., $C' \in \mathbb{C}^{\mathrm{green}}$ and $\{\mathcal{C}', \mathcal{C}', \mathcal{C}'\} \subseteq S^\#$. The latter implies $\{\mathcal{C}', \mathcal{C}', \mathcal{C}'\} \in S'^3 \subseteq (\mathrm{EF}^*(\mathrm{split}(S)))^{\#3}$. But this implies $\mathcal{C}' \in \mathbb{C}^{\mathrm{blue}}$ according to the definition of the RGB color scheme, contradicting $\mathcal{C}' \in \mathbb{C}^{\mathrm{green}}$.

"(3) ⇒ (1)" By Lemma 3.21, $\mathrm{EF}^*(\mathrm{split}(S))$ is treewidth bounded. Then, by Lemma 3.24, $\mathrm{split}(\mathrm{EF}^*(S))$ is treewidth bounded, thus $\mathrm{EF}^*(S)$ is treewidth bounded. □

A first consequence of this result is the equivalence between the treewidth boundedness of the sets $[\mathcal{A}]_\Delta$ and $\mathrm{EF}^*([\mathcal{A}]_\Delta^c)$. The following lemma establishes this equivalence, by providing the missing direction to Lemma 3.12:

**Lemma 3.26.** *Given a SID $\Delta$ and a nullary predicate symbol $A$, $\mathrm{EF}^*([\mathcal{A}]_\Delta^c)$ is treewidth bounded only if $\mathrm{IEF}^*([\mathcal{A}]_\Delta^c)$ is treewidth bounded.*

*Proof.* For any set of structures $S$, we have $\mathrm{IEF}^*(S) = \mathrm{IF}(\mathrm{EF}^*(S))$, because the operations of internal and external fusion commute, namely $\mathrm{EF}(\mathrm{IF}(S_1), S_2) \subseteq \mathrm{IF}(\mathrm{EF}(S_1, S_2))$, for any structures $S_1, S_2$. By Lemma 3.25, $\mathrm{EF}^*([\mathcal{A}]_\Delta^c)$ is treewidth-bounded only if $\mathrm{split}([\mathcal{A}]_\Delta^c)$ conforms to an RGB color scheme. Then, $\mathrm{IF}(\mathrm{EF}^*(\mathrm{split}([\mathcal{A}]_\Delta^c))) = \mathrm{IEF}^*(\mathrm{split}([\mathcal{A}]_\Delta^c)) = \mathrm{split}(\mathrm{IEF}^*([\mathcal{A}]_\Delta^c))$ is treewidth-bounded, by Lemma 3.21 and Lemma 3.24. Thus, $\mathrm{IEF}^*([\mathcal{A}]_\Delta^c)$ is treewidth bounded. □

Our algorithm that decides the treewidth boundedness of a set $\mathrm{EF}^*([\mathcal{A}]_\Delta^c)$ checks whether the set $(\mathrm{EF}^*(\mathrm{split}([\mathcal{A}]_\Delta^c)))^{\#3}$ meets condition (2) of Lemma 3.25. For this check to be effective, the latter set must be constructed in finite time from the description of $\Delta$ and $A$, provided as input. This construction proceeds in three consecutive stages. First, we show that, for any set $S$ of structures, the $k$-color abstraction $(^k\mathrm{EF}^*(S))$ can be built from $S^{\#k}$ by an effectively computable abstract operator. Second, we build a SID $\Gamma$ and a nullary predicate $P$, such that $[P]_\Gamma^c = \mathrm{split}([A]_\Delta^c)$, i.e., it encodes the set of maximally connected substructures from some canonical $\Delta$-model of $A$ (subsection 3.6). Finally, we compute the $k$-multiset color abstraction of $[P]_\Gamma^c$ (subsection 3.7). We end this section with a proof of decidability for the treewidth boundedness problem for expandable SIDs (Theorem 3.33).

**3.5. Color abstractions of externally fused sets.** We describe now the effective construction of a $k$-multiset abstraction $(\mathrm{EF}^*(S))^{\#k}$ from the abstraction $S^{\#k}$ of a set $S$ of structures, for a given integer $k \ge 1$. First, as we are interested only in $k$-multisets color abstractions, we can restrict external fusion to 1-generated matchings, with no loss of generality.

**Definition 3.27.** The single-pair external fusion of disjoint structures $S_1 = (U_1, \sigma_1)$ and $S_2 = (U_2, \sigma_2)$ is the external fusion (Definition 3.11) induced by 1-generated matchings. We denote by $\mathrm{EF}_1(S_1, S_2)$ the set of structures obtained by single-pair external fusion of $S_1$ and $S_2$. For a set of structures $S$, we denote by $\mathrm{EF}_1^*(S)$ the closure of $S$ under single-pair external fusions.
In general, the single-pair external fusion is strictly less expressive than external fusion, yet it produces the same k-multiset color abstractions:

**Lemma 3.28.** $(\mathrm{EF}^*(S))^{\sharp k} = (\mathrm{EF}_1^*(S))^{\sharp k}$ for any set $S$ of structures and integer $k \ge 1$.

*Proof.* “$(\mathrm{EF}_1^*(S))^{\sharp k} \subseteq (\mathrm{EF}^*(S))^{\sharp k}$” This direction follows directly from $\mathrm{EF}_1^*(S) \subseteq \mathrm{EF}^*(S)$. “$(\mathrm{EF}^*(S))^{\sharp k} \subseteq (\mathrm{EF}_1^*(S))^{\sharp k}$” We prove the stronger property:

$$ \forall S \in \mathrm{EF}^*(S). \exists S' \in \mathrm{EF}_1^*(S). S^{\sharp} \subseteq S'^{\sharp} $$

By induction on the derivation of $S \in \mathrm{EF}^*(S)$ from $S$.

**Base case:** Assume $S \in S$. Then $S' = S$ satisfies the property.

**Induction step:** Assume $S = (S_1 \bullet S_2)_{\approx}$ for some $S_1, S_2 \in \mathrm{EF}^*(S)$ and some equivalence relation $\approx$, defined as $\{(u_{1i}, u_{2i}) \mid i \in [1..n]\}^=$, that conforms to the requirements of external fusion for $S_1, S_2$. Let $C_{1i} = C_{S_1}(u_{1i})$, $C_{2i} = C_{S_2}(u_{2i})$, for all $i \in [1..n]$. According to the definition of external fusion, $S = (S_1 \bullet S_2)_{\approx}$ implies $C_{1i} \cap C_{2i} = \emptyset$ and moreover:

$$ S^{\sharp} = \{(C_{1i} \cup C_{2i}) \mid i \in [1..n]\} \cup (S_1^{\sharp} \setminus \{(C_{1i}) \mid i \in [1..n]\}) \cup (S_2^{\sharp} \setminus \{(C_{2i}) \mid i \in [1..n]\}) $$

By induction hypothesis, for $S_1, S_2$ there exists $S'_1, S'_2 \in \mathrm{EF}_1^*(S)$ such that $S_1^{\sharp} \subseteq S'_1^{\sharp}$, $S_2^{\sharp} \subseteq S'_2^{\sharp}$. We use $S'_1$ and $n$ disjoint copies $S'_{2,1}, \dots, S'_{2,n}$ of $S'_2$ to construct $S'$ with the required property. The idea is that, for every pair $u_{1i} \approx u_{2i}$, we fuse some element $u'_{1i}$ with color $C_{1i}$ from $S'_1$ with some element $u'_{2i}$ with color $C_{2i}$ from $S'_{2,i}$. Such elements always exist, because $S_1^{\sharp} \subseteq S'_1^{\sharp}$, $S_2^{\sharp} \subseteq S'_2^{\sharp}$. Therefore, consider the equivalence relations $\approx'_i = (u'_{1i}, u'_{2i})^=$ for some pair of elements as above, for all $i \in [1..n]$ and define:

$$ S' = (\dots((S'_1 \bullet S'_{2,1})_{\approx'_1} \bullet S'_{2,2})_{\approx'_2} \bullet \dots \bullet S'_{2,n})_{\approx'_n} $$

Then $S' \in \mathrm{EF}_1^*(S)$ and, moreover, we have $S^{\sharp} \subseteq S'^{\sharp}$, because:

$$ S'^{\sharp} = \{(C_{1i} \cup C_{2i}) \mid i \in [1..n]\} \cup (S'_1^{\sharp} \setminus \{(C_{1i}) \mid i \in [1..n]\}) \cup \bigcup_{i \in [1..n]} (S'_2^{\sharp} \setminus \{(C_{2i}) \mid i \in [1..n]\}) \quad \square $$

Second, the closure $(\mathrm{EF}_1^*(S))^{\sharp k}$ can be computed by a least fixpoint iteration of an abstract operation on the domain of k-multiset color abstractions. As the later domain is finite, this fixpoint computation is guaranteed to terminate.

**Definition 3.29.** The single-pair multiset fusion is defined below, for $M_1, M_2 \in \mathrm{mpow}(\mathbb{C})$:

$$ \begin{gathered} \mathrm{ef}_1^{\sharp}(M_1, M_2) \stackrel{\mathrm{def}}{=} \{M \in \mathrm{mpow}(\mathbb{C}) \mid \exists C_1 \in M_1. \exists C_2 \in M_2. C_1 \cap C_2 = \emptyset, \\ M = \{C_1 \cup C_2\} \cup \bigcup_{i=1,2} (M_i \setminus \{C_i\}) \} \end{gathered} $$

Given an integer $k \ge 1$, the single-pair k-multiset fusion is defined for $M_1, M_2 \in \mathrm{mpow}(\mathbb{C})$, such that $\mathrm{card}(M_1) \le k$ and $\mathrm{card}(M_2) \le k$:

$$ \mathrm{ef}_1^{\sharp k}(M_1, M_2) \stackrel{\mathrm{def}}{=} \{M \mid \exists M' \in \mathrm{ef}_1^{\sharp}(M_1, M_2). M \subseteq M', \mathrm{card}(M) \le k\} $$

For a set $M$ of multisets (resp. k-multisets) of colors, let $\mathrm{ef}_1^{\sharp k}(M)$ (resp. $\mathrm{ef}_1^{\sharp k}(M)$) be the closure of $M$ under taking single-pair fusion on multisets (resp. k-multisets).

**Lemma 3.30.** $(\mathrm{EF}_1^*(S))^{\sharp k} = \mathrm{ef}_1^{\sharp k}(S^{\sharp k})$, for any set $S$ of structures and integer $k \ge 1$.

*Proof.* Abusing notation, we write $M^{\sharp k} \stackrel{\mathrm{def}}{=} \{M' \mid M' \subseteq M, \mathrm{card}(M') \le k\}$. Then, we have $(\mathrm{EF}_1^*(S))^{\sharp k} = ((\mathrm{EF}_1^*(S))^{\sharp})^{\sharp k}$, by Definition 3.14. Using Definition 3.27 of single pair external fusion and Definition 3.29 of single pair fusion of multisets, we can prove that for all
structures $S_1, S_2$ it holds $(\mathrm{EF}_1(S_1, S_2))^\sharp = \mathrm{ef}_1^\sharp(S_1^\sharp, S_2^\sharp)$. This immediately extends to their respective closure, henceforth, $(\mathrm{EF}_1^*(S))^\sharp = \mathrm{ef}_1^{\sharp*}(S^\sharp)$. Henceforth, we are left with proving that $(\mathrm{ef}_1^{\sharp*}(S^\sharp))^\sharp^k = \mathrm{ef}_1^{\sharp k*}(S^{\sharp k})$.

“(ef$_1^{\sharp*}(S^\sharp))^\sharp^k \subseteq ef_1^{\sharp k*}(S^{\sharp k})” We prove that, for all $M \in ef_1^{\sharp*}(S^\sharp)$, we have $M^{\sharp k} \subseteq ef_1^{\sharp k*}(S^{\sharp k})$. The proof goes by induction on the derivation of $M \in ef_1^{\sharp*}(S^\sharp)$ from $S^\sharp$.

**Base case:** Assume $M \in S^\sharp$. Then $M^{\sharp k} \subseteq (S^\sharp)^{\sharp k} = S^{\sharp k} \subseteq ef_1^{\sharp k*}(S^{\sharp k})$.

**Induction step:** Assume $M \in ef_1^*(M_1, M_2)$ for some multisets of colors $M_1, M_2$ such that $M_1^{\sharp k}, M_2^{\sharp k} \subseteq ef_1^{\sharp k*}(S^{\sharp k})$. Then, there exists $C_1 \in M_1, C_2 \in M_2$ such that $C_1 \cap C_2 = \emptyset$ and $M = (M_1 \setminus \{C_1\}) \cup (M_2 \setminus \{C_2\}) \cup \{C_1 \cup C_2\}$, by Definition 3.29. Let $M' \in M^{\sharp k}$, that is, $M' \subseteq M$, $\mathrm{card}(M') \le k$. We distinguish several cases:

▷ $M' \subseteq M_1$ (the case $M' \subseteq M_2$ is symmetric): $M' \in M_1^{\sharp k}$, thus $M' \in ef_1^{\sharp k*}(S^{\sharp k})$.

▷ $M' \not\subseteq M_i$, for $i = 1, 2$ and $C_1 \cup C_2 \notin M'$: $M'$ can be partitioned in two nonempty parts $M'_1 \subseteq M_1, M'_2 \subseteq M_2$ such that $M = M'_1 \uplus M'_2$. As both parts are not empty, we have $M'_1 \in M_1^{\sharp k-1}, M'_2 \in M_2^{\sharp k-1}$, thus $(M'_1 \cup \{C_1\}) \in M_1^{\sharp k}, (M'_2 \cup \{C_2\}) \in M_2^{\sharp k}$. It is an easy check that $M' \in ef_1^{\sharp k}((M'_1 \cup \{C_1\}), (M'_2 \cup \{C_2\}))$. This implies $M' \in ef_1^{\sharp k*}(S^{\sharp k})$ as both subterms belong to $ef_1^{\sharp k*}(S^{\sharp k})$.

▷ $M' \not\subseteq M_i$, for $i = 1, 2$ and $C_1 \cup C_2 \in M'$: we proceed as in the previous case but considering a partitioning of $M' \setminus \{C_1 \cup C_2\}$. We obtain $M' \in ef_1^{\sharp k*}(S^{\sharp k})$, as well.

“ef$_1^{\sharp k*}(S^\sharp) \subseteq (ef_1^{\sharp*}(S^\sharp))^\sharp$” We prove that, for all $k$-multiset $M' \in ef_1^{\sharp k*}(S^{\sharp k})$, there exists $M \in ef_1^{\sharp*}(S^\sharp)$, such that $M' \subseteq M$, by induction on the derivation of $M'$ from $S^{\sharp k}$.

**Base case:** Assume $M' \in S^{\sharp k} = (S^\sharp)^{\sharp k}$. Then, there exists $M \in S^\sharp$ such that $M' \subseteq M$. Obviously, $M \in ef_1^{\sharp*}(S^\sharp)$.

**Induction step:** Assume $M' \in ef_1^{\sharp k}(M'_1, M'_2)$ for some $k$-multisets of colors $M'_1, M'_2 \in ef_1^{\sharp k*}(S^{\sharp k})$. By the inductive hypothesis, there exists multisets $M_1, M_2 \in ef_1^{\sharp*}(S^\sharp)$ such that $M'_1 \subseteq M_1, M'_2 \subseteq M_2$. Since $M'_1, M'_2$ can be composed such that to obtain (a superset of) the multiset $M'$, one can use precisely the same pairs of colors to compose $M_1, M_2$ and henceforth to obtain the multiset $M \in ef_1^{\sharp*}(S^\sharp)$, which is the superset of $M'$. $\square$

**3.6. Maximally connected substructures.** Since we consider canonical models, we can assume w.l.o.g. that the given SID $\Delta$ contains no disequalities (such atoms are trivially unsatisfiable or valid). We represent the set of maximally connected structures split($[A]^c_\Delta$) as a set of canonical models $[P]^c_\Gamma$, for a fresh nullary predicate $P$ and a SID $\Gamma$, whose construction is described next.

Given a qpf formula $\psi$, we define $\mathrm{conn}(\psi) \subseteq \mathrm{fv}(\psi) \times \mathrm{fv}(\psi)$ to be the least equivalence relation such that $(y, z) \in \mathrm{conn}(\psi)$ if $r(x_1, \dots, x_{\#r})$ occurs in $\psi$ and $y, z \in \{x_1, \dots, x_{\#r}\}$, for some $r \in \mathbb{R}$. Intuitively, $\mathrm{conn}(\psi)$ consists of the pairs of free variables of $\psi$ that are connected by a path (see Definition 3.22) in each canonical model of $\psi$.

Let $\mathbf{B}(y_1, \dots, y_{\#\mathbf{B}})$ be a predicate atom, $J = \{j_1, \dots, j_p\} \subseteq [1..\#\mathbf{B}]$ be a set of indices ordered as $j_1 \le \dots \le j_p$, $\xi \subseteq J \times J$ be an equivalence relation and $\mathbf{B}^\xi$ be a fresh predicate of arity $p$. In particular, $\#\mathbf{B}^\xi = 0$ if $\xi = \emptyset$ is the empty relation. We define the shorthands:

$$ \begin{align*} \mathrm{fv}_J(\mathbf{B}(y_1, \dots, y_{\#\mathbf{B}})) &\stackrel{\mathrm{def}}{=} \{y_j \mid j \in J\} & \xi(\mathbf{B}(y_1, \dots, y_{\#\mathbf{B}})) &\stackrel{\mathrm{def}}{=} \{(y_j, y_k) \mid (j, k) \in \xi\} \\ \mathbf{B}(y_1, \dots, y_{\#\mathbf{B}})/\xi &\stackrel{\mathrm{def}}{=} \mathbf{B}^\xi(y_{j_1}, \dots, y_{j_p}) \end{align*} $$
We build definitions for the predicate atoms $B^\xi(x_{j_1}, \dots, x_{j_p})$, by "narrowing" the definitions of $B(x_1, \dots, x_{\#B})$, respectively. More precisely, every structure $S \in [B^\xi(y_{j_1}, \dots, y_{j_p})]_\Delta^c$ will correspond to a set of maximally connected substructures in a structure $S' \in [B(y_1, \dots, y_{\#B})]_\Delta^c$ such that, moreover (i) for every such substructure, there exists an element associated with $y_j$, for some $j \in J$, and (ii) $y_j$ and $y_k$ are mapped to elements from the same connected substructure of $S'$ if and only if $(j, k) \in \xi$. In other words, the equivalence relation $\xi$ is used to summarize the information about the maximally connected structures from any canonical model of $B^\xi$.

We describe the construction of $\Gamma$ next. Consider a rule of $\Delta$ of the form:

$$ B_0(x_1, \dots, x_{\#B_0}) \leftarrow \exists y_1 \dots \exists y_m \cdot \psi * \ast_{i=1}^{\ell} B_i(z_{i,1}, \dots, z_{i,\#B_i}) \quad (3.1) $$

formulæ $\psi'$, $\psi''$, sets $J_i \uplus \bar{J}_i = [1..\#B_i]$, equivalence relations $\xi_i \subseteq J_i \times J_i$, for all $i \in [1..\ell]$, an equivalence relation $\Xi \subseteq (\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_m\}) \times (\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_m\})$, such that the following hold:

(1) $\psi = \psi' * \psi''$ modulo a reordering of atoms, such that $\mathrm{fv}(\psi') \cap \mathrm{fv}(\psi'') = \emptyset$,

(2) $\mathrm{fv}_{J_i}(B_i(z_{i,1}, \dots, z_{i,\#B_i})) \cap \mathrm{fv}(\psi'') = \emptyset$ and $\mathrm{fv}_{\bar{J}_i}(B_i(z_{i,1}, \dots, z_{i,\#B_i})) \cap \mathrm{fv}(\psi') = \emptyset$, for all $i \in [1..\ell]$,

(3) $\Xi = (\mathrm{conn}(\psi') \cup \bigcup_{i=1}^\ell \xi_i (B_i(z_{i,1}, \dots, z_{i,\#B_i})))^=$.

Intuitively, the conditions (1)–(3) above guarantee that the models of $B_i(z_{i,1}, \dots, z_{i,\#B_i})/\xi_i$ (recall, these are sets of maximally connected structures) compose with a model of $\psi'$ without losing neither connectivity nor maximality, in the context of the rule (3.1). At this point, we distinguish two cases:

▷ If there exist sets $J_0 \uplus \bar{J}_0 = [1..\#B_0]$, $J_0 \neq \emptyset$ and an equivalence relation $\xi_0 \subseteq J_0 \times J_0$, such that:

(4) $\mathrm{fv}_{J_0}(B_0(x_1, \dots, x_{\#B_0})) \cap \mathrm{fv}(\psi'') = \emptyset$ and $\mathrm{fv}_{\bar{J}_0}(B_0(x_1, \dots, x_{\#B_0})) \cap \mathrm{fv}(\psi') = \emptyset$,

(5) $\mathrm{fv}_{J_0}(B_0(x_1, \dots, x_{\#B_0})) \cap \mathrm{fv}_{\bar{J}_i}(B_i(z_{i,1}, \dots, z_{i,\#B_i})) = \emptyset$ and $\mathrm{fv}_{\bar{J}_0}(B_0(x_1, \dots, x_{\#B_0})) \cap \mathrm{fv}_{J_i}(B_i(z_{i,1}, \dots, z_{i,\#B_i})) = \emptyset$, for all $i \in [1..\ell]$,

(6) for all $y \in (\mathrm{fv}(\psi') \cup \bigcup_{i=1}^\ell \mathrm{fv}_{J_i}(B_i(z_{i,1}, \dots, z_{i,\#B_i}))) \cap \{y_1, \dots, y_m\}$ there exists $x \in \mathrm{fv}_{J_0}(B_0(x_1, \dots, x_{\#B_0}))$, such that $(x, y) \in \Xi$,

(7) $\xi_0(B_0(x_1, \dots, x_{\#B_0})) = \exists_{\{x_1, \dots, x_{\#B_0}\}} \cup \{(x, x) \mid x \in \mathrm{fv}_{J_0}(B_0(x_1, \dots, x_{\#B_0}))\}$

then we add to $\Gamma$ the following rule:

$$ B_0(x_1, \dots, x_{\#B_0})/\xi_0 \leftarrow \exists y_1 \dots \exists y_m \cdot \psi' * \ast_{i \in [1..\ell], J_i \neq \emptyset} B_i(z_{i,1}, \dots, z_{i,\#B_i})/\xi_i \quad (3.2) $$

Intuitively, the conditions (4)–(7) identify the set $J_0$ and the equivalence relation $\xi_0$ for which the result of the composition becomes a model of $B_0(x_1, \dots, x_{\#B_0})/\xi_0$. Altogether, these lead to the definition of the rules of the form 3.2 which propagate the construction of maximally connected structures in $\Gamma$.

▷ If (8) $\Xi$ defines an unique equivalence class, and (9) $(x, x) \notin \Xi$ for all $x \in \{x_1, \dots, x_{\#B_0}\}$ then we add to $\Gamma$ the following rule:

$$ P \leftarrow \exists y_1 \dots \exists y_m \cdot \psi' * \ast_{i \in [1..\ell], J_i \neq \emptyset} B_i(z_{i,1}, \dots, z_{i,\#B_i})/\xi_i \quad (3.3) $$

Intuitively, conditions (8)–(9) in addition to (1)–(3), ensure that by composing the models of $B_i(z_{i,1}, \dots, z_{i,\#B_i})/\xi_i$ with a model of $\psi'$ we obtain a single maximally connected structure in the context of the rule (3.1), which is moreover not referred by any of the parameters of $B_0$. Henceforth, the result of this composition is actually a model of $\mathrm{split}([A]^c_\Delta)$ and consequently is added as a model of $P$ by the rules of the form 3.3.
Recall that $\Delta$ was assumed to be equality-free (Definition 2.5) and all-satisfiable for A (Definition 2.8). Moreover, we assume that every predicate defined by a rule of $\Delta$ occurs on some complete $\Delta$-unfolding of A. Obviously, the rules that do not meet this requirement can be removed from $\Delta$ without changing $\llbracket A \rrbracket_{\Delta}^c$. The following lemma shows that the set of canonical $\Gamma$-models of P is a correct representation of the set of canonical $\Delta$-models of A:

**Lemma 3.31.** For each equality-free SID $\Delta$, which is all-satisfiable for a nullary predicate symbol A, one can effectively build a SID $\Gamma$ and a nullary predicate P, such that $\text{split}(\llbracket A \rrbracket_{\Delta}^c) = \llbracket P \rrbracket_{\Gamma}^c$.

*Proof.* For space reasons, this proof is given in subsection B.2. □

**3.7. Color abstractions of canonical models.** We compute the $k$-multiset color abstraction $(\llbracket P \rrbracket_{\Gamma}^c)^{\sharp k}$ by a least fixpoint iteration in a finite abstract domain, defined directly from the rules in the SID. The elements of the domain are composed of the colors of parameter values and the $k$-multiset color abstraction of the elements not referenced by parameters.

A $k$-bounded color triple $\langle X, c, M \rangle$ consists of a finite set of variables $X \subseteq \mathbb{V}$, a mapping $c: X \to \mathbb{C}$, and a multiset $M \in \text{mpow}(\mathbb{C})$, such that $\text{card}(M) \le k$. Since $X$ and $\mathbb{R}$ are finite, there are finitely many color triples. The following operations on color triples are lifted to sets, as usual:

**$k$-composition:** $\langle X_1, c_1, M_1 \rangle \bullet^{\sharp k} \langle X_2, c_2, M_2 \rangle \stackrel{\text{def}}{=} $

$$ \{ \langle X_1 \cup X_2, c_{12}, M_{12} \rangle \mid \begin{array}{l} c_{12}(x) = c_1(x) \lor c_2(x), \text{ for all } x \in X_1 \cap X_2, \\ c_{12}(x) = c_i(x) \text{ for all } x \in X_i \setminus X_{3-i}, \text{ for all } i \in \{1, 2\}, \\ M_{12} \subseteq M_1 \cup M_2, \text{ card}(M_{12}) \le k \end{array} \} $$

This operation is undefined, if $c_1(x) \cap c_2(x) \neq \emptyset$, for some $x \in X_1 \cap X_2$.

**substitution:** $\langle X, c, M \rangle[s] \stackrel{\text{def}}{=} \langle Y, c \circ s, M \rangle$, for any bijection $s: Y \to X$

**$k$-projection:** $(X, c, M)|_{Y}^{\sharp k} \stackrel{\text{def}}{=} \{\langle Y, c|_{Y}, M' \rangle \mid M' \subseteq M \cup \{c(x) \mid x \in X \setminus Y\}, \text{card}(M') \le k\}$, for $Y \subseteq X$.

For a qpf formula $\psi$, let $\gamma(\psi) \stackrel{\text{def}}{=} \langle \text{fv}(\psi), \lambda x \in \text{fv}(\psi) \mid \{r \in \mathbb{R} \mid r(x, \dots, x) \text{ occurs in } \psi\}, \emptyset \rangle$. Given a predicate B, we denote by $\langle B \rangle_{\Gamma}^{\sharp k}$ the least sets of $k$-bounded color triples over the variables $x_1, \dots, x_{\#B}$, the satisfies the following constraints:

$$ \langle B_0 \rangle_{\Gamma}^{\sharp k} \supseteq (\gamma(\psi) \bullet^{\sharp k} \bullet^{\sharp k} \underset{i \in [1..\ell]}{\cup} \langle B_i \rangle_{\Gamma}^{\sharp k} [x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}]) \mid_{\{x_1, \dots, x_{\#B_0}\}}^{\sharp k} \quad (3.4) $$

one for each rule of $\Gamma$ of the form (3.1). Note that the operations on sets of color triples are monotonic and the sets thereof are finite, since the arity of predicates is finite and $k$ is fixed. Henceforth, the least solution can be computed in finite time by an ascending Kleene iteration. For a $n$-ary relation $R$, we denote by $\pi_k(R)$ the set of elements that occur on the $k$-th position in a tuple from $R$.

**Lemma 3.32.** $(\llbracket P \rrbracket_{\Gamma}^{c})^{\sharp k} = \pi_3(\langle P \rangle_{\Gamma}^{\sharp k})$, for any $k \ge 1$, SID $\Gamma$ and nullary predicate P.

*Proof.* For space reasons, this proof is given in subsection B.3. □
**3.8. The expandable treewidth boundedness problem.** We end this section with a proof of decidability for the treewidth boundedness problem of the sets of $\Delta$-models of a nullary predicate $A$, provided that $\Delta$ is an expandable SID (see Definition 3.8). In case such a bound exists, we provide the optimal upper bound, in terms of the input SID $\Delta$. We recall that $\maxVars(\Delta)$ is the maximum number of variables that occur, either free or bound by an existential quantifier, in some rule from $\Delta$ (Lemma 3.2).

**Theorem 3.33.** There exists an algorithm that decides, for each expandable SID $\Delta$ and nullary predicate $A$, whether the set $[[A]]_\Delta$ has bounded treewidth. If, moreover, this is the case then $\text{tw}([[[A]]_\Delta]) \le \maxVars(\Delta)$.

*Proof.* Because $\Delta$ is expandable, by Lemma 3.12 and Lemma 3.26, $[[A]]_\Delta$ is treewidth bounded iff $\text{EF}^*([[[A]]_\Delta]^c)$ is treewidth bounded. By Lemma 3.25, $\text{EF}^*([[[A]]_\Delta]^c)$ is treewidth bounded iff $\{[C_1, C_1, C_1]\}, \{[C_2, C_2, C_2]\} \in (\text{EF}^*(\text{split}([[[A]]_\Delta])))^{\#3} \Rightarrow C_1 \cap C_2 \ne \emptyset$, for all $C_1, C_2 \in \mathbb{C}$. The latter condition can be effectively checked by computing the finite set $(\text{EF}^*(\text{split}([[[A]]_\Delta])))^{\#3}$. By Lemma 3.28 and Lemma 3.30, we have $(\text{EF}^*(\text{split}([[[A]]_\Delta])))^{\#3} = \text{ef}_1^{\#k^*}(\text{split}([[[A]]_\Delta])^{\#k})$. By Lemma 3.31, one can effectively build a SID $\Gamma$ and a nullary predicate $P$, such that $\text{split}([[[A]]_\Delta]) = [[P]]_\Gamma$. Moreover, by Lemma 3.32, we obtain $([[[P]]_\Gamma]^{\#3} = \pi_3(\langle P \rangle_\Gamma^{\#3})$, hence $(\text{EF}^*(\text{split}([[[A]]_\Delta])))^{\#3} = \pi_3(\langle P \rangle_\Gamma^{\#3})$, which is effectively computable by an ascending Kleene iteration in the finite domain of 3-bounded color triples.

For the upper bound, since $[[A]]_\Delta \subseteq \text{IEF}^*([[[A]]_\Delta]^c)$ (Lemma 3.6), we have $\text{tw}([[[A]]_\Delta]) \le \text{tw}(\text{IEF}^*([[[A]]_\Delta]))$. By Lemma 3.21, $\text{tw}([[[A]]_\Delta]) \le \text{tw}([[[A]]_\Delta]^c) + 1$ and, by Lemma 3.2, we obtain $\text{tw}([[[A]]_\Delta]) \le \maxVars(\Delta)$. $\square$

The bound given by Theorem 3.33 is optimal, as shown by the following example:

**Example 3.34.** Let us consider the following SID:

$$ \Delta = \begin{cases} A \leftarrow \exists y_1 \exists y_2 . \mathbf{a}(y_1) * \mathbf{e}(y_1, y_2) * A \\ A \leftarrow \text{emp} \end{cases} $$

This SID is expandable for $A$, because any canonical $\Delta$-model $S = (U, \sigma)$ of $A$ consists of a set of pairs $(u_1, u_2) \in \sigma(\mathbf{e})$, such that $u_1 \in \sigma(\mathbf{a})$ and $u_2 \notin \sigma(\mathbf{a})$. Hence, any sequence of canonical $\Delta$-models of $A$ can be embedded as substructures in a canonical $\Delta$-model of $A$. Moreover, $\maxVars(\Delta) = 2$ and any cyclic list of $\mathbf{e}$-related adjacent elements labeled by $\mathbf{a}$ is a $\Delta$-model of $A$ of treewidth 2.

## 4. THE REDUCTION TO EXPANDABLE SETS OF INDUCTIVE DEFINITIONS

This section completes the proof of decidability of the treewidth boundedness problem $\text{TWB}^{\text{SLR}}$, by showing a reduction to the decidable treewidth boundedness problem for expandable SIDs (Theorem 3.33). Moreover, an analysis of this reduction allows to compute upper bounds on the treewidth of the set of models of an SLR sentence, provided that such a bound exists. The core of the reduction is the following lemma:

**Lemma 4.1.** Let $\Delta$ be a SID and $A$ be a nullary predicate. Then, one can build finitely many SIDs $\Gamma_1, \dots, \Gamma_n$, that are expandable for a nullary predicate $B$, such that $[[A]]_\Delta$ is treewidth bounded iff each $[[B]]_{\Gamma_i}$ is treewidth bounded, for $i \in [1..n]$.
The rest of this section is concerned with the proof of this lemma. For technical reasons, the construction of expandable SIDs with an equivalent treewidth boundedness problem uses a representation of the SID as a tree automaton (subsection 4.1). This representation allows to distinguish the purely structural aspects, related to the dependencies between rules, from details related to the flow of parameters. An important class of automata distinguish between the so-called 1-transitions, that occur exactly once, from the $\infty$-transitions, that may occur any number of times on an accepting run. These automata are called choice-free (Definition 4.5). Each automaton admits a finite choice-free decomposition that preserves its language (Lemma 4.9).

Next, we consider tree automata whose alphabets are finite sets of qpf formulæ (subsection 4.2). The trees recognized by these automata are representations of the predicate-free formulæ produced by the complete $\Delta$-unfoldings of A. Since we assume that $\Delta$ is all-satisfiable for A (Definition 2.8), each accepting run of an automaton “produces” a canonical $\Delta$-model of A (Lemma 4.13).

Furthermore, we define *persistent variables*, whose values are carried along each sequence of $\infty$-transitions of a choice-free automaton (Definition 4.14). Identifying and removing the persistent variables from a choice-free automaton with an alphabet of qpf formulæ constitutes an important ingredient of the construction, because of point (3) of Definition 3.8, that requires the embedded canonical models of an expandable SID to be placed sufficiently far away one from another. In particular, this guarantees that the coloring (Definition 3.13) of an element from an embedded substructure does not change in the larger structure. The effective transformation of a choice-free automaton over an alphabet of qpf formulæ into an automaton without persistent variables is described in subsection 4.4. This transformation does not preserve the language, nor the set of models corresponding to the trees recognized by the automaton, but is shown to preserve the existence of a (computable) bound on the treewidths of these models.

**Tree Automata.** Let $\mathbb{A}$ be a *ranked alphabet*, each symbol $a \in \mathbb{A}$ having an associated integer $\operatorname{rank} \rho(a) \ge 0$. The elements of $\mathbb{N}_+^*$ are finite sequences of strictly positive natural numbers, called *positions*. We write $pq$ for the concatenation of $p, q \in \mathbb{N}^*$ and $q \cdot P \stackrel{\text{def}}{=} \{qp \mid p \in P\}$, for $P \subseteq \mathbb{N}^*$. A *ranked tree* is a finite partial function $t : \mathbb{N}^* \to \mathbb{A}$, such that the set $\operatorname{dom}(t)$ is *prefix-closed*, i.e., for each $p \in \operatorname{dom}(t)$, if $q$ is a prefix of $p$, then $q \in \operatorname{dom}(t)$, and *sibling-closed*, i.e., $\{i \in \mathbb{N} \mid pi \in \operatorname{dom}(t)\} = \{1, \dots, \rho(t(p))\}$, for all $p \in \operatorname{dom}(t)$. The *frontier* of $t$ is the set $\operatorname{fr}(t) \stackrel{\text{def}}{=} \{p \in \operatorname{dom}(t) \mid p1 \notin \operatorname{dom}(t)\}$. We denote by $t|_p$ the subtree of $t$ at position $p \in \operatorname{dom}(t)$ i.e., $t|_p$ is the tree such that $\operatorname{dom}(t|_p) = \{q \in \mathbb{N}^* \mid pq \in \operatorname{dom}(t)\}$ and $t|_p(q) = t(pq)$, for each $q \in \operatorname{dom}(t|_p)$. A tree $u$ is *embedded in t at position* $p \in \operatorname{dom}(t)$ iff $pq \in \operatorname{dom}(t)$ and $u(q) = t(pq)$, for each $q \in \operatorname{dom}(u)$.

**Definition 4.2.** An $(\mathbb{A}$-labeled tree) automaton is $\mathcal{A} = (\mathbb{A}, \mathcal{Q}, \mathcal{I}, \delta)$, where $\mathcal{Q}$ is a finite set of states, $\mathcal{I} \subseteq \mathcal{Q}$ is a set of initial states (if $\mathcal{I}$ is a singleton, we denote it by $\iota \in \mathcal{Q}$), $\delta$ is a finite set of transitions $\tau : q_0 \xrightarrow{a} (q_1, \dots, q_{\rho(a)})$. For a transition $\tau : q_0 \xrightarrow{a} (q_1, \dots, q_\ell) \in \delta$, let $\bullet\tau \stackrel{\text{def}}{=} q_0$ be the source and $\tau \stackrel{\text{def}}{=} \{q_1, \dots, q_\ell\}$ the multiset of targets of $\tau$. For a set of transitions $T \subseteq \delta$, let $\bullet T \stackrel{\text{def}}{=} \{\bullet\tau \mid \tau \in T\}$ and $T \stackrel{\text{def}}{=} \bigcup_{\tau \in T} \bullet\tau$. For a set of states $S \subseteq \mathcal{Q}$, let $\bullet S \stackrel{\text{def}}{=} \{\tau \mid \bullet\tau \notin S, \tau \bullet \cap S \neq \emptyset\}$, $S \stackrel{\text{def}}{=} \{\tau \mid \bullet\tau \in S, \tau \bullet \cap S = \emptyset\}$ and $\bullet S \stackrel{\text{def}}{=} \{\tau \mid \bullet\tau \in S, \tau \bullet \cap S \neq \emptyset\}$.

The following notions concern the structure of automata. The relation $\rightsquigarrow \subseteq \mathcal{Q} \times \mathcal{Q}$ is defined as $q \rightsquigarrow q'$ iff there exists $\tau \in \delta$ such that $q = \bullet\tau$ and $q' \in \tau\bullet$. A *strongly connected*
component (SCC) is a maximal set $S \subseteq \mathcal{Q}$, such that $q \rightsquigarrow^* q'$, for all $q, q' \in S$. An SCC $S$ is nonlinear iff there exists a transition $\tau \in \bullet S^\bullet$ such that $\text{card}(\tau^\bullet \cap S) \ge 2$ and linear otherwise. The SCC graph of $\mathcal{A}$ is the directed graph $\mathcal{G}_\mathcal{A} \stackrel{\text{def}}{=} (\mathcal{N}, \mathcal{E})$, where $\mathcal{N}$ is the set of SCCs of $\mathcal{A}$ and $(S, S') \in \mathcal{E}$ iff $S \neq S'$ and there exists $q \in S$ and $q' \in S'$, such that $q \rightsquigarrow q'$, for all $S, S' \in \mathcal{N}$. We write $\mathcal{G}_\mathcal{A} = (\mathcal{N}, \mathcal{E}, S)$ if $\mathcal{G}_\mathcal{A}$ is a tree with root $S \in \mathcal{N}$.

The execution of automata is defined next. A run $\theta$ of $\mathcal{A}$ over a ranked tree $t$ is a tree $\theta: \text{dom}(t) \to \mathcal{Q}$ such that $\theta(p) \xrightarrow{t(p)} (\theta(p1), \dots, \theta(p\ell)) \in \delta$, for all $p \in \text{dom}(t)$, where $\ell = \rho(t(p))$. Note that the frontier of a run is labeled by states $q$ such that there exists a transition $q \xrightarrow{\alpha} () \in \delta$, in analogy to the final states of a word automaton. A weaker notion is that of *partial* runs, where the previous condition holds for $\text{dom}(t) \setminus \text{fr}(t)$, instead of the entire $\text{dom}(t)$. A run $\theta$ is *accepting* if $\theta(\epsilon) \in \mathcal{I}$. The language of $\mathcal{A}$ is $\mathcal{L}(\mathcal{A}) \stackrel{\text{def}}{=} \bigcup_{q \in \mathcal{I}} \mathcal{L}_q(\mathcal{A})$, where $\mathcal{L}_q(\mathcal{A}) \stackrel{\text{def}}{=} \{t \mid \mathcal{A} \text{ has a run } \theta \text{ over } t \text{ and } \theta(\epsilon) = q\}$.

An automaton is *rooted* iff $\mathcal{I} = \{\iota\}$ and $\iota \notin \delta^\bullet$. For an automaton $\mathcal{A}$ one can build finitely many rooted automata $\mathcal{A}_1, \dots, \mathcal{A}_n$ such that $\mathcal{L}(\mathcal{A}) = \bigcup_{i=1}^n \mathcal{L}(\mathcal{A}_i)$. A rooted automaton $\mathcal{A}$ is *trim* iff $\iota \rightsquigarrow^* q$ and $\mathcal{L}_q(\mathcal{A}) \neq \emptyset$, for each state $q \in \mathcal{Q}$. Each automaton with non-empty language can be transformed into a trim one with the same language, by a simple marking algorithm. We use the following notions of *simulation* and *refinement* between automata:

**Definition 4.3.** Let $\mathcal{A} = (\mathcal{A}, \mathcal{Q}_\mathcal{A}, \iota_\mathcal{A}, \delta_\mathcal{A})$ and $\mathcal{B} = (\mathcal{A}, \mathcal{Q}_\mathcal{B}, \iota_\mathcal{B}, \delta_\mathcal{B})$ be automata. A mapping $h: \mathcal{Q}_\mathcal{A} \to \mathcal{Q}_\mathcal{B}$ is a *simulation* if and only if the following hold:

(1) $h(\iota_\mathcal{A}) = \iota_\mathcal{B}$ and

(2) $q_0 \xrightarrow{a} (q_1, \dots, q_\ell) \in \delta_\mathcal{A}$ only if $h(q_0) \xrightarrow{a} (h(q_1), \dots, h(q_\ell)) \in \delta_\mathcal{B}$, for all $q_0, \dots, q_\ell \in \mathcal{Q}_\mathcal{A}$.
A simulation $h$ is a *refinement* if and only if, moreover:

(3) $q_0 \xrightarrow{a} (q'_1, \dots, q'_\ell) \in \delta_\mathcal{B}$ only if there exist $q_0 \in h^{-1}(q'_0), \dots, q_\ell \in h^{-1}(q'_\ell)$, such that $q_0 \xrightarrow{a} (q_1, \dots, q_\ell) \in \delta_\mathcal{A}$, for all $q_0 \in \mathcal{Q}_\mathcal{A}$ and $q'_1, \dots, q'_\ell \in \mathcal{Q}_\mathcal{B}$.

If $h: \mathcal{Q}_\mathcal{A} \to \mathcal{Q}_\mathcal{B}$ is a simulation then $\mathcal{B}$ simulates $\mathcal{A}$. If $h$ is a refinement then $\mathcal{A}$ refines $\mathcal{B}$.

The key properties of simulations and refinements are stated and proved below:

**Lemma 4.4.** If $\mathcal{B}$ simulates $\mathcal{A}$ then $\mathcal{L}(\mathcal{A}) \subseteq \mathcal{L}(\mathcal{B})$. If $\mathcal{A}$ is a refinement of $\mathcal{B}$ then $\mathcal{L}(\mathcal{A}) = \mathcal{L}(\mathcal{B})$.

*Proof.* Let $\mathcal{A} = (\mathcal{A}, \mathcal{Q}_\mathcal{A}, \iota_\mathcal{A}, \delta_\mathcal{A})$, $\mathcal{B} = (\mathcal{A}, \mathcal{Q}_\mathcal{B}, \iota_\mathcal{B}, \delta_\mathcal{B})$ and $h: \mathcal{Q}_\mathcal{A} \to \mathcal{Q}_\mathcal{B}$ be a mapping. "$\subseteq$" Assume that $h$ is a simulation. Let $t \in \mathcal{L}(\mathcal{A})$ be a tree and $\theta$ be an accepting run of $\mathcal{A}$ over $t$. Then one shows that $h \circ \theta$ is an accepting run of $\mathcal{B}$ over $t$, by induction on $t$, using points (1) and (2) of Definition 4.3. "$\supseteq$" Assume that $h$ is a refinement. Let $t \in \mathcal{L}(\mathcal{B})$ be a tree and $\theta$ be an accepting run of $\mathcal{B}$ over $t$. We build an accepting run of $\mathcal{A}$ over $t$ by induction on $t$, using points (1) and (3) of Definition 4.3. $\square$

The following structural property of automata is key for building expandable SIDs:

**Definition 4.5.** An automaton $\mathcal{A} = (\mathcal{A}, \mathcal{Q}, \iota, \delta)$ is *choice-free* iff the following hold:

(1) the SCC graph of $\mathcal{A}$ is a tree $\mathcal{G}_\mathcal{A} = (\mathcal{N}, \mathcal{E}, S_0)$, where $\bullet S = \{\tau\}$ and $\text{card}(\tau^\bullet \cap S) = 1$, for all $S \in \mathcal{N} \setminus \{S_0\}$, i.e., any non-root SCC is entered by one branch of a single transition,

(2) there exists a mapping $\Lambda: \mathcal{N} \cup \delta \to \{1, \infty\}$ such that:

(a) for all $S \in \mathcal{N}$, if $S$ is linear and $\Lambda(S) = 1$ then $\text{card}(S^\bullet) = 1$.

(b) for all $\tau \in \delta$, $\Lambda(\tau) = 1$ iff $\tau \in S^\bullet$, for some linear $S \in \mathcal{N}$ such that $\Lambda(S) = 1$,

(c) for all $S \in \mathcal{N}$, $\Lambda(S) = 1$ iff $S = S_0$ or $\bullet S = \{\tau\}$, for some $\tau \in \delta$ such that $\Lambda(\tau) = 1$.
<figure><img src="image_13.png" /><figcaption>Figure 10: A choice-free tree automaton and its non-choice-free extension</figcaption></figure>

Let $\delta = \delta^1 \uplus \delta^\infty$, where $\delta^k \stackrel{\text{def}}{=} \{\tau \in \delta \mid \Lambda(\tau) = k\}$ and $k \in \{1, \infty\}$, be the partition of the set of transitions induced by the mapping $\Lambda$. A state $q \in (\delta^1)^{\bullet} \cap {\bullet}(\delta^\infty)$ is called a *pivot state*. Let $\mathcal{R}_q^\infty(\mathcal{A})$ denote the set of partial runs $\theta$ of $\mathcal{A}$, such that $\theta(\epsilon) = q$ and for all $p \in \text{dom}(\theta) \setminus \text{fr}(\theta)$, there exists $a \in \mathcal{A}$ such that $\theta(p) \xrightarrow{a} (\theta(p1), \dots, \theta(pn)) \in \delta^\infty$.

Intuitively, the structure of choice-free automata allows them to traverse a unique sequence of linear SCCs, before entering a non-linear SCC. Note that the labeling $\Lambda$ of SCCs and transitions from Definition 4.5 is unique, because the SCC graph of a choice-free automaton is a tree whose root is a 1-SCC, and $\Lambda$ is determined by the linearity of the SCCs in this tree. Hence, the partition of the transitions of a choice-free automaton into 1- and $\infty$-transitions is unambiguous.

**Example 4.6.** The automaton from Figure 10 is choice free. The linear (resp. nonlinear) SCCs are labeled by L (resp. NL). The labeling of transitions and SCCs, resp. the SCC graph by $\Lambda$ are represented in Figure 10 (resp. right). The choice-freeness is violated by adding the transitions $q_0 \xrightarrow{b} (q_5)$ and $q_5 \xrightarrow{c} ()$ (in red), because the linear SCC $\{q_0\}$ is labeled with 1 and has two outgoing transitions, thus contradicting point (2a) of Definition 4.5 (the additional transitions are not labeled).

The transitions from $\delta^1$, called 1-transitions, are used to move from one linear SCC to another, hence all of them occur exactly once on each accepting run:

**Lemma 4.7.** Let $\mathcal{A} = (\mathcal{A}, \mathcal{Q}, \iota, \delta)$ be a choice-free automaton, such that $\delta = \delta^1 \uplus \delta^\infty$ (Definition 4.5) and let $\theta$ be an accepting run of $\mathcal{A}$ over a tree $t$. Then, for each 1-transition $q_0 \xrightarrow{a} (q_1, \dots, q_\ell) \in \delta^1$ there exists exactly one position $p \in \text{dom}(\theta)$, such that $\theta(p) = q_0$, $t(p) = a$ and $\theta(pi) = q_i$, for all $i \in [1..\ell]$.

*Proof.* For space reasons, the proof of this lemma is given in subsection C.1. $\square$

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

The transitions from $\delta^\infty$, called $\infty$-transitions, can be applied any number of times on some accepting run. This fact occurs as an easy consequence of the lemma below:

**Lemma 4.8.** Let $\mathcal{A} = (\mathcal{A}, \mathcal{Q}, \iota, \delta)$ be a choice-free automaton, where $\delta = \delta^1 \uplus \delta^\infty$ (Definition 4.5). Then, for any state $q \in {\bullet}(\delta^\infty)$ there exists a pivot state $q_0 \in (\delta^1)^{\bullet} \cap {\bullet}(\delta^\infty)$ and a partial run $\theta_0 \in \mathcal{R}_{q_0}^\infty(\mathcal{A})$ consisting only of $\infty$-transitions, such that $\theta_0(p) = q$ for some $p \in \text{fr}(\theta_0)$ and either:

(1) $\{q, q_0\} \subseteq \{\theta_0(p) \mid p \in \text{fr}(\theta_0)\}$, i.e., if $q = q_0$ then $q$ occurs twice on $\text{fr}(\theta_0)$, or

(2) each partial run $\theta \in \mathcal{R}_q^\infty(\mathcal{A})$ can be extended to a partial run $\theta' \in \mathcal{R}_q^\infty(\mathcal{A})$ such that $q_0$ occurs on the frontier of $\theta'$.

*Proof.* For space reasons, the proof of this lemma is given in subsection C.2. $\square$

<figure><img src="image_15.png" /></figure>
Moreover, any automaton can be decomposed into finitely many choice-free automata:

**Lemma 4.9.** Given an automaton $\mathcal{A} = (\mathcal{A}, \mathcal{Q}, \iota, \delta)$, one can build finitely many choice-free automata $\mathcal{A}_i = (\mathcal{A}, \mathcal{Q}_i, \iota_i, \delta_i)$, for $i \in [1..n]$, such that $\mathcal{L}(\mathcal{A}) = \bigcup_{i=1}^n \mathcal{L}(\mathcal{A}_i)$ and, moreover, $\text{card}(\delta_i^1) \le \max(\text{card}(\mathcal{Q}), \max\{\rho(a) \mid a \in \mathcal{A}\}^{\text{card}(\mathcal{Q})})$, for all $i \in [1..n]$.

*Proof.* For space reasons, the proof of this lemma is given in subsection C.3. □

**Example 4.10.** The choice-free decomposition of the automaton $\mathcal{A}$ from Figure 10 consists of the following choice-free automata, with transitions labeled according to Definition 4.5:

$$ \mathcal{A}_1 = \left\{ \begin{array}{ll} q_0 \xrightarrow{a} (q_0, q_1) & (\infty) \\ q_1 \xrightarrow{b} (q_1) & (\infty) \\ q_1 \xrightarrow{c} () & (\infty) \\ q_0 \xrightarrow{b} (q_2) & (1) \\ q_2 \xrightarrow{a} (q_2, q_2) & (\infty) \\ q_2 \xrightarrow{b} (q_3) & (\infty) \\ q_2 \xrightarrow{b} (q_4) & (\infty) \\ q_3 \xrightarrow{c} () & (\infty) \\ q_4 \xrightarrow{c} () & (\infty) \end{array} \right. \quad \mathcal{A}_2 = \left\{ \begin{array}{ll} q_0 \xrightarrow{a} (q_0, q_1) & (\infty) \\ q_1 \xrightarrow{b} (q_1) & (\infty) \\ q_1 \xrightarrow{c} () & (\infty) \\ q_0 \xrightarrow{b} (q_5) & (1) \\ q_5 \xrightarrow{c} () & (1) \end{array} \right. $$

It can be seen that $\mathcal{L}_{q_0}(\mathcal{A}) = \mathcal{L}_{q_0}(\mathcal{A}_1) \cup \mathcal{L}_{q_0}(\mathcal{A}_2)$ because $\mathcal{A}$ has the choice in $q_0$ between taking the transition $q_0 \xrightarrow{b} (q_2)$ or $q_0 \xrightarrow{b} (q_5)$. Since these transitions occur at most once in each accepting run of $\mathcal{A}$, the choice-free decomposition of $\mathcal{A}$ produces two automata in which each such transition occurs exactly once on each accepting run.

**4.2. Automata with Alphabets of Formulæ.** The construction of the expandable SIDs from Lemma 4.1 uses automata that recognize trees labeled with qpf formulæ taken from a finite set. We recall that every model of a sentence is defined by a complete unfolding that replaces the predicate atoms with corresponding definitions, recursively. The steps of these unfoldings can be placed into a tree labeled with predicate-free formulæ from an alphabet $\Sigma$, reflecting the partial order in which the rules from the SID are applied. These unfolding trees form the language of an automaton defined directly from the syntax of the SID. Dually, from any $\Sigma$-labeled automaton one can build a SID whose unfolding trees form the language of the automaton.

**Definition 4.11.** Let $\Sigma$ be the set of qpf formulæ $\alpha$ of rank $\rho(\alpha) = \ell$, such that:

(1) $\text{fv}(\alpha) \subseteq \{x_1^{[\epsilon]}, \dots, x_{n_0}^{[\epsilon]}\} \cup \{y_1^{[\epsilon]}, \dots, y_m^{[\epsilon]}\} \cup \bigcup_{i=1}^{\ell} \{x_1^{[i]}, \dots, x_{n_i}^{[i]}\}$, for some $m, n_0, \dots, n_\ell \in \mathbb{N}$; a variable $x_j^{[i]}$ is called a $i$-variable, for all $i \in \{\epsilon\} \cup [1..\ell]$,

(2) $x_j^{[i]} \not\approx_{\alpha} x_k^{[i]}$, for all $i \in [1..\ell]$ and $1 \le j < k \le n_i$.

The characteristic formula of a $\Sigma$-labeled tree $t$ is the qpf formula $\Theta(t) \stackrel{\text{def}}{=} *_{p \in \text{dom}(t)} t(p)^{[p]}$, where the formulæ $t(p)^{[p]}$ are obtained from $t(p) \in \Sigma$ by replacing each occurrence of a variable $x^{[q]}$ by $x^{[pq]}$, for all $p \in \text{dom}(t)$.

Given a SID $\Delta$, the $\Sigma$-labeled automaton $\mathcal{A}_{\Delta, \mathcal{A}} \stackrel{\text{def}}{=} (\Sigma, \mathcal{Q}_{\Delta}, q_{\mathcal{A}}, \delta_{\Delta})$ is defined as follows:

▷ $\mathcal{Q}_{\Delta}$ contains states $q_{\mathcal{B}}$, where $\mathcal{B}$ is a predicate occurring in $\Delta$; each state has an associated
arity $\#q_{\mathcal{B}} \stackrel{\text{def}}{=} \#\mathcal{B}$,
▷ $\delta_\Delta$ contains a transition $q_{A_0} \xrightarrow{\alpha_\rho} (q_{A_1}, \dots, q_{A_\ell})$, where $\alpha_\rho$ is the symbol:

$$ \alpha_{\rho} \stackrel{\text{def}}{=} \psi[x_1/x_1^{[\epsilon]}, \dots, x_{n_0}/x_{n_0}^{[\epsilon]}, y_1/y_1^{[\epsilon]}, \dots, y_m/y_m^{[\epsilon]}] * \v{a}_{i=1}^{\ell} * \v{a}_{j=1}^{n_i} z_{i,j}^{[\epsilon]} = x_j^{[i]} $$

of rank $\rho(\alpha_\rho) = \ell$ that corresponds to the rule $\rho \in \Delta$, where $\psi$ is a qpf formula:

$$ \rho : A_0(x_1, \dots, x_{n_0}) \leftarrow \exists y_1 \dots \exists y_m . \psi * \v{a}_{i=1}^{\ell} A_i(z_{i,1}, \dots, z_{i,n_i}) $$

**Example 4.12.** Let us consider the following SID:

$$ \Delta = \left\{ \begin{array}{ll} A & \leftarrow \exists y_1 \exists y_2 \exists y_3 . B(y_1, y_2, y_3) \\ B(x_1, x_2, x_3) & \leftarrow \exists y_4 . e(x_1, x_3) * e(x_1, y_4) * B(y_4, x_2, x_3) \\ B(x_1, x_2, x_3) & \leftarrow e(x_1, x_3) * e(x_1, x_2) * e(x_2, x_3) \end{array} \right. $$

The automaton $A_{\Delta,A}$ has the following transitions:

$$ A_{\Delta,A} = \left\{ \begin{array}{ll} q_A & \xrightarrow{y_1^{[\epsilon]}=x_1^{[1]*} \ y_2^{[\epsilon]}=x_2^{[1]*} \ y_3^{[\epsilon]}=x_3^{[1]}} (q_B) \\ q_B & \xrightarrow{e(x_1^{[\epsilon]}, x_3^{[\epsilon]}) * e(x_1^{[\epsilon]}, y_4^{[\epsilon]}) * y_4^{[\epsilon]}=x_1^{[1]*} \ x_2^{[\epsilon]}=x_2^{[1]*} \ x_3^{[\epsilon]}=x_3^{[1]}} (q_B) \\ q_B & \xrightarrow{e(x_1^{[\epsilon]}, x_3^{[\epsilon]}) * e(x_1^{[\epsilon]}, x_2^{[\epsilon]}) * e(x_2^{[\epsilon]}, x_3^{[\epsilon]})} () \end{array} \right. $$

Dually, given an automaton $\mathcal{A} = (\Sigma, \mathcal{Q}, \iota, \delta)$, the SID $\Delta_{\mathcal{A}}$ consists of the following rules, one for each transition $q_0 \xrightarrow{\alpha_0} (q_1, \dots, q_\ell) \in \delta$:

$$ A_{q_0}(x_1, \dots, x_{\#q_0}) \leftarrow \exists y_1 \dots \exists y_m . \alpha[x_1^{[\epsilon]}/x_1, \dots, x_{\#q_0}^{[\epsilon]}/x_{\#q_0}] * \v{a}_{j=1}^{\ell} A_{q_j}(x_1^{[j]}, \dots, x_{\#q_j}^{[j]}) \quad (4.1) $$
$$ \text{where } \{y_1, \dots, y_m\} \stackrel{\text{def}}{=} \text{fv}(\alpha) \setminus (\{x_1^{[\epsilon]}, \dots, x_{\#q_0}^{[\epsilon]}\} \cup \bigcup_{j=1}^{\ell} \{x_1^{[j]}, \dots, x_{\#q_j}^{[j]}\}) $$

The similarity between SIDs and $\Sigma$-labeled automata (Lemma 4.13) motivates the use of similar terminology. For a $\Sigma$-labeled automaton $\mathcal{A}$, we define $[\mathcal{A}] \stackrel{\text{def}}{=} \bigcup_{t \in \mathcal{L}(\mathcal{A})} [[\Theta(t)]^\exists]$, $[\mathcal{A}]^c \stackrel{\text{def}}{=} \bigcup_{t \in \mathcal{L}(\mathcal{A})} [[\Theta(t)]^\exists]^c$ and $[\mathcal{A}]^r \stackrel{\text{def}}{=} \bigcup_{t \in \mathcal{L}(\mathcal{A})} [[\Theta(t)]^\exists]^r$. Moreover, a $\Sigma$-labeled automaton $\mathcal{A}$ is all-satisfiable if the formula $\Theta(t)$ is satisfiable, for all $t \in \mathcal{L}(\mathcal{A})$. The relation between SIDs and $\Sigma$-labeled automata is formally stated below:

**Lemma 4.13.**

(1) Given a SID $\Delta$ and a nullary predicate $A$, one can build an automaton $A_{\Delta,A}$ such that $[A]_\Delta = [A_{\Delta,A}]$. Moreover, if $\Delta$ is all-satisfiable for $A$, then $A_{\Delta,A}$ is all-satisfiable.

(2) Given an automaton $\mathcal{A} = (\Sigma, \mathcal{Q}, \iota, \delta)$, one can build a SID $\Delta_{\mathcal{A}}$, such that $[\mathcal{A}] = [A_\iota]_{\Delta_{\mathcal{A}}}$ and $[\mathcal{A}]^r = [A_\iota]_{\Delta_{\mathcal{A}}}^r$, for a nullary predicate $A$.

*Proof.* For space reasons, the proof of this lemma is given in subsection C.4. □

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

**4.3. Persistent Variables.** The second ingredient of the construction of the expandable SIDs from Lemma 4.1 are the persistent variables of a $\Sigma$-labeled choice-free automaton. These are variables introduced by the 1-transitions of the automaton, whose values propagate via equalities throughout each run of the choice-free automaton. We define persistent variables using the notion of *profile*:

**Definition 4.14.** Let $\mathcal{A} = (\Sigma, \mathcal{Q}, \iota, \delta)$ be a choice-free automaton, where $\delta = \delta^1 \uplus \delta^\infty$ (Definition 4.5). A *positional function* $\mathfrak{P}: \mathcal{Q} \to \text{pow}(\mathbb{N})$ associates each state $q$ with a set $\mathfrak{P}(q) \subseteq [1..\#q]$. The *profile* of $\mathcal{A}$ is the pointwise largest positional function $\mathfrak{P}_A$ such that, for each transition $q_0 \xrightarrow{\alpha_0} (q_1, \dots, q_\ell) \in \delta^\infty$, each $k \in [1..\ell]$ and each $r \in \mathfrak{P}_A(q_k)$, there exists
$s \in \mathfrak{P}_A(q_0)$, such that $x_s^{[\epsilon]} \approx_{\alpha} x_r^{[k]}$. A variable $x_j^{[i]}$ that occurs within the label of a transition $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in \delta$ is said to be persistent iff $j \in \mathfrak{P}_A(q_i)$, for all $i \in [0..\ell]$.

Intuitively, $\mathfrak{P}_A(q)$ is the set of indices of those variables, associated with a state, that will be equated, through a chain of equalities in the characteristic formula $\Theta(t)$, to the same variable associated with the corresponding pivot state (Lemma 4.8) in every run of $\infty$-transitions of $\mathcal{A}$ over $t$. Note that the profile is computable by a finite greatest fixpoint Kleene iteration over each SCC of the automaton (see the proof of Lemma 4.18 for an explicit statement of that fixed point).

Without loss of generality, we assume that a $\Sigma$-labeled automaton does not have trivial SCCs, i.e., consisting of a single state, with no transitions that are both outgoing and incoming to that state. The profile associated with such state $q$ would be the interval $[1..\#q]$ and any variable in the label of an incoming or outgoing transition would be unnecessarily considered persistent. The trivial SCCs of a $\Sigma$-labeled automaton can be eliminated by a pre-processing step which combines the labels of the incoming and outgoing transitions and renames the variables according to the convention (Definition 4.11).

**Example 4.15.** (continued from Example 4.12) The profile of the automaton $\mathcal{A}_{\Delta,\mathcal{A}}$, that corresponds to the SID $\Delta$ from Example 4.12 associates $q_A$ with the empty set and $q_B$ with the set $\{2,3\}$. Note that $\#q_A = 0$ and $\#q_B = 3$. The first and third transitions in Example 4.12 are 1-transitions, whereas the second transition is an $\infty$-transition. The variables $x_2^{[1]}$ and $x_3^{[1]}$ from the label of the second transition $(\infty)$ are persistent.

A context $\theta_{p \leftarrow q}$ is a partial run over a tree $t$ such that $p \in \text{fr}(\theta_{p \leftarrow q})$, $\theta_{p \leftarrow q}(p) = q$ and $\theta_{p \leftarrow q}(r) \xrightarrow{t(r)} ()$, for all $r \in \text{fr}(\theta_{p \leftarrow q}) \setminus p$, i.e., the partial run has exactly one “open” frontier position $p$ that is labeled with a state $q$. A key property of automata is that equalities between non-persistent variables vanish in contexts consisting of $\infty$-transitions only (Lemma 4.18). These contexts, called *resets*, are formally defined below:

**Definition 4.16.** A context $\theta_{p \leftarrow q} \in \mathcal{R}_q^{\infty}(\mathcal{A})$ over a tree $t$ is a $q$-reset iff (1) $x_j^{[\epsilon]} \approx_{\Theta(t)} x_j^{[p]}$, for all $j \in \mathfrak{P}_A(q)$, and (2) $x_j^{[\epsilon]} \not\approx_{\Theta(t)} x_k^{[p]}$, for all $j, k \in [1..\#q]$, such that $k \notin \mathfrak{P}_A(q)$. The path between $\epsilon$ and $p$ in $\theta_{p \leftarrow q}$ is called a *reset path*.

**Example 4.17.** (continued from Example 4.12) For instance, in the context $\theta_{1 \leftarrow q_B}$, that consists of the second transition $q_B \xrightarrow{\alpha} q_B$ of the automaton in Example 4.12, we have $x_1^{[\epsilon]} \not\approx_{\alpha} x_1^{[1]}$. Then, the value of $x_1^{[\epsilon]}$ is “forgotten” along any run that iterates this transition at least twice.

**Lemma 4.18.** Let $\mathcal{A} = (\Sigma, \mathcal{Q}, \iota, \delta)$ be a trim automaton. Then, there exists a $q$-reset for (1) each pivot state $q \in (\delta^1)^{\bullet} \cap (\bullet^{\delta^\infty})$, and (2) each state $q \in (\bullet^{\delta^1}) \cap (\bullet^{\delta^\infty})$, i.e., that is the origin of both a 1-transition and a $\infty$-transition of $\mathcal{A}$.

*Proof.* By Definition 4.14, $\mathfrak{P}_A$ is the greatest fixpoint of the monotone function $\mathcal{F}$ on the domain of positional functions $\mathfrak{P}: \mathcal{Q} \to \text{pow}(\mathbb{N})$, defined below:

$$ \mathcal{F}(\mathfrak{P}) \stackrel{\text{def}}{=} \lambda q . \bigcap_{\substack{q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in \delta^\infty \\ q=q_k \in \{q_1, \dots, q_\ell\}}} \{r \in [1..\#q_k] \mid \exists s \in \mathfrak{P}(q_0) . x_s^{[\epsilon]} \approx_{\alpha} x_r^{[k]}\} $$

Namely, we have $\mathfrak{P}_A = \mathcal{F}^i(\top) = \mathcal{F}^j(\top)$, for a sufficiently large $i \ge 1$ and any $j \ge i$, where $\top$ is the positional function $\lambda q . [1..\#q]$. Now consider the following “big-step” function $\mathcal{G}$
on the domain of positional functions:

$$
\mathcal{G}(\mathfrak{P}) \stackrel{\text{def}}{=} \lambda q . \quad \bigcap_{\substack{\theta \in \mathcal{R}_q^{\infty}(\mathcal{A}) \text{ partial run over } t \\ p \in \text{fr}(\theta), \text{ such that } \theta(p)=q}} \{r \in [1..\#q] \mid \exists s \in \mathfrak{P}(q) . x_s^{[e]} \approx_{\Theta_{(t)}} x_r^{[p]}\}
$$

We prove the following:

**Fact 4.19.** *gfp*(*F*)(*q*) = *gfp*(*G*)(*q*), for any pivot state *q* of *A*.

Proof. “⊆” Each partial run θ ∈ R ∞ q ( A ) such that θ ( p ) = q, for some p ∈ fr ( θ ) corresponds to a finite sequence of transitions from δ ∞ . “ ⊇ ” Since q is a pivot state we have q ∈ • ( δ ∞ ), thus necessarily q = q 0 , where q 0 ∈ ( δ 1 ) • is the state whose existence is stated by Lemma 4.8. Then every ∞ -transition incoming to q belongs to a partial run θ ∈ R ∞ q ( A ), such that q occurs on the frontier of θ . □

Back to the proof, we prove the two points of the statement below:

(1) Let $q$ be a pivot state of $\mathcal{A}$. By Fact 4.19, we have $\mathfrak{P}_A(q) = \mathcal{G}^i(\top)(q)$ for a sufficiently large finite integer $i \ge 0$. We show that the latter condition is equivalent to the existence of a $q$-reset $\theta_{p \leftarrow q} \in \mathcal{R}_q^\infty(\mathcal{A})$.

"<" Assume that there exists a q-reset θ ∈ R ∞ q ( A ) over some tree t . Then G ( ⊤ )( q ) = { j ∈ [1..#q] | ∃ k ∈ [1..#q] . x$_{j}$ [ e ] ≈$_{Θ}$$_{(}$$_{t}$$_{)}$ x$_{k}$ [ p ] } = P$_{A}$ ( q ) .

"⇒" Assume there exists $i \ge 0$, such that $\mathcal{G}^i(\top)(q) = \mathfrak{P}_A(q)$ and let $i$ be the smallest such integer. Then $\top, \mathcal{G}(\top), \mathcal{G}^2(\top), \dots, \mathcal{G}^i(\top)$ is a strictly decreasing sequence hence, for each $j \in [1..i]$, there exists a partial run $\theta_j \in \mathcal{R}_q^\infty(\mathcal{A})$ over some tree $t_j$ and a position $p_j \in \text{fr}(t_j)$, such that $\theta_j(p_j) = q$ and $\{r \in [1..\#q] \mid \exists s \in \mathcal{G}^{j-1}(\top)(q) . x_s^{[e]} \approx_{\Theta_{(t_j)}} x_r^{[p_j]}\} \subsetneq \mathcal{G}^{j-1}(\top)(q)$. We compose these partial runs $\theta_1, \dots, \theta_i$ by appending each $\theta_j$ to $\theta_{j-1}$ at position $p_{j-1} \in \text{fr}(\theta_{j-1})$, for all $j \in [2..i]$ into a partial $\theta'' \in \mathcal{R}_q^\infty(\mathcal{A})$. We define a context $\bar{\theta}_{p_i \leftarrow q}$ by appending to each position $r \in \text{fr}(\theta) \setminus \{p_i\}$ a complete run starting in $\theta(r)$. By the fact that $\mathcal{A}$ is trim, such a run exists. The context $\bar{\theta}_{p_i \leftarrow q}$ satisfies condition (2) of Definition 4.16, but not necessarily (1). Let $\pi : \mathfrak{P}_A(q) \to \mathfrak{P}_A(q)$ be a permutation defined as $\pi(i) = j$ iff $x_i \approx_{\Theta_{(i)}} x_j$, there $\bar{t}$ is the tree recognized by the partial run $\bar{\theta}_{p_i \leftarrow q}$ of $\mathcal{A}$. Note that the choice of $j$ is not unique, but one exists, by Definition 4.14. Then we define the $q$-reset $\theta_{p_i \leftarrow q}$ by appending $\bar{\theta}_{p_i \leftarrow q}$ to itself at position $p_i$ a number of times equal to the order of $\pi$. Then, one can check that $\theta_{p_i \leftarrow q}$ satisfies both conditions of Definition 4.16.

(2) Let $S$ be the SCC of $q$ in $\mathcal{A}$. Since $q = \bullet \tau$, for some transition $\tau \in \delta^1$, it must be the case that $S$ is a linear SCC, by Definition 4.5. Also $q \in \bullet (\delta^\infty)$ thus, by Lemma 4.8, there exists a pivot state $q_0$ in $S$ and let $\theta^0 \in \mathcal{R}_q^\infty(\mathcal{A})$ be a partial run from $q$ to $q_0$ with transitions from $\bullet S \bullet \subseteq \delta^\infty$. From point (1) above we obtain a $q_0$-reset $\theta^1_{p_1 \leftarrow q_0} \in \mathcal{R}_{q_0}^\infty(\mathcal{A})$ such that $x_j^{[e]} \approx_{\Theta_{(t)}} y_k^{[p_1]}$, for all $j, k \in \mathfrak{P}_A(q_0)$ and $x_j^{[e]} \not\approx_{\Theta_{(t)}} y_k^{[p_1]}$, for all $j, k \in [1..\#q_0]$, $k \notin \mathfrak{P}_A(q_0)$. Moreover, there exists another context $\theta^2_{p_2 \leftarrow q} \in \mathcal{R}_{q_0}^\infty(\mathcal{A})$. By the choice of the pivot state $q_0$, there exists a position $p_0 \in \text{fr}(\theta^0)$ such that $\theta^0(p_0) = q_0$. Let $p \stackrel{\text{def}}{=} p_0 p_1 p_2$ and $\bar{\theta}_{p \leftarrow q}$ be the context consisting of $\theta^0$ to which we append, in this order:

▷ θ 1 on position p 0 ,

▷ θ² on the position p₀p₂,

▷ to any other position $r \in (\text{fr}(\theta^0) \setminus \{p_0\}) \cup (p_0 \cdot \text{fr}(\theta^1) \setminus \{p_1\}) \cup (p_0 p_1 \cdot \text{fr}(\theta^2) \setminus \{p_2\})$ a complete run starting in:

$$
- \theta^0(r) \text{ if } r \in \text{fr}(\theta^0) \setminus \{p_0\},
$$
- $\theta^1(r')$ if $r = p_0r'$ and $r' \in \text{fr}(\theta^1) \setminus \{p_1\}$, and

- $\theta^2(r'')$ if $r = p_0p_1r''$ and $r'' \in \text{fr}(\theta^2) \setminus \{p_2\}$.

Such runs exist by the assumption that $\mathcal{A}$ is trim. Moreover, these runs use only $\infty$-transitions, because their states are from $\infty$-SCCs (Definition 4.5).

It is easy to check that $\bar{\theta}$ satisfies condition (2) of Definition 4.16. In order to satisfy condition (1), in addition to (2), we append $\bar{\theta}$ to itself at position $p$, using the same idea as in the construction at point (1). $\square$

The purpose of introducing resets is proving that any sequence of partial runs consisting of $\infty$-transitions can be embedded in a complete run, such that each two such partial runs are separated by any number of resets. This is a key ingredient for the proof of the “embedding” property of the canonical models of expandables SIDs (Definition 3.8).

<figure><img src="image_17.png" /><figcaption>Figure 11: Embedding of a partial run $\theta_i$ in $\theta$</figcaption></figure>

**Lemma 4.20.** Let $\mathcal{A}$ be a trim choice-free automaton. Given partial runs $\theta_1 \in \mathcal{R}_{q_1}^{\infty}(\mathcal{A})$, ..., $\theta_n \in \mathcal{R}_{q_n}^{\infty}(\mathcal{A})$ and an integer $k \ge 1$, there exists an accepting run $\theta$ of $\mathcal{A}$ such that:

(1) $\theta_i$ is embedded in $\theta$ at some position $p_i \in \text{dom}(\theta)$, for each $i \in [1..n]$,

(2) $p_i \cdot \text{dom}(\theta_i) \cap p_j \cdot \text{dom}(\theta_j) = \emptyset$, for all $1 \le i < j \le n$,

(3) the path between $p_i$ and $p_j$ in $\theta$ traverses $k$ times some reset path disjoint from $\cup_{\ell=1}^n p_\ell \cdot \text{dom}(\theta_\ell)$, for all $1 \le i < j \le n$.

*Proof.* Let $\theta$ be an arbitrary accepting run of $\mathcal{A}$. By Lemma 4.7, each 1-transition occurs exactly once on $\theta$, hence $\theta$ visits each pivot state at least once. The partial runs $\theta_1, \dots, \theta_n$ will be inserted into $\theta$ one by one, as described next. First, for each $\theta_i \in \mathcal{R}_{q_i}^{\infty}(\mathcal{A})$, we have a pivot state $q_i^0$ and a partial run $\theta_i^0 \in \mathcal{R}_{q_i^0}^{\infty}(\mathcal{A})$, satisfying condition 1 or 2 of Lemma 4.8. Since $q_i^0$ occurs on $\theta$, we can insert in $\theta$ a new partial run $\theta'_i \in \mathcal{R}_{q_i^0}^{\infty}(\mathcal{A})$ defined next. By Lemma 4.18 (1), there exists a $q_0^i$-reset sequence $\theta_r^i \in \mathcal{R}_{q_0^i}^{\infty}(\mathcal{A})$. The partial run $\theta'_i$ is obtained by composing $\theta_r^i$ with itself $k$ times, followed by $\theta_0^i$. These compositions are possible, because $q_0^i$ occurs at the root of $\theta_r^i$ and $\theta_0^i$, as well as the frontier of $\theta_r^i$. Depending on which condition of Lemma 4.8 is satisfied by $q_0^i$ and $\theta_0^i$, we distinguish the following cases (see Figure 11 for an illustration):
▷ condition (1) of Lemma 4.8 holds: in this case $q_i$ and $q_0^i$ occur on different positions on the frontier of $\theta_0^i$, thus we append $\theta_i$ on the position where $q_i$ occurs and the rest of $\theta$ on the position where $q_0^i$ occurs.

▷ condition (2) of Lemma 4.8 holds: in this case only $q_0^i$ occurs on the frontier of $\theta_0^i$, thus we continue with $\theta_i$, which can be extended to reach $q_0^i$ again, by Lemma 4.8. From this second occurrence of $q_0^i$, we continue with $\theta$.

We prove the points from the statement of the Lemma below:

(1) The runs $\theta_1, \dots, \theta_n$ are inserted into $\theta$ at positions $p_1, \dots, p_n$, respectively.

(2) Since $\theta_1, \dots, \theta_n$ are inserted one after the other (the order is not important), we have $p_i \cdot \text{dom}(\theta_i) \cap p_j \cdot \text{dom}(\theta_j) = \emptyset$, for all $1 \le i < j \le n$.

(3) By the definition of $\theta'_1, \dots, \theta'_n$, the path between $p_i$ and $p_j$ traverses $k$ times the $\theta_r^i$ or $\theta_r^j$ reset sequences that are, moreover, disjoint from each $p_k \cdot \text{dom}(\theta_k)$, for $k \in [1..n]$. $\square$

**4.4. Eliminating Persistent Variables.** For the rest of this section, let $\mathcal{A}_{\Delta,A} = (\Sigma, \mathcal{Q}_{\Delta}, q_A, \delta_{\Delta})$ be the automaton built for the given SID $\Delta$ and nullary predicate $A$, by the construction of Lemma 4.13. Since $\Delta$ was assumed to be all-satisfiable, the same can be assumed about $\mathcal{A}_{\Delta,A}$, by Lemma 4.13 (1).

Moreover, we can assume, without loss of generality, that $\mathcal{A}_{\Delta,A}$ is choice-free and let $\delta_{\Delta} = \delta_{\Delta}^{\downarrow} \uplus \delta_{\Delta}^{\uparrow}$ be the partition of the transitions of $\mathcal{A}_{\Delta,A}$ (Definition 4.5). If this is not the case, we consider one of the finitely many automata in the language-preserving choice-free decomposition of $\mathcal{A}_{\Delta,A}$ (Lemma 4.9).

The transformation proceeds in three stages, denoted (I), (II) and (III) below. The result of each stage is one or more choice-free automata that are treewidth bounded if and only if the set $[\mathcal{A}_{\Delta,A}]$ is treewidth bounded.

**Example 4.21.** We shall illustrate each stage of the construction on the following SID:

$$ \mathcal{A}_{\Delta} \left\{ \begin{array}{ll} A & \leftarrow \exists y_1 \exists y_2 \exists y_3 . C_1(y_1, y_2, y_3) \\ C_1(x_1, x_2, x_3) & \leftarrow \exists y_4 . e(x_1, y_4) * e(x_3, y_4) * C_1(y_4, x_2, x_3) \\ C_1(x_1, x_2, x_3) & \leftarrow \exists y_5 . e(x_1, x_2) * C_2(x_2, y_5, x_3) \\ C_2(x_1, x_2, x_3) & \leftarrow \exists y_6 . e(x_1, y_6) * e(x_3, y_6) * C_2(y_6, x_2, x_3) \\ C_2(x_1, x_2, x_3) & \leftarrow e(x_1, x_2) \end{array} \right. \quad (q_{C_1}) $$

For simplicity, the existentially quantified variables are given pairwise distinct names. The automaton $\mathcal{A}_{\Delta,A}$ has the following transitions:

$$ \mathcal{A}_{\Delta,A} \left\{ \begin{array}{ll} \tau_1 : & q_A \xrightarrow{y_1^{[\epsilon]} = x_1^{[1]} \ast y_2^{[\epsilon]} = x_2^{[1]} \ast y_3^{[\epsilon]} = x_3^{[1]}} (q_{C_1}) \quad (1) \\ \tau_2 : & q_{C_1} \xrightarrow{e(x_1^{[\epsilon]}, y_4^{[\epsilon]}) \ast e(x_3^{[\epsilon]}, y_4^{[\epsilon]}) \ast y_4^{[\epsilon]} = x_1^{[1]} \ast x_2^{[\epsilon]} = x_2^{[1]} \ast x_3^{[\epsilon]} = x_3^{[1]}} (q_{C_1}) \quad (\infty) \\ \tau_3 : & q_{C_1} \xrightarrow{e(x_1^{[\epsilon]}, x_2^{[\epsilon]}) \ast x_2^{[\epsilon]} = x_1^{[1]} \ast y_5^{[\epsilon]} = x_2^{[1]} \ast x_3^{[\epsilon]} = x_3^{[1]}} (q_{C_2}) \quad (1) \\ \tau_4 : & q_{C_2} \xrightarrow{e(x_1^{[\epsilon]}, y_6^{[\epsilon]}) \ast e(x_3^{[\epsilon]}, y_6^{[\epsilon]}) \ast y_6^{[\epsilon]} = x_1^{[1]} \ast x_2^{[\epsilon]} = x_2^{[1]} \ast x_3^{[\epsilon]} = x_3^{[1]}} (q_{C_2}) \quad (\infty) \\ \tau_5 : & q_{C_2} \xrightarrow{e(x_1^{[\epsilon]}, x_2^{[\epsilon]})} () \quad (1) \end{array} \right. $$

The $\Delta$-models of $A$ have the structure depicted in Figure 12 (a), with elements that are values of persistent variables annotated by the name of the first occurrence of the persistent variable during the run.
<figure><img src="image_18.png" /><figcaption>Figure 12: Models of the Running Example for the Elimination of Persistent Variables</figcaption></figure>

**I. Removing relation and disequality atoms from 1-transitions.** This step replaces each symbol $\alpha$ that labels a 1-transition $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell)$ of $\mathcal{A}_{\Delta, A}^I$ with the symbol obtained by removing all relation and disequality atoms from $\alpha$. The outcome of this transformation is denoted $\mathcal{A}_{\Delta, A}^I \stackrel{\text{def}}{=} (\Sigma, Q_\Delta, q_A, \delta_\Delta^I)$.

**Example 4.22.** (continued from Example 4.21) The result of removing the relation and disequality atoms from the 1-transitions of the choice-free automaton given in Example 4.21 is shown below:

$$ \mathcal{A}_{\Delta,A}^I = \left\{ \begin{array}{ll} \tau_1: & q_A \xrightarrow{\substack{y_1^{[\epsilon]}=x_1^{[1]} \\ e(x_1^{[\epsilon]}, y_4^{[\epsilon]}) * e(x_3^{[\epsilon]}, y_4^{[\epsilon]}) * y_4^{[\epsilon]}=x_1^{[1]} \\ x_2^{[\epsilon]}=x_1^{[1]}}}} (q_{C_1}) & (1) \\ \tau_2: & q_{C_1} \xrightarrow{\substack{y_5^{[\epsilon]}=x_2^{[1]} \\ e(x_3^{[\epsilon]}, y_6^{[\epsilon]}) * e(x_5^{[\epsilon]}, y_6^{[\epsilon]}) * y_6^{[\epsilon]}=x_2^{[1]} \\ x_3^{[\epsilon]}=x_3^{[1]}}} (q_{C_2}) & (1) \\ \tau_3: & q_{C_1} \xrightarrow{\substack{y_6^{[\epsilon]}=x_3^{[1]} \\ e(x_1^{[\epsilon]}, y_6^{[\epsilon]}) * e(x_3^{[\epsilon]}, y_6^{[\epsilon]}) * y_6^{[\epsilon]}=x_3^{[1]} \\ x_2^{[\epsilon]}=x_2^{[1]}}}} (q_{C_2}) & (1) \\ \tau_4: & q_{C_2} \xrightarrow{\text{emp}} (1) \\ \tau_5: & q_{C_2} \xrightarrow{\text{emp}} (1) \end{array} \right. $$

The formal properties of $\mathcal{A}_{\Delta,A}^I$ are stated and proved below. Note that $\mathcal{A}_{\Delta,A}^I$ is choice-free, because $\mathcal{A}_{\Delta,A}$ is choice-free, i.e., the re-labeling of the transitions of $\mathcal{A}_{\Delta,A}$ does not change the structure of its SCC graph. In the statement of this and the upcoming lemmas, we assume addition and order within the set of natural numbers with infinity, i.e., $n + \infty = \infty + n = \infty$, $n \le \infty$ and $\infty \le \infty$, for all $n \in \mathbb{N}$.

**Lemma 4.23.**

(1) $\mathcal{A}_{\Delta,A}^I$ is all-satisfiable

(2) $\text{tw}(\llbracket \mathcal{A}_{\Delta,A}^I \rrbracket) \le \text{tw}(\llbracket \mathcal{A}_{\Delta,A} \rrbracket) + \text{card}(\delta_\Delta^1) \cdot (\text{maxRelAtoms}(\Delta) + \text{maxVars}(\Delta))$

(3) $\text{tw}(\llbracket \mathcal{A}_{\Delta,A} \rrbracket) \le \text{tw}(\llbracket \mathcal{A}_{\Delta,A}^I \rrbracket) + \text{card}(\delta_\Delta^1) \cdot \text{maxVars}(\Delta)$

*Proof.* For space reasons, the proof of the lemma is given in subsection C.5. $\square$

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

**II. Removing equalities involving non-persistent variables.** At this point, the labels of the 1-transitions of $\mathcal{A}_{\Delta,A}^I$ consist of equalities only. We now remove the equalities that would be lost when adding resets before and after 1-transitions that is, we forget equalities involving non-persistent variables while keeping equalities between persistent ones. To this end, we modify the label of each 1-transition $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell)$ of $\mathcal{A}_{\Delta,A}^I$ in two steps:

(1) for each non-persistent $\epsilon$-variable $x_j^{[\epsilon]}$, i.e., $j \in [1..\#q_0] \setminus \mathfrak{P}_{\mathcal{A}_{\Delta,A}^I}(q_0)$, occurring in $\alpha$ in some equality with a persistent $i$-variable, i.e., $x_j^{[\epsilon]} = x_k^{[\epsilon]}$, $k \in \mathfrak{P}_{\mathcal{A}_{\Delta,A}^I}(q_i)$, we substitute $x_j^{[\epsilon]}$ in $\alpha$ with a fresh variable $y^{[\epsilon]} \not\in \text{fv}(\alpha)$,
(2) remove each equality involving a non-persistent variable $x_j^{[i]}$, for $i = \epsilon$ and $j \in [1..\#q_0]$, or $i \in [1..\ell]$ and $j \in [1..\#q_i]$.

**Example 4.24.** (continued from Example 4.22) The profile of the automaton $\mathcal{A}_{\Delta, A}^I$ from Example 4.22 is $\mathfrak{P}_{\mathcal{A}_{\Delta, A}^I}(q_A) = \emptyset$ and $\mathfrak{P}_{\mathcal{A}_{\Delta, A}^I}(q_{C_1}) = \mathfrak{P}_{\mathcal{A}_{\Delta, A}^I}(q_{C_2}) = \{2, 3\}$. By removing the equalities involving non-persistent variables, we obtain $\mathcal{A}_{\Delta, A}^{II}$ from $\mathcal{A}_{\Delta, A}^I$ by transforming only the 1-transition $\tau_3$ into:

$$ \tau'_3 : q_{C_1} \xrightarrow{y_5^{[\epsilon]} = x_2^{[1]} * x_3^{[\epsilon]} = x_3^{[1]}} (q_{C_2}) \quad (1) $$

Since $x_1^{[1]}$ is non-persistent, the equality $x_2^{[\epsilon]} = x_1^{[1]}$ is removed from the label of the original transition. Note that the equalities $y_5^{[\epsilon]} = x_2^{[1]}$ and $x_3^{[\epsilon]} = x_3^{[1]}$ are kept, because $x_2^{[1]}$, $x_3^{[\epsilon]}$ and $x_3^{[1]}$ are persistent variables. Note that $y_5^{[\epsilon]}$ is not persistent, because it is not associated with a state in $\tau'_3$.

The result is the choice-free automaton $\mathcal{A}_{\Delta, A}^{II} \stackrel{\text{def}}{=} (\Sigma, \mathcal{Q}_{\Delta}, q_A, \delta_{\Delta}^{II})$, whose properties are stated and proved below:

**Lemma 4.25.**

(1) $\mathcal{A}_{\Delta, A}^{II}$ is all-satisfiable,

(2) $\text{tw}([\mathcal{A}_{\Delta, A}^{II}]) \le \text{tw}([\mathcal{A}_{\Delta, A}^{I}]) + \text{card}((\delta_{\Delta}^{I})^{1}) \cdot \text{maxVars}(\Delta)$,

(3) $\text{tw}([\mathcal{A}_{\Delta, A}^{I}]) \le \text{tw}([\mathcal{A}_{\Delta, A}^{II}])$.

*Proof.* For space reasons, the proof of this lemma is given in subsection C.6. $\square$

**III. Removing persistent variables.** We build from the choice-free automaton $\mathcal{A}_{\Delta, A}^{II}$ a set of choice-free automata $\tilde{B}_1, \dots, \tilde{B}_m$, having no persistent variables within the transition labels, such that $[\mathcal{A}_{\Delta, A}^{II}]$ is treewidth bounded if and only if $[\tilde{B}_i]$ is treewidth bounded, for each $i \in [1..m]$.

We recall that each 1-transition of a choice free automata occurs exactly once in each accepting run over a $\Sigma$-labeled tree $t$ and each such occurrence corresponds to one subformula $t(p)^p$ of $\Theta(t)$, for a position $p \in \text{dom}(t)$ (Lemma 4.7). Using renaming, if necessary, we can assume that the $\epsilon$-variables that are not associated with the states of the transition have distinct names between the labels of the 1-transitions of $\mathcal{A}_{\Delta, A}^{II}$ and let $\mathcal{Y} \stackrel{\text{def}}{=} \{y_1^{[\epsilon]}, \dots, y_M^{[\epsilon]}\}$ denote their set, in the following. For instance, we have $\mathcal{Y} = \{y_1^{[\epsilon]}, y_2^{[\epsilon]}, y_3^{[\epsilon]}, y_5^{[\epsilon]}\}$ in Example 4.22. The transformation is done in three steps:

(A) We annotate each state $q$ of $\mathcal{A}_{\Delta, A}^{II}$ with an injective partial function $a : [1..\#q] \to [1..M]$ that maps each persistent variable $x_j^{[i]}$, associated with $q$, to a variable $y_{a(j)}^{[\epsilon]} \in \mathcal{Y}$, such that $x_j^{[i]} \approx_{\Theta(t)} y_{a(j)}^{[\epsilon]}$ holds for each tree $t \in \mathcal{L}(\mathcal{A}_{\Delta, A}^{II})$.

(B) We split the automaton obtained from the annotation of $\mathcal{A}_{\Delta, A}^{II}$ into several choice-free automata $\tilde{B}_1, \dots, \tilde{B}_m$ such that $\mathcal{L}(\mathcal{A}_{\Delta, A}^{II}) = \bigcup_{i=1}^m \mathcal{L}(\tilde{B}_i)$.

(C) The annotation of the states in each $\tilde{B}_i$ is used to replace each occurrence of a relation atom $r(z_1^{[\epsilon]}, \dots, z_{\#r}^{[\epsilon]})$, occurring within the label of an annotated transition $(q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell))$, with a fresh relation atom $r_g(z_{i_1}^{[\epsilon]}, \dots, z_{i_k}^{[\epsilon]})$, where $g : [1..\#r] \to [1..M]$ maps each persistent variable from the set $\{z_1^{[\epsilon]}, \dots, z_{\#r}^{[\epsilon]}\}$ to its corresponding
variable from $\mathcal{Y}$ and $\{z_{i_1}^{[\epsilon]}, \dots, z_{i_k}^{[\epsilon]}\}$ are the remaining non-persistent variables. The persistent variables are subsequently removed from $\alpha$ and the remaining variables are renamed according to the conventions from Definition 4.11. Consequently, the arities of the states $(q_i, a_i)$, $i \in [0..\ell]$ are changed as well.

**Example 4.26.** (continued from Example 4.24) Let us consider the automaton $\mathcal{A}_{\Delta,A}^{II}$ from Example 4.24. The $\epsilon$-variables from the labels of 1-transitions, that are not associated with states thereof, are $y_1^{[\epsilon]}$, $y_2^{[\epsilon]}$, $y_3^{[\epsilon]}$, $y_5^{[\epsilon]}$, renamed as $\mathcal{Y} = \{y_1^{[\epsilon]}, y_2^{[\epsilon]}, y_3^{[\epsilon]}, y_4^{[\epsilon]}\}$, respectively. We recall that $\mathfrak{P}_{\mathcal{A}_{\Delta,A}^{II}}(q_A) = \emptyset$ and $\mathfrak{P}_{\mathcal{A}_{\Delta,A}^{II}}(q_{C_1}) = \mathfrak{P}_{\mathcal{A}_{\Delta,A}^{II}}(q_{C_2}) = \{2,3\}$ is the profile of $\mathcal{A}_{\Delta,A}^{II}$. The automaton obtained by annotating the states of $\mathcal{A}_{\Delta,A}^{II}$ with assignments is already choice-free and the result of the elimination of persistent variables is shown below:

$$ \tilde{\mathcal{B}} = \left\{ \begin{array}{ll} \tau_1 : & (q_A, \emptyset) \xrightarrow{\text{emp}} ((q_{C_1}, a)) \quad (1) \\ \tau_2 : & (q_{C_1}, a) \xrightarrow{\frac{e(x_1^{[\epsilon]}, y_4^{[\epsilon]} * e_g(y_4^{[\epsilon]} * y_4^{[\epsilon]} = x_1^{[1]})}{e(x_1^{[\epsilon]}, y_6^{[\epsilon]} * e_g(y_6^{[\epsilon]} * y_6^{[\epsilon]} = x_1^{[1]})}} ((q_{C_2}, a)) \quad (\infty) \\ \tau_3 : & (q_{C_1}, a) \xrightarrow{\text{emp}} ((q_{C_2}, a)) \quad (1) \\ \tau_4 : & (q_{C_2}, a) \xrightarrow{\frac{e(x_1^{[\epsilon]}, y_6^{[\epsilon]} * e_g(y_6^{[\epsilon]} * y_6^{[\epsilon]} = x_1^{[1]})}{e(x_1^{[\epsilon]}, y_6^{[\epsilon]} * e_g(y_6^{[\epsilon]} * y_6^{[\epsilon]} = x_1^{[1]})}} ((q_{C_2}, a)) \quad (\infty) \\ \tau_5 : & (q_{C_2}, a) \xrightarrow{\text{emp}} () \quad (1) \end{array} \right. $$

where:

▷ $a: [1..3] \to [1..4]$ is the partial mapping defined as $a(2) = 2$, $a(3) = 3$ and undefined at 1,

▷ $g: [1..2] \to [1..4]$ is the partial mapping defined as $g(1) = 3$ and undefined at 2.

Note that, because the equality between the persistent variables $x_3^{[\epsilon]}$ and $x_3^{[1]}$ has been kept in $\mathcal{A}_{\Delta,A}^{II}$ (see Example 4.24), both variables are mapped by $g$ to the same variable $y_3^{[\epsilon]}$, hence the same relation symbol $e_g$ replaces both $e(x_3^{[\epsilon]}, y_4^{[\epsilon]})$ in $\tau_2$ and $e(x_3^{[\epsilon]}, y_6^{[\epsilon]})$ in $\tau_4$. Figure 12 (b) shows the shape of the structures from $\llbracket \tilde{\mathcal{B}} \rrbracket$. Since all but the first elements in both the $C_1$ and $C_2$ chains are now labeled with the same unary relation symbol $e_g$, these structures are of treewidth at most two.

We recall that $\mathcal{A}_{\Delta,A}^{II} = (\Sigma, \mathcal{Q}_{\Delta}^{I}, q_A, \delta_{\Delta}^{II})$ and describe the transformation formally:

(A) Let $\widetilde{\mathcal{A}}_{\Delta,A}^{II} \stackrel{\text{def}}{=} (\Sigma, \widetilde{\mathcal{Q}}_{\Delta}^{I}, (q_A, \emptyset), \widetilde{\delta}_{\Delta}^{II})$ be the automaton, whose set of states is:

$$ \widetilde{\mathcal{Q}}_{\Delta}^{I} \stackrel{\text{def}}{=} \{(q, a) \mid q \in \mathcal{Q}_{\Delta}^{I}, a: [1..\#q] \to [1..\mathcal{M}] \text{ is a partial injective mapping}\} $$

The initial state of $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$ consists of the initial state $q_A$ of $\mathcal{A}_{\Delta,A}^{II}$ annotated with the empty mapping, because we have considered $\#q_A = 0$. The set $\widetilde{\delta}_{\Delta}^{II}$ contains a transition $(q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell))$ if and only if either one of the following holds (by Definition 4.5, these conditions are exclusive):

▷ $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in (\delta_{\Delta}^{II})^1$: in this case, for all $k \in [1..\ell]$ and $i \in \mathfrak{P}_{\mathcal{A}_{\Delta,A}^{II}}(q_k)$, we define:

$$ a_k(i) \stackrel{\text{def}}{=} \begin{cases} a_0(j) & \text{if there exists } j \text{ such that } x_i^{[k]} \approx_{\alpha} x_j^{[\epsilon]}, \\ m & \text{else, if } m \text{ is such that } x_i^{[k]} \approx_{\alpha} y_m^{[\epsilon]} \end{cases} $$

Note that $a_k$ is well defined, because each $i$-variable is equated to a unique $\epsilon$-variable in the definition of $\mathcal{A}_{\Delta,A}$ and this fact is unchanged by the constructions of $\mathcal{A}_{\Delta,A}^{I}$ and $\mathcal{A}_{\Delta,A}^{II}$.

▷ $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in (\delta_{\Delta}^{II})^\infty$: in this case, for all $k \in [1..\ell]$ and $i \in [1..\#q_k]$, we define $a_k(i) \stackrel{\text{def}}{=} a_0(j)$ if there exists $j$, such that $x_i^{[k]} \approx_{\alpha} x_j^{[\epsilon]}$ and undefined, otherwise.
The property of the first step of persistent variable elimination is summarized below:

**Lemma 4.27.** $\mathcal{L}(\widetilde{\mathcal{A}}_{\Delta,A}^{II}) = \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$.

*Proof.* Let $h: \widetilde{\mathcal{Q}}_{\Delta}^{I} \to \mathcal{Q}_{\Delta}^{I}$ be the function defined as $h((q, a)) \stackrel{\text{def}}{=} q$, for all $(q, a) \in \widetilde{\mathcal{Q}}_{\Delta}^{I}$. We show that $h$ is a refinement. By Lemma 4.4, we obtain $\mathcal{L}(\widetilde{\mathcal{A}}_{\Delta,A}^{II}) = \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$. We prove the three points of Definition 4.3:

(1) $h((q_A, \emptyset)) = q_A$, by the definition of $h$.

(2) $(q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell)) \in \widetilde{\delta}_{\Delta}^{II}$ only if $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in \delta_{\Delta}^{II}$, by the definition of $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$.

(3) Let $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in \delta_{\Delta}^{II}$ be a transition and assume w.l.o.g. that $\mathcal{A}_{\Delta,A}^{II}$ is trim (if this is not the case, a trim automaton with the same language can be considered instead). Then, there exists an accepting run $\theta$ of $\mathcal{A}_{\Delta,A}^{II}$, such that the transition $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell)$ occurs on $\theta$. Each state $q$ on $\theta$ can be annotated with an injective partial mapping $a: [1..\#q] \to [1..M]$ and the result is an accepting run of $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$. Hence there exist injective partial functions $a_i: [1..\#q_i] \to [1..M]$, for $i \in [0..\ell]$ such that $(q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell)) \in \widetilde{\delta}_{\Delta}^{II}$. Moreover, $(q_i, a_i) \in h^{-1}(q_i)$, for each $i \in [0..\ell]$. $\square$

(B) The problem, at this point, is that $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$ is not necessarily choice-free, because annotating the states of $\mathcal{A}_{\Delta,A}^{II}$ may cause several transitions to occur between different linear SCCs. These transitions originate from the same 1-transition of $\mathcal{A}_{\Delta,A}^{II}$ and differ only in the annotations added at step (A). We circumvent this problem by decomposing $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$ into choice-free automata $\widetilde{\mathcal{B}}_1, \dots, \widetilde{\mathcal{B}}_m$, such that $\mathcal{L}(\widetilde{\mathcal{A}}_{\Delta,A}^{II}) = \bigcup_{i=1}^{m} \mathcal{L}(\widetilde{\mathcal{B}}_i)$. To this end, we choose sets $\widetilde{\delta}_1^1, \dots, \widetilde{\delta}_m^1$, such that:

$$ \triangleright (\widetilde{\delta}^{II})^1 = \bigcup_{i=1}^{m} \widetilde{\delta}_i^1, \text{ and} $$

$\triangleright$ for each $i \in [1..m]$, the set $\widetilde{\delta}_i^1$ contains exactly one transition $(q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell))$ from $\widetilde{\delta}_{\Delta}^{II}$, for each transition $q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell)$ from $(\delta_{\Delta}^{II})^1$.

Moreover, we define the set:

$$ (\bar{\delta})^{\infty} \stackrel{\text{def}}{=} \{(q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell)) \in \widetilde{\delta}_{\Delta}^{II} \mid q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in (\delta_{\Delta}^{II})^{\infty}\} $$

For each $i \in [1..m]$, let $\widetilde{\mathcal{B}}_i \stackrel{\text{def}}{=} (\Sigma, \widetilde{\mathcal{Q}}_{\Delta}^{I}, (q_A, \emptyset), \widetilde{\delta}_i^1 \uplus \widetilde{\delta}^{\infty})$. We prove below that $\widetilde{\mathcal{B}}_1, \dots, \widetilde{\mathcal{B}}_m$ is indeed a choice-free decomposition of $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$:

**Lemma 4.28.**

(1) $\widetilde{\mathcal{B}}_i$ is all-satisfiable and choice-free, for $i \in [1..m]$.

(2) $\mathcal{L}(\widetilde{\mathcal{A}}_{\Delta,A}^{II}) = \bigcup_{i=1}^{m} \mathcal{L}(\widetilde{\mathcal{B}}_i)$.

*Proof.* For space reasons, the proof of this lemma is given in subsection C.7. $\square$

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

(C) Let us fix a choice-free automaton $\widetilde{\mathcal{B}} = (\Sigma, \widetilde{\mathcal{Q}}_{\Delta}^{I}, (q_A, \emptyset), \widetilde{\delta}_1^1 \uplus \widetilde{\delta}^{\infty})$ among $\widetilde{\mathcal{B}}_1, \dots, \widetilde{\mathcal{B}}_m$. Consider an arbitrary transition $\tau: (q_0, a_0) \xrightarrow{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell)) \in \widetilde{\delta}_1^1 \uplus \widetilde{\delta}^{\infty}$. We denote by $P_0 \stackrel{\text{def}}{=} \{x_j^{[\ell]} | j \in \text{dom}(a_0)\} \cup \{y_j^{[\ell]} \in \text{fv}(\alpha) | \tau \in \widetilde{\delta}_1^1\}$, $P_i \stackrel{\text{def}}{=} \{x_j^{[i]} | j \in \text{dom}(a_i)\}$, for $i \in [1..\ell]$ and $P \stackrel{\text{def}}{=} \bigcup_{i=0}^{\ell} P_i$ the set of persistent variables occurring in $\alpha$. The goal of this step is
to remove from $\alpha$ the variables from $P$. The outcome of this transformation of $\alpha$ will be denoted as $\bar{\alpha}$. In order to guarantee the preservation of the naming conventions from Definition 4.11, the remaining (non-persistent) variables from $fv(\alpha) \setminus P$ are renamed using the injective mapping $\zeta_{\tau} : fv(\alpha) \setminus P \to fv(\alpha)$ defined as follows:

$$ \triangleright \zeta_{\tau}(x_k^{[i]}) \stackrel{\text{def}}{=} x_{k-p}^{[i]} \quad \text{where } p \stackrel{\text{def}}{=} \text{card}(\{x_j^{[i]} \mid j < k\} \cap P_i) \text{ for all } i \in [0..l], k \in [1..n_i], x_k^{[i]} \notin P_i, $$

$$ \triangleright \zeta_{\tau}(y_k^{[\epsilon]}) = y_k^{[\epsilon]}, \text{ for all } k \in [1..m], y_k^{[\epsilon]} \notin P_0 $$

where $m, n_0, \dots, n_l$ are the numbers of $y_j^{[\epsilon]}$, $x_j^{[\epsilon]}$, \dots, $x_j^{[i]}$, respectively (see Definition 4.11). Intuitively, the renaming *shifts to the left* the $j$ indices of the $x_j^{[i]}$ variables so that the persistent variables indexed according to the assignments $a_i$ are ignored. The transformation of $\alpha$ to $\bar{\alpha}$ is described for each atom of $\alpha$, as follows:

▷ every relation atom $r(z_1^{[\epsilon]}, \dots, z_{\#r}^{[\epsilon]})$ is replaced by $r_g(\zeta_{\tau}(z_{i_1}^{[\epsilon]}), \dots, \zeta_{\tau}(z_{i_k}^{[\epsilon]}))$, where $r_g$ is a fresh relation symbol of arity $k$ such that $\{z_{i_1}, \dots, z_{i_k}\} \stackrel{\text{def}}{=} \{z_1, \dots, z_{\#r}\} \setminus P_0$ and $g : [1..\#r] \to [1..M]$ is the partial function:

$$ g(j) \stackrel{\text{def}}{=} \begin{cases} a_0(j), & \text{if } z_j^{[\epsilon]} \in P_0 \\ \text{undefined}, & \text{otherwise} \end{cases} $$

Note that the arity of $r_g$ is at least one, for the following reason. Since relation atoms occur only in $\infty$-transitions, they can repeat arbitrary many times in characteristic formulæ over runs. Hence, if such an atom has only persistent variables, these characteristic formulæ will become unsatisfiable if the atom repeat more than twice. This contradicts, however, the hypothesis that $\tilde{B}_i$ is all-satisfiable.

▷ every (dis-)equality atom $x \sim y$ is replaced by $\zeta_{\tau}(x) \sim \zeta_{\tau}(y)$ for $\sim \in \{=, \ne\}$ if $\{x, y\} \cap P = \emptyset$ and removed otherwise. In particular, note that there is no equality in $\alpha$ between a variable in $P$ and another one not in $P$ due to elimination of equalities with non-persistent variables in 1-transitions and to the rule of propagation through $\infty$-transitions. Moreover, this transformation turns the label of each 1-transition into `emp`, because the labels of 1-transitions contain only equalities involving persistent variables.

The result of this transformation of $\tilde{B}_i$ is denoted $\bar{B}_i$, for each $i \in [1..m]$. Let $\bar{B}$ be any of $\bar{B}_1, \dots, \bar{B}_m$ and $\tilde{B}$ be the corresponding automaton before the removal of persistent variables. The properties of this transformation are stated and proved below:

**Lemma 4.29.**

(1) $\bar{B}$ is all-satisfiable and choice-free,

(2) $\text{tw}(\llbracket \bar{B} \rrbracket) \le \text{tw}(\llbracket \tilde{B} \rrbracket),$

(3) $\text{tw}(\llbracket \tilde{B} \rrbracket) \le \text{tw}(\llbracket \bar{B} \rrbracket) + \text{card}(\tilde{\delta}^1) \cdot \text{maxVars}(\Delta).$

*Proof.* For space reasons, the proof of this lemma is given in subsection C.8. □

**4.5. Wrapping 1-transitions.** In subsection 4.4 we have transformed a given automaton $A_{\Delta, \mathcal{A}}$ into choice-free automata $\bar{B}_1, \dots, \bar{B}_m$ without persistent variables. We can assume w.l.o.g. that the 1-transitions of these automata are labeled by `emp`, because the only remaining equalities are between variables $y^{[\epsilon]}$ not associated with states and non-persistent variables $x^{[i]}$. In the following, let $\bar{B} = (\Sigma, \mathcal{Q}, \iota, \bar{\delta})$ be any of $\bar{B}_1, \dots, \bar{B}_m$ and $\bar{\delta} = \bar{\delta}^1 \uplus \bar{\delta}^\infty$ be the partition of its transitions into 1- and $\infty$-transitions (Definition 4.5). In order to obtain an expandable SID from $\bar{B}$, i.e., using Lemma 4.13 (2), we must be able to embed
any sequence of runs of $\bar{B}$ into a single run of $\bar{B}$. However, this is currently not possible, because the labels of the 1-transitions cannot be viewed as labels of $\infty$-transitions. The problem is shown by the following example:

**Example 4.30.** Consider two disjoint structures $S_1 = (U_1, \sigma_1)$, $S_2 = (U_2, \sigma_2) \in [\bar{B}]^c$, having the shape depicted in Figure 12 (b). Each $S_i$ has all but two elements, call them $e_i^1$ and $e_i^2$, labeled with a unary relation symbol $e_g$. Then, the composition $S_1 \bullet S_2$ will have four unlabeled elements $e_1^1, e_1^2, e_2^1$ and $e_2^2$. Since any structure $S = (U, \sigma) \in [\bar{B}]^c$ has exactly two unlabeled elements, the structure $S_1 \bullet S_2$ is not a substructure of $S$, according to Definition 3.7. This is because $e_1^1, e_2^1, e_2^2 \in (\text{supp}(\sigma_1) \cup \text{supp}(\sigma_2)) \setminus (\sigma_1(e_g) \uplus \sigma_2(e_g))$ are pairwise distinct, hence $\text{card}((\text{supp}(\sigma_1) \cup \text{supp}(\sigma_2)) \setminus (\sigma_1(e_g) \uplus \sigma_2(e_g))) = 4$, whereas $\text{card}(\text{supp}(\sigma) \setminus \sigma(e_g)) = 2$, independently of the choice of $S$.

For a $\Sigma$-labeled tree $t$, two positions $p$ and $s$, such that $p \in \text{dom}(t)$ (nothing is required about $s$), and a sequence of variables $x_1, \dots, x_k$, we define the formula:

$$ \Omega_t^{p/s}(x_1, \dots, x_k) \stackrel{\text{def}}{=} \ast \{r(x_1^{[s]}, \dots, x_k^{[s]}) \mid r(x_1^{[p_1]}, \dots, x_k^{[p_k]})\} \text{ occurs in } \Theta(t), x_i^{[p_i]} \approx_{\Theta(t)} x_i^{[p]}, \forall i \in [1..k] \} $$

For simplicity, assume, for each transition $q_0 \xrightarrow{\text{emp}} (q_1, \dots, q_\ell) \in \bar{\delta}^1$ of $\bar{B}$, that $q_0, \dots, q_\ell$ belong to non-trivial SCCs. If some $q_i$ belongs to a trivial SCC, i.e., with no transitions from $q_i$ to itself or other states in the same SCC, then $\#q_i$ must be zero, because all parameters from its profile have been removed by the previous transformation. In this case, the construction below is adapted by replacing the formulae $\Omega_{t_0}^{\epsilon/\epsilon}$ and $\Omega_{t_j}^{p_j/p_j}$ by $\text{emp}$, for the corresponding states that belong to trivial SCCs. The automaton $\mathcal{B}$ is obtained from $\bar{B}$ by replacing the label of each such 1-transition with the following formula, for some trees $t_i$ corresponding to resets $\theta_{p_i \leftarrow q_i}^i$ of $\bar{B}$, for $i \in [0..\ell]$:

$$ q_0 \xrightarrow{\ast_{i_1, \dots, i_k \in [1..\#q_0]} \Omega_{t_0}^{\epsilon/\epsilon}(x_{i_1}, \dots, x_{i_k}) \ast \ast_{j \in [1..\ell], i_1, \dots, i_k \in [1..\#q_j]} \Omega_{t_j}^{p_j/p_j}(x_{i_1}, \dots, x_{i_k})} (q_1, \dots, q_\ell) $$

Note that the existence of such resets is guaranteed by Lemma 4.18 and the previous assumption. This construction is illustrated by the following example:

**Example 4.31.** (continued from Example 4.26) The outcome of applying the above transformation to the automaton $\bar{B}$ from Example 4.26 is the automaton $\mathcal{B}$ given below:

$$ \mathcal{B} = \left\{ \begin{array}{ll} \tau_1 : (q_A, \emptyset) & \xrightarrow{e_g(x_1^{[1]})} ((q_{C_1}, a)) \qquad (1) \\ \tau_2 : (q_{C_1}, a) & \xrightarrow{e_g(x_1^{[\epsilon]}, y_4^{[\epsilon]}) \ast e_g(y_4^{[\epsilon]}) \ast y_4^{[\epsilon]} = x_1^{[1]}} ((q_{C_1}, a)) \qquad (\infty) \\ \tau_3 : (q_{C_1}, a) & \xrightarrow{e_g(x_1^{[1]})} ((q_{C_2}, a)) \qquad (1) \\ \tau_4 : (q_{C_2}, a) & \xrightarrow{e_g(x_1^{[\epsilon]}, y_6^{[\epsilon]}) \ast e_g(y_6^{[\epsilon]}) \ast y_6^{[\epsilon]} = x_1^{[1]}} ((q_{C_2}, a)) \qquad (\infty) \\ \tau_5 : (q_{C_2}, a) & \xrightarrow{\text{emp}} () \qquad (1) \end{array} \right. $$

The transformation adds the relation atoms $e_g(x_1^{[1]})$ to the labels of $\tau_1$ and $\tau_3$, respectively. Note that $\tau_2$ and $\tau_4$ are $(q_{C_1}, a)$- and $(q_{C_2}, a)$-resets, respectively. The added relation atoms correspond to the relation atoms that label the $x_1^{[1]}$ variable within the labels of these resets, taken backwards. All elements from a structure $S \in [\bar{B}]^c$ are now labeled by $e_g$, hence the composition of any sequence of structures from $[\bar{B}]^c$ can be embedded as a substructure of a structure from the same set. In other words, the SID obtained from $\mathcal{B}$ using Lemma 4.13 (2) is expandable (Definition 3.8).
The formal properties of $\mathcal{B}$ are stated and proved below:

**Lemma 4.32.**

(1) $\mathcal{B}$ is all-satisfiable,

(2) $\mathrm{tw}(\llbracket \mathcal{B} \rrbracket) \le \mathrm{tw}(\llbracket \overline{\mathcal{B}} \rrbracket) + \mathrm{card}(\bar{\delta}^1) \cdot \mathrm{maxVars}(\Delta),$

(3) $\mathrm{tw}(\llbracket \overline{\mathcal{B}} \rrbracket) \le \mathrm{tw}(\llbracket \mathcal{B} \rrbracket) + \mathrm{card}(\bar{\delta}^1) \cdot (1 + \mathrm{maxPredAtoms}(\Delta)) \cdot \mathrm{relNo}(\Delta) \cdot \mathrm{maxVars}(\Delta)^{\mathrm{maxRelArity}(\Delta)}.$

*Proof.* For space reasons, the proof of this lemma is given in subsection C.9. $\square$

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

**4.6. The Proof of Lemma 4.1.** We have collected all the ingredients needed to prove the decidability of the treewidth boundedness problem, for SLR formulæ interpreted over general SIDs. The key point is the proof of Lemma 4.1, the main result being an immediate consequence of this lemma and Theorem 3.33. To prove Lemma 4.1, we rely on Lemma 4.20, which states that any sequence of $\infty$-runs of a choice-free automaton can be disjointly embedded into an accepting run of the same automaton, such that any two of the embedded runs are separated by a given number of reset paths in the enclosing run.

Before proving Lemma 4.1, we state a property of the outcome of the above transformation of automata (Figure 14). This property uses the following notion:

**Definition 4.33.** Let $\mathcal{A}$ be a choice-free automaton. A view for $\mathcal{A}$ is a tuple $(\theta, t, \mathfrak{s}, S)$, such that $\theta \in \mathcal{R}_q^{\infty}(\mathcal{A})$ is a partial $\infty$-run over a $\Sigma$-labeled tree $t$, $\mathfrak{s}$ is a canonical store for $\Theta(t)$ and $S$ is a structure, such that $S \models^{\mathfrak{s}} \Theta(t)$. A structure $S' = (U', \sigma')$ is encapsulated by the view $(\theta, t, \mathfrak{s}, S)$ if (i) $S' \subseteq S$, (ii) $\mathrm{supp}(\sigma') \cap \mathfrak{s}(\{x_1^{[\epsilon]}, \dots, x_{\#\theta(\epsilon)}^{[\epsilon]}\}) = \emptyset$, and (iii) $\mathrm{supp}(\sigma') \cap \mathfrak{s}(\{x_1^{[p]}, \dots, x_{\#q}^{[p]}\}) = \emptyset$ if, moreover, the partial run $\theta$ is a $\theta_{p \leftarrow q}$ context.

Intuitively, a structure is encapsulated by a view if it is a substructure of the structure in the view and it does not “touch” the values of the variables from the root (resp. frontier) point of the partial run in the view.

Let $\mathcal{B}$ be any choice-free automaton resulting from the transformation in Figure 14. The following lemma shows that each canonical model from $\llbracket \mathcal{B} \rrbracket^c$ can be decomposed into pairwise disjoint structures, each of which being encapsulated by a separate view for $\mathcal{B}$:

**Lemma 4.34.** For each structure $S = (U, \sigma) \in \llbracket \mathcal{B} \rrbracket^c$, there exist pairwise disjoint structures $S_1, \dots, S_n$ and views $(\theta_1, t_1, \mathfrak{s}_1, S'_1), \dots, (\theta_n, t_n, \mathfrak{s}_n, S'_n)$ for $\mathcal{B}$ such that $S'_1, \dots, S'_n$ are pairwise disjoint, $S = S_1 \bullet \dots \bullet S_n$ and $S_i$ is encapsulated by $(\theta_i, t_i, \mathfrak{s}_i, S'_i)$, for each $i \in [1..n]$.

*Proof.* Let $\mathcal{B} \stackrel{\mathrm{def}}{=} (\Sigma, \mathcal{Q}, \iota, \delta)$. Since $S = (U, \sigma) \in \llbracket \mathcal{B} \rrbracket^c$, there exists a tree $t_0 \in \mathcal{L}(\mathcal{B})$ such that $S \models^{\mathfrak{s}_0} \Theta(t_0)$ for a store $\mathfrak{s}_0$, that is canonical for $\Theta(t_0)$. Let $\theta_0$ be an accepting run of $\mathcal{B}$ over $t_0$. Because $\mathcal{B}$ is choice-free, $\theta_0$ can be decomposed into (i) maximal partial runs $\theta_{01} \in \mathcal{R}_{r_1}^{\infty}(\mathcal{B}), \dots, \theta_{0n} \in \mathcal{R}_{r_n}^{\infty}(\mathcal{B})$ consisting of (arbitrarily many) connected $\infty$-transitions, and (ii) partial runs $\tau_1, \dots, \tau_m$ consisting of a single 1-transition each, such that $r_i$ is the state at the root of $\theta_{0i}$ and $q_i$ is the left-hand side of a 1-transition, for each $i \in [1..n]$. We refer to Figure 13 (a) for an illustration of the decomposition.

For every $i \in [1..n]$ we define $S_i$ as the substructure of $S$ constructed along the maximal partial run $\theta_{0i}$. That is, $S_i$ contains all the relation atoms defined on $\infty$-transitions in $\theta_{0i}$ and the relation atoms defined on the entering (and possibly exiting) 1-transition(s) involving common variables for entering (resp. exiting) state(s). Intuitively, all these relation atoms occur in the gray part in Figure 13 (a). Note that, since the 1-transitions of $\mathcal{B}$ do not equate variables $x_j^{[i]}$, for $i \in \mathbb{N} \cup \{\epsilon\}$, the structures $S_i$ are pairwise disjoint, and $S = S_1 \bullet \dots \bullet S_n$.
<figure><img src="image_22.png" /><figcaption>Figure 13: Run decomposition</figcaption></figure>

We build the views $\{\langle\theta_i, t_i, s_i, S'_i\rangle\}_{i\in[1..n]}$ as follows. For every $i \in [1..n]$, we define the partial run $\theta_i$ by extending the partial run $\theta_{0i}$ by the same $r_{i-}$ and $q_{i-}$ resets used in the transformation of $\bar{B}$ into $\mathcal{B}$ (note that the $q_{i-}$ reset is needed only if $\theta_{0i}$ reaches a 1-transition). This construction is illustrated in Figure 13 (b). Let $t_i$ be the $\Sigma$-labeled tree corresponding to the run $\theta_i$. Let $s_i$ be a canonical store for $\Theta(t_i)$ constructed by extending $s_0$ such that $s_0(x^{[p]}) = s_i(x^{[p']})$ whenever $p$ and $p'$ correspond to the same relative position within $\theta_{0i}$. In other words, $s_i$ preserves the elements occurring in $S_i$ and associates new distinct elements to all other variables introduced by the resets (in particular, all variables that are equated in $\Theta(t_i)$ are mapped to the same element). The store $s_i$ defines a structure $S'_i = (U, \sigma'_i)$, such that $S'_i \models^{s_i} \Theta(t_i)$, as $\sigma'_i(r) \stackrel{\text{def}}{=} \{\langle s_i(z_1^{[p_1]}), \dots, s_i(z_k^{[p_k]}) \rangle | r(z_1^{[p_1]}, \dots, z_k^{[p_k]}) \text{ occurs in } \Theta(t_i)\}$, for each relation symbol $r \in \mathbb{R}$. We prove below that $S_i$ is encapsulated by the view $\langle\theta_i, t_i, s_i, S'_i\rangle$:

* By the choice of $s_i$, that extends $s_0$ as explained above, we have $S_i \subseteq S'_i$. Moreover, no tuples are added to $S_i$ by the inserted resets, because the labeling of 1-transitions in $\mathcal{B}$ is constructed precisely from the resets that guarantee this property, i.e., the construction of $\mathcal{B}$ guarantees that the set of relation atoms occurring in the reset was used to label the 1-transitions. Thus, we have $S_i \subseteq S'_i$.

* By the construction of the partial run $\theta_i$, the set of variables $\{x_1^{[e]}, \dots, x_{\#r_i}^{[e]}\}$ in $\theta_i$ are not related by equalities to any of the variables at the root of $\theta_{0i}$ in $\Theta(t_i)$. In particular, this is ensured by the fact that $\mathcal{B}$ has no persistent variables. Since, $s_i$ is canonical for $\Theta(t_i)$, we obtain that $\text{supp}(\sigma_i) \cap \{s_i(\{x_1^{[e]}, \dots, x_{\#r_i}^{[e]}\})\} = \emptyset$. The same argument applies to the set of variables occurring at the frontier position of $\theta_i$, i.e., when $\theta_{0i}$ reaches the left-hand side $q_i$ of a 1-transition, as in Figure 13 (b). □

Dually, the following lemma gathers pairwise disjoint structures into a single rich canonical model, that meets the conditions of expandability (Definition 3.8):

**Lemma 4.35.** Let $S_1, \dots, S_n$ be pairwise disjoint structures encapsulated by the views $\langle\theta_1, t_1, s_1, S'_1\rangle, \dots, \langle\theta_n, t_n, s_n, S'_n\rangle$ for $\mathcal{B}$, where $S'_1, \dots, S'_n$ are also pairwise disjoint. Then, there exists a rich canonical model $(S, \mathcal{D}) \in [\mathcal{B}]^r$, such that the conditions (1), (2) and (3) from Definition 3.8 hold for $S_1, \dots, S_n$ and $(S, \mathcal{D})$.

*Proof.* Since $\mathcal{B}$ is a choice-free automaton, by Lemma 4.20, there exists an accepting run $\theta$ of $\mathcal{B}$ over a tree $t$, such that the following hold:
(a) each partial run $\theta_i$ is embedded in $\theta$ at some position $r_i \in \text{dom}(\theta)$, for all $i \in [1..n]$,

(b) $r_i \cdot \text{dom}(\theta_i) \cap r_j \cdot \text{dom}(\theta_j) = \emptyset$, for all $1 \le i < j \le n$,

(c) each path between the positions $r_i$ and $r_j$ traverses at least once some reset path, disjoint from $\bigcup_{k=1}^n r_k \cdot \text{dom}(\theta_k)$, for all $1 \le i < j \le n$.

For each $i \in [1..n]$, since $\langle \theta_i, t_i, \mathfrak{s}_i, \mathfrak{S}'_i \rangle$ is a view, we have $\mathfrak{S}'_i \models^{\mathfrak{s}_i} \Theta(t_i)$, hence $\mathfrak{s}_i(\text{fv}(\Theta(t_i))) \subseteq \text{supp}(\sigma'_i)$, where we assume w.l.o.g. that $\mathfrak{S}'_i \stackrel{\text{def}}{=} (\mathbb{U}, \sigma'_i)$. By point (b) above, the subformulæ corresponding to the subtrees of $t$ with domains $r_i \cdot \text{dom}(\theta_i)$, for $i \in [1..n]$, have disjoint sets of free variables. We define a store $\mathfrak{s}$ as follows, for each variable $x^{[p]} \in \text{fv}(\Theta(t))$:

▷ if $p = r_i p'$ and $p' \in \text{dom}(t_i)$, for some $i \in [1..n]$, then we set $\mathfrak{s}(x^{[p]}) \stackrel{\text{def}}{=} \mathfrak{s}_i(x^{[p']})$,

▷ otherwise, we chose a fresh value $\mathfrak{s}(x^{[p]})$, such that $\mathfrak{s}(x^{[p]}) \notin \bigcup_{i=1}^n \text{supp}(\sigma'_i)$ and $\mathfrak{s}(x^{[p]}) \neq \mathfrak{s}(z^{[r]})$, for each variable $z^{[r]}$, such that $x^{[p]} \not\approx_{\Theta(t)} z^{[r]}$.

By the fact that $\text{supp}(\sigma'_i) \cap \text{supp}(\sigma'_j) = \emptyset$, i.e., $\mathfrak{s}_i(\text{fv}(\Theta(t_i))) \cap \mathfrak{s}_j(\text{fv}(\Theta(t_j))) = \emptyset$, for all $1 \le i < j \le n$, and the construction of $\mathfrak{s}$, we obtain that $\mathfrak{s}$ is canonical for $\Theta(t)$. The store $\mathfrak{s}$ defines the structure $S = (\mathbb{U}, \sigma)$, as follows:

$$ \sigma(\mathbf{r}) \stackrel{\text{def}}{=} \{\langle \mathfrak{s}(z_1), \dots, \mathfrak{s}(z_{\#\mathbf{r}}) \rangle \mid \mathbf{r}(z_1, \dots, z_{\#\mathbf{r}}) \text{ occurs in } \Theta(t)\}, \text{ for all } \mathbf{r} \in \mathbb{R} $$

By the definition of $S$, we have $S \models^{\mathfrak{s}} \Theta(t)$. Moreover, we define the relation:

$$ \mathfrak{d} \stackrel{\text{def}}{=} \{ (\mathfrak{s}(x), \mathfrak{s}(y)) \mid x \neq y \text{ or } y \neq x \text{ occurs in } \Theta(t) \} $$

We have obtained a rich canonical model $(S, \mathfrak{d}) \in [\Theta(t)]^3$ and, since $t \in \mathcal{L}(\mathcal{B})$, we have $(S, \mathfrak{d}) \in [\mathcal{B}]^3$. We prove below the three conditions from Definition 3.8:

(1) By the construction of $S$, we have $\mathfrak{S}'_i \subseteq S$, for all $i \in [1..n]$. Since $S_1, \dots, S_n$ are pairwise disjoint, their composition is defined, hence $S_1 \bullet \dots \bullet S_n \subseteq \mathfrak{S}'_1 \bullet \dots \bullet \mathfrak{S}'_n \subseteq S$. W.l.o.g., let $S_i = (\mathbb{U}, \sigma_i)$, for all $i \in [1..n]$. To prove $S_1 \bullet \dots \bullet S_n \subseteq S$, by Definition 3.7, we must prove that:

$$ \sigma_1(\mathbf{r}) \uplus \dots \uplus \sigma_n(\mathbf{r}) = \{ \langle u_1, \dots, u_{\#\mathbf{r}} \rangle \in \sigma(\mathbf{r}) \mid u_1, \dots, u_{\#\mathbf{r}} \in \text{supp}(\sigma_1) \cup \dots \cup \text{supp}(\sigma_n) \} \quad (4.2) $$

The “$\subseteq$” direction follows from $S_1 \bullet \dots \bullet S_n \subseteq S$, hence we are left with proving the dual “$\supseteq$” direction. Let $\langle u_1, \dots, u_{\#\mathbf{r}} \rangle \in \sigma(\mathbf{r})$ be a tuple, such that $u_1, \dots, u_{\#\mathbf{r}} \in \bigcup_{i=1}^n \text{supp}(\sigma_i)$. By the definition of $\sigma$, there exists a relation atom $\mathbf{r}(z_1^{[p]}, \dots, z_{\#\mathbf{r}}^{[p]})$ in $\Theta(t)$, such that $\mathfrak{s}(z_i) = u_i$, for all $i \in [1..\#\mathbf{r}]$. To simplify matters, we assume that the position of each variable in the relation atom is the same, the case where these positions are either $p$ and $pi$, or $pi$ and $pj$, for some $p \in \mathbb{N}^*$ and $i \neq j \in \mathbb{N}$ is treated in a similar way and left to the reader. Moreover, for each $i \in [1..\#\mathbf{r}]$, there exists a unique $k_i \in [1..n]$, such that $u_i \in \text{supp}(\sigma_{k_i})$. Suppose, for a contradiction, that $k_i \neq k_j$, for some $1 \le i < j \le n$. Then, there exist paths between $p$ and some positions $s_i \in r_i \cdot \text{dom}(t_i)$ and $s_j \in r_j \cdot \text{dom}(t_j)$, such that $z_i^{[p]} \approx_{\Theta(t)} \xi_i^{[s_i]}$ and $z_j^{[p]} \approx_{\Theta(t)} \xi_j^{[s_j]}$. Consider the case where $\theta_i$ and $\theta_j$ are runs (the case where one of them is a context uses a similar argument and is left to the reader). Since $t_i$ and $t_j$ are embedded in $t$ at positions $r_i$ and $r_j$, respectively, at least one of these paths, say the one from $p$ to $s_i$, contains the position $r_i$. Then, there exists a variable $x_{\ell_i}^{[r_i]}$, for $\ell_i \in [1..\#\theta_i(\epsilon)]$, such that $\mathfrak{s}(x_{\ell_i}^{[r_i]}) = u_i$. Hence, $\text{supp}(\sigma_i) \cap \mathfrak{s}(\{x_1^{[r_i]}, \dots, x_{\#\theta_i(\epsilon)}^{[r_i]}\}) = \text{supp}(\sigma_i) \cap \mathfrak{s}_i(\{x_1^{[\epsilon]}, \dots, x_{\#\theta_i(\epsilon)}^{[\epsilon]}\}) \neq \emptyset$, in contradiction with the fact that $S_i$ is encapsulated by $\langle \theta_i, t_i, \mathfrak{s}_i, \mathfrak{S}'_i \rangle$, by condition (ii) of Definition 4.33. We obtained that $k_1 = \dots = k_{\#\mathbf{r}}$, hence $u_1, \dots, u_{\#\mathbf{r}} \in \text{supp}(\sigma_k)$, leading to $\langle u_1, \dots, u_{\#\mathbf{r}} \rangle \in \sigma_k(\mathbf{r})$, for some index $k \in [1..n]$.
This proves (4.2). Since the choice of $\mathbf{r}$ was arbitrary, we obtain that $S_1 \bullet \dots \bullet S_n \subseteq S$, by Definition 3.7.

(2) Suppose, for a contradiction, that there exists a pair $(u, v) \in \mathfrak{d}$, such that $u \in \text{supp}(\sigma_i)$ and $v \in \text{supp}(\sigma_j)$, for some indices $1 \le i < j \le n$. Then, there exists a disequality $x^{[p]} \ne y^{[p]}$ (or $y \ne x$, this case being symmetric) in $\Theta(t)$, such that $\mathfrak{s}(x^{[p]}) = u$ and $\mathfrak{s}(y^{[p]}) = v$. Since $u \in \text{supp}(\sigma_i)$, there exists a variable $\xi_i^{[p_i]}$ such that $p_i \in r_i \cdot \text{dom}(t_i)$ and $\mathfrak{s}(\xi_i^{[p_i]}) = u$. Since $\mathfrak{s}$ is canonical for $\Theta(t)$, we have $x \approx_{\Theta(t)} \xi_i^{[p_i]}$. Suppose, for a contradiction, that $p \notin r_i \cdot \text{dom}(t_i)$. Then, by a similar argument as the one used in the proof of point (1), we obtain a contradiction with condition (ii) of Definition 4.33, hence $p \in r_i \cdot \text{dom}(t_i)$. Symmetrically, we obtain $p \in r_j \cdot \text{dom}(t_j)$, hence $r_i \cdot \text{dom}(t_i) \cap r_j \cdot \text{dom}(t_j) \ne \emptyset$, which contradicts point (b) above.

(3) Suppose, for a contradiction, that there exists a relation symbol $\mathbf{r} \in \mathbb{R}$ and tuples $(u_1, \dots, u_{\#\mathbf{r}}), (v_1, \dots, v_{\#\mathbf{r}}) \in \sigma(\mathbf{r})$, such that $\{u_1, \dots, u_{\#\mathbf{r}}\} \cap \text{supp}(\sigma_i) \ne \emptyset$, $\{v_1, \dots, v_{\#\mathbf{r}}\} \cap \text{supp}(\sigma_j) \ne \emptyset$ and $\{u_1, \dots, u_{\#\mathbf{r}}\} \cap \{v_1, \dots, v_{\#\mathbf{r}}\} \ne \emptyset$, for some indices $1 \le i < j \le n$. Then, there exists two distinct relation atoms $\mathbf{r}(z_1^{[p_1]}, \dots, z_{\#\mathbf{r}}^{[p_1]})$ and $\mathbf{r}(z_1^{[p_2]}, \dots, z_{\#\mathbf{r}}^{[p_2]})$ in $\Theta(t)$ and variables $\xi_i^{[s_i]}$, $s_i \in r_i \cdot \text{dom}(t_i)$ and $\xi_j^{[s_j]}$, $s_j \in r_j \cdot \text{dom}(t_j)$, such that $z_k^{[p_1]} \approx_{\Theta(t)} \xi_i^{[s_i]}$, $z_k^{[p_2]} \approx_{\Theta(t)} \xi_j^{[s_j]}$, for some indices $k, \ell \in [1..\#\mathbf{r}]$. For simplicity, we consider that the position of the variables is the same in the above relation symbols, i.e., $p_1$ and $p_2$, respectively. By an argument similar to the one used in the proof of point (2), we obtain that $p_1 \in r_i \cdot \text{dom}(t_i)$ and $p_2 \in r_j \cdot \text{dom}(t_j)$. However, since $\{u_1, \dots, u_{\#\mathbf{r}}\} \cap \{v_1, \dots, v_{\#\mathbf{r}}\} \ne \emptyset$, there exist indices $g, h \in [1..\#\mathbf{r}]$ such that $z_g^{[p_1]} \approx_{\Theta(t)} z_h^{[p_2]}$. For simplicity, we consider the case where $\theta_i$ and $\theta_j$ are runs, the case where at least one of them is a context uses a similar argument being left to the reader. Then the path between $r_i$ and $r_j$ is contained with the path between $p_1$ and $p_2$. By point (c) above, this path contains a reset path disjoint from $\cup_{k=1}^n r_k \cdot \text{dom}(\theta_k)$. Since, moreover, $\mathcal{B}$ has no persistent variables, by construction, we obtain $z_g^{[p_1]} \not\approx_{\Theta(t)} z_h^{[p_2]}$, contradiction. $\square$

<figure><img src="image_23.png" /><figcaption>Figure 14: The Chain of Automata Transformations</figcaption></figure>

We are now ready to prove Lemma 4.1:

*Proof.* Let $\mathcal{A}_{\Delta,\mathbf{A}}$ be the $\Sigma$-labeled automaton corresponding to $\Delta$ and $\mathbf{A}$, such that $[[\mathcal{A}]]_{\Delta} = [[\mathcal{A}_{\Delta,\mathbf{A}}]]$, by Lemma 4.13 (1). The chain of transformations depicted in Figure 14 produces the set $\{\mathcal{B}_j^i\}_{i \in [1..n]}$, $j \in [1..m_i]$ of choice-free and all-satisfiable automata, such that $[[\mathcal{A}_{\Delta,\mathbf{A}}]]$ is treewidth bounded if and only if $[[\mathcal{B}_j^i]]$ is treewidth bounded, for each $i \in [1..n]$ and $j \in [1..m_i]$. In particular, $\mathcal{A}_{\Delta,\mathbf{A}}^1, \dots, \mathcal{A}_{\Delta,\mathbf{A}}^n$ is the language-preserving choice-free decomposition of $\mathcal{A}_{\Delta,\mathbf{A}}$ (Lemma 4.9) and $\bar{\mathcal{B}}_1^i, \dots, \bar{\mathcal{B}}_{m_i}^i$ are obtained by removing the persistent variables
from each automaton $\tilde{B}^i$ in the language-preserving choice-free decomposition of $(\tilde{\mathcal{A}}_{\Delta,A})^i$ (Lemma 4.28). We assume, without loss of generality, that the initial state of each $\mathcal{B}_j^i$ is $q_B$ and let $\Gamma_j^i$ be the SID, such that $[\mathcal{B}_j^i] = [[B]]_{\Gamma_j^i}$ and $[\mathcal{B}_j^i]' = [[B]]_{\Gamma_j^i}$, by Lemma 4.13 (2). We are left with proving that $\Gamma_j^i$ is expandable for $B$, for each $i \in [1..n]$ and $j \in [1..m_i]$. Let $\Gamma$ be any of the SIDs $\Gamma_1^1, \dots, \Gamma_{mn}^n$ and $\mathcal{B}$ be the automaton such that $[[\mathcal{B}]]_\Gamma = [[\mathcal{B}]]^c$, by Lemma 4.13 (2). Let $S_1, \dots, S_k \in [[\mathcal{B}]]_\Gamma^c$ be pairwise disjoint structures. By Lemma 4.34, for each $i \in [1..k]$ there exists a decomposition $S_i = S_1^i \bullet \dots \bullet S_{\ell_i}^i$ into pairwise disjoint structures, such that the structure $S_j^i$ is encapsulated by a view $\langle \theta_j^i, t_j^i, s_j^i, \bar{s}_j^i \rangle$ for $\mathcal{B}$, for each $i \in [1..k]$ and $j \in [1..\ell_i]$. Without loss of generality, we assume that the structures $\{\bar{s}_j^i\}_{i \in [1..k]}$, $j \in [1..\ell_i]$ are pairwise disjoint, hence the composition of $S_1^1, \dots, S_{\ell_n}^n$ is defined, thus we obtain $S_1 \bullet \dots \bullet S_k = S_1^1 \bullet \dots \bullet S_{\ell_n}^n$. By Lemma 4.35, there exists a rich canonical model $(S, \mathfrak{d}) \in [[\mathcal{B}]]^r$, such that conditions (1), (2) and (3) from Definition 3.8 hold for $S_1, \dots, S_{\ell_k}^k$ and $(S, \mathfrak{d})$. Since $[[\mathcal{B}]]^r = [[\mathcal{B}]]_\Gamma^c$, by Lemma 4.13 (2), $\Gamma$ is expandable for $B$. $\square$

**4.7. The Decidability of the Treewidth Boundedness Problem for SLR.** The proof of the main result (Theorem 4.36) uses a reduction of an arbitrary SID to a set of expandable SIDs, having an equivalent treewidth boundedness status (Lemma 4.1). Since treewidth boundedness is decidable for expandable SIDs (Theorem 3.33), this proves the decidability of the problem, in the general case. We conclude this section with the proof of the main result, that is the decidability of the TWB<sup>SLR</sup> problem, for unrestricted SIDs:

**Theorem 4.36.** There exists an algorithm that decides, for each SID $\Delta$ and nullary predicate $A$, whether the set $[[A]]_\Delta$ has bounded treewidth. If, moreover, this is the case, then $\mathrm{tw}([A]_\Delta) \le \max\mathrm{Vars}(\Delta) + N \cdot M$, where:

$$M \stackrel{\mathrm{def}}{=} 2 \cdot \max\mathrm{Vars}(\Delta) + (1 + \max\mathrm{PredAtoms}(\Delta)) \cdot \mathrm{relNo}(\Delta) \cdot \max\mathrm{Vars}(\Delta)^{\max\mathrm{RelArity}(\Delta)}$$

$$N \stackrel{\mathrm{def}}{=} \max(K, \max\mathrm{PredAtoms}(\Delta)^K)$$

$$K \stackrel{\mathrm{def}}{=} \mathrm{predNo}(\Delta) \cdot \mathrm{relNo}(\Delta) \cdot \max\mathrm{Vars}(\Delta)^{\max\mathrm{Vars}(\Delta)+\max\mathrm{RelArity}(\Delta)}$$

*Proof.* By Lemma 4.1, the treewidth boundedness problem for the set $[[A]]_\Delta$ can be effectively reduced to finitely many treewidth boundedness problems for sets $[[B]]_{\Gamma_1}, \dots, [[B]]_{\Gamma_k}$, where $\Gamma_1, \dots, \Gamma_k$ are expandable for $B$. The latter problem is decidable, by Theorem 3.33. The upper bound follows from the sequence of transformations given in Figure 14. Let $\Gamma$ be any of the expandable SIDs $\Gamma_1, \dots, \Gamma_k$. By Theorem 3.33, we have $\mathrm{tw}([B]_\Gamma) \le \max\mathrm{Vars}(\Delta)$. Note that the maximum number of variables occurring in a rule is not increased by the construction of $\Gamma$ from $\Delta$. By Lemma 4.23 (3), Lemma 4.25 (3), Lemma 4.29 (3) and Lemma 4.32 (3), we obtain $\mathrm{tw}([A]_\Delta) \le \mathrm{tw}([B]_\Gamma) + \mathrm{card}(\delta^1) \cdot M$, where $\delta^1$ is the set of 1-transitions of the choice-free automaton used to define $\Gamma$ (point (2) of Lemma 4.13) and $M = 2 \cdot \max\mathrm{Vars}(\Delta) + (1 + \max\mathrm{PredAtoms}(\Delta)) \cdot \mathrm{relNo}(\Delta) \cdot \max\mathrm{Vars}(\Delta)^{\max\mathrm{RelArity}(\Delta)}$. Note that $\mathrm{card}(\delta^1) \cdot M$ is the sum of the increases in the upper bounds of the treewidth along the transformation. By Lemma 4.9, we obtain $\mathrm{card}(\delta^1) \le \max(\mathrm{card}(Q_\Delta), \max\mathrm{PredAtoms}(\Delta)^{\mathrm{card}(Q_\Delta)})$, where $Q_\Delta$ denotes the set of states of $\mathcal{A}_{\Delta,A}$ (Lemma 4.13). Since the entire construction was done assuming that $\Delta$ is equality-free and all-satisfiable, by lifting these assumptions, we obtain $\mathrm{card}(Q_\Delta) \le \mathrm{predNo}(\Delta) \cdot \mathrm{relNo}(\Delta) \cdot \max\mathrm{Vars}(\Delta)^{\max\mathrm{Vars}(\Delta)+\max\mathrm{RelArity}(\Delta)}$ (Lemma 2.6 and Lemma 2.9). $\square$
Note that, unlike Theorem 3.33, that gives an optimal upper bound for the treewidths of the structures described by an expandable SID, Theorem 4.36 does not provide such an optimal upper bound. In particular, the upper bound of Theorem 4.36 grows doubly exponential in the $maxVars(\Delta)$ and $maxRelArity(\Delta)$ parameters and simply exponential in the $predNo(\Delta)$ and $relNo(\Delta)$ parameters. Finding an optimal bound for the general case is considered as subject for future work.

## 5. THE TREEWIDTH BOUNDEDNESS PROBLEM FOR FIRST ORDER LOGIC

This section proves the undecidability of the treewidth boundedness problem for first-order logic. This result places the frontier of decidability for this problem between the classical first-order logic and substructural SLR with simple inductive definitions, i.e., using only existentially quantified separating conjunctions of atoms.

We recall that the first-order logic (FO) is the set of formulæ consisting of equalities and relation atoms, connected by boolean conjunction, negation and existential quantification. The semantics of first order logic is given by the satisfaction relation $(U, \sigma) \Vdash^s \phi$ between structures and formulæ, parameterized by a store $s: \mathbb{V} \to \mathbb{U}$ such that $(U, \sigma) \Vdash^s r(x_1, \dots, x_{\#r})$ iff $\langle s(x_1), \dots, s(x_{\#r}) \rangle \in \sigma(r)$. If $\phi$ is a sentence the store is not important, thus we omit the superscript and write $S \Vdash \phi$ instead. The set of models of a FO sentence $\phi$ is denoted as $[[\phi]]^{\text{def}} = \{S \mid S \Vdash \phi\}$. Although we use the same notation for the sets of models of FO and SLR formulæ, the underlying logic is clear from the context.

This section is concerned with the proof of the following theorem:

**Theorem 5.1.** The problem is $[[\phi]]$ treewidth-bounded, for a given FO sentence $\phi$ with at least two binary relation symbols and several unary relation symbols, is undecidable.

*Proof.* We will reduce from the undecidability of the Tiling Problem [Ber66]. We first recall its definition. Given a finite set of tiles $S = \{t_1, \dots, t_n\}$ is there a tiling of the plane such that the colors of neighbouring tiles match? (We note that rotating or reflecting the tiles is not allowed.) In more detail: We assume the plane is given by integer coordinates $(x, y)$ with $x, y \in \mathbb{Z}$. We want to put a copy of a tile at every coordinate. We will require that neighbouring tiles match. For this we assume to be given a relation $H \subseteq S \times S$ specifying which tiles match can be placed next to each other horizontally – and $V \subseteq S \times S$ specifying which tiles match can be placed next to each other vertically. We now require for every tiling that $(t_i, t_j) \in H$, for all tiles $t_i$ and $t_j$ placed at coordinates $(x, y)$ and $(x+1, y)$, and $(t_i, t_j) \in V$, for all tiles $t_i$ and $t_j$ placed at coordinates $(x, y)$ and $(x, y+1)$. It is well-known that it is undecidable whether such a tiling exists [Ber66]. In fact, it is known that is already undecidable whether such a tiling exists for the upper-right quadrant of the plane, i.e., when coordinates $(x, y)$ are restricted to $x, y \in \mathbb{N}$.

We will now reduce the tiling problem to deciding whether a given first-order formula has infinitely many non-isomorphic models of unbounded treewidth. We consider some instance of the tiling problem. For encoding this problem, we define the signature $\mathbb{R} = \{\text{up}, \text{right}, \mathbb{N}, \mathcal{S}, \mathcal{E}, \mathcal{W}, \mathbb{I}, \mathcal{T}_1, \dots, \mathcal{T}_n\}$ to consist of the binary relations `up` and `right`, the unary relations $\mathcal{S}, \mathcal{E}, \mathcal{W}, \mathbb{N}, \mathbb{I}$ and the unary relations $\mathcal{T}_1, \dots, \mathcal{T}_n$ (one for each tile in the tiling instance). We then consider the following formula:

$$ \phi \stackrel{\text{def}}{=} \bigwedge_{i=1}^{13} \psi_i \wedge \bigwedge_{j=1}^{4} \phi_j $$

where: