# Iterating Non-Aggregative Structure Compositions

Marius Bozga, Radu Iosif, Florian Zuleger

► To cite this version:

Marius Bozga, Radu Iosif, Florian Zuleger. Iterating Non-Aggregative Structure Compositions. 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science FSTTCS 2025, Dec 2025, Goa, India. 10.4230/LIPIcs.CVIT.2016.23 . hal-05342996

HAL Id: hal-05342996

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

Submitted on 3 Nov 2025

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

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

<figure><img src="image_1.png" /></figure>
# Iterating Non-Aggregative Structure Compositions

Marius Bozga ⬒

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

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

Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France

Radu Iosif ⬒

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

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

Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France

Florian Zuleger ⬒

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

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

Institute of Logic and Computation, Technische Universität Wien, Austria

## Abstract

An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface.

In this paper, we study a non-aggregative composition operation, called *fusion*, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite *hyperedge-replacement* (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called *context-free*. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possibility of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.

2012 ACM Subject Classification • Theory of computation Logic Graph grammars

Keywords and phrases Hyperedge replacement, Tree-width

Digital Object Identifier 10.4230/LIPIcs.CVIT.2016.23

Related Version https://arxiv.org/abs/2510.06019

**Acknowledgements** Marius Bozga and Radu Iosif wish to acknowledge the support of the French National Research Agency project Non-Aggregative Resource Compositions (NARCO) under grant number ANR-21-CE48-0011. Florian Zuleger wishes to acknowledge the support of the FWF project AUTOSARD: "Automated Sublinear Amortised Resource Analysis of Data Structures" No. P36623 and the project VASSAL: "Verification and Analysis for Safety and Security of Applications in Life" funded by the European Union under Horizon Europe WIDERA Coordination and Support Action/Grant Agreement No. 101160022.

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

## 1 Introduction

The *tree-width* of a graph is a numerical measure of how “tree-like” the graph is. This notion extends naturally to the relational structures, used to define the semantics of classical first and second-order logic. Relational structures generalize a broad range of graph-like objects, such as edge-labeled graphs, hypergraphs, and multi-edge graphs. Tree-width plays a foundational role in logic and verification. Courcelle’s theorem [6] shows that *Monadic Second-order Logic (MSO)* is decidable on classes of structures having bounded tree-width, while Seese’s theorem [19] asserts that unbounded tree-width leads to undecidability of MSO

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

<figure><img src="image_10.png" /></figure>
## 23:2 Iterating Non-Aggregative Structure Compositions

theories. Thus, proving that a given class of structures has bounded tree-width is tantamount for establishing the decidability of logical theories for that class.

In principle, one is interested in reasoning about infinite families of structures. These families are typically generated inductively from a finite set of basic building blocks, using operations such as composition and renaming. These operations are usually formalized by the Hyperedge Replacement (HR) algebra introduced by Courcelle [8]. The principle of inductive definition is captured by the notion of a *context-free set*, i.e., the language of a finite grammar written using *HR* operations, or equivalently, the set of evaluations of a set of ground *HR* terms recognized by a tree automaton.

For both graphs and relational structures, HR algebras are built on *aggregative composition* operations, in which the whole is determined by the sum of its parts. These compositions are typically defined as the disjoint union of the arguments, where the elements designated by shared constants on both sides are joined together. In other words, aggregative composition preserves the identity of the substructures while merging them at known interface points. Importantly, context-free sets of graphs and relational structures defined by grammars based on such bounded-interface<fnref n="1" /> aggregative compositions have bounded tree-width.

In this paper, we investigate a more flexible but less controlled operation, called *non-aggregative fusion*. Fusion allows elements from two disjoint structures to be merged non-deterministically, even when they are not marked by constants. To maintain a certain level of semantic coherence, we require fusion to be constrained by a *coloring discipline*: elements can only be joined if their colors (i.e., sets of designated unary relations) are disjoint. This idea stems from existing work in the area of reasoning about the correctness of systems with dynamically reconfigurable connectivity, such as distributed protocols [1] or pointer structures with aliasing [15].

Due to its nondeterministic nature, fusion can cause a dramatic shift in structure: even if a set $S$ consists of structures having bounded tree-width, by taking the closure of $S$ under fusion one may introduce infinitely many structures of unbounded tree-width. This phenomenon raises two natural and fundamental questions:

1. Given a context-free set of relational structures, does the closure of this set under fusion have bounded tree-width ?

2. If the answer to the above question is yes, is this closure again a context-free set ?
The result this paper is that both questions have a positive answer (Theorem 9):

1. The existence of a bound on the tree-width of the closure by fusion of a context-free set is a decidable problem.

2. If the fusion-closure of context-free set has bounded tree-width, then it is the language of an effectively constructible context-free grammar, that uses only aggregative composition. These results provide tools for reasoning about nondeterministic structural iteration. For instance, one can check MSO properties over the tree-width bounded fusion-closure of a context-free set, thereby extending algorithmic verification techniques to a broader class of systems. We sketch below two possible application domains that have motivated our work. *Separation Logic of Relations (SLR)* A key motivation for studying non-aggregative fusion comes from SLR, a generalization of classical Separation Logic to relational structures. This logic has been first considered for relational databases and object-oriented languages [14]. More recently, SLR (combined with inductive definitions [12]) has been proposed as an assertion language for the verification of distributed reconfigurable systems [1]. Here, the

<footnote n="1">¹ Vertex-replacement algebras [8] using disjoint union and edge addition between arbitrarily large interfaces may produce sets of unbounded tree-width.</footnote>
separating conjunction $\phi * \psi$ means that the models of two formulæ $\phi$ and $\psi$ must not have overlapping interpretations of the same relation symbol.

A subtle but crucial point is that, while the separating conjunction enforces *disjointness* of the tuples that interpret a relation symbol, i.e., that tuples cannot overlap in *all* positions, the tuples may overlap in *some* positions. However, by the disjointness of *, such overlapping is only possible if the variables at these positions do not occur within the same unary relation symbol <fnref n="2" />. From a semantic point of view, this behavior corresponds precisely to our notion of fusion: joining elements of two separate structures is allowed, as long as their sets of unary relation labels are disjoint. Thus, fusion abstracts the semantics of SLR, where aliasing is controlled implicitly by colors (i.e., sets of relation symbols) and the semantics of the separating conjunction. Moreover, considering inductive definitions on top of the basic SLR logic is akin to considering context-free sets generated by recursive grammars here.

*Chemical and Biological Systems* We believe that fusion-like operations naturally arise in the modeling of chemical and biological systems, where complex structures (e.g., proteins or polymeric carbon chains) are formed by joining smaller components through local interactions. Here non-aggregative fusion abstracts the joining of components not only at fixed attachment points, but also through general, property-based interactions, modeled via color compatibility in our framework. Studying the tree-width of these structures is essential for enabling automated reasoning about their properties. We consider the exploration of this area as future work.

## Related Work

The notion of composition is central to substructural logics [17]. One of the foremost such logics is Bunched Implications (BI), whose first definition of semantics is based on partially ordered monoids (i.e., the multiplicative connective is interpreted as the multiplication in the monoid) [16]. In particular, the monoidal semantics of BI (and many other follow-up logics) do not assume the composition to be aggregative. The advent of the more popular semantics of BI based on finite partial functions, called heaps, has made aggregative composition popular among the users of Separation Logic [13, 18]. We list below several substructural logics where composition is not aggregative.

Docherty and Pym developed Intuitionistic Layered Graph Logic (ILGL), a substructural logic tailored to reasoning about graph structures with a fixed, non-commutative and non-associative notion of layering [9]. Calcagno et al. [2] introduce Context Logic as a framework for local reasoning about structured data, emphasizing compositionality through structural connectives that describe data and context separately rather than flattening them into aggregates. In [3], they formalize these connectives as modal operators and demonstrate that such non-aggregative reasoning is essential for expressing weakest preconditions and verifying updates. Cardelli et al. [4] present a spatial logic for reasoning about graphs that, like our work, emphasizes local, non-aggregative composition via structural connectives such as spatial conjunction.

## 2 Definitions

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. By writing $B \subseteq_{\text{fin}} A$ we mean that $B$

<footnote n="2">² For each unary relation symbol $r$ in the alphabet, the SLR formula $r(x) * r(y)$ entails $x \neq y$.</footnote>
23:4 Iterating Non-Aggregative Structure Compositions

is a finite subset of A. The cardinality of a finite (multi)set A is written card(A). By writing
$A = A_1 \uplus A_2$ we mean that $A_1$ and $A_2$ partition A, i.e., $A = A_1 \cup A_2$ and $A_1 \cap A_2 = \emptyset$.
The n-times Cartesian product of A with itself is denoted $A^n$ and the set of possibly empty
(resp. nonempty) sequences of elements from A by $A^*$ (resp. $A^+$). Multisets are denoted as
$\{a, b, \dots\}$, $\sqcup$ and $\sqcap$ denote the operations of multiset union and intersection, respectively.
The multi-powerset (i.e., the set of multisets) of A is written mpow(A).

2.1 Relational Structures

Let $\mathbb{R}$ be a finite alphabet of relation symbols $r \in \mathbb{R}$, of arities $\#r \ge 1$, and $\mathbb{C}$ be a countably infinite set of constants $c \in \mathbb{C}$ of arity zero. As usual, relation symbols of arity 1, 2 and 3 are called unary, binary and ternary, respectively. A $C$-structure, for some finite set $C \subseteq_{fin} \mathbb{C}$ of constants, is a pair $S = (U_S, \sigma_S)$, where $U_S$ is a finite set called universe and $\sigma_S$ is an interpretation that maps each relation symbol $r \in \mathbb{R}$ to a subset of $U_S^{\#r}$ and each constant $c \in C$ to an element of $U_S$. The sort of the structure $S$ is the set $C$. Two structures are disjoint iff their universes are disjoint and isomorphic iff they are defined over the same alphabet and differ only by a renaming of their elements$^3$. For a given sort $C \subseteq_{fin} \mathbb{C}$, we denote by $S(C)$ the set of $C$-structures.

We define the composition of two relational structures as the component-wise union of disjoint isomorphic copies of the structures followed by joining the elements that interpret the common constants. This is the same as the gluing operation defined by Courcelle [7, Definition 2.1], that we recall below, for self-completeness:

**Definition 1.** Let $S \in S(C)$ be a structure and $\sim \subseteq U_S \times U_S$ be an equivalence relation, where $[u]_\sim$ denotes the equivalence class of $u \in U_S$. The quotient of $S$ with respect to $\sim$ is the $C$-structure $S_\sim$ defined as follows:

$$
\begin{align*}
U_{S_\sim} &\stackrel{\text{def}}{=} \{[u]_\sim \mid u \in U_S\} \\
\sigma_{S_\sim}(r) &\stackrel{\text{def}}{=} \{([u_1]_\sim, \dots, [u_{\#r}]_\sim) \mid (u_1, \dots, u_{\#r}) \in \sigma_S(r)\}, \text{ for each } r \in \mathbb{R} \\
\sigma_{S_\sim}(c) &\stackrel{\text{def}}{=} [\sigma_S(c)]_\sim, \text{ for each } c \in C
\end{align*}
$$

Let $S_i = (U_i, \sigma_i)$ be disjoint $C_i$-structures, for $i = 1, 2$, and $\approx \subseteq (U_1 \uplus U_2) \times (U_1 \uplus U_2)$ be the least equivalence relation such that $\sigma_1(c) \approx \sigma_2(c)$, for all $c \in C_1 \cap C_2$. The composition of $S_1$ with $S_2$ is the $C_1 \cup C_2$-structure $S_1 * S_2 = (U, \sigma)$, where:

$$
\begin{align*}
U &\stackrel{\text{def}}{=} \{[u] \approx | u \in U_1 \uplus U_2\} \\
\sigma(r) &\stackrel{\text{def}}{=} \{([u_1] \approx, \dots, [u_{\#r}] \approx) \mid (u_1, \dots, u_{\#r}) \in \sigma_1(r) \uplus \sigma_2(r)\}, \text{ for each } r \in \mathbb{R} \\
\sigma(c) &\stackrel{\text{def}}{=} [\sigma_i(c)] \approx, \text{ if } c \in C_i, \text{ for each } c \in C_1 \cup C_2 \quad (\text{i.e., } [\sigma_1(c)] \approx = [\sigma_2(c)] \approx \text{ if } c \in C_1 \cap C_2)
\end{align*}
$$

We remark that the composition of $\emptyset$-structures $S_1$ and $S_2$ is the same as their disjoint union,
denoted $S_1 \uplus S_2$.

The composition of structures is *aggregative*, meaning that it keeps both structures separate except for the interpretation of the common constants. In the following, we define a non-aggregative *fusion* operation that matches also some of the elements which are not interpretations of common constants. In contrast to the deterministic composition, the equivalence relation that matches elements in the fusion operation is chosen nondeterministically.

<footnote n="3">³ See, e.g., [10, Section A3] for a formal definition of isomorphism between structures.</footnote>
Before formalizing the notion of non-aggregative fusion, we introduce a generic mechanism for controlling which pairs of elements are allowed to join. We assume a designated set of unary relation symbols $\mathcal{C} \subseteq \mathbb{R}$. The sets of relation symbols $\gamma \in \text{pow}(\mathcal{C})$ are called colors. Given some $\mathcal{C}$-structure $S = (U_S, \sigma_S)$, we denote by $\text{col}_S(u) = \{r \in \mathcal{C} | u \in \sigma_S(r)\}$ the color of each element $u \in U_S$. Note that the empty set is a color.

Back to the definition of non-aggregative fusion, we use colors to prevent joining elements labeled with non-disjoint colors. This is captured by the following notion of compatibility:

**Definition 2.** Let $S = (U, \sigma)$ be a $\mathcal{C}$-structure. A relation $\sim \subseteq U \times U$ is compatible with $S$ if and only if $\text{col}_S(u_1) \cap \text{col}_S(u_2) = \emptyset$, for each pair $u_1 \sim u_2$.

We now define the non-aggregative fusion operation. The operation is non-deterministic, i.e., returns a (possibly empty) set of structures. For reasons of simplicity, the fusion operation is only defined for structures of sort $\emptyset$, i.e., for structures that do not interpret any constants. This restriction can be lifted at the expense of complexifying the definition below, by considering fusion in which the interpretation of common constants in both structures must always be joined, as in Definition 1.

Given disjoint sets $A$ and $B$, a relation $\sim \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 \sim$. The least equivalence relation that contains $\sim$ is denoted $\equiv_{\sim} \subseteq (A \uplus B) \times (A \uplus B)$. We say that an equivalence relation $\equiv_{\sim}$ is $k$-generated iff $\sim$ is a matching consisting of $k$ pairs.

**Definition 3.** Let $S_i = (U_i, \sigma_i)$, for $i = 1, 2$, be two disjoint $\emptyset$-structures. The fusion of $S_1$ and $S_2$ is the following set of $\emptyset$-structures:

$$F(S_1, S_2) \stackrel{\text{def}}{=} \{(S_1 * S_2)/\equiv_{\sim} | \sim \text{ non-empty } U_1-U_2 \text{ matching compatible with } S_1 * S_2\}$$

Let $S$ be a set of $\emptyset$-structures. The closure of $S$ under fusion is the least set $F^*(S)$ such that $S \cup \{F(S_1, S_2) | S_1, S_2 \in F^*(S)\} \subseteq F^*(S)$.

Note that $F(S_1, S_2) = \emptyset$ iff $\text{col}_{S_1}(u_1) \cap \text{col}_{S_1}(u_2) \neq \emptyset$, for all pairs $(u_1, u_2) \in U_1 \times U_2$. The problems considered in the rest of this paper concern the uses of fusion, in addition to the composition and the unary operations on structures introduced next.

## 2.2 An Algebra of Structures

We recall the definitions of sorted terms and algebras [6, Definition 1.1]. Let $\Sigma$ be a countably infinite set of sorts and let $\mathbb{F}$ be a countably infinite set of function symbols, where the set $\mathbb{F}$ is called a signature. Each $f \in \mathbb{F}$ has an associated tuple of argument sorts $\alpha(f)$ and a value sort $\rho(f)$. The arity of $f$, denoted $\#f$, is the length of $\alpha(f)$. Moreover, each variable has a sort. A $\mathbb{F}$-term $t[x_1, \dots, x_n]$ is built as usual from function symbols and variables $x_1, \dots, x_n$ of matching sorts. A ground term is a term without variables. A trivial term consists of a single variable. A term $t'$ is a subterm of $t$ iff there exists a term $u[x]$ such that $t = u[t']$, where $u[t']$ denotes the replacement of $x$ by $t'$ in $u$. The sort of a term $t$, denoted $\rho(t)$ is the value sort of the top-most symbol, i.e., either the value sort $\rho(f)$ of the top-most function symbol $f$, in case of a non-trivial term $t$, or the sort $\rho(x)$ of the variable $x$, in case of a trivial term $x$. A position $p$ in a term $t$ is a node of the tree that uniquely represents $t$, in the usual way (see [5] for a formal definition). $T(\mathbb{F})$ denotes the set of ground terms having function symbols taken from a finite set $\mathcal{F} \subseteq_{\text{fin}} \mathbb{F}$.

An $\mathbb{F}$-algebra $\mathcal{A} = (\{A_s\}_{s \in \Sigma}, \{f^A\}_{f \in \mathbb{F}})$ consists of domains $A_s$ of each sort $s \in \Sigma$ and interprets the function symbols $f \in \mathbb{F}$ as functions $f^A : A_{s_1} \times \dots \times A_{s_n} \to A_{\rho(f)}$, where
23:6 Iterating Non-Aggregative Structure Compositions

$\alpha(f) = (s_1, \dots, s_n)$. By the domain of $\mathcal{A}$ we understand the set $\mathcal{A} = \bigcup_{s \in \Sigma} \mathcal{A}_s$. We denote by $t^A$ the interpretation of an $\mathbb{F}$-term $t$ in $\mathcal{A}$, i.e., the function obtained by replacing each function symbol that occurs in $t$ by its interpretation. In particular, $t^A$ is an element of the domain of $\mathcal{A}$ if $t$ is ground.

We define an algebra of structures, called $\mathcal{HR}$, with sorts $\Sigma_{\mathcal{HR}} \stackrel{\text{def}}{=} \{C \mid C \subseteq_{\text{fin}} C\}$, where each universe $\mathbb{HR}$ is the set of $C$-structures. The signature $\mathbb{F}_{\mathcal{HR}}$ consists of:

- constant symbols $r(C_1, \dots, C_{\#r})$, for $r \in \mathbb{R}$ and $C_i \subseteq_{\text{fin}} \mathbb{C}$ such that either $C_i = C_j$ or $C_i \cap C_j = \emptyset$ for all $1 \le i < j \le \#r$, interpreted as $r(C_1, \dots, C_{\#r})^{\mathcal{HR}} \stackrel{\text{def}}{=} (\mathbb{U}, \sigma)$, where:

$$ U \stackrel{\text{def}}{=} \{u_1, \dots, u_{\#r}\} \quad \text{for some (possibly equal) elements } u_1, \dots, u_{\#r} \\ \text{such that } u_i = u_j \iff C_i = C_j, \text{ for all } 1 \le i < j \le \#r $$

$$ \sigma(r) \stackrel{\text{def}}{=} \{(u_1, \dots, u_{\#r})\} \text{ and } \sigma(r') \stackrel{\text{def}}{=} \emptyset, \text{ for all } r' \in \mathbb{R} \setminus \{r\} $$

$$ \sigma(c) \stackrel{\text{def}}{=} u_i, \text{ for all } c \in C_i \text{ and } 1 \le i \le \#r $$

- binary function symbols $\oplus_{c,c'}$, for $C, C' \subseteq_{\text{fin}} \mathbb{C}$, interpreted by the composition operation $*$ from Definition 1 applied to structures of sorts $C$ and $C'$, respectively, see Figure 1 (a).

- unary function symbols $\text{rename}_c^\alpha$, for all $C, C' \subseteq_{\text{fin}} \mathbb{C}$ and surjective function $\alpha : C \to C'$, interpreted as the operations $\text{rename}_c^\alpha$ : $\mathbb{HR}_C \to \mathbb{HR}_{C'}$ where, for each $C$-structure $S$, the output $S' = \text{rename}_c^\alpha(S)$ is defined below:

$$ U_{S'} \stackrel{\text{def}}{=} U_S \quad \sigma_{S'}(r) \stackrel{\text{def}}{=} \sigma_S(r) \quad \sigma_{S'}(\alpha(c)) \stackrel{\text{def}}{=} \sigma_S(c), \text{ for all } r \in \mathbb{R} \text{ and } c \in C \setminus C' $$

- unary function symbols $\text{forget}_c^{c'}$, for $C \subseteq_{\text{fin}} \mathbb{C}$ and $C' \subseteq C$, interpreted as the operations $\text{forget}_c^{c'}$ : $\mathbb{HR}_C \to \mathbb{HR}_{C'}$ where, for each $C$-structure $S$, the output $S' = \text{forget}_c^{c'}(S)$ is defined below:

$$ U_{S'} \stackrel{\text{def}}{=} U_S \quad \sigma_{S'}(r) \stackrel{\text{def}}{=} \sigma_S(r) \quad \sigma_{S'}(c) \stackrel{\text{def}}{=} \sigma_S(c), \text{ for all } r \in \mathbb{R} \text{ and } c \in C $$

To ease the notation, we omit the sorts of the arguments from the $\mathcal{HR}$ function symbols $\mathbb{F}_{\mathcal{HR}}$ when they are understood from the context.

**► Example 4.** The two leftmost graphs in Figure 1 (a) are the values of the following terms, respectively (singleton sets are denoted by their elements, to avoid clutter):

$$ t_1 \stackrel{\text{def}}{=} \text{rename}_{c^3 \to c^1} (\text{forget}_{c^1} (a(c_0, c_1, c_2) \oplus c(c_1, c_3)) \oplus b(c_0, c_3)) $$

$$ t_2 \stackrel{\text{def}}{=} b(c_0, c_1) \oplus \text{forget}_{c^2} (a(c_1, c_3, c_2)) $$

The graph in Figure 1 (c) is the value of the term $t_0 \stackrel{\text{def}}{=} \text{rename}_{c^0 \leftrightarrow c^1} (\text{forget}_{c^2} (t_1 \oplus t_2))$.

We comment on the relationship to the algebra of relational structures introduced in [7, Definition 2.3], as a generalization of both the hyperedge-replacement (HR) algebra of hypergraphs and the vertex-replacement (VR) algebra of binary graphs, to relational structures. As a matter of fact, we do not use this algebra. Instead, our algebra of relational structures algebra $\mathcal{HR}$ follows the standard HR algebra on hypergraphs [6]. This relationship can be easily understood by viewing relational structures as hypergraphs in the adjacency encoding, i.e., each tuple $(u_1, \dots, u_{\#r})$ from the interpretation of a relation symbol $r$ corresponds to a $r$-labeled hyperedge attached to the vertices $u_1, \dots, u_{\#r}$ in this order. For reasons of space, we omit further details.

We now introduce the subalgebras of $\mathcal{HR}$ that define the tree-width parameter of a structure. For this, we assume some enumeration of the constants $\mathbb{C} = \{c_0, c_1, \dots\}$ and denote by $\mathbb{F}_{\mathcal{HR}} \le_k$ the subset of $\mathbb{F}_{\mathcal{HR}}$ consisting of the function symbols whose argument and value sorts are all contained in $\{c_0, \dots, c_k\}$.
<figure><img src="image_11.png" /><figcaption>■ **Figure 1** HR operations on structures over the alphabet $\{a, b, c\}$, where $\#a = 3$ and $\#b = \#c = 2$. The order of vertices attached to an edge is indicated by an arrow pointing to the last vertex.</figcaption></figure>

**► Definition 5.** The tree-width of a structure $\mathbf{S}$, denoted $\text{tw}(\mathbf{S})$, is the minimal integer $k \ge 0$ for which there exists a ground term $t \in \mathcal{T}(\mathbb{F}_{HR \le k})$ such that $t^{HR} = \mathbf{S}$. A set $\mathbf{S}$ of structures has bounded tree-width if and only if the set $\{\text{tw}(\mathbf{S}) \mid \mathbf{S} \in \mathcal{S}\}$ is finite.

In particular, for each tree-width bounded set $\mathbf{S}$, there exists a set $\mathcal{T}$ of ground terms and a finite set $\mathcal{C} \subseteq_{\text{fin}} \mathbb{C}$ of constants such that each term $t \in \mathcal{T}$ uses only constants from $\mathcal{C}$ and $\mathbf{S} = \{t^{HR} \mid t \in \mathcal{T}\}$.

This algebraic definition of tree-width of a relational structure is analogous to the definition of the tree-width of a hypergraph using a subalgebra of HR defined by a restriction of sorts to finite sets of vertex labels (see, e.g., [8, Proposition 1.19] for a proof of equivalence between the graph-theoretic and algebraic definitions of tree-width for hypergraphs). Moreover, the tree-width of a structure can be equivalently defined in terms of the tree-width of its Gaifman-graph:

**► Definition 6.** Let $\mathbf{S}$ be a $\mathcal{C}$-structure. The Gaifman graph of $\mathbf{S}$ is the simple undirected graph $\text{Gaif}(\mathbf{S}) = (V, E)$, where $V^\text{def} = U_\mathbf{S}$ and $E^\text{def} = \{\{u_i, u_j\} \mid (u_1, \dots, u_{\#r}) \in \sigma_\mathbf{S}(r), 1 \le i \ne j \le \#r, r \in \mathbb{R}\}$.

It is known that the tree-width of a structure equals the tree-width of its Gaifman graph [11, Proposition 11.27].

We recall below two standard notions of graph theory. Given binary graphs $G$ and $H$, we say that $H$ is a minor of $G$ iff $H$ is obtained from a subgraph of $G$ by edge contractions, where the contraction of a binary edge $e \in E_G$ attached to vertices $u$ and $v$ means deleting $e$ and joining $u$ and $v$ into a single vertex $x$ (the edges attached to $x$ are the ones attached to either $u$ or $v$). It is well-known that the tree-width of each minor of a graph $G$ is bounded by the tree-width of $G$.

A $n \times m$-grid is a binary graph whose vertices can be labeled with pairs $(i, j) \in [1..n] \times [1..m]$ such that there is an edge between $(i, j)$ and $(i', j')$ iff either $i < n$, $i' = i + 1$ and $j' = j$ or $j < m$, $i' = i$ and $j' = j + 1$. It is well-known<fnref n="4" /> that each $n \times n$-grid has tree-width $n$. By bluring the distinction between isomorphic grids, we obtain the following:

**► Proposition 7.** A set of structures whose Gaifman graphs contain infinitely many non-isomorphic square grids has unbounded tree-width.

## 2.3 Context-Free Sets of Structures

Context-free sets are usually defined as languages of grammars, i.e., finite sets of inductive rules written using nonterminals and function symbols from a given signature. To simplify some of the upcoming proofs, we use here an equivalent definition of context-free sets based on recognisable sets of ground terms, defined using tree automata [5]. For self-containment reasons, we briefly introduce context-free grammars and discuss their equivalence with tree automata in Section 3.5 (see the statement of Theorem 24).

<footnote n="4">⁴ This can be shown by using the characterisation of tree-width in terms of the cops and robber game [20].</footnote>
23:8 Iterating Non-Aggregative Structure Compositions

Let $\mathcal{F} \subseteq_{fin} \mathbb{F}$ be a finite signature of function symbols. A tree automaton over $\mathcal{F}$ is a tuple $\mathcal{A} = (Q, F, \rightarrow)$, where $Q$ is a finite set of states, $F \subseteq Q$ is a set of accepting states and $\rightarrow$ is a set of transition rules of the form $(q_1, \dots, q_{\#f}) \stackrel{f}{\rightarrow} q$, where $q_1, \dots, q_{\#f}, q \in Q$ and $f \in \mathcal{F}$. A run $\pi \in \mathcal{A}$ over a ground term $t \in \mathcal{T}(\mathcal{F})$ maps each position $p$ within $t$ to a state $q = \pi(p)$ if the automaton has a rule $(\pi(p_1), \dots, \pi(p_{\#f})) \stackrel{f}{\rightarrow} q$, where $p_1, \dots, p_{\#f}$ are the positions of the children of $p$ in $t$. A ground term $t$ is accepted by $\mathcal{A}$ iff $\mathcal{A}$ has a run that labels the root of $t$ with an accepting state. The language of $\mathcal{A}$, denoted $\mathcal{L}(\mathcal{A})$, is the set of ground terms accepted by $\mathcal{A}$. A set $T \subseteq \mathcal{T}(\mathcal{F})$ is recognisable iff it is the language of a tree automaton over the finite signature $\mathcal{F}$.

**Definition 8.** A set $\mathbf{S}$ of structures is context-free if and only if there exists a recognisable set of ground terms $T \subseteq \mathcal{T}(\mathcal{F})$, over a finite signature $\mathcal{F} \subseteq \mathbb{F}_{HR}$, such that $\mathbf{S} = \{t^{HR} \mid t \in T\}$.

Note that a context-free set of structures has finitely many sorts, because the signature of terms used to describe the set is finite. For this reason, any context-free set of structures has bounded tree-width. On the other hand, there are bounded tree-width sets which are not context-free, for instance the set of linear structures over the alphabet $\{a, b, c\}$ of binary relations of the form $a^n b^n c^n$, for all $n \ge 1$.

3 The Closure of Context-Free Sets under Fusion

This section is concerned with the statement and proof of the main result of the paper (Theorem 9). For simplicity, we assume that $\mathbf{S}$ is a set of *connected* structures, where connectivity of a structure $\mathbf{S}$ means that there exists an undirected path in $\mathbf{Gaif}(\mathbf{S})$ between each pair of elements $u_1, u_2 \in \mathcal{U}_\mathbf{S}$. We note that, because $\mathbf{S}$ contains only connected structures, each structure from its closure $\mathbf{F}^*(\mathbf{S})$ is necessarily connected.

The assumption of $\mathbf{S}$ being a context-free set of connected structures loses no generality, because it is possible, from a tree automaton $\mathcal{A}$ such that $\mathbf{S} = \mathcal{L}(\mathcal{A})^{HR}$, to build a tree automaton $\mathcal{B}$ such that $\mathcal{L}(\mathcal{B})^{HR}$ is the set of connected substructures of a structure in $\mathbf{S}$. Intuitively, $\mathcal{B}$ is obtained from $\mathcal{A}$ be labeling each state $q$ with finite information concerning the existence of a path between each pair of constant symbols in each structure that is the value of a ground term recognized by $q$ in $\mathcal{A}$. This construction can be used to generalize the statement of Theorem 9 below from connected to arbitrary structures. We will detail this construction in an extended version of the present article.

**Theorem 9.** Let $\mathbf{S}$ be a context-free set of connected $\emptyset$-structures.

1. $\mathbf{F}^*(\mathbf{S})$ has bounded tree-width if and only if $\mathbf{F}^*(\mathbf{S})$ is context-free.

2. It is decidable whether $\mathbf{F}^*(\mathbf{S})$ has bounded tree-width.

An obvious consequence of this theorem is the decidability of the problem: *given a context-free set $\mathbf{S}$, is $\mathbf{F}^*(\mathbf{S})$ context-free?*

We give an overview of the proof before going into technical details. The core idea is the equivalence between the (A) tree-width boundedness of the closure $\mathbf{F}^*(\mathbf{S})$ of a context-free set $\mathbf{S}$ and (B) the non-existence of two structures $S_1, S_2 \in \mathbf{F}^*(\mathbf{S})$ having each at least three elements each $u_i, v_i, w_i \in \mathcal{U}_{S_i}$, labeled with disjoint colors $\gamma_i$, for $i = 1, 2$. This equivalence is established via a third, more technical, condition about the disjointness relations between the colors that may occur in a structure from $\mathbf{F}^*(\mathbf{S})$. The latter implies that the matching relation of each fusion of two structures from $\mathbf{F}^*(\mathbf{S})$ is generated by at most two pairs of elements with compatible colors.

The equivalence between (A) and (B) is used to prove both points of Theorem 9. For point (1) suppose, for a contradiction, that (B) does not hold. Then, $S_1$ and $S_2$ can be
<figure><img src="image_12.png" /><figcaption>Figure 2 Building structures whose Gaifman graphs have infinitely large grid minors</figcaption></figure>

composed by joining their $u_i$, $v_i$ or $w_i$ elements, for $i = 1, 2$, respectively, as in Figure 2. Consequently, the set of Gaifman graphs corresponding to the structures in $F^*(S)$ contains an infinite set of grid minors, thus $F^*(S)$ has unbounded tree-width (Proposition 7). Else, if (B) holds (i.e., such structures cannot be found), we prove that the matching relation considered in the fusion of any two structures is generated by either one or two pairs of elements. In each of these cases, by adding a finite number of constants to the signature of the $F_{HR}$-terms from the language of $A$, we can build a tree automaton $A^*$ such that $L(A^*)^{HR} = F^*(S)$, thus taking care of point (1) of the theorem.

To prove point (2), we rely on the equivalence of (A) and (B) and show that (B) is decidable. This is done by arguing that the existence of two structures with the above property is equivalent to the existence of two multiset abstractions of structures $\{\gamma_1, \gamma_1, \gamma_1\}$, $\{\gamma_2, \gamma_2, \gamma_2\}$ in the domain of multisets of colors having multiplicity at most three. These multiset abstractions of colors can be effectively computed by a finite fixpoint iteration over the rules of the tree automaton that recognizes the set of ground terms which evaluates to the elements of $S$.

## 3.1 Color Multisets

In the following, let $S$ be a context-free set of $\emptyset$-structures. We denote the set of colors by $\Gamma \stackrel{\text{def}}{=} \text{pow}(\mathcal{C})$, where $\mathcal{C}$ is a fixed finite set of unary relation symbols. First, we define an abstraction of structures as finite multisets of colors:

**Definition 10.** The multiset color abstraction $S^\# \in \text{mpow}(\Gamma)$ of a structure $S$ is $S^\# \stackrel{\text{def}}{=} \{\text{col}_S(u) \mid u \in \text{U}_S\}$. For an integer $k \ge 0$, the $k$-multiset color abstraction $S^{\#k} \subseteq \text{mpow}(\Gamma)$ is $S^{\#k} \stackrel{\text{def}}{=} \{M \subseteq S^\# \mid \text{card}(M) \le k\}$. These abstractions are lifted to sets of structures as sets of multisets $S^\# \stackrel{\text{def}}{=} \{S^\# \mid S \in S\}$ and $S^{\#k} \stackrel{\text{def}}{=} \bigcup_{S \in S} S^{\#k}$.

Note that $S^\#$ is a multiset, whereas $S^{\#k}$ is a set of multisets. When lifted to sets of structures, both $S^\#$ and $S^{\#k}$ are sets of multisets.

The core of the proof of Theorem 9 is the equivalence between the following two conditions stated formally below:

$$ \text{tw}(F^*(S)) \le k, \text{ for some } k \ge 1 \qquad (A) $$

$$ \{\gamma_1, \gamma_1, \gamma_1\}, \{\gamma_2, \gamma_2, \gamma_2\} \in (F^*(S))^{\#3} \Rightarrow \gamma_1 \cap \gamma_2 \ne \emptyset, \text{ for all } \gamma_1, \gamma_2 \in \Gamma \qquad (B) $$

Note that condition (A) is more general than the premiss of Theorem 9. We prove the (A) $\Rightarrow$ (B) direction below.
23:10 Iterating Non-Aggregative Structure Compositions

<figure><img src="image_13.png" /><figcaption>Figure 3 Examples of RGB color schemes</figcaption></figure>

► Lemma 11. If S has bounded tree-width, then (A) implies (B).

**Proof.** By contradiction, assume that there exist $\llbracket \gamma_1, \gamma_1, \gamma_1 \rrbracket, \llbracket \gamma_2, \gamma_2, \gamma_2 \rrbracket \in (F^*(S))^\#^3$ such that $\gamma_1 \cap \gamma_2 = \emptyset$. Then, there exist structures $S_1, S_2 \in F^*(S)$ such that $\llbracket \gamma_1, \gamma_1, \gamma_1 \rrbracket \in S_1^\sharp$ and $\llbracket \gamma_2, \gamma_2, \gamma_2 \rrbracket \in S_2^\sharp$. We shall use $S_1$ and $S_2$ to build infinitely many structures whose Gaifman graphs have arbitrarily large square grid minors, as illustrated in Figure 2.

First, construct the structure $S_{12} \in F^*(S)$ by fusing one pair $(u_1, u_2)$, having colors $\gamma_1$ and $\gamma_2$, respectively. Let $v_1$ and $w_1$ (resp. $v_2$ and $w_2$) be the remaining distinct elements of $S_{12}$, having color $\gamma_1$ (resp. $\gamma_2$) from $S_1$ and $S_2$, respectively. For an arbitrarily large integer $n \ge 1$, consider $n \times n$ disjoint copies $(S_{12}^{i,j})_{i,j=1,n}$ of $S_{12}$. Let $\approx^{1,j}$ be the equivalence relation generated by $\{(v_1^{1,j}, v_2^{1,j-1})\}$ and $\approx^{i,1}$ be generated by $\{(w_2^{i,1}, w_1^{i-1,1})\}$, $\approx^{i,j}$ be generated by $\{(v_1^{i,j}, v_2^{i,j-1}), (w_2^{i,j}, w_1^{i-1,j})\}$, for all $i, j = 2, n$. Second, construct the grid-like connected structure $X^{n,n} \in F^*(S)$:

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

where structures $S_{12}^{i,j}$ are added to the fusion in the increasing order of $i + j$. We can show that Gaif($X^{n,n}$) has an $n \times n$ square grid minor. Finally, as $n$ can be taken arbitrarily large, we conclude that $F^*(S)$ does not have bounded tree-width, which contradicts (A). ◀

## 3.2 Color Schemes

For the proof of the (A) "<=" (B) direction, we first organize the set of colors using the *RGB color schemes* defined below:

► Definition 12. A partition $(\Gamma^{red}, \Gamma^{green}, \Gamma^{blue})$ of $\Gamma$ is an RGB color scheme if and only if:

1. $\gamma_1 \cap \gamma_2 \neq \emptyset$, for all $\gamma_1, \gamma_2 \in \Gamma^{blue}$,

2. $\gamma_1 \cap \gamma_2 \neq \emptyset$, for all $\gamma_1 \in \Gamma^{green}$ and all $\gamma_2 \in \Gamma^{blue}$,

3. for all $\gamma_1 \in \Gamma^{red}$ there exists $\gamma_2 \in \Gamma^{blue}$ such that $\gamma_1 \cap \gamma_2 = \emptyset$.

Note that an RGB color scheme is fully specified by the set $\Gamma^{blue}$. Indeed, any color not in $\Gamma^{blue}$ is unambiguously placed within $\Gamma^{red}$ or $\Gamma^{green}$, depending on whether or not it is disjoint from some color in $\Gamma^{blue}$. In particular, if $\Gamma^{blue} = \emptyset$ then $\Gamma^{red} = \emptyset$ and $\Gamma^{green} = \Gamma$. For example, Figure 3 shows several RGB color schemes for the set $\mathcal{C} = \{a, b, c\}$ of unary relation symbols.

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. We define below what is meant for a set of structures to conform to an RGB color scheme:

► Definition 13. A set $S$ of structures conforms to $(\Gamma^{red}, \Gamma^{green}, \Gamma^{blue})$ if and only if:

1. for all structures $S \in S$, if $\mathrm{col}_S(u) \in \Gamma^{red}$, for some element $u \in U_S$, then $\mathrm{col}_S(u') \in \Gamma^{blue}$, for all other elements $u' \in U_S \setminus \{u\}$, and
<table><thead><tr><th>F(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>

**Table 1** The types of structures obtained by fusion, where Ø means that the result of the fusion is the empty set.

2. $S^\# \cap \Gamma^{green} \subseteq \{\{\gamma, \gamma | \gamma \in \Gamma^{green}\}\}$, for all structures $S \in F^*(S)$.

In other words, $S$ conforms to a given color scheme if each structure from $S$ has either a single red and the rest blue, or at most occurrences of the same green color and the rest blue elements. Moreover, the number of occurrences of a green color must not exceed two, for each structure obtained by taking fusions of some structures in $S$. This observation justifies the following notion of type of a structure:

**Definition 14.** A structure $S$ is of type $R$ if it has exactly one red element and the rest blue, $G$ if it has at least one green element and the rest blue and $B$ if it has only blue elements.

Note that there can be structures of neither $R$, $G$ or $B$ type, but these are the only types of interest, as justified by the following:

**Lemma 15.** Let $S$ be a set of structures conforming to an RGB color scheme. Then, each structure $S \in F^*(S)$ is of type either $R$, $G$ or $B$.

**Proof.** By induction on the construction of $S \in F^*(S)$ from one or more structures from $S$. Table 1 summarizes the possible types of $F(S_1, S_2)$ on structures $S_1$ and $S_2$ of types $R$, $G$ or $B$, respectively. ◀

The (B) “⇒” (A) direction will be established via a third condition (C), which is conformance to an RGB color scheme defined by taking the $\Gamma^{blue}$ set to be the colors occurring three times in some structure from $F^*(S)$:

**Lemma 16.** If (B) holds then:

$$ S \text{ conforms to } (\Gamma^{red}, \Gamma^{green}, \Gamma^{blue}), \text{ where } \Gamma^{blue} \stackrel{\text{def}}{=} \{\gamma \in \Gamma \mid \{\{\gamma, \gamma, \gamma\}\} \in (F^*(S))^{\mathbb{Z}^3}\} \quad (C) $$

**Proof.** We show that $S$ conforms to the $(\Gamma^{red}, \Gamma^{green}, \Gamma^{blue})$ RGB color scheme from the statement, by checking the two points of Definition 13:

(1) Let $S \in S$ and prove that for any two colors $\gamma_1, \gamma_2 \in \mathbb{C}$, if $\{\{\gamma_1, \gamma_2\}\} \subseteq S^\#$ and $\gamma_1 \in \Gamma^{red}$ then $\gamma_2 \in \Gamma^{blue}$. Since $\gamma_1 \in \Gamma^{red}$, there must exists a color $\gamma'_1 \in \Gamma^{blue}$, such that $\gamma_1 \cap \gamma'_1 = \emptyset$, by Definition 12. By the definition of $\Gamma^{blue}$, this further implies $\{\{\gamma'_1, \gamma'_1, \gamma'_1\}\} \in (F^*(S))^{\mathbb{Z}^3}$. Henceforth, there exists a structure $S' \in F^*(S)$ such that $\{\{\gamma'_1, \gamma'_1, \gamma'_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 $\gamma'_1$ in $S'$ to the element of color $\gamma_1$ of $S$. Then, by construction, the structure $S''$ will also contain three elements of color $\gamma_2$, one from each disjoint copy of $S$. Therefore, $\{\{\gamma_2, \gamma_2, \gamma_2\}\} \in S''^\#$ and because $S'' \in F^*(S)$ this implies $\{\{\gamma_2, \gamma_2, \gamma_2\}\} \in (F^*(S))^{\mathbb{Z}^3}$ and therefore $\gamma_2 \in \Gamma^{blue}$.

(2) By contradiction, let $S \in F^*(S)$ be such that $S^\# \cap \Gamma^{green} \not\subseteq \{\{\gamma, \gamma | \gamma \in \Gamma^{green}\}\}$. Then there exists $\gamma' \in (S^\# \cap \Gamma^{green}) \setminus \{\{\gamma, \gamma | \gamma \in \Gamma^{green}\}\}$, i.e., $\gamma' \in \Gamma^{green}$ and $\{\{\gamma', \gamma', \gamma'\}\} \subseteq S^\#$. The latter implies $\{\{\gamma', \gamma', \gamma'\}\} \in S^{\mathbb{Z}^3} \subseteq (F^*(S))^{\mathbb{Z}^3}$. But this implies $\gamma' \in \Gamma^{blue}$ according to the definition of the RGB color scheme, contradicting $\gamma' \in \Gamma^{green}$.

<figure><img src="image_14.png" /></figure>
<figure><img src="image_15.png" /><figcaption>Figure 4 Fusion of G structures by 3-generated matchings</figcaption></figure>

In the rest of this and the next subsections, we are concerned with the proof of the following implication, that establishes the equivalence of (A) and (B). As previously mentioned, this direction of the proof uses the third condition (C) that is, conformance to the RGB color scheme from the statement of Lemma 16:

**Lemma 17.** If S has bounded tree-width and (C) holds then (A) holds.

The proof of the above lemma is split into two technical results (Lemmas 18 and 19). The first (Lemma 18) involves reasoning about the number of pairs of elements that are joined by the fusion operation in order to obtain a structure from $F^*(S)$:

**Lemma 18.** If S conforms to an RGB scheme ($\Gamma^{red}, \Gamma^{green}, \Gamma^{blue}$) and $S = (S_1 \uplus S_2)/\approx$ for some $S_i = (U_i, \sigma_i) \in F^*(S)$, for $i = 1, 2$, and some equivalence closure $\approx$ of a $U_1$-$U_2$ matching, then exactly one of the following holds:

1. $\approx$ is 1-generated, or

2. $\approx$ is 2-generated, S is of type B, and either:

a. $S_1, S_2$ are both of type R, or

b. $S_1, S_2$ are both of type G and $\text{card}(S_1^{\#} \cap \Gamma^{green}) = \text{card}(S_2^{\#} \cap \Gamma^{green}) = 2$.

*Proof.* 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 $\Gamma^{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 $\Gamma^{red}$, from either $S_1$ or $S_2$, thus matching the case 2a from the statement. In this latter case, S is of type B because joining a red with a blue element always results in a blue element.

- $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} = \text{col}_{S_1}(u_{1i})$, $G_{2i} = \text{col}_{S_2}(u_{2i})$ be the colors from $\Gamma^{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 4. Finally, note that the construction depicted in Figure 4 fusion 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 $\Gamma^{green}$. By the same argument, it follows that S is of type B, if $\approx$ is generated by two pairs of green elements. $\quad$
<figure><img src="image_16.png" /><figcaption>Figure 5 The join($t_1$, $t_2$, $c_{\gamma_1}^{i_1}$, $c_{\gamma_2}^{i_2}$) (a) and append($t_1$, $t_2$, $n$, $k$, $c_{\gamma}^i$) (b) operations</figcaption></figure>

## 3.3 Fusions as Operations on Terms

The second technical result required for the proof of Lemma 17 is a characterization of the $k$-generated fusion, for $k = 1, 2$, via operations on witness $\mathbb{F}_{HR}$-terms. We assume that $\mathbf{S}$ is a given tree-width bounded set of structures that conforms to a fixed RGB color scheme $(\Gamma^{\text{red}}, \Gamma^{\text{green}}, \Gamma^{\text{blue}})$. The goal is to prove that $\text{tw}(\mathbf{F}^*(\mathbf{S})) \le \text{tw}(\mathbf{S}) + K$, for an integer $K \ge 0$.

Since $\mathbf{S}$ has bounded tree-width, there exists a set $\mathcal{T}$ of terms such that $\mathbf{S} = \{t^{\mathbb{HR}} \mid t \in \mathcal{T}\}$ and a finite set $\mathcal{C}$ of constants such that each term $t \in \mathcal{T}$ uses only constants from $\mathcal{C}$ and assume w.l.o.g. $\mathcal{C}$ to be the least such set. Moreover, consider the following set of special constants $\bar{\mathcal{C}}^{\text{def}} = \{c_{\gamma}^i \mid \gamma \in \Gamma, 1 \le i \le 2\}$. The intuition behind these special constants is the following. Each element of a structure $t^{\mathbb{HR}}$ is the common interpretation of all the constants $c \in C_i$ in the label $\mathfrak{r}(C_1, \dots, C_{\#r})$ of a leaf of $t$. By adding a special constant $c_{\gamma}^i$ to the set $C_i$ we indicate further that the color of the element in the structure is $\gamma$. We further say that a special constant is *visible* in a term if it is not in the scope of a *rename* or *forget* operation. Let $K^{\text{def}} = \text{card}(\bar{\mathcal{C}})$, in the following and note that $\text{card}(K) = 2 \cdot \text{card}(\Gamma)$.

We shall prove that $\text{tw}(\mathbf{S}) \le \text{tw}(\mathbf{S}) + K$ by building, for any $\mathbf{S} \in \mathbb{F}^*(\mathbf{S})$, a term $t$ that uses only constants from $\mathcal{C} \uplus \bar{\mathcal{C}}$, such that $\text{forget}^{\bar{\mathcal{C}}} (t^{\mathbb{HR}}) = \mathbf{S}$. We then note that $\mathbf{S}$ has tree-width at most $\text{card}(\mathcal{C}) + K$ and obtain $\text{tw}(\mathbf{S}) \le \text{card}(\mathcal{C}) + K = \text{tw}(\mathbf{S}) + K$. Since the choice of $\mathbf{S} \in \mathbb{F}^*(\mathbf{S})$ was arbitrary, this leads to $\text{tw}(\mathbb{F}^*(\mathbf{S})) \le \text{tw}(\mathbf{S}) + K$.

In the following, we understand terms as trees whose nodes are labeled by function symbols from $\mathbb{F}_{HR}$. For each node $n$ of a term $t$, we write $\mathfrak{lab}(n)$ for its label. The children of each node $n$ form an ordered sequence of length equal to the arity of $\mathfrak{lab}(n)$. In order to build the witness terms for the structures $\mathbf{S} \in \mathbb{F}^*(\mathbf{S})$, we make use of the following operations on terms $t$, $t_1$ and $t_2$ having constants in $\mathcal{C} \uplus \bar{\mathcal{C}}$:

1. **label**($t, n, k, c_{\gamma}^i$), where $n$ is a leaf of $t$, $\mathfrak{lab}(n) = \mathfrak{r}(C_1, \dots, C_{\#r})$ and $k \in [1..\#r]$: Let $1 \le k_1 < \dots < k_\ell \le \#r$ be the indices of the sets of constants from $\mathfrak{lab}(n)$ that are equal to $C_k$ (see the definition of $HR$ in Section 2.2). The operation changes the label of $n$ in $t$ only, by replacing the set $C_{k_j}$ with $C_{k_j} \cup \{c_{\gamma}^i\}$, for each $1 \le j \le \ell$.

2. **join**($t_1, t_2, c_{\gamma_1}^{i_1}, c_{\gamma_2}^{i_2}$): The result is the following term, for a nondeterministic choice of $j$, such that $c_{\gamma_1 \cup \gamma_2}^j$ is not visible in either $t_1$ or $t_2$ (the operation is undefined otherwise):

$$ \text{forget}^{\mathbb{B}}(\text{rename}[c_{\gamma_1}^{i_1} \to c_{\gamma_1 \cup \gamma_2}^{j}](t_1) \oplus \text{rename}[c_{\gamma_2}^{i_2} \to c_{\gamma_1 \cup \gamma_2}^{j}](t_2)), \mathcal{B}^{\text{def}} = \{c_{\gamma_1 \cup \gamma_2}^{j} \mid \gamma_1 \uplus \gamma_2 \in \Gamma^{\text{blue}}\} $$

We refer to Figure 5 (a) for an illustration. In addition, we consider an overloaded version of $\text{join}(t_1, t_2, c_{\gamma_{11}}^{i_1}, c_{\gamma_{12}}^{i_2}, c_{\gamma_{21}}^{i_2}, c_{\gamma_{22}}^{i_2})$ that fuses the interpretation of $c_{\gamma_{1j}}^{i_1}$ with that of $c_{\gamma_{2j}}^{i_2}$, for both $j = 1, 2$. This definition is similar to the one above, thus omitted for brevity.

3. **append**($t_1, t_2, n, k, c_{\gamma}^i$), where $n$ is a leaf of $t_1$, $\mathfrak{lab}(n) = \mathfrak{r}(C_1, \dots, C_{\#r})$ and $k \in [1..\#r]$: the result is the term $t_1[n/\text{forget}^{c_{\gamma}^i}(\text{label}(n, n, k, c_{\gamma}^i) \oplus t_2)]$, where $t[n/s]$ denotes the substitution
of the leaf $n$ by the term $s$ in $t$. We refer to Figure 5 (b) for an illustration.

Then, Lemma 17 is an immediate consequence of the following lemma, whose proof builds
the required term by induction on the derivation of $S \in F^*(S)$, using the above operations:

**Lemma 19.** For each structure $S \in F^*(S)$ there exists a $F^{HR}$-term $t$ using only constants from $C \cup \bar{C}$, such that (i) forget$^c$ ($t^{HR}$) = $S$ and (ii) for each element $u \in U_S$ such that $\gamma = \text{col}_S(u) \in \Gamma^{\text{red}} \uplus \Gamma^{\text{green}}$ there exists a special constant $c_\gamma^i \in \bar{C}$ such that $\sigma_S(c_\gamma^i) = u$.

**Proof.** We build $t$ by induction of the derivation of $S = (U, \sigma) \in F^*(S)$. For the base case $S \in S$, let $t' \in \mathcal{T}$ be a term such that $S = t'^{HR}$ (such a term exist because $S = \{t^{HR} | t \in \mathcal{T}\}$). By repeating the label $(t, n, k, c_\gamma^i)$ operation, we add a special constant $c_\gamma^i$ to each leaf $n$ of $t$, on the appropriate position $1 \le k \le \#r$, where lab$(n) = r(C_1, \dots, C_{\#r})$, such that $\sigma(C_k) = \{u\}$ and $\gamma \stackrel{\text{def}}{=} \text{col}_S(u) \in \Gamma^{\text{red}} \uplus \Gamma^{\text{green}}$. The choice of $1 \le i \le 2$ is nondeterministic. The result of applying these labeling operations to $t'$ is $t$. Then, forget$^c$ ($t^{HR}$) = $S$ and the condition (ii) holds, by construction.

For the inductive step, let $S = (S_1 \uplus S_2)/\approx$, where $S_1, S_2 \in F^*(S)$ and $\approx$ is an equivalence relation that is generated by the set of pairs $\{(u_1, u_{2i})\}_{i \in I}$, where $I$ is either $\{1\}$ or $\{1, 2\}$. Let $\gamma_{ji} \stackrel{\text{def}}{=} \text{col}_{S_j}(u_{ji})$ for all $1 \le j \le 2$ and $i \in I$. By the inductive hypothesis, there exist terms $t_j$ and integers $1 \le k_{ji} \le 2$, such that $(U_j, \sigma_j) \stackrel{\text{def}}{=} t_j^{HR}$ and forget$^c(t_j^{HR}) = S_j$, for all $1 \le j \le 2$ and $i \in I$. We distinguish the following cases:

1. $I = \{1\}$, i.e., $\approx$ is 1-generated. We consider further the cases:

a. $\gamma_{11}, \gamma_{21} \in \Gamma^{\text{red}} \uplus \Gamma^{\text{green}}$: in this case, there are special constants $c_{\gamma_{11}}^{i_1}$ and $c_{\gamma_{21}}^{i_2}$ such that $u_{j1} = \sigma_j(c_{\gamma_{j1}}^{i_j})$, for both $1 \le j \le 2$, by the inductive hypothesis (ii). Now suppose that $c_{\gamma_{11} \uplus \gamma_{21}}^{\ell}$ is visible in $t_1$ (visibility in $t_2$ is a symmetric case), for some $1 \le \ell \le 2$. Then $\gamma_{11} \uplus \gamma_{21}$ must belong to $\Gamma^{\text{red}} \uplus \Gamma^{\text{green}}$, by the inductive hypothesis (ii). If $c_{\gamma_{11} \uplus \gamma_{21}}^{3-\ell}$ is not visible in $t_2$, suppose first that $c_{\gamma_{11} \uplus \gamma_{21}}^{3-\ell}$ is visible in $t_1$. Then, $c_{\gamma_{11}}^{i_1}, c_{\gamma_{11} \uplus \gamma_{21}}^{\ell}$ and $c_{\gamma_{11} \uplus \gamma_{21}}^{3-\ell}$ are visible in $t_1$. By Lemma 15, both $\gamma_{11}$ and $\gamma_{11} \uplus \gamma_{21}$ are green colors and $\gamma_{11} \uplus \gamma_{21}$ occurs 3 times in $S$, thus contradicting the definition of $\Gamma^{\text{blue}}$. Hence $c_{\gamma_{1} \uplus \gamma_{2}}^{3-\ell}$ is not visible in either $t_1$ or $t_2$ and $t \stackrel{\text{def}}{=} \text{join}(t_1, t_2, c_{\gamma_{11}}^{i_1}, c_{\gamma_{21}}^{i_2})$ is well-defined. Else, if $c_{\gamma_{11} \uplus \gamma_{21}}^{3-\ell}$ is visible in $t_2$, then $\gamma_{11} \uplus \gamma_{21}$ occurs 3 times in $S$, thus contradicting the definition of $\Gamma^{\text{blue}}$.

b. $\gamma_{11} \in \Gamma^{\text{blue}}$ and $\gamma_{21} \in \Gamma^{\text{red}}$ ($\gamma_{11} \in \Gamma^{\text{red}}$ and $\gamma_{21} \in \Gamma^{\text{blue}}$ is a symmetric case): Let $n$ be the leaf of $t_1$ such that lab$(n) = r(C_1, \dots, C_{\#r})$ and $C_k$ be a set of constants that are (all) interpreted as $u_{11}$, for some $1 \le k \le \#r$. Let $c_{\gamma_{21}}^{\ell}$ be the special constant such that $u_{21} = \sigma_2(c_{\gamma_{21}}^{\ell})$, for some $1 \le \ell \le 2$. We can assume w.l.o.g. that $c_{\gamma_{21}}^{\ell}$ is not visible in $n$. If this were not to be the case, then $n$ must have been involved in a previous join of a term $t_3$ with another term $t'_1$, such that $t_1$ is the outcome of this join. In this case, we change the construction, by first joining $t_2$ with $t_3$, as in the previous case, then joining the result with $t'_1$. Note that this is possible due of the associativity of the $\oplus$ operation. Finally, we define $t \stackrel{\text{def}}{=} \text{append}(t_1, t_2, n, k, c_{\gamma_{21}}^{\ell})$.

2. $I = \{1, 2\}$, i.e., $\approx$ is 2-generated. By Lemma 18, either one of the following holds:

a. $S_1$ and $S_2$ are of type G: let $c_{\gamma_{ji}}^{k_{ji}}$ be special constants such that $u_{ji} = \sigma_j(c_{\gamma_{ji}}^{k_{ji}})$, for all $1 \le i, j \le 2$. Then, we define $t \stackrel{\text{def}}{=} \text{join}(t_1, t_2, (c_{\gamma_{1i}}^{k_{ji}})_{i \in I}, (c_{\gamma_{2i}}^{k_{ji}})_{i \in I})$ and check that the operation is well-defined, following a similar argument as in case (1a).

b. $S_1$ and $S_2$ are of type R: we can assume w.l.o.g. that $u_{ii}$ is the interpretation of a special constant $c_{\gamma_{ii}}^{j_i}$, for some $1 \le j_i \le 2$, where $\gamma_{ii} \in \Gamma^{\text{red}}$, for both $i=1,2$. Let $n_1$ be the leaf of $t_1$ such that lab$(n_1) = r(C_1, \dots, C_{\#r})$ and $u_{11}$ is the interpretation of (all) constants from $C_{k_1}$, for some $1 \le k_1 \le \#r$. Analogously, we consider $n_2$ to be the leaf of $t_2$ and $k_2$ the position of the constants from its label, that are interpreted as $u_{22}$.
Under similar assumptions as in the case (2a), ensuring that the result is well defined, we let $t = \text{forget}^{c_{\gamma_1}^{j_1}}(\text{append}(t_1, \text{label}(t_2, n_2, k_2, c_{\gamma_1}^{j_1}), n_1, k_1, c_{\gamma_2}^{j_2}))$. The only difference with the previous case is that the indices $j_1$ and $j_2$ must be different to avoid name clashes, hence we require 2 special constants $c_\gamma^1$ and $c_\gamma^2$, for each color $\gamma \in \Gamma^{\text{red}}$.

It is easy to check that $\text{forget}^c(t^{HR}) = S$, in all cases.

## 3.4 Tree-width Bounded Fusion-closed Sets are Context-free

This subsection completes the proof of the first point of Theorem 9. The final ingredient is the following lemma, whose proof relies on the lifting of the construction that simulates the 1- or 2-generated fusion of structures from terms to tree automata recognising sets of terms:

**Lemma 20.** Let $S$ be a context-free set of structures conforming to some RGB color scheme. Then, the set $F^*(S)$ is context-free.

**Proof of Theorem 9 (1)** "⇒" Since $S$ is a context-free set, it has bounded tree-width. If $F^*(S)$ has bounded tree-width, then $S$ conforms to an RGB color scheme, by the combined results of Lemmas 11 and 16. Because $S$ is context-free, we obtain that $F^*(S)$ is context-free, by Lemma 20. "<=" Because each context-free set has bounded tree-width.

## 3.5 Color Abstractions

This section is concerned with the proof of the second point of Theorem 9. Let $S$ be a context-free set of structures given by a tree automaton $\mathcal{A}$ over a finite signature $\mathcal{F} \subseteq \mathbb{F}_{HR}$. In the rest of this section, $S$, $\mathcal{F}$ and $\mathcal{A}$ are considered to be fixed.

Note that the equivalence between (A) and (B) follows from (A) ⇒ (B) (Lemma 11), (B) ⇒ (C) (Lemma 16) and (C) ⇒ (A) (Lemma 17). Hence, it is sufficient to establish the decidability of the condition (B) for $S$. To this end, we compute the $k$-multiset abstraction $(F^*(S))^{\mathfrak{k}}$, for an arbitrary given integer $k \ge 1$ (note that checking (B) requires $k = 3$). First, we reduce the computation of $(F^*(S))^{\mathfrak{k}}$ to that of $S^{\mathfrak{k}}$. Second, we sketch the argument behind the effective computability of $S^{\mathfrak{k}}$.

The following lemma shows that, because we are interested only in $k$-multisets color abstractions, we can restrict fusion to 1-generated equivalence relations, while preserving the $k$-multiset color abstraction. We denote by $F_1^*(S)$ the set of structures obtained by taking the closure of $S$ only with respect to fusions induced by 1-generated matchings.

**Lemma 21.** $(F^*(S))^{\mathfrak{k}} = (F_1^*(S))^{\mathfrak{k}}$ for any set $S$ of structures and integer $k \ge 1$.

The set $(F_1^*(S))^{\mathfrak{k}}$ can be computed by a least fixpoint iteration of the following abstract operation on the domain of $k$-multiset color abstractions. As the latter domain is finite, this fixpoint computation is guaranteed to terminate.

**Definition 22.** The single-pair multiset fusion is defined below, for all $M_1, M_2 \in \text{mpow}(\Gamma)$:

$$f_1^*(M_1, M_2) \stackrel{\text{def}}{=} \{ M \in \text{mpow}(\Gamma) \mid \begin{array}{l} \exists \gamma_1 \in M_1 \ . \ \exists \gamma_2 \in M_2 \ . \ \gamma_1 \cap \gamma_2 = \emptyset, \\ M = \{ \gamma_1 \cup \gamma_2 \} \cup \bigcup_{i=1,2} (M_i \setminus \{ \gamma_i \}) \end{array} \}$$

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

$$f_1^{\mathfrak{k}}(M_1, M_2) \stackrel{\text{def}}{=} \{ M \mid \exists M' \in f_1^*(M_1, M_2). M \subseteq M', \text{card}(M) \le k \}$$

For a set $\mathcal{M}$ of multisets (resp. $k$-multisets) of colors, let $f_1^{\mathfrak{k}}(\mathcal{M})$ (resp. $f_1^{\mathfrak{k}*}(\mathcal{M})$) be the closure of $\mathcal{M}$ under taking single-pair fusion on multisets (resp. $k$-multisets).
closure of a context-free set has bounded tree-width. Moreover, if this is the case, we show
that the closure set is context-free as well, described by an effectively constructible grammar.

Future work involves considering more general notions of coloring, e.g., coloring functions
defined by MSO-definable transductions. Moreover, we plan to investigate generalizations of
Theorem 9 for other notions of width, such as generalizations of clique-width and rank-width
from graphs and hypergraphs to relational structures.

References

1. Emma Ahrens, Marius Bozga, Radu Iosif, and Joost-Pieter Katoen. Reasoning about distributed reconfigurable systems. Proc. ACM Program. Lang., 6(OOPSLA2):145–174, 2022. doi:10.1145/3563293.

2. Cristiano Calcagno, Philippa Gardner, and Uri Zarfaty. Context logic and tree update. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 271–282. ACM, 2005. URL: https://doi.org/10.1145/1040305.1040328.

3. Cristiano Calcagno, Philippa Gardner, and Uri Zarfaty. Context logic as modal logic: completeness and parametric inexpressivity. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 123–134. ACM, 2007. doi:10.1145/1190216.1190236.

4. Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A Spatial Logic for Querying Graphs. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan Eidenbenz, and Ricardo Conejo, editors, Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP’02), volume 2380 of Lecture Notes in Computer Science, pages 597–610. Springer, July 2002.

5. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. HAL, 2008. URL: https://inria.hal.science/hal-03367725.

6. Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12–75, 1990. doi:10.1016/0890-5401(90)90043-H.

7. Bruno Courcelle. The monadic second-order logic of graphs VII: graphs as relational structures. Theor. Comput. Sci., 101(1):3–33, 1992. doi:10.1016/0304-3975(92)90148-9.

8. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012. doi:10.1017/CBO9780511977619.

9. Simon Docherty and David J. Pym. Intuitionistic layered graph logic: Semantics and proof theory. Log. Methods Comput. Sci., 14(4), 2018. doi:10.23638/LMCS-14(4):112018.

10. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995.

11. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. doi:10.1007/3-540-29953-X.

12. Radu Iosif and Florian Zuleger. Expressiveness results for an inductive logic of separated relations. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory (CONCUR 2023), volume 279 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2023.20.

13. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 14–26. ACM, 2001.
23:18 Iterating Non-Aggregative Structure Compositions

14 Viktor Kuncak and Martin Rinard. Generalized records and spatial conjunction in role logic. In *Static Analysis*, pages 361–376, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.

15 Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In *Proceedings of the 15th International Workshop on Computer Science Logic*, CSL '01, pages 1–19, 2001.

16 David J. Pym, Peter W. O'Hearn, and Hongseok Yang. Possible worlds and resources: the semantics of bi. *Theoretical Computer Science*, 315(1):257–305, 2004. Mathematical Foundations of Programming Semantics. URL: https://www.sciencedirect.com/science/article/pii/S0304397503006248, doi:https://doi.org/10.1016/j.tcs.2003.11.020.

17 Greg Restall. Substructural Logics. In Edward N. Zalta and Uri Nodelman, editors, *The Stanford Encyclopedia of Philosophy*. Metaphysics Research Lab, Stanford University, Fall 2024 edition, 2024.

18 John C. Reynolds. Separation logic: A logic for shared mutable data structures. In *17th IEEE Symposium on Logic in Computer Science (LICS 2002)*, 22-25 July 2002, Copenhagen, Denmark, *Proceedings*, pages 55–74. IEEE Computer Society, 2002. doi:10.1109/LICS.2002.1029817.

19 D. Seese. The structure of the models of decidable monadic theories of graphs. *Annals of Pure and Applied Logic*, 53(2):169–195, 1991. doi:10.1016/0168-0072(91)90054-P.

20 P.D. Seymour and R. Thomas. Graph searching and a min-max theorem for tree-width. *Journal of Combinatorial Theory, Series B*, 58(1):22–33, 1993. doi:10.1006/jctb.1993.1027.

A Proofs

**► Lemma 20.** Let $\mathbf{S}$ be a context-free set of structures conforming to some RGB color scheme. Then, the set $\mathbf{F}^*(\mathbf{S})$ is context-free.

**Proof of Lemma 20.** Let $(\Gamma^{\text{red}}, \Gamma^{\text{green}}, \Gamma^{\text{blue}})$ be the RGB color scheme from the hypothesis and $\mathcal{A} = (Q, F, \to_A)$ be a tree automaton that recognizes a set of terms over a finite signature $\mathcal{F} \subseteq \mathbb{F}_{\mathcal{H}\mathcal{R}}$, such that $S = \{t^{\mathcal{HR}} \mid t \in \mathcal{L}(\mathcal{A})\}$. Let $\mathcal{C}$ be the finite set of constants that occur in some term from $\mathcal{T}(\mathcal{F})$. By pre-processing $\mathcal{A}$, we assume w.l.o.g. that each state $q \in Q$ carries (i.e., is annotated with) the following information, that holds in each run $\pi$ of $\mathcal{A}$ over a term $t \in \mathcal{T}(\mathcal{F})$, such that $q$ is the state labeling the root of $t$:

i. $t$ consists of a single leaf node labeled $r(C_1, \dots, C_k)$ such that the (common) interpretation $u_\ell$ of the constants in each set $C_\ell \subseteq \mathcal{C}$ in the structure $t^{\mathcal{HR}}$ has color $\gamma_\ell$, i.e., $\text{col}_t^{\mathcal{HR}}(u_\ell) = \gamma_\ell$. This fact is denoted as $\text{col}_q(C_\ell) = \gamma_\ell$, by abuse of notation. This information can be inferred by tracking bottom-up the visibility and identity (through *rename*$^c$ and *forget*$^\alpha$ operations) of each constant $c \in \mathcal{C}_\ell$, while guessing its final color. The automaton has a run over $t$ only if all such guesses are correct, otherwise it gets stuck. Moreover, we denote by $\lambda(q) \in \{\top, \bot\}$ the boolean information whether $q$ labels a leaf subterm in each run.

ii. $t \in \mathcal{L}(\mathcal{A})$ (i.e., $q \in F$) and $t^{\mathcal{HR}}$ is a structure of type R, G or B. This information can be inferred by counting the number of red and green elements up to or more than 1, based on the information on colors provided at the previous point. We denote by $\tau(q) \in \{\text{R}, \text{G}, \text{B}\}$ this information.

Note that this pre-processing step involves splitting the transitions of $\mathcal{A}$ over multiple copies of the same original state having different annotations.
We build a tree automaton $\mathcal{A}^*$ over the finite signature:

$$ \bar{\mathcal{F}}^{\text{def}} = \{r(C'_1, \dots, C'_k) \mid r(C_1, \dots, C_k) \in \mathcal{F}, C_i \subseteq C'_i \subseteq C_i \uplus \bar{C}, \text{ for all } 1 \le i \le k\} \\ \cup \{f \in \mathcal{F} \mid f = \text{forget}_{C''}^{C'}, C', C'' \subseteq C \cup \bar{C}\} \\ \cup \{f \in \mathcal{F} \mid f = \text{rename}_{C'}^{C'}, \alpha : C \cup \bar{C} \to C \cup \bar{C}, C' \subseteq C \cup \bar{C}\} $$

such that $\mathcal{F}^*(\mathbf{S}) = \{t^{\mathcal{H}\mathcal{R}} | t \in \mathcal{L}(\mathcal{A}^*)\}$. The construction of $\mathcal{A}^*$ follows the structure of the inductive proof of Lemma 19.

The states and transitions of $\mathcal{A}^*$ contain the states and some of the transitions of $\mathcal{A}$, respectively. In addition, $\mathcal{A}^*$ has states of the form $(m, P, q)$, where:

- $m \in \{\mu, \mu_1, \mu'_1, \mu_2, \mu_3\}$ indicates in which mode the automaton $\mathcal{A}^*$ is currently: $\mu$ is the default mode, in which the special constants are propagated upwards, $\mu_1$ and $\mu'_1$ are used to build the gadget of case (??), $\mu_2$ the one of case (??) and $\mu_3$ is used for case (??) of the proof of Lemma 19. The mode indicator allows the $\mathcal{A}^*$ to finish building these intermediate terms correctly, before re-entering the default mode.

- $P \subseteq \bar{C}$ is a set of special constants, that are visible from the current position in the term,

- $q \in Q \cup \{\perp\}$ is either the currently tracked state of $\mathcal{A}$, or $\perp$. Intuitively, $q \in Q$ indicates that $\mathcal{A}^*$ is currently reading a term from $\mathcal{L}(\mathcal{A})$, whereas $q = \perp$ means that $\mathcal{A}^*$ has finished reading the terms from $\mathcal{L}(\mathcal{A})$.

<figure><img src="image_17.png" /><figcaption>■ **Figure 6** The implementation of the join$(t_1, t_2, c_{\gamma_1}^{i_1}, c_{\gamma_2}^{i_2})$ (a) and append$(t_1, t_2, n, k, c_{\gamma}^i)$ (b) operations in $\mathcal{A}^*$, where the states of $\mathcal{A}^*$ are depicted in red.</figcaption></figure>

In addition to transitions inherited from $\mathcal{A}$, the automaton $\mathcal{A}^*$ has the following transitions, defined according to the cases of the inductive proof of Lemma 19:
For the base case, $\mathcal{A}^*$ has the following transitions:

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

Moreover, the transitions $\xrightarrow{r(c_1, \dots, c_{\#r})} q$ such that $\mathrm{col}_q(C_\ell) \in \Gamma^{\mathrm{red}} \uplus \Gamma^{\mathrm{green}}$ for some $1 \le \ell \le \#r$ (i.e., inherited from $\mathcal{A}$) are removed, because red and green elements must be always initially marked by special constants. These constants are then propagated upwards during each run of $\mathcal{A}^*$.

The case (??) of the proof of Lemma 19 is concerned with joining two structures via a 1- or 2-generated equivalence relation. We give the construction of $\mathcal{A}^*$ in the first case, the second being similar. Consider that these structures are evaluations of $\mathcal{F}$-terms $t_1$ and $t_2$ that have been labeled by $\mathcal{A}^*$ with states $(\mu, P_1, q_1)$ and $(\mu, P_2, q_2)$, respectively. Then, the new term is the result of the nondeterministic operation $\mathrm{join}(t_1, t_2, c_{\gamma_1}^{k_1}, c_{\gamma_2}^{k_2})$, implemented in $\mathcal{A}^*$ by the following transitions, for each $j \in \{1, 2\}$:

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

We refer to Figure 6 (a) for an illustration of this construction.

The case (??) of the proof of Lemma 19 is concerned with joining a red element of $t_2^{\mathcal{H}\mathcal{R}}$ with a blue element of $t_1^{\mathcal{H}\mathcal{R}}$ via a special constant $c_{\gamma_2}^k$, that is immediately forgotten after the join, because the resulting element is blue. The new term is the result of an operation $\mathrm{append}(t_1, t_2, n, k, c_{\gamma_2}^k)$, where $n$ is a leaf of $t_1$ having label $\mathrm{lab}(n) = r(C_1, \dots, C_{\#r})$ and $k \in [1..\#r]$ is the position of that leaf corresponding to the blue element of $t_1^{\mathcal{H}\mathcal{R}}$ involved
in the fusion. This operation is implemented in $\mathcal{A}^*$ by the following transitions:

$$ \begin{array}{r@{\;}c@{\;}l@{\quad}l} \xrightarrow{r(c'_1, \dots, c'_{\#r})} & (\mu, P_0 \cup \{c_{\gamma_2}^k\}, q_0), & \text{where} \\ & C'_\ell & \begin{cases} C_\ell \cup \{c_{\gamma_2}^k\} & \text{if } C_\ell = C_k \\ C_\ell & \text{otherwise} \end{cases}, & \text{for all } 1 \le \ell \le \#r \\ \xrightarrow{r(c_1, \dots, c_{\#r})} & (\mu, P_0, q_0) & \text{was added to } \mathcal{A}^* \text{ by the base case} \\ & ((\mu, P_0 \cup \{c_{\gamma_2}^k\}, q_0), (\mu, P_2, q_2)) \xrightarrow{\oplus} & (\mu_2, P', \perp), \text{ where} \\ & & \lambda(q_0) = \top, c_{\gamma_2}^k \notin P_0, c_{\gamma_2}^k \in P_2 \\ & & P' \stackrel{\text{def}}{=} P_0 \cup P_2 \\ & (\mu_2, P', \perp) \xrightarrow{\text{forget } \{c_{\gamma_2}^k\}} & (\mu, P'', \perp), \text{ where } P'' \stackrel{\text{def}}{=} P' \setminus \{c_{\gamma_2}^k\} \end{array} $$

Finally, we add a new transition $L[(\mu, P_0, q_0)/(\mu, P'', \perp)] \xrightarrow{f} (\mu, P, q)$ for each transition $L \xrightarrow{f} (\mu, P, q)$ introduced at the construction for the base case, where $L[(\mu, P_0, q_0)/(\mu, P'', \perp)]$ denotes the substitution of the state $(\mu, P_0, q_0)$ with the state $(\mu, P'', \perp)$ on the left-hand side of the transition. We refer to Figure 6 (b) for an illustration of this construction.

■ The case (??) of the proof of Lemma 19 is concerned with joining a red element, that interprets the constant $c_{\gamma_{ii}}^{k_i}$ from the structure $S_i$, with a blue element from the structure $S_{3-i}$, for both $i = 1, 2$. The new term is the result of an operation $\text{forget}^{c_{\gamma_{11}}^{k_1}}$ (append$(t_1, \text{label}(t_2, n_2, k_2, c_{\gamma_{11}}^{k_1}), n_1, k_1, c_{\gamma_{22}}^{k_2}))$, where $n_i$ is the leaf of $t_i$ and $k_i$ is the position within that leaf of the blue element of $S_i$ involved in the 2-generated fusion. This operation $\text{append}(t_1, \text{label}(t_2, n_2, k_2, c_{\gamma_{11}}^{k_1}), n_1, k_1, c_{\gamma_{22}}^{k_2})$ is implemented in $\mathcal{A}^*$ by a similar construction to the one at the previous point, the only difference being the extra transitions needed to implement $\text{label}(t_2, n_2, k_2, c_{\gamma_{11}}^{k_1})$ and propagate $c_{\gamma_{11}}^{k_1}$ to the root of $t_2$. The final $\text{forget}^{c_{\gamma_{11}}^{k_1}}$ (...) is implemented as in the previous case (the last transition). The automaton $\mathcal{A}^*$ has a single final state $q_f$ that is reached from each state $(m, P, q)$ such that $q$ is either a final state of $\mathcal{A}$ or $\perp$, via an operation that forgets all the special constants from $\bar{C}$. We sketch the proof of $\mathcal{F}^*(S) = \{t^{\mathcal{HR}} | t \in \mathcal{L}(\mathcal{A}^*)\}$ below:

“$\subseteq$” For each structure $S \in \mathcal{F}^*(S)$ there exists a $\mathcal{F}$-term $t$ such that $t^{\mathcal{HR}} = \bar{S}$, by the argument used in the proof of Lemma 19. This term is labeled by $\mathcal{A}^*$ with a state of the form $(m, P, q)$, by the construction of $\mathcal{A}^*$. Then $q$ is a final state of $\mathcal{A}$ if $S \in S$ and $q = \perp$ otherwise. In both cases, $\mathcal{A}^*$ has a transition to its final state, in order to accept the term $\text{forget}^{\bar{c}}(t)$. Since $S = \text{forget}^{\bar{c}^{\mathcal{HR}}}(t^{\mathcal{HR}})$, we obtain $S \in \{t^{\mathcal{HR}} | t \in \mathcal{L}(\mathcal{A}^*)\}$.

“$\supseteq$” Let $t \in \mathcal{L}(\mathcal{A}^*)$ be a $\bar{\mathcal{F}}$-term and $S \stackrel{\text{def}}{=} t^{\mathcal{HR}}$ be the structure obtained by evaluating $t$. Let $(m, P, q) \xrightarrow{\text{forget}^{\bar{c}}}$ $q_f$ be the last transition of $\mathcal{A}^*$ on some accepting run over $t = \text{forget}^{\bar{c}}(\bar{t})$, for some $\bar{\mathcal{F}}$-term $\bar{t}$. Then, we have $\bar{t}^{\mathcal{HR}} = \bar{S}$. If $q \in F$ is a final state of $\mathcal{A}$, by the construction of $\mathcal{A}^*$, we have $t' \in \mathcal{L}(\mathcal{A})$, where $t'$ is the term obtained by removing the special constants from the labels of the leaves of $\bar{t}$. Hence, $t^{\mathcal{HR}} = t'^{\mathcal{HR}} \in S \subseteq \mathcal{F}^*(S)$.

Otherwise, $q = \perp$ and $\bar{t}$ is a term built inductively from terms in $\mathcal{L}(\mathcal{A})$ annotated with special constants, as in the proof of Lemma 19. Then $\bar{S}' = \bar{t}^{\mathcal{HR}}$, where $S'$ is the structure agreeing with $\bar{t}^{\mathcal{HR}}$, except for the interpretation of the special constants, where $\sigma_{S'}$ is undefined. By the choice of $\bar{t}$, $S'$ is obtained from structures in $S$ by inductively applying a 1- or 2-generated fusion, i.e., $S' \in \mathcal{F}^*(S)$. Since $t = \text{forget}^{\bar{c}}(\bar{t})$, we have $S' = t^{\mathcal{HR}} = S$, thus $S \in \mathcal{F}^*(S)$.

► Lemma 21. $(\mathcal{F}^*(S))^{\otimes k} = (\mathcal{F}_1^*(S))^{\otimes k}$ for any set $S$ of structures and integer $k \ge 1$.
**Proof of Lemma 21.** “$(F_1^*(S))^k \subseteq (F^*(S))^k$” This direction follows directly from $F_1^*(S) \subseteq F^*(S)$.

“(F^*(S))^k \subseteq (F_1^*(S))^k” We prove the stronger property:

$$ \forall S \in F^*(S). \exists S' \in F_1^*(S). S^\sharp \subseteq S'^\sharp $$

By induction on the derivation of $S \in F^*(S)$ from $S$.

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

**Induction step:** Assume $S = (S_1 * S_2)_{/\approx}$ for some $S_1, S_2 \in F^*(S)$ and some equivalence relation $\approx$ generated by the independent set $\{(u_{1i}, u_{2i}) | i \in [1..n]\}$, that conforms to the compatibility condition of Definition 3 for $S_1, S_2$. Let $\gamma_{1i} = \text{col}_{S_1}(u_{1i}), \gamma_{2i} = \text{col}_{S_2}(u_{2i})$, for all $i \in [1..n]$. By Definition 3, $S = (S_1 * S_2)_{/\approx}$ implies $\gamma_{1i} \cap \gamma_{2i} = \emptyset$, for all $i \in [1..n]$, and moreover:

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

By the inductive hypothesis, there exists $S'_1, S'_2 \in F_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 $\gamma_{1i}$ from $S'_1$ with some element $u'_{2i}$ with color $\gamma_{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$ generated by $\{u'_{1i}, u'_{2i}\}$ for some pair of elements as above, for each $i \in [1..n]$, and define:

$$ S' \stackrel{\text{def}}{=} (\dots ((S'_1 * S'_{2,1})/\approx'_1 * S'_{2,2})/\approx'_2 * \dots * S'_{2,n}) \approx'_n $$

Then $S' \in F_1^*(S)$ and, moreover, we have $S^\sharp \subseteq S'^\sharp$, because:

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

►

**Lemma 23.** $(F_1^*(S))^k = f_1^{k*}(S^k)$, for any set $S$ of structures and integer $k \ge 1$.

**Proof of Lemma 23.** Abusing notation, we write $M^{\sharp k} \stackrel{\text{def}}{=} \{M' | M' \subseteq M, \text{card}(M') \le k\}$. Then, we have $(F_1^*(S))^k = ((F_1^*(S))^k)^{\sharp k}$, by Definition 10. We can prove that for all structures $S_1, S_2$ it holds $(F_1(S_1, S_2))^k = f_1^*(S_1^k, S_2^k)$. This immediately extends to their respective closure, henceforth, $(F_1^*(S))^k = f_1^{k*}(S^k)$. Henceforth, we are left with proving that $(f_1^{k*}(S^k))^k = f_1^{k*}(S^k)$.

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

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

**Induction step:** Assume $M \in f_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 f_1^{k*}(S^k)$. Then, there exists $\gamma_1 \in M_1, \gamma_2 \in M_2$ such that $\gamma_1 \cap \gamma_2 = \emptyset$ and $M = (M_1 \setminus \{\{\gamma_1\}\}) \cup (M_2 \setminus \{\{\gamma_2\}\}) \cup \{\{\gamma_1 \cup \gamma_2\}\}$, by Definition 22. Let $M' \in M^{\sharp k}$, that is, $M' \subseteq M$, $\text{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 f_1^{k*}(S^k)$.

- $M' \not\subseteq M_i$, for $i = 1, 2$ and $\gamma_1 \cup \gamma_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 \{\{\gamma_1\}\}) \in M_1^{\sharp k}, (M'_2 \cup \{\{\gamma_2\}\}) \in M_2^{\sharp k}$. It is an easy check that $M' \in f_1^{\sharp k}((M'_1 \cup \{\{\gamma_1\}\}), (M'_2 \cup \{\{\gamma_2\}\}))$. This implies $M' \in f_1^{k*}(S^k)$ as both subterms belong to $f_1^{k*}(S^k)$.

- $M' \not\subseteq M_i$, for $i = 1, 2$ and $\gamma_1 \cup \gamma_2 \in M'$: we proceed as in the previous case but considering a partitioning of $M' \setminus \{\{\gamma_1 \cup \gamma_2\}\}$. We obtain $M' \in f_1^{k*}(S^k)$, as well.
"$f_1^{\mathbb{S}^{k*}}(\mathbb{S}^{\mathbb{S}k}) \subseteq (f_1^{\mathbb{S}*}(\mathbb{S}^\mathbb{S}))^{\mathbb{S}k}$" We prove that, for all $k$-multiset $M' \in f_1^{\mathbb{S}^{k*}}(\mathbb{S}^{\mathbb{S}k})$, there exists $M \in f_1^{\mathbb{S}*}(\mathbb{S}^\mathbb{S})$, such that $M' \subseteq M$, by induction on the derivation of $M'$ from $\mathbb{S}^{\mathbb{S}k}$.

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

**Induction step:** Assume $M' \in f_1^{\mathbb{S}k}(M'_1, M'_2)$ for some $k$-multisets of colors $M'_1, M'_2 \in f_1^{\mathbb{S}k*}(\mathbb{S}^{\mathbb{S}k})$. By the inductive hypothesis, there exists multisets $M_1, M_2 \in f_1^{\mathbb{S}*}(\mathbb{S}^\mathbb{S})$ 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 f_1^{\mathbb{S}*}(\mathbb{S}^\mathbb{S})$, which is the superset of $M'$. $\quad$

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