# Regular Grammars for Sets of Graphs of Tree-Width 2

Marius Bozga, Radu Iosif, Florian Zuleger

► To cite this version:

Marius Bozga, Radu Iosif, Florian Zuleger. Regular Grammars for Sets of Graphs of Tree-Width 2. 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2025), Jun 2025, Singapour, Singapore. pp.704-717, 10.1109/LICS65433.2025.00059. hal-05333637

HAL Id: hal-05333637

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

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>

Distributed under a Creative Commons Attribution 4.0 International License
Regular Grammars for Sets of Graphs of
Tree-Width 2

Marius Bozga

Verimag, CNRS

Grenoble, France,

marius.bozga@univ-grenoble-alpes.fr

Radu Iosif

Verimag, CNRS

Grenoble, France,

radu.iosif@univ-grenoble-alpes.fr

Florian Zuleger

TU Wien

Wien, Austria

florian.zuleger@tuwien.ac.at

*Abstract*—Regular word grammars are restricted context-free grammars that define all the recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier “regular” is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulæ without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width.

# I. INTRODUCTION

Recognizability is a central pillar of the theory of formal languages. This foundational role is underpinned by the variety of well-established formalisms that define recognizable languages. For instance, recognizable word languages can be represented by finite automata, semigroups, regular expressions, regular grammars and monadic-second order logic. These formalisms provide a robust framework for understanding the structure of recognizable languages.

While the cases of words and trees are largely understood, the case of graphs is currently facing several open problems. One such problem is the lack of a notion of automaton defining a class of graph languages that is closed under boolean operations and has a logical characterization. A seminal development in this direction is the work of Courcelle that introduced graph algebras [1], [2]. In particular, the *hyperedge replacement* (HR) algebra generalizes the notion of recognizability from words to graphs. Courcelle established that all CMSO-definable sets of graphs are recognizable [1], but there are recognizable sets of graphs that are not CMSO-definable. Notably, the class of graphs of tree-width at most 2 is chronologically the first for which recognizability in the HR algebra has been shown to be equivalent to definability in counting monadic-second order logic (CMSO) [3]. The picture has been since completed by the seminal papers of Bojańczyk

and Pilipczuk [4], [5], that established the equivalence between recognizability and CMSO-definability, for all classes of graphs defined by a bound on their tree-width.

Unlike for words and trees, the equivalence between recognizability and definability for graphs does not provide finite syntactic descriptions of the recognizable sets (e.g., automata, regular expression or grammars) that can be used to compute boolean operations (union, intersection, complement) and decide emptiness of a set, membership in a set, or inclusion between sets. For the class of graphs of tree-width at most 2, the finite representation problem has been addressed by the development of regular expressions that capture exactly the CMSO-definable sets thereof [6]. Moreover, grammars that capture the CMSO-definable sets of graphs of bounded *embeddable* tree-width (i.e., an over-approximation of tree-width that considers only decompositions whose backbones are spanning trees of the given graph) have been defined [7].

Despite these recent advances, the problems of computing boolean operations and deciding emptiness, membership and inclusion for sets of graphs (other than trees) have received scant attention. Moreover, the definition of finite algebraic descriptions of the CMSO-definable sets of graphs of tree-width bounded by $k \ge 3$ is currently an open problem.

a) *Contributions*: (1) We introduce grammars that capture precisely the recognizable sets for the classes of (1) unordered and unranked trees, (2) series-parallel graphs, and, more generally, (3) graphs of tree-width at most 2. Following the initial terminology of Courcelle [3], we call these grammars *regular*. For each of the mentioned classes, the regular grammars are defined by composite (derived) HR operations and by simple syntactic restrictions on the form of their rules.

Just as a regular word grammar can be converted into a finite automaton recognizing its language, a regular graph grammar can be converted into a finite algebra that recognizes its language. The elements of this algebra are finite sets of either multisets or tuples of nonterminals, that describe (sets of) derivations of the grammar, used to interpret the algebraic operations on graphs. For each of the three classes of graphs considered, the size of the recognizer algebra for a regular grammar is at most doubly exponential in the size of the grammar. This uniform upper bound provides a 2EXPTIME algorithm for the problem of inclusion of a context-free graph language into a regular language (i.e., the language of a regular
grammar) for the three classes of graphs considered. To the best of our efforts, we could not find a matching lower bound, other than the simply exponential blowup incurred by the determinization of automata on words or ranked trees [8].

Conversely, we prove that each recognizable set is regular in its respective class. Moreover, a restriction on the form of the rules of regular grammars suffices to define precisely the sets of graphs recognized by algebras having an aperiodic parallel composition semigroup, or simply aperiodic algebras.

(2) We investigate the relation between recognizable and MSO-definable sets, i.e., defined by logical formulæ without modulo constraints on the cardinality of set variables. Since the equivalence of recognizability and CMSO-definability has been already established for tree-width bounded classes of graphs [4], we prove that the sets recognized by aperiodic algebras, i.e., for the three classes of graphs considered, are the same as the ones definable in MSO. A roughly similar situation occurs for words, where recognizability by aperiodic monoids is equivalent to definability in first-order logic [9]. However, this elegant result does not generalize to trees<fnref n="1" />, let alone graphs. Furthermore, we generalize the equivalence between recognizability by aperiodic algebras and MSO-definability, for all classes of graphs defined by a bound on the tree-width.

b) Related Work: Data tree description languages such as XML (eXtensible Markup Language) or JSON (JavaScript Object Notation) have motivated a systematic study of automata and logics for unranked trees, see [11] for an overview. Two-variable first-order logics for unranked trees with total sibling order and equality between data values are studied in [12]. Deterministic automata on unranked trees with total sibling order are investigated in [13]. Several definitions of unranked tree automata, whose languages are equivalent to various fragments of CMSO are given in [14]. Notably, bottom-up tree automata with transitions triggered by counting constraints on the multiset of states labeling the children of the current node have the same expressivity as CMSO. However, there is no result on the complexity of the inclusion problem for this particular class of automata. Subclasses with more restrictive transition triggers have membership problems ranging from PTIME and NP-hardness and inclusion problems from PTIME and co-NP-completeness. Algebraic recognizers for unranked (ordered and unordered) trees are also defined in [15], in terms of forest algebras consisting of a horizontal monoid (with disjoint union) and a vertical monoid (with context composition). However, the focus of this work is logical definability of unranked tree languages in the EF fragment of the CTL temporal logic, based on certain axiomatic properties of these monoids, such as commutativity and aperiodicity.

The regular expressions for graphs of tree-width at most 2, introduced by Doumane [6], capture the CMSO-definable sets, just as the regular grammars we propose in this paper. However, establishing a formal connection between these regular expressions and the regular grammars in this paper

(i.e., a Kleene theorem for graphs of tree-width at most 2) requires further study. A major difficulty is that the definition of the guard conditions on iteration variables from a regular expression [6, Definition 39] is not syntactic, but relies on a decidable semantic check [6, Proposition 42]. In contrast, our regular grammars have an easily-checkable syntactic definition, where iteration variables are confined to rules of the form (A) in Definition 8. Moreover, the proof of recognizability of a regular language is quite different from ours: [6] establishes recognizability via CMSO-definability, whereas we directly construct a finite recognizer algebra from a regular grammar. In principle, it is possible to derive an algebra of k-exponential size from the constructions of a CMSO formula, where k is the quantifier rank of the formula. However, this analysis is stated as future work in [6]. In contrast, each regular grammar is guaranteed to have a recognizer algebra of size at most 2-exponential in the size of the grammar. We state as an open problem the question whether this upper bound can be further improved and conjecture that this is the case at least for grammars in which the rules of the form (A) are aperiodic.

The work [7] introduced tree-verifiable graph grammars, a strict generalization of the regular graph grammars of Courcelle [3] that capture the CMSO-definable sets of graphs of bounded embeddable tree-width. This parameter is an overapproximation of the tree-width that uses tree decompositions whose backbone is a spanning tree of the considered graph. The authors of [7] already proved the equivalence with CMSO-definability of the tree grammars considered in this paper. We reprove their result using an explicit construction of a recognizer algebra, which provides complexity upper bounds for the language inclusion problem. However, our results on regular grammars for series-parallel graphs and graphs of tree-width 2 are orthogonal to the results of [7].

## II. DEFINITIONS

The set of natural numbers is denoted by $\mathbb{N}$. Given numbers $i, j \in \mathbb{N}$, we write $[i, j] =^{\text{def}} \{i, i+1, \dots, j\}$, assumed to be empty if $i > j$. The cardinality of a finite set $A$ is denoted by $\text{card}(A)$. By writing $A \subseteq_{\text{fin}} B$ we mean that $A$ is a finite subset of $B$. The disjoint union $A \uplus B$ is defined as the union of $A$ and $B$, if $A \cap B = \emptyset$, and undefined, otherwise. For a set $A$, we denote by $\text{pow}(A)$ its powerset and by $\text{pow}_{\text{fin}}(A)$ the set of finite subsets of $A$. For a set $A$, we denote by $A^+$ the set of non-empty ordered sequences of elements from $A$ and by $|s|$ the length of a sequence $s \in A^+$.

We denote by $\text{mpow}(A)$ the power-multiset of $A$, i.e., the set of multisets $m: A \to \mathbb{N}$ and by $m_1 + m_2$ we denote the union of the multisets, i.e., $(m_1 + m_2)(a) \stackrel{\text{def}}{=} m_1(a) + m_2(a)$, for all $a \in A$.

For a relation $R \subseteq A \times B$, we denote by $\text{dom}(R)$ and $\text{img}(R)$ the sets consisting of the first and second components of the pairs in $R$, respectively. We write $R^{-1}$ for the inverse relation, $R(S)$ for the image of a set $S$ via $R$ and $R(a)$ for $R(\{a\})$, for some $a \in A$.

A bijective function $f: \mathbb{N} \to \mathbb{N}$ is a finite permutation if the set $\{n \in \mathbb{N} | f(n) \neq n\}$ is finite. The finite permutation

<footnote n="1">¹A characterization of the aperiodic sets of trees definable in first-order logic is given in [10].</footnote>
$(n, m)$ swaps $n$ and $m$ mapping each $i \in \mathbb{N} \setminus \{n, m\}$ onto itself and $[i_1, \dots, i_n]$ maps each $j \in [1, n]$ to $i_j$ and any other $j > n$ to itself.

We denote by $\text{poly}(x)$ the set of functions $p : \mathbb{N} \to \mathbb{N}$ for which there exist $a, b, k \in \mathbb{N}$ such that $p(n) \le a \cdot n^k + b$, for all $n \in \mathbb{N}$. This notation is used in exponentiation, e.g., $f \in 2^{\text{poly}(x)}$ stands for $f(x) = 2^{p(x)}$, for some $p(x) \in \text{poly}(x)$.

The proofs of the technical results are in Appendix A.

## A. Algebras and Recognizability

Let $\Sigma = \{\sigma_1, \sigma_2, \dots\}$ be a set of sorts and $\mathcal{F} = \{f_1, f_2, \dots\}$ be a signature of function symbols. Each function symbol $f$ has an associated tuple of argument sorts $\alpha(f) = (\sigma_1, \dots, \sigma_n)$ and a value sort $\sigma(f)$. The arity of $f$ is denoted $\#f = \def{\#f}{n}$. If $\#f = 0$ we call $f$ a constant. A variable is a sorted symbol of arity zero, not part of the signature. We denote by $\mathcal{V} = \{x, y, \dots\}$ the set of variables. The sort of a variable $x \in \mathcal{V}$ is denoted $\sigma(x)$. A term $t[x_1, \dots, x_n]$ is built as usual from function symbols and the variables $x_1, \dots, x_n$ of matching sorts. A term without variables is ground. A term consisting of a single variable is trivial. A term $t[x]$ having a single variable is a context. By $t[u_1, \dots, u_n]$ we denote the term obtained by replacing each occurrence of $x_i$ by $u_i$, for all $i \in [1, n]$. A subterm of $t$ is a term $u[x_1, \dots, x_n]$ such that $t = w[u[t_1, \dots, t_n]]$ for a context $w[x]$ and terms $t_1, \dots, t_n$. Note that this is not the usual definition of subterm, usually defined as a full subtree rooted at some position within $t$.

An $(\mathcal{F}, \Sigma)$-algebra is a tuple $\mathcal{A} = (\{\mathcal{A}^{\sigma}\}_{\sigma \in \Sigma}, \{f^{\mathcal{A}}\}_{f \in \mathcal{F}})$, where each $\mathcal{A}^{\sigma}$ is the domain of sort $\sigma$ and $f^{\mathcal{A}} : \mathcal{A}^{\sigma_1} \times \dots \times \mathcal{A}^{\sigma_n} \to \mathcal{A}^{\sigma}$ is the interpretation of the function symbol $f \in \mathcal{F}$, where $\alpha(f) = (\sigma_1, \dots, \sigma_n)$ and $\sigma(f) = \sigma$. We sometimes omit writing $\Sigma$ and assume that $\Sigma = \{\sigma \mid f \in \mathcal{F}, \sigma = \sigma(f) \text{ or } \sigma \in \alpha(f)\}$. The domains of different sorts are assumed to be disjoint and $\mathcal{A} \stackrel{\text{def}}{=} \bigsqcup_{\sigma \in \Sigma} \mathcal{A}^{\sigma}$ denotes the domain of $\mathcal{A}$. The algebra $\mathcal{A}$ is locally finite if $\mathcal{A}_{\sigma}$ is finite, for each $\sigma \in \Sigma$ and finite if $\mathcal{A}$ is finite.

A term $t[x_1, \dots, x_n]$ defines a function $t^{\mathcal{A}} : \mathcal{A}^{\sigma(x_1)} \times \dots \times \mathcal{A}^{\sigma(x_n)} \to \mathcal{A}^{\sigma(t)}$ obtained by interpreting each function symbol from $t$ in $\mathcal{A}$. An $\mathcal{F}$-algebra is representable if its universe is the set of values of the ground $\mathcal{F}$-terms. Each algebra considered in this paper will be representable.

Given $\mathcal{F}$-algebras $\mathcal{A}$ and $\mathcal{B}$, a homomorphism between $\mathcal{A}$ and $\mathcal{B}$ is a function $h : \mathcal{A} \to \mathcal{B}$ such that $\sigma(h(a)) = \sigma(a)$, for all $a \in \mathcal{A}$ and $h(f^{\mathcal{A}}(a_1, \dots, a_n)) = f^{\mathcal{B}}(h(a_1), \dots, h(a_n))$, for all $f \in \mathcal{F}$ and elements $a_1, \dots, a_n \in \mathcal{A}$ of matching sorts. Note that a homomorphism between multi-sorted algebras is sort-preserving. Assuming that $\mathcal{A}$ and $\mathcal{B}$ are representable algebras, it can be shown that, if a homomorphism between $\mathcal{A}$ and $\mathcal{B}$ exists<fnref n="2" />, then it is unique and surjective. In this case, the unique homomorphism between $\mathcal{A}$ and $\mathcal{B}$ is denoted $h_{\mathcal{A},\mathcal{B}}$. The following notions are central to this paper:

**Definition 1:** Let $\mathcal{A}$ be an $\mathcal{F}$-algebra. An $\mathcal{F}$-recognizer for $\mathcal{A}$ is a pair $(\mathcal{B}, \mathcal{C})$, where $\mathcal{B}$ is a locally finite $\mathcal{F}$-algebra,

$\mathcal{C} \subseteq \mathcal{B}$ and the homomorphism $h_{\mathcal{A},\mathcal{B}}$ exists. A set $\mathcal{L} \subseteq \mathcal{A}$ is recognized by $(\mathcal{B}, \mathcal{C})$ iff $\mathcal{L} = h_{\mathcal{A},\mathcal{B}}^{-1}(\mathcal{C})$. A set is recognizable in $\mathcal{A}$ if $\mathcal{L} = h_{\mathcal{A},\mathcal{B}}^{-1}(\mathcal{C})$, for an $\mathcal{F}$-recognizer $(\mathcal{B}, \mathcal{C})$.

The recognizable sets of an algebra are closed under union, intersection and complement with respect to the domain of that algebra. These operations are effectively computable when the recognizer algebra is effectively computable.

We say that a $(\mathcal{F}_{\mathcal{B}}, \Sigma_{\mathcal{B}})$-algebra $\mathcal{B}$ is derived from the $(\mathcal{F}_{\mathcal{A}}, \Sigma_{\mathcal{A}})$-algebra $\mathcal{A}$ if $\Sigma_{\mathcal{B}} \subseteq \Sigma_{\mathcal{A}}$ and, for every function symbol $f \in \mathcal{F}_{\mathcal{B}}$, there exists some $\mathcal{F}_{\mathcal{A}}$-term $t_f$ such that $f^{\mathcal{B}} = t_f^{\mathcal{A}}$. It is easy to prove that recognizability in an algebra implies recognizability in each of its derived algebras, but not viceversa. For instance, the word language $\{a^n b^n \mid n \in \mathbb{N}\}$ is recognizable in the algebra of words with operation $x \mapsto axb$, but not in the classical monoid of words with concatenation.

Additional material concerning recognizability is given in Appendix B.

## B. Graphs

Let $\mathcal{A}$ be a fixed finite alphabet of edge labels, having associated arities $\#a \ge 1$ for each $a \in \mathcal{A}$. The following definition introduces hypergraphs, where edges are attached to ordered sequences of vertices, of length one or more, in which a vertex can occur multiple times. For simplicity, we call these objects graphs, in the rest of the paper.

**Definition 2:** A graph of sort $\tau \subseteq_{\text{fin}} \mathbb{N}$ is a tuple $G = (V, E, \lambda, v, \xi)$, where $V$ and $E$ are finite sets of vertices and edges, respectively, $\lambda : E \to \mathcal{A}$ and $v : E \to V^+$ give the label and sequence of vertices attached to each edge, respectively, such that $\#\lambda(e) = |v(e)|$, for each edge $e \in E$, and $\xi : \tau \to V$ is a one-to-one mapping that designates the sources of $G$. A vertex $\xi(s)$ is called the $s$-source of $G$. We write $V_G, E_G, \lambda_G, E_G$ and $\xi_G$ for the elements of $G$.

**Definition 3:** The graph algebra $\mathcal{G}$ has the signature:

$$ \mathcal{F}_{\mathcal{G}}^{\text{def}} = \{ \mathbf{0}_{\tau}, \text{restrict}_{\tau} \mid \tau \subseteq_{\text{fin}} \mathbb{N} \} \cup \\ \{ a_{s_1, \dots, s_n} \mid a \in \mathcal{A}, \#a = n, s_1, \dots, s_n \in \mathbb{N} \} \cup \\ \{ \text{rename}_{\alpha} \mid \alpha \text{ finite permutation of } \mathbb{N} \} \cup \\ \{ \|_{\tau_1, \tau_2} \mid \tau_1, \tau_2 \subseteq_{\text{fin}} \mathbb{N} \} $$

interpreted over the domain $\mathcal{G}$ of graphs as follows:

- $\mathbf{0}_{\tau}^{\mathcal{G}}$ is the graph of sort $\tau$ consisting of one $s$-source, for each $s \in \tau$ and no edges,

- $a_{s_1, \dots, s_n}^{\mathcal{G}}$ is the graph of sort $\{s_1, \dots, s_n\}$ consisting of a single $a$-labeled edge attached to the $s$-source of a source $s_1, \dots, s_n$ (note that the sources $s_1, \dots, s_n$ are not required to be pairwise distinct),

- $\text{restrict}_{\tau}^{\mathcal{G}}(x)$ forgets the source labels $s \in \sigma(x) \setminus \tau$ from $x$,

- $\text{rename}_{\alpha}^{\mathcal{G}}(x)$ renames the sources of $x$ according to $\alpha$,

- $x_1 \|_{\sigma(x_1), \sigma(x_2)}^{\mathcal{G}}$, $x_2$ is the disjoint union of $x_1$ and $x_2$, followed by joinining the $s$-sources, respectively, for all $s \in \sigma(x_1) \cap \sigma(x_2)$.

**Example.** For example, the leftmost graph in Figure 1 (a) has four vertices of which tree sources labeled 1, 2 and 3 and three edges labeled $a, b$ and $c$. The $a$-labeled edge is attached to three vertices, whereas the $b$- and $c$-labeled edges are

<footnote n="2">²For instance, there is no homomorphism between the $\mathcal{F}$-algebras $\mathcal{A}$ and $\mathcal{B}$ if $c_1^A = c_2^A$ and $c_1^B \neq c_2^B$, for distinct constants $c_1, c_2 \in \mathcal{F}$.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. Composition (a), Restriction (b) and Renaming (c) of Graphs. Append (d) and Composition (e) of Trees. Sources are denoted by hollow circles. Each arrow indicates the order of vertices attached to the corresponding edge.</figcaption></figure>

binary. The middle graph is of sort $\{1, 2, 4\}$ and the rightmost one of sort $\{1, 2, 3, 4\}$. Figure 1 (a) shows the result of the composition of two graphs, whereas (b) and (c) show the result of applying restriction and renaming to this composition.

Note that the parallel composition of graphs of equal sorts $\|_{\tau,\tau}^G$ is associative and commutative, for each sort $\tau \subseteq_{fin} \mathbb{N}$. For simplicity, we write $\|_{\tau,\tau}$ instead of $\|_{\tau,\tau}$ if $\tau$ can be inferred from the context. We use the syntactic shorthands:

$$x^{\#0} = \mathbf{0}_{\sigma(x)} \qquad x^{\#n} \stackrel{\text{def}}{=} \underbrace{x \| \dots \| x}_{n \ge 1 \text{ times}}$$

The following definition is used to introduce trees, series-parallel graphs and graphs of tree-width at most 2:

**Definition 4:** A class $\mathcal{C}$ of graphs is a derived $(\mathcal{F}_C, \Sigma_C)$-algebra of $\mathcal{G}$, where $\mathcal{F}_C$ is a finite signature and $\Sigma_C$ is finite set of sorts such that $\|_{\tau,\tau} \in \mathcal{F}_C$, for each $\tau \in \Sigma_C$.

For each integer $k \ge 1$, we define the subalgebra $\mathcal{G}^{\le k}$ over the signature $\mathcal{F}_{\mathcal{G}}^{\le k}$ consisting of the function symbols from $\mathcal{F}_G$ restricted to sorts that are subsets of $[1, k+1]$, having the same interpretation as in $\mathcal{G}$. Since $\mathcal{F}_{\mathcal{G}}^{\le k}$ is a finite signature that contains $\|_{\tau,\tau}$, for each $\tau \subseteq [1, k+1]$, we obtain that each algebra $\mathcal{G}^{\le k}$ is a class. Note that $\mathcal{G}$ is not a class because the signature $\mathcal{F}_G$ is infinite.

We also consider aperiodic algebras over signatures containing parallel composition(s). Given an algebra $\mathcal{A}$ having sorts $\Sigma_{\mathcal{A}}$ over a signature $\mathcal{F}_{\mathcal{A}}$ containing $\|_{\tau,\tau}$, for each sort $\tau \in \Sigma_{\mathcal{A}}$, an element $a \in \mathcal{A}$ is idempotent if $a \|^{\mathcal{A}} a = a$. An idempotent power of $a$ is an idempotent element of the form $a^{\#n}$, for some $n \ge 1$. It is easy to see that each element $a$ of a locally finite algebra has a unique idempotent power, denoted $\mathrm{idem}(a)$.

**Definition 5:** A locally finite algebra $\mathcal{A}$ is aperiodic if and only if $\mathrm{idem}(a) \|^{\mathcal{A}} a = \mathrm{idem}(a)$, for each element $a \in \mathcal{A}$. A recognizer $(\mathcal{A}, \mathcal{B})$ is aperiodic if the algebra $\mathcal{A}$ is aperiodic.

### C. Trees

Trees form a class of graphs having a single sort $\{1\}$, where the 1-source of a tree is its root. Following the definitions of Courcelle [3], we consider trees with edges of parity two or more, where the first vertex attached to an edge is the parent of the latter vertices attached to the same edge. The children of a node are thus grouped into several sets of same-edge siblings. The set of trees is generated by operations from Figure 1 (d) and (e), starting from graphs with a single vertex and no edges.

**Definition 6:** The class $\mathcal{T}$ of trees has signature:

$$\mathcal{F}_{\mathcal{T}} \stackrel{\text{def}}{=} \{ \mathrm{append}_b | b \in \mathcal{A} \} \cup \{ \|, \mathbf{0}_{\{1\}} \}$$

where $\mathrm{append}_b^T(x_1, \dots, x_{\#b-1})$ joins the roots of the trees $x_1, \dots, x_{\#b-1}$ to the positions 2, \dots, \#b of an edge labeled $b$, whose first position becomes the root of the resulting tree. The interpretations of $\|$ and $\mathbf{0}_{\{1\}}$ are the same in the tree algebra $\mathcal{T}$ as in the graph algebra $\mathcal{G}$ (Definition 3).

It is easy to see that $\mathcal{T}$ is indeed a derived algebra of $\mathcal{G}^3$. The standard terminology is immediately retrieved from the above definition. The vertices of a tree are called *nodes*. For each edge, the first vertex attached to it is the *parent* of the other vertices called *children*. Note that a node may be attached to several edges on the first position and hence may have children corresponding to different edges. The *rank* of a tree is the maximum number of children of a node. A set of trees is *ranked* if the corresponding set of ranks is finite and *unranked*, otherwise. In particular, the domain of $\mathcal{T}$ is unranked. A binary tree is a tree with binary edges only.

Binary trees are used in the definition of the tree-width parameter of a graph. A set of nodes $N$ in a tree is connected iff between any two nodes in $N$ there exists an undirected path of edges that traverses only nodes from $N$.

**Definition 7:** A tree decomposition of a graph $G$ is a pair $(T, \beta)$, where $T$ is a binary tree and $\beta: V_T \to \mathrm{pow}(V_G)$ is a mapping of the nodes of $T$ with bags of vertices from $G$, such that: (1) the sources of $G$ are contained in some bag, (2) for each edge of $G$, the vertices attached to it are contained in some bag, (3) for each vertex of $G$, the nodes of $T$ whose bags contain it form a non-empty connected component of $T$. The width of the tree decomposition is $\mathrm{wd}(T, \beta) \stackrel{\text{def}}{=} \max\{\mathrm{card}(\beta(n)) \mid n \in V_T\} - 1$ and the *tree-width* of $G$ is $\mathrm{twd}(G) \stackrel{\text{def}}{=} \min\{\mathrm{wd}(T, \beta) \mid (T, \beta) \text{ tree decomposition of } G\}$.

In this paper we consider graphs of tree-width at most 2, and some proper subclasses such as (disoriented) series-parallel graphs.

## III. GRAMMARS

We aim at using grammars to define the recognizable sets of graphs pertaining to certain classes, e.g., trees, series-parallel

$$^3\mathrm{append}_b^T(x_1, \dots, x_{\#b-1}) \stackrel{\text{def}}{=} \mathrm{restrict}_{\{1\}}^{\mathcal{G}}(b_{1,2,\dots,\#b}^{\mathcal{G}}) \|^{\mathcal{G}} \mathrm{rename}_{(1,2)}^{\mathcal{G}}(x_1) \|^{\mathcal{G}} \dots \mathrm{rename}_{(1,\#b)}^{\mathcal{G}}(x_{\#b-1})$$
and tree-width 2 graphs. Given a signature $\mathcal{F}$, a $\mathcal{F}$-grammar
$\Gamma = (\mathcal{N}, \mathcal{R})$ consists of a finite set $\mathcal{N}$ of sorted nonterminals
and a finite set $\mathcal{R}$ of rules of the form (i) $X \to t[X_1, \dots, X_n]$,
where $X, X_1, \dots, X_n \in \mathcal{N}$ and $t$ is an $\mathcal{F}$-term of sort $\sigma(X)$,
or (ii) $\to X$, for some $X \in \mathcal{N}$, called axioms. We denote by
size($\Gamma$) the total number of occurrences of a nonterminal or
function symbol in some rule of $\mathcal{R}$.

Given terms *u* and *w*, a derivation step *u* $\Rightarrow_{\Gamma}$ *w* obtains *w*
by replacing an occurrence of a variable *X* in *u* by a term
*t*, where *X* $
rightarrow *t$ is a rule of $\Gamma$. A *X*-derivation of *t* is a
finite sequence of derivation steps *X* $\Rightarrow_{\Gamma}^{*}$ *t*. The derivation
is complete iff *t* is a ground term. Given an $\mathcal{F}$-algebra
$\mathcal{A}$, the language of $\Gamma$ in $\mathcal{A}$ is $\mathcal{L}^{\mathcal{A}}(\Gamma) \stackrel{\text{def}}{=} \bigcup_{\to X \in \mathcal{R}} \mathcal{L}_{\mathcal{X}}^{\mathcal{A}}(\Gamma)$,
where $\mathcal{L}_{\mathcal{X}}^{\mathcal{A}}(\Gamma) \stackrel{\text{def}}{=} \{t^{\mathcal{A}} \mid X \Rightarrow_{\Gamma}^{*} t \text{ complete derivation}\}$. A set
is context-free iff it is the language of a grammar.

Alternatively, a context-free set is the set of evaluations of
a recognizable set of terms in a given algebra. Note that the
rules of a grammar are an equivalent representation of a set
of terms recognized by a tree automaton, see [8].

The filtering of an $\mathcal{F}$-grammar $\Gamma = (\mathcal{N}, \mathcal{R})$ by an $\mathcal{F}$-recognizer $(\mathcal{B}, \mathcal{C})$ is the $\mathcal{F}$-grammar $\Gamma^{(\mathcal{B}, \mathcal{C})}$ having a non-terminal $X^b$ for each $X \in \mathcal{N}$ and $b \in \mathcal{B}$ and rules either (i) $X^b \to t[X_1^{b_1}, \dots, X_n^{b_n}]$, for each rule $X \to t[X_1, \dots, X_n] \in \mathcal{R}$ and each sequence of elements $b, b_1, \dots, b_n \in \mathcal{B}$, such that $b = t^\mathcal{B}(b_1, \dots, b_n)$, or (ii) $\to X^c$, for each axiom $\to X \in \mathcal{R}$ and each element $c \in \mathcal{C}$. The following result is also known as the Filtering Theorem:

Theorem 1 (Theorem 3.88 in [2]): Let $\mathcal{A}$ be an $\mathcal{F}$-algebra.
For each $\mathcal{F}$-grammar $\Gamma = (\mathcal{N}, \mathcal{R})$ and $\mathcal{F}$-recognizer $(\mathcal{B}, \mathcal{C})$
for $\mathcal{A}$, we have $\mathcal{L}^\mathcal{A}(\Gamma^{(\mathcal{B}, \mathcal{C})}) = \mathcal{L}^\mathcal{A}(\Gamma) \cap h_{\mathcal{A}, \mathcal{B}}^{-1}(\mathcal{C})$. Moreover,
$\Gamma^{(\mathcal{B}, \mathcal{C})}$ can be built in time $\mathcal{O}(\mathrm{card}(\mathcal{R}) \cdot \mathrm{card}(\mathcal{B})^{\mathrm{card}(\Gamma)} \cdot \Omega^{\mathrm{size}(\Gamma)})$,
where $\Omega$ is an upper bound on the time needed to
compute $f^\mathcal{A}(b_1, \dots, b_{\#f})$, for each function symbol $f \in \mathcal{F}$
and elements $b_1, \dots, b_{\#f} \in \mathcal{B}$.

The estimation on the time needed to build a filtered grammar
follows immediately from its definition$^4$.

A. Stratified Grammars

Stratified grammars have been introduced by Courcelle
(under the name AC grammars, for associative-commutative)
as a simple syntactic restriction that ensures the recognizability
of an unranked context-free set of trees [3, Definition 3.7].
However, the initial definition of AC grammars does not
capture all recognizable unranked sets of trees (e.g., trees
with an even number of leaves cannot be defined by AC
grammars). In contrast, we prove later that our definition of
stratified grammars completely characterize the recognizable
sets of unranked trees and beyond (i.e., series-parallel and
graphs of tree-width 2). Moreover, a syntactic fragment of
stratified grammars defines exactly those sets recognized by
aperiodic algebras (Definition 5).

*Definition 8:* A stratified *F*-grammar $\Gamma = (\mathcal{N}, \mathcal{R})$ has non-terminals partitioned as $\mathcal{N} = \mathcal{X} \uplus \mathcal{Y}$ and rules of the following

forms, for some nonterminals $X \in \mathcal{X}$ and $Y, Y_1, \dots, Y_k \in \mathcal{Y}$
pairwise distinct:

A. $X \to X \parallel Y^{\sharp q}$, for an integer $q \ge 1$,

B. $X \to Y_1^{\sharp q_1} \parallel \dots \parallel Y_k^{\sharp q_k}$, for integers $q_1, \dots, q_k \ge 1$,

C. $Y \to t[Z_1, \dots, Z_m]$, for an $\mathcal{F}$-term $t$, $Z_1, \dots, Z_m \in \mathcal{N}$,

D. $X \to t$, for a ground $\mathcal{F}$-term $t$,

E. $\to Z, Z \in \mathcal{N}$.

We say that $\Gamma$ is *aperiodic* if and only if, for every pair of non-terminals $X \in \mathcal{X}$ and $Y \in \mathcal{Y}$, the set of rules $\{X \to X \parallel Y^{\sharp q_i} \in \mathcal{R}\}_{i \in [1,k]}$ (A) is either (i) empty, (ii) a singleton and $q_1 = 1$, or (iii) $k \ge 2$ and $q_1, \dots, q_k$ are coprime.

We define the footprint of stratified grammars in terms of
templates describing the shape of the rules of the form other
than (A). The templates will be defined as grammar rules
over a special set of nonterminals consisting of exactly two
nonterminals $X_{\tau}$ and $Y_{\tau}$ of sort $\tau$, for every sort $\tau$ of the
considered class. Intuitively, $X_{\tau}$ resp. $Y_{\tau}$ describe the possible
occurrences of the nonterminals $X \in \mathcal{X}$ (resp. $Y \in \mathcal{Y}$) with
$\sigma(X) = \tau$ (resp. $\sigma(Y) = \tau$). We introduce the following
notation that relates the nonterminals $Z \in \mathcal{X} \uplus \mathcal{Y}$ of a
stratified grammar to the corresponding template nonterminals:
$\theta(Z) \stackrel{\text{def}}{=} X_{\sigma(Z)}$, for $Z \in \mathcal{X}$, and $\theta(Z) \stackrel{\text{def}}{=} Y_{\sigma(Z)}$, for $Z \in \mathcal{Y}$.

*Definition 9:* The footprint of a stratified grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ is the set $\mathrm{FP}(\Gamma)$ consisting of the templates:

1. $X_{\tau} \to Y_{\tau}^{\sharp m}$, where $m \stackrel{\text{def}}{=} \min\{\sum_{i=1}^k q_i \mid X \to Y_1^{\sharp q_1} \parallel \dots \parallel Y_k^{\sharp q_k} \in \mathcal{R}, \sigma(X) = \sigma(Y_i) = \tau\}$, where $\min \emptyset = \infty$ if there is no such rule,

2. $\theta(Z) \to t[\theta(Z_1), \dots, \theta(Z_m)]$, for each rule $Z \to t[Z_1, \dots, Z_m] \in \mathcal{R}$ of the form (C) or (D),

3. $\to \theta(Z)$, for each axiom $\to Z$ of $\Gamma$.

Given sets of templates FP<sub>1</sub> and FP<sub>2</sub>, we write FP<sub>1</sub> ⊆ FP<sub>2</sub>
if and only if m<sub>1</sub> ≥ m<sub>2</sub>, for all X<sub>τ</sub> → Y<sub>τ</sub><sup>tm<sub>1</sub></sup> ∈ FP<sub>1</sub> and
X<sub>τ</sub> → Y<sub>τ</sub><sup>tm<sub>2</sub></sup> ∈ FP<sub>2</sub>, and each template of types 2 or 3 from
FP<sub>1</sub> belongs to FP<sub>2</sub>.

Footprints will be used in the definition of regular gram-
mars. For each class $\mathcal{C}$, we will fix a footprint $\mathrm{FP}_{\mathcal{C}}$ and define
the regular grammars for the class as the set of grammars $\Gamma$
having $\mathrm{FP}(\Gamma) \subseteq \mathrm{FP}_{\mathcal{C}}$.

Certain uses of stratified grammars require a normal form:

*Definition 10:* A stratified grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ is *normalized* iff, for each pair of nonterminals $(X, Y) \in \mathcal{X} \times \mathcal{Y}$, there exists at most one rule $X \to X \parallel Y^{\sharp q} \in \mathcal{R}$ of form (A).

The following lemma shows that the normalization of a
stratified grammar is effective, at the cost of an exponential
blowup in size, and incurs a restriction of the footprint:

Lemma 1: Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ be a stratified grammar for a class $\mathcal{C}$. Then, one can build a normalized stratified grammar $\Gamma' = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R}')$ such that:

1. $\mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma)$,

2. $\mathrm{FP}(\Gamma') \subseteq \mathrm{FP}(\Gamma)$,

3. size(Γ') ∈ 2^poly(size(Γ)·log(size(Γ))),

Moreover, $\Gamma$ is aperiodic only if $q = 1$, for all rules $X \to X \parallel Y^{\sharp q}$ of the form (A) from $\Gamma'$.

See proof on page 14. It is worth pointing out that the
above lemma is true in any algebra that interprets the parallel
composition as an associative and commutative operation.

<footnote n="4">⁴The upper bound $\Omega$ is needed to evaluate the side condition $b = t^\mathcal{B}(b_1, \dots, b_n)$ for a term $t$ in a rule $X \to t[X_1, \dots, X_n] \in \mathcal{R}$, where the size of $t$ is bounded by $\mathrm{size}(\Gamma)$.</footnote>
The result of applying the Filtering Theorem (Theorem 2) directly to a stratified grammar and a recognizer ($\mathcal{B}, \mathcal{C}$) is not necessarily a stratified grammar, e.g., because a rule $X \to X \parallel Y$ (A) yields zero or more rules $X^a \to X^b \parallel Y^c$, for each $a, b, c \in \mathcal{B}$ such that $a \neq b$ and $a = b \parallel \mathcal{B}^c$, that are not of the form (A). The next result strengthens the Filtering Theorem, showing that the intersection of the language of a stratified grammar with a recognizable set can be represented by an effectively constructible stratified grammar, whose footprint is included in the original one:

**Theorem 2 (Refinement Theorem):** Let $\mathcal{C}$ be a class. For each stratified $\mathcal{F}_\mathcal{C}$-grammar $\Gamma$ and each $\mathcal{F}_\mathcal{C}$-recognizer $(A, B)$ one can build a stratified $\mathcal{F}_\mathcal{C}$-grammar $\Gamma'$ such that $\mathrm{FP}(\Gamma') \subseteq \mathrm{FP}(\Gamma)$ and $\mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma^{(A,B)})$. Moreover, $\Gamma'$ is aperiodic whenever $\Gamma$ is an aperiodic stratified grammar and $\mathcal{A}$ is an aperiodic $\mathcal{F}_\mathcal{C}$-algebra.

See proof on page 15.

The refinement theorem will be used as follows: We first establish the existence of a universally stratified grammar, i.e., a grammar $\Gamma_C$ with $\mathrm{FP}(\Gamma_C) = \mathrm{FP}_C$ and $\mathcal{L}^c(\Gamma_C) = \mathcal{C}$. The upcoming definitions of regular grammars via the condition $\mathrm{FP}(\Gamma) \subseteq \mathrm{FP}_C$ will then ensure that these families of grammars are closed under refinement (Theorem 2), see Corollary 1:

**Definition 11:** A class $\mathcal{C}$ is (aperiodic) universally stratified if there exists a (aperiodic) stratified grammar $\Gamma_C$ such that $\mathrm{FP}(\Gamma_C) = \mathrm{FP}_C$ and $\mathcal{L}^c(\Gamma_C) = \mathcal{C}$, for the domain $\mathcal{C}$ of $\mathcal{C}$.

**Corollary 1:** Let $\mathcal{C}$ be a (aperiodic) universally stratified class and $\mathcal{L} \subseteq \mathcal{C}$ be a set recognizable in $\mathcal{C}$ (by an aperiodic recognizer). Then, there exists a (aperiodic) stratified grammar $\Gamma$ for $\mathcal{C}$ such that $\mathrm{FP}(\Gamma) \subseteq \mathrm{FP}(\Gamma_C)$ and $\mathcal{L} = \mathcal{L}^c(\Gamma)$.

See proof on page 16.

In the rest, we introduce several notions needed to prove the contrapositive of Corollary 1, namely that the language of a stratified grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ in a given class $\mathcal{C}$ is recognizable in $\mathcal{C}$. This is achieved by building, from the grammar $\Gamma$ a recognizer $(\mathcal{A}_\Gamma, \mathcal{B}_\Gamma)$ for its language. The elements of the recognizer algebra $\mathcal{A}_\Gamma$ will include multisets of nonterminals from the set $\mathcal{Y}$ of the given stratified grammar. These multisets are finite representations of graphs consisting of arbitrarily large parallel compositions of subgraphs. The purpose of the notions below is bounding the multiplicity of these multisets, in order to define the finite algebra $\mathcal{A}_\Gamma$.

Given a multiset $m \in \mathrm{mpow}(\mathcal{Y})$, we define the reduced multiset $\lceil m \rceil_\Gamma$, in which each nonterminal $Y$ has multiplicity $\lceil m \rceil_\Gamma(Y)$ bounded by a constant depending on $\Gamma$. A multiset $m$ is said to be reduced iff $m = \lceil m \rceil_\Gamma$. The definition of the reduction operation relies on the exponents occurring in the rules of the form (A) and (B) from $\Gamma$.

Formally, let $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ be a stratified grammar. For each nonterminal $Y \in \mathcal{Y}$, we define the following integers, depending on $\Gamma$:

$$b(Y) \stackrel{\text{def}}{=} \max\{q_i \mid X \to Y_1^{\sharp q_1} \parallel \dots \parallel Y_n^{\sharp q_n} \in \mathcal{R}, Y_i = Y\}$$

$$p(Y) \stackrel{\text{def}}{=} \max\{1, \lcm\{q \mid X \to X \parallel Y^{\sharp q} \in \mathcal{R}\}\}$$

$$q(Y) \stackrel{\text{def}}{=} b(Y) + p(Y)$$

$$[m]_\Gamma(Y) \stackrel{\text{def}}{=} \begin{cases} m(Y), & \text{if } m(Y) < q(Y) \\ q(Y) + (m(Y) - q(Y)) \bmod p(Y), & \text{otherwise} \end{cases}$$

**Lemma 2:** Given a stratified grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$, for all multi-sets $m_1, m_2 \in \mathrm{mpow}(\mathcal{Y})$, we have $\lceil m_1 + m_2 \rceil_\Gamma = \lceil \lceil m_1 \rceil_\Gamma + \lceil m_2 \rceil_\Gamma \rceil_\Gamma$.

*Proof.* Immediate from the definition of the operation $\lceil \cdot \rceil_\Gamma$. □

Given a class $\mathcal{C}$, a $\parallel$-term is a $\mathcal{F}_\mathcal{C}$-term consisting of occurrences of some function symbol $\parallel_{\tau,\tau}$ and variables of sort $\tau \in \Sigma_\mathcal{C}$ only. For a stratified $\mathcal{F}_\mathcal{C}$-grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ and a nonterminal $X \in \mathcal{X}$, we denote by $X \rightsquigarrow_\Gamma m$ the existence of a derivation $X \Rightarrow^* \Gamma t$, where $t$ is a $\parallel$-term $t$ and $m$ is the multiset of variables from $t$. Intuitively, $X \rightsquigarrow_\Gamma m$ means that $X$ can produce the multiset $m$ of $\mathcal{Y}$ nonterminals using only the rules of the form (A) and (B) from $\Gamma$. This matching relation will be used to define the interpretation of the signature $\mathcal{F}_\mathcal{C}$ in the recognizer algebra $\mathcal{A}_\Gamma$.

*Example.* For a stratified grammar $\Gamma$ having $\mathcal{X} = \{X\}$, $\mathcal{Y} = \{Y_1, Y_2\}$ and the following rules:

$$X \to X \parallel Y_1^{\sharp 3} \quad X \to X \parallel Y_2^{\sharp 5} \quad X \to Y_1^{\sharp 2} \parallel Y_2^{\sharp 3}$$

$$X \rightsquigarrow_\Gamma m \text{ iff } m(Y_1) = 2 \bmod 3 \text{ and } m(Y_2) = 3 \bmod 5.$$

## IV. REGULAR GRAMMARS

We define formally the classes of trees (Definition 6), series-parallel graphs (Definition 14) and graphs of tree-width at most 2 (Definition 15). The regular grammars for each class are stratified grammars whose footprint is subsumed by a footprint depending on the class. Each of the considered classes is shown to have a universal aperiodic regular grammar, ensuring that every recognizable subset of the class is the language of some regular grammar (Corollary 1). The bulk of this section is devoted to establishing the reverse direction, i.e., that the language of each regular grammar is recognizable. This is achieved by an effective construction of a recognizer from the given regular grammar. This construction yields a uniform doubly-exponential upper bound on the size of the recognizer.

In the rest of this section, we prove the following result:

**Theorem 3:** Let $\mathcal{C}$ be one of the classes of trees, (dis-oriented) series-parallel graphs and graphs of tree-width at most 2. A set $\mathcal{L} \subseteq \mathcal{C}$ is recognizable (by an aperiodic recognizer) if and only if there exists a (aperiodic) regular grammar $\Gamma$ such that $\mathcal{L} = \mathcal{L}^c(\Gamma)$.

For the class of trees (Definition 6), two terms that represent the same graph differ only by a reordering of their $\parallel$-subterms, modulo associativity and commutativity. This leads to an almost canonical decomposition of trees, that is instrumental in proving the two directions of Theorem 3, i.e., the existence of a universal aperiodic stratified grammar ("only if") and of a recognizer for the language of a regular tree grammar ("if"). In particular, the elements of the recognizer are sets of multisets of nonterminals used to parse the $\parallel$-subterms of trees, where the outer sets are necessary to deal with the nondeterminism in the grammar. Hence, the doubly-exponential upper bound on the size of the recognizer algebra.
For graphs of tree-width at most 2, the proof of Theo-
rem 3 uses a standard decomposition of connected graphs
into blocks (i.e., maximally 2-connected components) [16,
Theorem III.23] in conjunction with the fact that each block of
tree-width at most 2 is a disoriented series-parallel graph [3,
Lemma 6.15]. For technical purposes, we prove a stronger
version of this result, that allows to pick any vertex for the
1-source of a block. The decomposition of a graph of tree-
width 2 as a tree of disoriented series-parallel blocks leads to
the definition of an algebra (i.e., a class) and of a family of
regular grammars, having sorts {1, 2} and {1} for blocks and
block trees, respectively. Accordingly, the recognizer algebra
is 2-sorted, multisets of nonterminals sort {1} represent block
trees, whereas multisets and pairs of nonterminals of sort
{1, 2} represent disoriented series-parallel blocks.

The upper bound on the size of the recognizer algebra for a
regular grammar generalizes from trees to graphs of tree-width
at most 2. Despite the best of our efforts, we could not find
a matching lower bound, namely a regular grammar Γ whose
language could not be recognized by an algebra with less than
$2^{2^{\text{size}(\Gamma)}}$ elements.

An application of the effective construction of recognizer
algebras is bounding the time complexity for the problem of
inclusion between an arbitrary context-free language and a
regular language:

**Theorem 4:** Let $\mathcal{C}$ be one of the classes of trees, (dis-oriented) series-parallel graphs and graphs of tree-width at most 2. The problem "given $\mathcal{F}_\mathcal{C}$-grammars $\Gamma$ and $\Gamma'$ such that $\Gamma'$ is regular, does $\mathcal{L}^c(\Gamma) \subseteq \mathcal{L}^c(\Gamma')$?" belongs to 2EXPTIME and is EXPTIME-hard, even if $\Gamma'$ is aperiodic.

See proof on page 16.

We believe that the above upper bound can be improved
for aperiodic regular grammars and conjecture that the size of
the minimal recognizer is bounded by a simple exponential
in the size of the grammar. If this conjecture is proved, a
consequence is that the inclusion problem between a context-
free language and an aperiodic regular language is EXPTIME-
complete, at least for the classes of graphs considered in this
paper, thus matching the complexity of the inclusion between
ranked tree languages [8, Corollary 1.7.9].

Another application of effectively constructible recognizers
is the computation of the union, intersection and complement
of recognizable sets, within their respectively classes. As a
side remark, the generalized inclusion problem, of a context-
free language into a boolean combination of recognizable
languages has the same 2EXPTIME upper bound as the
problem from Theorem 4.

A. *Trees*

Let $\mathbb{A}$ be a finite alphabet of edge labels, of arities $\#a \ge 1$ for each $a \in \mathbb{A}$. We recall that the class $\mathcal{T}$ of unordered trees has signature $\mathcal{F}_{\mathcal{T}} = \{\text{append}_b | b \in \mathbb{A}\} \cup \{\|, \mathbf{0}_{\{1\}}\}$ and sort $\{1\}$, where the 1-source of a tree is its root (Definition 6). For simplicity, the footprint $\text{FP}_{\mathcal{T}}$ of the class of trees is written using X and Y instead of $X_{\{1\}}$ and $Y_{\{1\}}$, respectively:

<figure><img src="image_3.png" /><figcaption>Fig. 2. A view $\{\{Y_1, \dots, Y_n\}\}$ of a tree $(v_1 \| \dots \| v_n)^T$.</figcaption></figure>

**Definition 12:** A regular tree grammar is a stratified $\mathcal{F}_{\mathcal{T}}$-grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ such that $\text{FP}(\Gamma) \subseteq \text{FP}_{\mathcal{T}}$, where:

$$
\begin{align*}
\text{FP}_{\mathcal{T}} &\stackrel{\text{def}}{=} \{\mathbf{X} \to \mathbf{Y}^{\#\ge 0}\} \cup \{\mathbf{Y} \to \text{append}_b(\mathbf{X}, \dots, \mathbf{X}) \mid b \in \mathbb{A}\} \\
&\phantom{=} \cup \{\to \mathbf{X}\}
\end{align*}
$$

To establish the “only if” direction of Theorem 3 for the
class $\mathcal{T}$ it is sufficient to prove the existence of an aperiodic
universal regular tree grammar (Corollary 1). Lemma 3 below
shows that such a grammar exists. To improve clarity, we
annotate each rule with its type, according to Definition 8:

*Lemma 3:* Let $\Gamma_{\mathcal{T}} \stackrel{\text{def}}{=} (\{X, Y\}, \mathcal{R})$ be the regular tree grammar having the following rules:

$$
\begin{array}{rcl}
Y & \to & \text{append}_a(X, \dots, X), \text{ for all } a \in \mathbb{A} \quad (\text{C}) \\
X & \to & X \parallel Y \quad (\text{A}) \quad X \to \mathbf{0}_{\{1\}} \quad (\text{B}) \quad \to X \quad (\text{E})
\end{array}
$$

Then, we have $\mathcal{L}^{\tau}(\Gamma_{\tau}) = \mathcal{T}$.

See proof on page 17.

Note that the rule $X \to \mathbf{0}_{\{1\}}$ is of the form (B) because the
right-hand side is an empty parallel composition. It is easy to
see that $\text{FP}(\Gamma_{\mathcal{T}})$ is a subset of the footprint $\text{FP}_{\mathcal{T}}$ of the class
of trees (Definition 12) and the only rule of the form (A) has
exponent 1, hence $\Gamma_{\mathcal{T}}$ is an aperiodic regular tree grammar.

To establish the “if” direction of Theorem 2 for the class $\mathcal{T}$, let us fix a normalized regular tree grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$. Assuming that $\Gamma$ is normalized loses no generality (Lemma 1). Intuitively, a view of a tree $T$ is a multiset of $\mathcal{Y}$ nonterminals that gives the complete information on how $T$ is parsed by a subsequence of some derivation of $\Gamma$. Reduced views provide a finitary abstraction of this information, that loses no precision. A profile (i.e., the set of all possible reduced views) describes all the possible ways in which $T$ can be parsed by the grammar. Figure 2 depicts this intuition, formalized below:

**Definition 13:** Let $T$ be a tree and $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ be a normalized regular tree grammar. A view of $T$ for $\Gamma$ is a multiset $\{\{Y_1, \dots, Y_n\}\} \in \text{mpow}(\mathcal{Y})$ such that there exist complete derivations $Y_i \Rightarrow_{\Gamma}^* v_i$, for all $i \in [1, n]$ and $T = (v_1 \parallel \dots \parallel v_n)^T$. A reduced view of $T$ is a multiset $[m]_{\Gamma}$, where $m$ is a view of $T$ of $T$, for $\Gamma$. The profile of $T$ for $\Gamma$ is the set $h_{\Gamma}(T) \stackrel{\text{def}}{=} \{[m]_{\Gamma} | m \text{ is a view of } T \text{ for } \Gamma\}$.

We shall build a $\mathcal{F}_{\mathcal{T}}$-recognizer $(\mathcal{A}_{\Gamma}, B_{\Gamma})$ such that
$\mathcal{L}^{\tau}(\Gamma) = h_{\Gamma}^{-1}(B_{\Gamma})$, where $h_{\Gamma}$ is the function that maps a
tree to its profile. The $\mathcal{F}_{\mathcal{T}}$-algebra $\mathcal{A}_{\Gamma}$ has domain $\mathcal{A}_{\Gamma} \stackrel{\text{def}}{=} \{h_{\Gamma}(T) \mid T \in \mathcal{T}\}$. The interpretations of the function symbols
from $\mathcal{F}_{\mathcal{T}}$ are the least sets built according to the inference
rules from Figure 3.

Note that the algebra $\mathcal{A}_{\Gamma}$ is finite, because there are
finitely many reduced views, i.e., a reduced view counts
each nonterminal $Y \in \mathcal{Y}$ up to a bound depending on the
is partitioned into P-graphs, that are ◦-atomic, and S-graphs, that are not ◦-atomic. For example, Figure 4 (a) shows an S-graph on the top-right and a P-graph on the bottom-right.

**Lemma 8 (Lemma 6.3 in [3]):** For each $G \in SP$, we have:

1. If $G$ is an S-graph then there exists a unique sequence $G_1, \dots, G_k$ of P-graphs such that $G = G_1 \circledSP \dots \circledSP G_k$, for some $k \ge 2$.

2. If $G$ is a P-graph then either $G$ is a single edge, or there exists a unique nonempty set $\{G_1, \dots, G_k\}$ of single edges and S-graphs such that $G = G_1 \Vert^{SP} \dots \Vert^{SP} G_k$, for some $k \ge 2$.

To apply this canonical decomposition to a disoriented series-parallel graph of sort $\{1, 2\}$, one notices that each disoriented series-parallel graph can be transformed into an oriented one by a unique reversal of zero or more edges. For instance, the triangle in Figure 4 (b) has a unique decomposition as $(c_{1,2} \circ a_{1,2}) \Vert b_{2,1}$. We say that a disoriented series-parallel graph is a P-graph (resp. S-graph) iff its corresponding series-parallel orientation is a P-graph (resp. S-graph).

**2) An Algebra of Tree-Width 2 Graphs:** We recall several graph-theoretic notions [16]. A cutvertex $w$ of $G$ is a vertex for which there exist two distinct vertices $u, v \in V_G \setminus \{w\}$ such that there is a path between $u$ and $v$ in $G$ and no path between $u$ and $v$ in the graph obtained from $G$ by removing the vertex $w$ and all edges incident to it. A block of $G$ is a maximal subgraph of $G$ without a cutvertex. A block is nontrivial if it has more than one vertex.

**Lemma 9:** Each connected graph with at least two vertices has only nontrivial blocks.

See proof on page 19.

A block tree of $G$ is an undirected graph<fnref n="7" /> whose vertices are the blocks and the cutvertices of $G$, and there is an edge between a block $B$ and a cutvertex $c$ of $G$ if and only if $c \in V_B$. The proof that the block tree of a graph is indeed a tree can be found in, e.g., [16, Theorem III.23]. The following lemma relates connected graphs of tree-width at most 2 with disoriented series-parallel graphs:

**Lemma 10 (Lemma 6.15 in [3]):** Let $G$ be a connected graph without sources. Then $G$ has tree-width at most 2 if and only if its blocks are either trivial or disoriented P-graphs.

We shall also need the following stronger statement:

**Lemma 11:** Let $G$ be a connected graph of tree-width at most 2, $B$ be a nontrivial block of $G$ and $x$ be a vertex of $B$. Then, there exists another vertex $y$ of $B$ such that $B_{(x,y)}$ (the graph $B$ having 1-source $x$ and 2-source $y$) is a disoriented P-graph.

See proof on page 19.

The class of connected graphs of tree-width at most 2 is the following two-sorted algebra:

**Definition 15:** The class $G_2$ has sorts $\Sigma_2 = \{\{1\}, \{1, 2\}\}$ and signature:

$$ \mathcal{F}_2 \stackrel{\text{def}}{=} \{\Vert, \circ, \triangleright, \mathbf{0}_{\{1\}}\} \cup \{b_{i,3-i} \mid b \in \mathbb{B}, i = 1, 2\}, $$

<figure><img src="image_4.png" /><figcaption>Fig. 5. Ternary serial-composition (a) and binary $\triangleright$-composition (b) for graph of tree-width at most 2.</figcaption></figure>

where we recall that we overload $\Vert$, which denotes the operations $\Vert_{\tau, \tau}$ for $\tau \in \Sigma_2 = \{\{1\}, \{1, 2\}\}$. The function symbols from $\mathcal{F}_2$ are interpreted as follows:

- $\circledG_2(x, y, z)$, where $\sigma(x) = \sigma(y) = \{1, 2\}$ and $\sigma(z) = \{1\}$, joins the 2-source of $x$ with the 1-sources of $y$ and $z$; the joined vertex is not a source of the result, of sort $\{1, 2\}$,

- $x \triangleright^{G_2} y$, where $\sigma(x) = \{1, 2\}$ and $\sigma(y) = \{1\}$, joins the 2-source of $x$ with the 1-source of $y$; the joined vertex is not a source of the result, of sort $\{1\}$.

- The rest of the function symbols from $\mathcal{F}_2$ are interpreted same as in the graph algebra $G$.

Figure 5 shows the interpretation of $\circ$ (a) and $\triangleright$ (b) in $G_2$. Note that $G_2$ is a derived algebra of the graph algebra $G^8$. We denote by $G_2^\tau$ the restriction of the domain $G_2$ of $G_2$ to the elements of sort $\tau \in \{\{1\}, \{1, 2\}\}$. The notion of disoriented P-graph (resp. S-graph) naturally extends from DSP to $G_2^{\{1,2\}}$.

We define regular grammars for the $G_2$ class. For purposes of presentation, we write $X, Y$ (resp. $\mathcal{X}$ and $\mathcal{Y}$) for the non-terminals (resp. sets of nonterminals) of sort $\{1\}$ and $P, S$ (resp. $\mathcal{P}$ and $\mathcal{S}$) for the non-terminals (resp. sets of nonterminals) of sort $\{1, 2\}$. Likewise, we will use the template names $X, Y, P$ and $S$ for footprints. Since the sorts of nonterminals are clear from this naming convention, we omit writing them.

**Definition 16:** A regular tree-width 2 grammar is a stratified grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus \mathcal{S}, \mathcal{R})$, where $\mathrm{FP}(\Gamma) \subseteq \mathrm{FP}_2$ and:

$$ \begin{aligned} \mathrm{FP}_2 &\stackrel{\text{def}}{=} \{X \to Y^{\Vert \ge 0}, P \to S^{\Vert \ge 2}, Y \to P \triangleright X, \\ &S \to \circ(P, S, X), S \to \circ(P, P, X), \to X\} \cup \\ &\{P \to b_{i,3-i}, S \to b_{i,3-i} \mid b \in \mathbb{B}, i = 1, 2\} \end{aligned} $$

First, we establish the existence of a universal aperiodic regular tree-width 2 grammar. Intuitively, a complete derivation of this grammar mimicks the block tree decomposition of a graph (Lemma 10). To this end, the sources of a disoriented series-parallel block $B$ are chosen such that the 1-source of $B$ is the cutvertex that is the parent of $B$ in the block-tree. Note that such a choice is always possible (Lemma 11).

**Lemma 12:** Let $\Gamma_2 \stackrel{\text{def}}{=} (\{X, Y, P, S\}, \mathcal{R})$ be the regular tree-width 2 grammar with the below rules, for $b \in \mathbb{B}$ and $i = 1, 2$:

<footnote n="7">⁷A directed tree is obtained by chosing any vertex as root and orienting the edges from the root downwards.</footnote>

<footnote>$^8\circledG_2(x, y, z) \stackrel{\text{def}}{=} \mathrm{rename}_{G_2^{(2,3)}}(\mathrm{restrict}_{G_2^{(1,3)}}(x \Vert^{\mathcal{G}} \mathrm{rename}_{G_2^{[2,3,1]}}(y) \Vert^{\mathcal{G}} \mathrm{rename}_{G_2^{(1,2)}}(z)))$ and $x \triangleright^{G_2} y \stackrel{\text{def}}{=} \mathrm{restrict}_{\{1\}}(x \Vert^{\mathcal{G}} \mathrm{rename}_{G_2^{(1,2)}}(y))$.</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 6. A partial derivation of an S-graph $G = (\circ(\circ(v_1, v_2, t_1), v_3, t_2), \dots, v_n, t_{n-1})^{\mathcal{G}_2}$ (a) A view of $G$ corresponding to that partial derivation (b)

(a) (b)</figcaption></figure>

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\rightarrow X \ (\text{E}) & Y \rightarrow P \triangleright X \ (\text{C}) & S \rightarrow b_{i,3-i} \ (\text{C}) \\
X \rightarrow X \parallel Y \ (\text{A}) & S \rightarrow \circ(P, S, X) \ (\text{C}) & P \rightarrow b_{i,3-i} \ (\text{D}) \\
X \rightarrow \mathbf{0}_{\{1\}} \ (\text{B}) & S \rightarrow \circ(P, P, X) \ (\text{C}) & P \rightarrow P \parallel S \ (\text{A}) \\
& & P \rightarrow S \parallel S \ (\text{B})
\end{array}
$$

The sets $\mathcal{L}^{\mathcal{G}_2}(\Gamma_2)$, $G_2^{\{1\}}$ and $\{G \in \mathcal{G} \text{ connected } | \text{tw}(G) \le 2, \sigma(G) = \{1\}\}$ are equal.

See proof on page 20.

Note that $\Gamma_2$ is an aperiodic regular tree-width 2 grammar, because $FP(\Gamma_2) \subseteq FP_2$ and the two rules of the form (A) have period 1. As in the case of trees, the result of Lemma 12 proves the “only if” direction of Theorem 3 for the $G_2$ class (Corollary 1). The “if” direction is dealt with by the construction of a recognizer for the language of a given regular tree-width 2 grammar (Theorem 6). Just as before, the size of the recognizer is doubly-exponential in the size of the input regular grammar.

The definition of views for graphs of tree-width at most 2 (Definition 18) relies on the following associative-like re-
arrangement of serial composition terms. Formally, we con-
sider an equivalence relation between $\mathcal{F}_2$-terms, such that
$u \stackrel{\sim}{\approx} w$ if and only if $w$ can be obtained from $u$ (or viceversa)
by zero or more applications of the following axiom:

$$
\circ(x_1, \circ(x_2, y, z_2), z_1) = \circ(\circ(x_1, x_2, z_1), y, z_2) \quad (1)
$$

It is easy to see that both sides of the (1) axiom evaluate to the
same graph, for any substitution of $x_i, z_i, y$, for $i = 1, 2$, with
ground terms. The $\stackrel{\sim}{\approx}$ relation allows to regroup the ground
$\mathcal{F}_2$-terms which evaluate to the P-components of an S-graph
into a single ground $\mathcal{F}_2$-term $u$ that evaluates to the serial
composition of its P-components (Figure 6). We denote by
$u \stackrel{\mathrm{a}}{\Rightarrow}_{\Gamma} w$ the existence of a derivation $u \Rightarrow_{\Gamma}^* v$ such that $v \stackrel{\mathrm{a}}{\sim} w$.

In order to simplify the development of the recognizer
we consider regular tree-width 2 grammars in the following
alternative form:

Definition 17: A regular tree-width 2 grammar in alterna-
tive form is a stratified grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus \mathcal{S}, \mathcal{R})$
such that $FP(\Gamma) \subseteq FP'_2$, where:

$$
\mathrm{FP}'_2 \stackrel{\mathrm{def}}{=} \left\{
\begin{array}{@{}l@{}}
  \mathbf{X} \to \mathbf{Y}^{\# \ge 0}, \quad \mathbf{P} \to \mathbf{S}^{\# \ge 1}, \quad \mathbf{Y} \to \mathbf{P} \triangleright \mathbf{X}, \\
  \quad \mathbf{S} \to \circ(\mathbf{P}, \mathbf{S}, \mathbf{X}), \quad \mathbf{S} \to \circ(\mathbf{P}, \mathbf{P}, \mathbf{X}), \quad \to \mathbf{X} \} \cup \\
  \quad \{\mathbf{S} \to b_{i,3-i} \mid b \in \mathbb{B}, i = 1, 2\}
\end{array}
\right\}
$$

such that for every rule $P \to S \in \mathcal{R}$ there is some rule
$S \to b_{i,3-i} \in \mathcal{R}$ and $S$ does not occur anywhere else in $\mathcal{R}$.
Each regular grammar $\Gamma$ can be transformed into a regular
grammar in alternative form $\hat{\Gamma} = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus \hat{\mathcal{S}}, \hat{\mathcal{R}})$, by
setting $\hat{\mathcal{S}} \stackrel{\mathrm{def}}{=} \mathcal{S} \uplus \{S_{b_{i,3-i}} \mid b \in \mathbb{B}, i=1,2\}$, for some fresh
nonterminals $S_{b_{i,3-i}} \notin \mathcal{S}$, and replacing each rule $P \to$
$b_{i,3-i} \in \mathcal{R}$ by the rules $P \to S_{b_{i,3-i}}$, $S_{b_{i,3-i}} \to b_{i,3-i} \in \hat{\mathcal{R}}$.
It is straightforward that $\mathcal{L}^{\mathrm{SP}}(\hat{\Gamma}) = \mathcal{L}^{\mathrm{SP}}(\Gamma)^9$ and that $\hat{\Gamma}$ is
aperiodic iff $\Gamma$ is aperiodic. Moreover, the size of the grammar
is preserved, i.e., $\mathrm{size}(\Gamma) = \Theta(\mathrm{size}(\hat{\Gamma}))$.

Intuitively, the profile for a graph $G \in G_2$ maintains
sufficient information about $G$ in order to determine how $G$
can be parsed during some derivation; the cases for $G \in G_2^{\{1\}}$
resp. $G \in G_2^{\{1,2\}}$ build on the ideas developed for trees and
series-parallel graphs (Appendix C). The views of the graphs
from $G_2$ for a regular tree-width 2 grammar are defined below:

Definition 18: Let $G$ be a graph of tree-width $\le 2$ and $\Gamma = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus \mathcal{S}, \mathcal{R})$ be a normalized regular tree-width 2 grammar in alternative form. We distinguish the cases:

1. $G \in G_2^{\{1\}}$: a view of $G$ for $\Gamma$ is a multiset $\{\{Y_1, \dots, Y_n\}\} \in \text{mpow}(\mathcal{Y})$ for which there exist complete derivations $Y_i \Rightarrow_{\Gamma}^* v_i$, for all $i \in [1, n]$, such that $G = (v_1 \parallel \dots \parallel v_n)^{\mathcal{G}_2}$. A reduced view of $G$ is a multiset $[m]_{\Gamma}$, where $m$ is a view of $G$ for $\Gamma$.

2. $G \in G_2^{\{1,2\}}$ is a P-graph: a *view of G for Γ* is a multiset $\{\{S_1, \dots, S_n\}\} \in \text{mpow}(S)$ for which there exist complete derivations $S_i \Rightarrow_{\Gamma}^* v_i$, for all $i \in [1, n]$, such that $G = (v_1 \parallel \dots \parallel v_n)^{\mathcal{G}_2}$. The reduced views are defined as before (1).

3. $G \in G_2^{\{1,2\}}$ is an S-graph: a *view of G for $\Gamma$* is either:

a) a triple $(S, Q, X) \in S \times (P \uplus S) \times \mathcal{X}$ for which there exists a derivation $S \stackrel{\mathrm{a}}{\Rightarrow}_{\Gamma}^* \circ(u, Q, X)$, for some ground $\mathcal{F}_2$-term $u$ such that $u^{\mathcal{G}_2} = G$, or

b) a pair $(S, \perp) \in S \times \{\perp\}$ for which there exists a
derivation $S \Rightarrow_{\Gamma}^{*} u$, for some ground $\mathcal{F}_2$-term $u$ such
that $u^{\mathcal{G}_2} = G$.

The views of S-graphs are reduced, by definition.

The *profile* of $G$ is the set of reduced views, denoted $h_{\Gamma}(G)$.

We define the finite algebra $\mathcal{A}_\Gamma$ having the sorted domain $\mathcal{A}^\tau \stackrel{\mathrm{def}}{=} \{h_\Gamma(G) \mid G \in G_2, \sigma(G) = \tau\}$, for $\tau \in \{\{1\}, \{1, 2\}\}$. A P-profile (resp. S-profile) is the profile of a P-graph (resp. S-graph) of sort $\{1, 2\}$. The function symbols from $\mathcal{F}_2$ are interpreted in $\mathcal{A}_\Gamma$ by the least sets built according to the inference rules from Figure 7. The names of the inference rules distinguish between P-profile and S-profiles, e.g., $P \parallel_{\{1,2\}} S$ defines $\parallel^{\mathcal{G}_2}$ when one argument is a P-profile and the other is an S-profile, $\circ^1(P, S)$ and $\circ^2(P, S)$ define $\circ^{\mathcal{G}_2}$ when the first and second arguments are a P- and an S-profile, respectively. While the inference rules for parallel composition resemble the $(\parallel)$ rule for trees (Figure 3), the inference rules for serial composition rely on finding grammar rules from $\Gamma$ that match either the multiset arguments using the $\rightsquigarrow_\Gamma$ relation (for P-profile arguments) or the nonterminals from the tuples (for S-profile arguments).

<footnote>$^9$In every derivation one can replace the derivation steps $P \to S_{b_{i,3-i}}$, $S_{b_{i,3-i}} \to b_{i,3-i}$ with $P \to b_{i,3-i}$, and viceversa.</footnote>
$$ \emptyset_m \in \mathbf{0}_{\{1\}}^{\mathbf{A}_{\Gamma}} \text{ vertex} \quad \frac{k_i \in a_i, i = 1, 2}{\lceil k_1 + k_2 \rceil_{\Gamma} \in a_1 \, \|^{\mathbf{A}_{\Gamma}} \, a_2} \|\{1\} $$

$$ \frac{S \to b_{i,3-i} \in \mathcal{R}}{\|\{S\}\} \text{ edge} $$

$$ \frac{P \rightsquigarrow \Gamma m \in a_1, X \rightsquigarrow \Gamma k \in a_2}{Y \to P \triangleright X \in \mathcal{R}} \triangleright \frac{\|\{Y\}\} {a_1 \triangleright^{\mathbf{A}_{\Gamma}} a_2} $$

$$ \frac{m_i \in a_i, i = 1, 2}{\lceil m_1 + m_2 \rceil_{\Gamma} \in a_1 \, \|^{\mathbf{A}_{\Gamma}} \, a_2} \mathbf{P} \|\{1,2\} \mathbf{P} $$

$$ \frac{m_1 \in a_1, (S, \perp) \in a_2}{\lceil m_1 + \|\{S\}\rceil_{\Gamma} \in a_1 \, \|^{\mathbf{A}_{\Gamma}} \, a_2} \mathbf{P} \|\{1,2\} \mathbf{S} $$

$$ \frac{\{(S_i, \perp) \in a_i\}_{i=1,2}}{\lceil \|\{S_1\}\rceil + \|\{S_2\}\rceil_{\Gamma} \in a_1 \, \|^{\mathbf{A}_{\Gamma}} \, a_2} \mathbf{S} \|\{1,2\} \mathbf{S} $$

$$ \{P_i \rightsquigarrow \Gamma m_i \in a_i\}_{i=1,2}, X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ S \to \mathcal{O}(P_1, S_1, X_1) \in \mathcal{R} $$

$$ S_1 \to \mathcal{O}(P_2, Q, X) \in \mathcal{R} $$

$$ \frac{(S, Q, X) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{1}(\mathbf{P}, \mathbf{P})} $$

$$ \{P_i \rightsquigarrow \Gamma m_i \in a_i\}_{i=1,2}, X \rightsquigarrow \Gamma k \in a_3 $$

$$ S \to \mathcal{O}(P_1, P_2, X) \in \mathcal{R} $$

$$ \frac{(S, \perp) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{2}(\mathbf{P}, \mathbf{P})} $$

$$ P \rightsquigarrow \Gamma m \in a_1, (S_1, Q, X) \in a_2 $$

$$ X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ S \to \mathcal{O}(P, S_1, X_1) \in \mathcal{R} $$

$$ \frac{(S, Q, X) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{1}(\mathbf{P}, \mathbf{S})} $$

$$ P \rightsquigarrow \Gamma m \in a_1, (S_1, \perp) \in a_2 $$

$$ X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ S \to \mathcal{O}(P, S_1, X_1) \in \mathcal{R} $$

$$ \frac{(S, \perp) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{2}(\mathbf{P}, \mathbf{S})} $$

$$ (S, S_1, X_1) \in a_1, P \rightsquigarrow \Gamma m \in a_2 $$

$$ X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ S_1 \to \mathcal{O}(P, Q, X) \in \mathcal{R} $$

$$ \frac{(S, Q, X) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{1}(\mathbf{S}, \mathbf{P})} $$

$$ (S, P, X_1) \in a_1, P \rightsquigarrow \Gamma m \in a_2 $$

$$ X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ \frac{(S, \perp) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{2}(\mathbf{S}, \mathbf{P})} $$

$$ (S, S_1, X_1) \in a_1, (S_1, Q, X) \in a_2 $$

$$ X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ \frac{(S, Q, X) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{1}(\mathbf{S}, \mathbf{S})} $$

$$ (S, S_1, X_1) \in a_1, (S_1, \perp) \in a_2 $$

$$ X_1 \rightsquigarrow \Gamma k \in a_3 $$

$$ \frac{(S, \perp) \in \mathcal{O}^{\mathbf{A}_{\Gamma}}(a_1, a_2, a_3)}{\mathbf{o}^{1}(\mathbf{S}, \mathbf{S})} $$

<caption>Fig. 7. The interpretation of the signature $\mathcal{F}_2$ in $\mathcal{A}_{\Gamma}$</caption>

The size of $a \in \mathcal{A}_{\Gamma}$ is $\sigma(a) = \{1\}$ or $\sigma(a) = \{1, 2\}$ and $a$ is a P-profile, or $\sum_{s \in a} |s|$ if $a$ is an S-profile.

**Lemma 13:** Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus \mathcal{S}, \mathcal{R})$ be a normal-

ized regular tree-width 2 grammar in alternative form. Then, $\text{card}(\mathcal{A}_{\Gamma}) \in 2^{2^{\text{poly}(\text{size}(\Gamma))}}$ and $\text{size}(a) \in 2^{\text{poly}(\text{size}(\Gamma))}$ for each $a \in \mathcal{A}_{\Gamma}$. Moreover, $f^{\mathbf{A}_{\Gamma}}(a_1, \dots, a_{\#f})$ can be computed in time $2^{\text{poly}(\text{size}(\Gamma))}$, for each function symbol $f \in \mathcal{F}_2$ and all elements $a_1, \dots, a_{\#f} \in \mathcal{A}_{\Gamma}$.

See proof on page 22.

We establish the counterparts of Lemmas 5 and 6, below:

**Lemma 14:** For all $G_1, G_2 \in \mathcal{G}_2$, if $h_{\Gamma}(G_1) = h_{\Gamma}(G_2)$ then $G_1 \in \mathcal{L}^{\mathcal{G}_2}(\Gamma) \iff G_2 \in \mathcal{L}^{\mathcal{G}_2}(\Gamma)$.

See proof on page 22.

**Lemma 15:** $h_{\Gamma}$ is a homomorphism between $\mathcal{G}_2$ and $\mathcal{A}_{\Gamma}$.

See proof on page 22.

Furthermore, Lemma 7 carries over from the class of trees, because the idempotent power idem$(a)$ of each S-profile $a$ has the aperiodic property idem$(a) \|^{\mathbf{A}_{\Gamma}} a = \text{idem}(a)$, by the definition of $\|^{\mathbf{A}_{\Gamma}}$ for S-profiles.

The main result of this subsection is the “if” direction of Theorem 3 for the class of graphs of tree-width at most 2.

**Theorem 6:** The language of each (aperiodic) regular tree-width 2 grammar $\Gamma$ is recognizable by an (aperiodic) recognizer $(\mathcal{A}, \mathcal{B})$. Moreover, $\text{card}(\mathcal{A}) \in 2^{2^{\text{poly}(\text{size}(\Gamma))}}$ and $f^{\mathbf{A}}(a_1, \dots, a_{\#f})$ can be computed in time $2^{\text{poly}(\text{size}(\Gamma))}$, for each function symbol $f \in \mathcal{F}_{\mathcal{S}\mathcal{P}}$ and elements $a_1, \dots, a_n \in \mathcal{A}$.

See proof on page 24.

## V. LOGICAL DEFINABILITY OF APERIODIC RECOGNIZABLE SETS

This section focuses on the relation between definability in Monadic Second Order Logic (MSO) and recognizability of sets of graphs from the three classes considered in the previous. The equivalence between recognizability and MSO-definability for sets of words and ranked sets of trees are well-known [18], [19]. For unranked sets of trees, recognizability equals definability in Counting MSO (CMSO), i.e., MSO extended with modulo constraints on cardinalities of sets [1, Theorem 5.3]. For graphs, in general, CMSO-definability implies recognizability in the graph algebra $\mathcal{G}$ [1, Theorem 4.4], but not viceversa$^{10}$. Moreover, the equivalence between recognizability in the graph algebra and CMSO-definability has been established for classes of graphs defined by bounded tree-width [4], [5], also known as partial $k$-trees [20].

Since recognizability in $\mathcal{G}$ implies recognizability in each class $\mathcal{C}$ (i.e., derived algebra of $\mathcal{G}$), CMSO-definability implies recognizability in $\mathcal{C}$. However, the contrapositive does not hold, even if the domain of $\mathcal{C}$ has tree-width bounded by an integer $k$, because recognizability in $\mathcal{C}$ does not necessarily imply recognizability in the class $\mathcal{G}^{\leq k}$. The equivalence is recovered if the class $\mathcal{C}$ is *parsable*, i.e., for each $G \in \mathcal{C}$, some ground $\mathcal{F}_{\mathcal{C}}$-term $t$ such that $t^{\mathcal{C}} = G$ can be derived using a finite set of MSO formulae [3, Theorem 4.8(2)].

The main result of this section is the following refinement of the equivalence between CMSO-definable and recognizable subsets of parsable classes:

<footnote>$^{10}$There are uncountably many recognizable sets of graphs and only countably many CMSO-definable ones [1, Proposition 2.14].</footnote>
**Theorem 7:** Let $\mathcal{C}$ be a parsable class of graphs. A set $\mathcal{L} \subseteq \mathcal{C}$ is recognizable by an aperiodic recognizer if and only if it is MSO-definable.

This result is inspired by a characterization of MSO-definability for the class of trees in terms of aperiodic recognizers [17, Theorem 5.10]. Since each $G^{\le k}$ has been shown to be parsable in [21], based on the combined results of [4], [5], Theorem 7 applies to these classes as well. This was previously noticed by Bojańczyk [22, Theorem 4.18], who proved the following result, now a consequence of Theorem 7:

**Corollary 2:** For each integer $k \ge 1$, a set $\mathcal{L} \subseteq G^{\le k}$ is recognizable in $G^{\le k}$ by an aperiodic recognizer if and only if it is MSO-definable.

The rest of this section introduces the definitions and lemmas for the proof of Theorem 7.

## A. Counting Monadic Second Order Logic

The counting monadic second order logic (CMSO) is the set of formulæ defined inductively by the following syntax:

$$ \psi := x = y \mid a(x, y_1, \dots, y_{\#a}), \quad a \in \mathbb{A} \mid X(x) \mid \text{card}_{q,p}(X) \\ \mid \psi \wedge \psi \mid \neg \psi \mid \exists x. \psi \mid \exists X. \psi $$

where $x, y_1, \dots, y_{\#a} \in \mathcal{V}$ are individual variables, $X \in \mathcal{X}$ are set variables and $p, q \in \mathbb{N}$ are integers such that $p \in [0, q - 1]$. By MSO we denote the subset of CMSO consisting of formulæ that do not contain atomic propositions of the form $\text{card}_{q,p}(X)$. A sentence is a formula in which each variable occurs in the scope of a quantifier.

The semantics of CMSO is given by the usual satisfaction relation $G \models^s \psi$, where $G$ is a graph and $s$ is a mapping of individual (resp. set) variables to vertices or edges (resp. sets mixing vertices with edges). The relation is defined inductively on the structure of formulæ, as usual. In particular, $G \models^s a(x, y_1, \dots, y_n)$ holds iff $s(x)$ is an $a$-labeled edge attached to vertices $s(y_1), \dots, s(y_n)$, and $G \models^s \text{card}_{q,p}(X)$ holds iff $\text{card}(s(X)) = p \mod q$.

If $\phi$ is a sentence, we write $G \models^s \phi$ instead of $G \models^s \phi$. A set of graphs $\mathcal{L}$ is (C)MSO-definable iff there exists a (C)MSO sentence $\phi$ such that $\mathcal{L} = \{G \mid G \models \phi\}$. We recall the following result relating MSO-definability with recognizability for unranked sets of trees:

**Theorem 8 (Theorem 5.10 in [17]):** A set $\mathcal{L} \subseteq \mathcal{T}$ of trees is MSO-definable if and only if $\mathcal{L}$ is recognizable in $\mathcal{T}$ by an aperiodic recognizer.

A definable transduction is a relation on graphs, defined by finitely many MSO formulæ. For an input graph $G$, a definable transduction produces zero or more output graphs, as follows:

1. $G$ is accepted or rejected according to a formula $\varphi(X_1, \dots, X_n)$ that, moreover, assigns sets of vertices and edges from $G$ to the variables $X_1, \dots, X_n$; the transduction is said to be parameterless if $n = 0$.

2. $G$ is copied into $k \ge 1$ disjoint layers,

3. for the chosen valuation of $X_1, \dots, X_n$, the output graph $G'$ consists of the vertices and edges $x$ from the $i$-th layer, as defined by formulæ $\psi_i^{\text{vert/edge}}(x, X_1, \dots, X_n)$,

<figure><img src="image_6.png" /><figcaption>Fig. 8. A $\mathcal{F}_2$-term (a) and its corresponding parse tree (b) The order of the nodes attached to an edge is counter-clockwise.</figcaption></figure>

for $i \in [1, k]$. The incidence relation between the $a$-labeled edges $x$ and the vertices $y_1, \dots, y_{\#a}$ of $G'$, taken from the $i_1, \dots, i_{\#a}$ layers, are defined by formulæ $\theta_{(a,i_1,\dots,i_{\#a})}(x, y_1, \dots, y_{\#a}, X_1, \dots, X_n)$.

The relation $\delta \subseteq G \times G$ is defined by the sets $\delta(G)$ of outputs for the input graph $G$, for all valuations of $X_1, \dots, X_n$.

The main property of definable transductions is the Backwards Translation Theorem, which states that (C)MSO-definable sets are closed under inverse definable transductions. A consequence is that definable transductions are closed under relational composition:

**Theorem 9 (Theorem 1.40 in [2]):** If $\mathcal{L}$ is an (C)MSO-definable set of graphs and $\delta$ is an definable transduction then the set $\delta^{-1}(\mathcal{L})$ is (C)MSO-definable. Consequently, the composition of definable transductions is a definable transduction.

## B. Parse Tree Algebras

In the rest of this section, we fix an alphabet $\mathbb{A}$ and a class $\mathcal{C}$ with signature $\mathcal{F}_\mathcal{C}$ and sorts $\Sigma_\mathcal{C}$ (Definition 4). Let

$$ \mathcal{A}_\mathcal{C} \stackrel{\text{def}}{=} \{ \bar{f} \mid f \in \mathcal{F}_\mathcal{C} \setminus \{ \|_{\tau,\tau'} | \tau \in \Sigma_\mathcal{C} \} \} $$

be an alphabet of edge labels of arities $\#\bar{f} = \#f + 1$. A parse tree for $\mathcal{C}$ is a tree, having $\mathcal{A}_\mathcal{C}$-labeled edges, obtained from a $\mathcal{F}_\mathcal{C}$-term $t$ by collapsing each $\|\text{-subterm}^{11}$ of $t$ into a single node and transforming each occurrence of a function symbol $f \in \mathcal{F}_\mathcal{C}$ from $t$ into an edge with label $\bar{f} \in \mathcal{A}_\mathcal{C}$. Example. Figure 8 (a) shows a $\mathcal{F}_2$-term that evaluates to the rightmost graph on Figure 5 (b), where all edge labels are $b \in \mathbb{B}$. Figure 8 (b) shows the parse tree of that term.

For a given class $\mathcal{C}$, the parse tree algebra $\mathcal{P}_\mathcal{C}$ is a $(\mathcal{F}_\mathcal{C}, \Sigma_\mathcal{C})$-algebra of trees over the edge label alphabet $\mathcal{A}_\mathcal{C}$. The domain $\mathcal{P}_\mathcal{C}$ of $\mathcal{P}_\mathcal{C}$ is the set of $\mathcal{A}_\mathcal{C}$-labeled trees having associated sorts from $\Sigma_\mathcal{C}$. The function symbols $f \in \mathcal{F}_\mathcal{C} \setminus \{ \|_{\tau,\tau'} | \tau \in \Sigma_\mathcal{C} \}$ are interpreted over $\mathcal{A}_\mathcal{C}$-labeled trees instead of graphs as follows:

$$ f^{\mathcal{P}_\mathcal{C}}(T_1, \dots, T_{\#f}) \stackrel{\text{def}}{=} \text{append}_{\bar{f}}^T(T_1, \dots, T_{\#f}) $$

We denote by $\mathcal{T}(\mathcal{A}_\mathcal{C})$ the algebra of $\mathcal{T}(\mathcal{A}_\mathcal{C})$-labeled trees, of sort $\{1\}$, and its universe by $\mathcal{T}(\mathcal{A}_\mathcal{C})$. Note that not every tree

<footnote n="11">¹¹A subterm consisting of occurrences of some symbol $\|_{\tau,\tau'}$ and variables, for some $\tau \in \Sigma_\mathcal{C}$.</footnote>
from $T(\mathbb{A}_C)$ is a parse tree, because parse trees correspond to
well-sorted terms. However, recognizability in the multi-sorted
algebra of parse trees equals recognizability in the single-
sorted tree algebra:

**Lemma 16:** Let $\mathcal{C}$ be a class. Each set $\mathcal{L} \subseteq \mathcal{P}_C$ of parse trees is (aperiodic) recognizable in the parse tree algebra $\mathcal{P}_C$ iff $\mathcal{L}$ is (aperiodic) recognizable in the tree algebra $\mathcal{T}(\mathbb{A}_C)$.

See proof on page 24.

Each parse tree $T \in \mathcal{P}_C$ obtained by compacting a $\mathcal{F}_C$-
term $t$, has an associated graph, denoted $\mathbf{val}_C(T) \stackrel{\text{def}}{=} t^C$. The
following result ensures that $\mathbf{val}_C$ is well-defined:

**Proposition 1:** For every parse tree $T \in \mathcal{P}_C$ there is only one $\mathcal{F}_C$-term up to the associativity and commutativity of the operations $\parallel_{\tau,\tau}$, with $\tau \in \Sigma_C$, such that $T = t^{\mathcal{P}_C}$.

See proof on page 25.

It is manifest that $\sigma(\mathbf{val}_C(T)) = \sigma(T)$, for each $T \in \mathcal{P}_C$ and that $\mathbf{val}_C$ is a (sort-preserving) homomorphism between $\mathcal{P}_C$ and $\mathcal{C}$. Since both algebras are representable, this homomorphism is unique, thus called the evaluation homomorphism. It is known that the evaluation homomorphism is a definable transduction, for each class $\mathcal{G}^{\leq k}$ [2, Proposition 7.48]. The following is a generalization of this result to arbitrary classes:

**Proposition 2:** For each class $\mathcal{C}$, the function $\mathbf{val}_\mathcal{C}$ is a parameterless definable transduction.

See proof on page 25.

Then, recognizability of a set in the class $\mathcal{C}$ of graphs equals recognizability of the inverse $\mathbf{val}$-image in the algebra $\mathcal{P}_C$:

**Lemma 17:** Let $\mathcal{C}$ be a class and $\mathcal{L} \subseteq \mathcal{C}$ be a set of graphs. Then, $\mathcal{S} \stackrel{\text{def}}{=} \mathbf{val}_\mathcal{C}^{-1}(\mathcal{L})$ is (aperiodic) recognizable in $\mathcal{P}_C$ if and only if $\mathcal{L}$ is (aperiodic) recognizable in $\mathcal{C}$.

See proof on page 25.

### C. Parsable Classes

In general, the inverse of the evaluation homomorphism $\mathbf{val}$
is not a definable transduction. The parsable classes are the
ones for which this is the case. The following definition is
closely related to the parsable presentations of sets of graphs,
introduced by Courcelle [3, Definition 4.2]:

**Definition 19:** The class $\mathcal{C}$ is *parsable* iff there exists a definable transduction $\pi \subseteq \mathbf{val}_\mathcal{C}^{-1}$ such that $\text{dom}(\pi) = \mathcal{C}$.

Parsability ensures the equivalence between recognizability and CMSO-definability:

**Theorem 10 (Theorem 4.8(2) in [3]):** Let $\mathcal{C}$ be a parsable class and $\mathcal{L} \subseteq \mathcal{C}$ be a set. Then, $\mathcal{L}$ is CMSO-definable if and only if $\mathcal{L}$ is recognizable in $\mathcal{C}$.

We prove the main result of this section before showing its applicability to the class $\mathcal{G}_2$. Note that this result was already proved for the class of trees (Theorem 8).

a) *Proof of Theorem 7:* “⇒” Let $(\mathcal{A}, \mathcal{B})$ be an aperiodic $(\mathcal{F}_C, \Sigma_C)$-recognizer for $\mathcal{L}$ such that $\mathcal{L} = h_{\mathcal{C},\mathcal{A}}^{-1}(\mathcal{B})$. Then, $h_{\mathcal{C},\mathcal{A}} \circ \mathbf{val}_\mathcal{C}$ is a homomorphism between $\mathcal{P}_C$ and $\mathcal{A}$ and $\mathcal{S} \stackrel{\text{def}}{=} \mathbf{val}_\mathcal{C}^{-1}(\mathcal{L}) = (h_{\mathcal{C},\mathcal{A}} \circ \mathbf{val}_\mathcal{C})^{-1}(\mathcal{B})$ is aperiodic recognizable in $\mathcal{P}_C$. By Lemma 16, $\mathcal{S}$ is aperiodic recognizable in $\mathcal{T}(\mathbb{A}_C)$, hence $\mathcal{S}$ is MSO-definable, by Theorem 8. Since $\mathcal{C}$ is parsable, there exists a definable transduction $\pi \subseteq \mathbf{val}_\mathcal{C}^{-1}$

such that $\text{dom}(\pi) = \mathcal{C}$. We obtain $\mathcal{L} = \pi^{-1}(\mathcal{S})$, thus $\mathcal{L}$ is
MSO-definable, by Theorem 9.

“<” Assume that $\mathcal{L}$ is MSO-definable and $\mathcal{S} = \mathbf{val}_\mathcal{C}^{-1}(\mathcal{L})$ be the set of parse trees that evaluate to some graph from $\mathcal{L}$. By Proposition 2, $\mathbf{val}_\mathcal{C}$ is a definable transduction, hence $\mathcal{S}$ is an MSO-definable set of trees, by Theorem 9. By Theorem 8, $\mathcal{S}$ is aperiodic recognizable in $\mathcal{T}(\mathbb{A}_\mathcal{C})$, hence also aperiodic recognizable in $\mathcal{P}_\mathcal{C}$, by Lemma 16. By Lemma 17, $\mathcal{L}$ is aperiodic recognizable in $\mathcal{C}$. $\square$

It is already known that the classes of (disoriented) series-
parallel graphs are parsable [3, Theorems 6.10 and 6.12]. For
self-completeness reasons, we re-prove the following theorem
using our notation:

**Theorem 11:** The classes $\mathcal{SP}$ and $\mathcal{DSP}$ are parsable.

See proof on page 25.

Moreover, each class $\mathcal{G}^{\leq k}$ is parsable, by the combined results of [4], [5]. Note that, even though the connected graphs from the domain of $\mathcal{G}^{\leq 2}$ are the exactly the ones from the domain of $\mathcal{G}_2$, the signatures of the two classes are different, since $\mathcal{G}_2$ is a derived algebra of $\mathcal{G}^{\leq 2}$. Finally, we prove that:

**Theorem 12:** The class $\mathcal{G}_2$ is parsable.

See proof on page 27.

## VI. CONCLUSION

We introduce regular grammars for classes of graphs of tree-width at most 2. These grammars provide finite and compact representations for the recognizable sets in each class. The inclusion of a context-free language into a regular language can be decided in doubly-exponential time. A further restriction of regular grammars describes exactly the MSO-definable sets thereof, that are, moreover, recognized by aperiodic algebras.

As future work, we consider a more precise assessment of the size of the minimal recognizer algebra for the classes considered in this paper, as well as addressing the problem of finding regular grammars for the class of graphs of tree-width at most 3.

## 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 WIDER A Coordination and Support Action/Grant Agreement No. 101160022 All authors thank the anonymous reviewers for their insightful comments.

## REFERENCES

[1] B. Courcelle, “The monadic second-order logic of graphs. i. recognizable sets of finite graphs,” *Information and Computation*, vol. 85, no. 1, pp. 12–75, 1990. [Online]. Available: https://www.sciencedirect.com/science/article/pii/089054019090043H
[2] B. Courcelle and J. Engelfriet, *Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach*, ser. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012.

[3] B. Courcelle, "The monadic second-order logic of graphs v: on closing the gap between definability and recognizability," *Theoretical Computer Science*, vol. 80, no. 2, pp. 153-202, 1991. [Online]. Available: https://www.sciencedirect.com/science/article/pii/030439759190387H

[4] M. Bojańczyk and M. Pilipczuk, "Definability equals recognizability for graphs of bounded treewidth," in *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science*, ser. LICS '16. New York, NY, USA: Association for Computing Machinery, 2016, p. 407-416. [Online]. Available: https://doi.org/10.1145/2933575.2934508

[5] M. Bojanczyk and M. Pilipczuk, "Optimizing tree decompositions in MSO, Log. Methods Comput. Sci., vol. 18, no. 1, 2022. [Online]. Available: https://doi.org/10.46298/lmcs-18(1:26)2022

[6] A. Doumane, "Regular expressions for tree-width 2 graphs," in *49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France*, ser. LIPICS, M. Bojanczyk, E. Merelli, and D. P. Woodruff, Eds., vol. 229. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp. 121:1-121:20. [Online]. Available: https://doi.org/10.4230/LIPICS.ICALP.2022.121

[7] M. Chimes, R. Iosif, and F. Zuleger, "Tree-verifiable graph grammars," in *LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024*, ser. EPiC Series in Computing, N. S. Bjørner, M. Heule, and A. Voronkov, Eds., vol. 100. EasyChair, 2024, pp. 165-180.

[8] H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison, and M. Tommasi, *Tree Automata Techniques and Applications*. HAL, 2008. [Online]. Available: https://inria.hal.science/ hal-03367725

[9] M. Schützenberger, "On finite monoids having only trivial subgroups," *Information and Control*, vol. 8, no. 2, pp. 190-194, 1965. [Online]. Available: https://www.sciencedirect.com/science/article/pii/ S0019995865901087

[10] M. Benedikt and L. Segoufin, "Regular tree languages definable in fo and in fomod," *ACM Trans. Comput. Logic*, vol. 11, no. 1, Nov. 2009. [Online]. Available: https://doi.org/10.1145/1614431.1614435

[11] L. Libkin, "Logics for unranked trees: An overview," in *Automata, Languages and Programming*, L. Caires, G. F. Italiano, L. Monteiro, C. Palamidessi, and M. Yung, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 35-50.

[12] M. Bojanczyk, A. Muscholl, T. Schwentick, and L. Segoufin, "Two-variable logic on data trees and XML reasoning," *J. ACM*, vol. 56, no. 3, pp. 13:1-13:48, 2009. [Online]. Available: https://doi.org/10.1145/1516512.1516515

[13] J. Cristau, C. Löding, and W. Thomas, "Deterministic automata on unranked trees," in *Fundamentals of Computation Theory*, M. Liškiewicz and R. Reischuk, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 68-79.

[14] A. Boiret, V. Hugot, J. Niehren, and R. Treinen, "Automata for unordered trees," *Inf. Comput.*, vol. 253, pp. 304-335, 2017.

[15] M. Bojanczyk and I. Walukiewicz, "Forest algebras," in *Logic and Automata: History and Perspectives* [in Honor of Wolfgang Thomas], ser. Texts in Logic and Games, J. Flum, E. Grädel, and T. Wilke, Eds., vol. 2. Amsterdam University Press, 2008, pp. 107-132.

[16] W. Tutte, *Graph theory*. Cambridge university press, 2001.

[17] M. Bojanczyk, "Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic," *CoRR*, vol. abs/2008/11635, 2020. [Online]. Available: https://arxiv.org/abs/2008.11635

[18] J. R. Büchi, *Weak Second-Order Arithmetic and Finite Automata*. New York, NY: Springer New York, 1990, pp. 398-424. [Online]. Available: https://doi.org/10.1007/978-1-4613-8928-6_22

[19] J. Doner, "Tree acceptors and some of their applications," *J. Comput. Syst. Sci.*, vol. 4, no. 5, p. 406-451, oct 1970. [Online]. Available: https://doi.org/10.1016/S0022-0000(70)80041-1

[20] H. L. Bodlaender, "A partial k-arboretum of graphs with bounded treewidth," *Theoretical Computer Science*, vol. 209, no. 1, pp. 1-45, 1998. [Online]. Available: https://www.sciencedirect.com/science/ article/pii/S0304397597002284

[21] R. Iosif and F. Zuleger, "Characterizations of definable context-free graphs," *CoRR*, vol. abs/2310.04764, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2310.04764

[22] M. Bojanczyk, "Two monads for graphs," *CoRR*, vol. abs/1804.09408, 2018. [Online]. Available: http://arxiv.org/abs/1804.09408

[23] P. Erdös and R. Graham, "On a linear diophantine problem of frobenius," *Acta Arithmetica*, vol. 21, no. 1, pp. 399-408, 1972. [Online]. Available: http://eudml.org/doc/205124

[24] J. Flum and M. Grohe, *Parameterized Complexity Theory*, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. [Online]. Available: https://doi.org/10.1007/3-540-29953-X

## APPENDIX A
PROOFS

**Lemma 1:** Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ be a stratified grammar for a class $\mathcal{C}$. Then, one can build a normalized stratified grammar $\Gamma' = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R}')$ such that:

1. $\mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma)$,

2. $\mathrm{FP}(\Gamma') \subseteq \mathrm{FP}(\Gamma)$,

3. $\mathrm{size}(\Gamma') \in 2^{\mathrm{poly}(\mathrm{size}(\Gamma) \cdot \log(\mathrm{size}(\Gamma)))}$,

Moreover, $\Gamma$ is aperiodic only if $q = 1$, for all rules $X \to X \parallel Y^q$ of the form (A) from $\Gamma'$.

[Proof of Lemma 1] We perform the following transformation of $\Gamma$, for each pair $(X, Y) \in \mathcal{X} \times \mathcal{Y}$. Let $X \to X \parallel Y^q$, $q_1, \dots, X \to X \parallel Y^q$, be the rules of the form (A) from $\Gamma$, for the given pair $(X, Y)$. We assume w.l.o.g. that each rule above occurs on at least one complete derivation starting with an axiom nonterminal; rules that do not comply with this assumption can be identified in $\mathrm{poly}(\mathrm{size}(\Gamma))$ time and removed without changing the language of $\Gamma$. Moreover, we assume w.l.o.g. that each nonterminal from $\mathcal{X} \uplus \mathcal{Y}$ occurs in at least one rule from $\Gamma$ and that $q_1 < \dots < q_h$. We distinguish two cases:

- if $h \ge 1$, let $d \ge 1$ be the gcd of the integers $q_1, \dots, q_h$. By Schur's theorem, there exists a computable integer $n \ge 1$ such that for each integer $x > n$ there exist $x_1, \dots, x_h \in \mathbb{N}$ such that $dx = q_1x_1 + \dots + q_hx_h$. More precisely, $n$ is the Frobenius number of the primes $\frac{q_1}{d}, \dots, \frac{q_h}{d}$. We further observe that the set $M \stackrel{\mathrm{def}}{=} \{q_1x_1 + \dots + q_hx_h \mid x_1, \dots, x_h \in \mathbb{N}\} \cap [1, dn]$ is finite and computable.

- else $h = 0$, in which case we set $d = 0$ and $M = \emptyset$. We now obtain the set of rules $\mathcal{R}'$ from $\mathcal{R}$ as follows:

(a) we keep the rules $Z \to t[Z_1, \dots, Z_m]$ of the form (C) or (D),

(b) we remove the rules $X \to X \parallel Y^q$, $\dots$, $X \to X \parallel Y^q$, $q = 1, \dots, n$ (A) and we add the rule $X \to X \parallel Y^d$ if $d > 0$ (there are no such rules if $d = 0$),

(c) for every rule $X \to Y_1^{q_1} \parallel \dots \parallel Y_k^{q_k}$ (B) such that $Y = Y_\ell$, for some $\ell \in [1, k]$, we add a rule $X \to Y_1^{q_1} \parallel \dots \parallel Y_{\ell-1}^{q_{\ell-1}} \parallel Y^{q_\ell+m} \parallel Y_{\ell+1}^{q_{\ell+1}} \parallel \dots \parallel Y_k^{q_k}$, for each $m \in M$.

It is easy to show that each derivation of $\Gamma$ can be simulated by a derivation of $\Gamma'$ with the same outcome, and viceversa. Since we perform iteratively the above transformation for every pair $(X, Y) \in \mathcal{X} \times \mathcal{Y}$, we obtain the grammar $\Gamma'$ such that $\mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma)$ and $\mathrm{FP}(\Gamma') \subseteq \mathrm{FP}(\Gamma)$, having the stated property regarding the rules of the form (A). We note that in general we only have the inclusion $\mathrm{FP}(\Gamma') \subseteq \mathrm{FP}(\Gamma)$ because step (c) of the transformation potentially increases the size of
the right-hand side of the rules of the form (B), raising the lower bound in the footprint, for the case (1).

Moreover, $\Gamma$ is aperiodic if and only if $d = 1$ for all rules introduced at step (b), by Definition 8. We note that these are the only rules of the form (A) from $\Gamma'$, by construction.

It remains to prove that $\text{size}(\Gamma') \in \text{2poly}((\text{card}(\mathcal{X})+\text{card}(\mathcal{Y}))\cdot\log(\text{size}(\Gamma)))$. Consider the changes described in the previous. Clearly, steps (a) and (b) do not increase the size of the grammar. Step (c) adds, for each $m \in M$ and each rule $\rho$ of form (B), a rule of size at most $\text{size}(\rho)+m$. We have $m \le n$ and note that $n \in \text{poly}(\text{size}(\Gamma))$ follows from the upper bound on the Frobenius number $n \le (\frac{q_1}{d}-1)(\frac{q_b}{d}-1)-1 \le \text{size}(\Gamma)^2 \in \text{poly}(\text{size}(\Gamma))$, see, e.g., [23]. Moreover, this transformation is applied once for each pair $(X, Y) \in \mathcal{X} \times \mathcal{Y}$. Hence, we obtain for every rule $\rho \in \mathcal{R}$ of form (C) at most $\text{poly}(\text{size}(\Gamma))^{\text{card}(\mathcal{X})\cdot\text{card}(\mathcal{Y})}$ rules of form (C) in $\mathcal{R}'$, each of size at most $\text{size}(\rho)+\text{poly}(\text{size}(\Gamma))^{\text{card}(\mathcal{Y})}$. We note that for every $X$ we apply the transformation at most once for every $Y$, i.e., at most $\text{card}(\mathcal{Y})$ many times. Thus, we obtain $\text{size}(\Gamma') \le \text{poly}(\text{size}(\Gamma))^{\text{poly}((\text{card}(\mathcal{X})+\text{card}(\mathcal{Y})))} \in \text{2poly}(\text{size}(\Gamma)\cdot\log(\text{size}(\Gamma)))$, by the assumption that each nonterminal from $\mathcal{X} \uplus \mathcal{Y}$ occurs in some rule of $\Gamma$. $\square$

**Theorem 2 (Refinement Theorem):** Let $\mathcal{C}$ be a class. For each stratified $\mathcal{F}_\mathcal{C}$-grammar $\Gamma$ and each $\mathcal{F}_\mathcal{C}$-recognizer $(A, B)$ one can build a stratified $\mathcal{F}_\mathcal{C}$-grammar $\Gamma'$ such that $\text{FP}(\Gamma') \subseteq \text{FP}(\Gamma)$ and $\mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma^{(A,B)})$. Moreover, $\Gamma'$ is aperiodic whenever $\Gamma$ is an aperiodic stratified grammar and $\mathcal{A}$ is an aperiodic $\mathcal{F}_\mathcal{C}$-algebra.

[Proof of Theorem 2]

Let $N \stackrel{\text{def}}{=} \text{card}(\mathcal{A})$ and $\Gamma \stackrel{\text{def}}{=} (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$. By Lemma 1, we can assume that for each pair of nonterminals $(X, Y) \in \mathcal{X} \times \mathcal{Y}$ there is at most one rule $X \to X \parallel Y^{\sharp q}$ (A) in $\mathcal{R}$. We define the grammar $\Gamma' \stackrel{\text{def}}{=} (\mathcal{X}' \uplus \mathcal{Y}', \mathcal{R}')$, where $\mathcal{X}' \stackrel{\text{def}}{=} \{X_a \mid X \in \mathcal{X}, a \in \mathcal{A}\}$ and $\mathcal{Y}' \stackrel{\text{def}}{=} \{Y_a \mid Y \in \mathcal{Y}, a \in \mathcal{A}\}$ and $\sigma(Z_a) \stackrel{\text{def}}{=} \sigma(Z)$ for all $Z \in \mathcal{X} \uplus \mathcal{Y}$ and $a \in \mathcal{A}$. The set of rules $\mathcal{R}'$ of $\Gamma'$ is the following:

E. $X_b \to X_b \parallel Y_a^{\sharp q_r}$, for every rule $X \to X \parallel Y^{\sharp q} \in \mathcal{R}$ and each $a, b \in \mathcal{A}$ and $r \in [1, N]$ such that $b = b \parallel a^{\sharp A} a^{\sharp q_r}$,

F. $X_b \to \|_{Y \in \mathcal{Y}} \|_{a \in A} Y_a^{\sharp s(Y,a)+q(Y,a)}$, for each nonterminal $X \in \mathcal{X}$, element $b \in \mathcal{A}$ and integers $s(Y, a), q(Y, a) \in \mathbb{N}$ such that $\sum_{a \in A} s(Y, a) = s(Y)$ and $0 \le q(Y, a) \le N \cdot q(Y)$ and:

- there exists a rule $X \to \|_{Y \in \mathcal{Y}} Y^{\sharp s(Y)} \in \mathcal{R}$, and

- for all $Y \in \mathcal{Y}$, either:

* $\sum_{a \in A} q(Y, a) = k \cdot q(Y)$ if there exists a rule $X \to X \parallel Y^{\sharp q(Y)} \in \mathcal{R}$ and an integer $k \in \mathbb{N}$, or

* $q(Y, a) = 0$, for each $a \in \mathcal{A}$, if no rule of the form $X \to X \parallel Y^{\sharp q} \in \mathcal{R}$ exists,

- $b = \|_{Y \in \mathcal{Y}} \|_{a \in A} a^{\sharp s(Y,a)+q(Y,a)}$.

G. $Z_b \to t[(Z_1)_{a_1}, \dots, (Z_m)_{a_m}]$ for every rule $Z \to t[Z_1, \dots, Z_m] \in \mathcal{R}$ of the form (C) or (D) and $b, a_1, \dots, a_m \in \mathcal{A}$ such that $b = t^A(a_1, \dots, a_m)$,

H. $\to Z_b$ for each axiom $\to Z$ in $\mathcal{R}$ and $b \in B$.

First, it is an easy check that $\Gamma' = (\mathcal{X}' \uplus \mathcal{Y}', \mathcal{R}')$ is indeed a stratified grammar and moreover satisfies $\text{FP}(\Gamma') \subseteq \text{FP}(\Gamma)$, by construction. In particular, the templates for rules of the forms (C), (D) and (E) are the same for $\Gamma$ and $\Gamma'$, whereas the lower bound $m$ of template $X \to Y^{\sharp m}$ for the rules of the form (B) is increased in $\Gamma'$ w.r.t. $\Gamma$, by the definition of $\mathcal{R}'$ in the case (F). More precisely, this is because, for each rule $X_b \to \|_{Y \in \mathcal{Y}} \|_{a \in A} Y_a^{\sharp s(Y,a)+q(Y,a)} \in \mathcal{R}'$, there exists a rule $X \to \|_{Y \in \mathcal{Y}} \|_{Y^{\sharp s(Y)}} \in \mathcal{R}$ such that $\sum_{a \in A} s(Y, a)+q(Y, a) \ge s(Y)$.

Moreover, if $\Gamma$ is aperiodic, we have $q = 1$, for each rule $X \to X \parallel Y^{\sharp q}$ of the form (A), by Lemma 1. By the fact below, the only rules of the form (E) from $\Gamma'$ are such that $qr = 1$, hence $\Gamma'$ is an aperiodic stratified grammar.

**Fact 1:** If $\mathcal{A}$ is an aperiodic algebra, we have $b = b \parallel^A a$, for all $a, b \in \mathcal{A}$ and $r \ge 1$ such that

$$b = b \parallel^A a \underbrace{\parallel^A \dots \parallel^A a}_{\stackrel{\text{def}}{=} a^{\sharp A} r (r \text{ times})}$$

Assume that $\text{idem}(a) = a^{\sharp A} n$, for some $n \ge 1$. By composing the left and right-hand sides of the above equality $n$ times with $a^{\sharp A} r$, we obtain $b = b \parallel^A a^{\sharp A} r n = b \parallel^A (\text{idem}(a))^{\sharp A} r$. By the aperiodicity of $\mathcal{A}$, we have $\text{idem}(a) \parallel^A a = \text{idem}(a)$, hence $b = b \parallel^A (\text{idem}(a))^{\sharp A} r = (b \parallel^A (\text{idem}(a))^{\sharp A} r) \parallel^A a = b \parallel^A (\text{idem}(a))^{\sharp A} r \parallel^A a = b \parallel^A (\text{idem}(a) \parallel a) = b \parallel^A a$. $\square$

Second, we argue that $\mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma^{(A,B)})$:

“$\subseteq$” We will argue that the same $\mathcal{F}_\mathcal{C}$-terms can be derived from $\Gamma^{(A,B)}$ and $\Gamma'$. More precisely, we prove the following equality, for each nonterminal $Z_a \in \mathcal{X}' \uplus \mathcal{Y}'$:

$$\{t \mid Z_a \stackrel{*}{\to}_{\Gamma^{(A,B)}} t\} = \{t \mid Z_a \stackrel{*}{\to}_{\Gamma'} t\} \quad (2)$$

We first observe that $\Gamma^{(A,B)}$ and $\Gamma'$ have the same set of axioms of the form (H). Further, the rules of the form (G) of $\Gamma'$ are exactly the rules in $\Gamma^{(A,B)}$ obtained by refinement of the rules of form either (C) or (D) of $\Gamma$, and hence will generate the same set of terms. It remains to prove that the rules of the forms (E), (F) and (A), (B) produce the same set of terms starting from a nonterminal $X_b$ in the grammars $\Gamma'$ and $\Gamma^{(A,B)}$, respectively.

We now consider an arbitrary $\parallel$-term $t = \|_{Y \in \mathcal{Y}} \|_{a \in A} Y_a^{\sharp s(Y,a)+q(Y,a)}$ that can be generated by $\Gamma^{(A,B)}$ starting with some nonterminal $X_b$ using the refined rules of the forms (A) and (B), where $s(Y, a)$ and $q(Y, a)$ are positive integers satisfying the following constraints:

1. there exists a rule $X \to \|_{Y \in \mathcal{Y}} Y^{\sharp s(Y)}$ in $\Gamma$,

2. there exists a rule $X \to X \parallel Y^{\sharp q(Y)}$ in $\Gamma$,

3. $b = \|_{Y \in \mathcal{Y}} \|_{a \in A} a^{\sharp s(Y,a)+q(Y,a)}$.

To prove that $X_b \stackrel{\Gamma'}{\to} t$, we distinguish two cases. First, assume that there is a rule $X \to X \parallel Y^{\sharp q(Y)} \in \mathcal{R}$; we recall that this rule is unique, and hence $q(Y)$ is unique. By the pigeonhole principle, for each $a \in \mathcal{A}$ there exist integers $0 \le p(Y, a) < N$ and $1 \le r(Y, a) \le N$ such that
$p(Y, a) + r(Y, a) \le N$ and $a^{\#A}p(Y, a)+r(Y, a) = a^{\#A}p(Y, a)$. By composing both sides of this equality $q(Y)$ times, we obtain $a^{\#A}q(Y) \cdot p(Y, a)+q(Y) \cdot r(Y, a) = a^{\#A}q(Y) \cdot p(Y, a)$. Next, we define integers $0 \le q'(Y, a) < N \cdot q(Y)$, for each $a \in A$ and $Y \in \mathcal{Y}$, as follows:

$$ q'(Y, a) \stackrel{\text{def}}{=} \begin{cases} p(Y, a) \cdot q(Y) + \\ (q(Y, a) - p(Y, a) \cdot q(Y)) \mod (r(Y, a) \cdot q(Y)), \\ \text{if } q(Y, a) \ge N \cdot q(Y) \\ q(Y, a), \text{ otherwise} \end{cases} $$

For each $a \in A$ and $Y \in \mathcal{Y}$, we have $q(Y, a) = q'(Y, a) + k(Y, a) \cdot r(Y, a) \cdot q(Y)$, for some coefficients $k(Y, a) \ge 0$. Moreover, by point 3., we obtain that $b = b \parallel a^{q(Y) \cdot r(Y, a)}$, if $q(Y, a) \ge N \cdot q(Y)$, for each $a \in A$ and $Y \in \mathcal{Y}$ (†).

Second, if there is a no rule $X \to X \parallel Y^{\#q(Y)} \in \mathcal{R}$, we have $q(Y, a) = 0$ for all $a \in A$, and we set $q'(Y, a) \stackrel{\text{def}}{=} 0$ for all $a \in A$.

We now observe that $X_b \Rightarrow_{\Gamma'} \parallel_{Y \in \mathcal{Y}} \parallel_{a \in A} Y_a^{\#s(Y, a)+q'(Y, a)}$, because a rule $X_b \to \parallel_{Y \in \mathcal{Y}} \parallel_{a \in A} Y_a^{\#s(Y, a)+q'(Y, a)}$ of the form (F) exists in $\Gamma'$. According to the definition of $\Gamma'$, this is the case provided that $b = \parallel_{Y \in \mathcal{Y}} \parallel_{a \in A} a^{\#s(Y, a)+q'(Y, a)}$. The latter condition can be obtained from (†), by subtracting $k(Y, a)$ times $r(Y, a) \cdot q(Y)$ from $q(Y, a)$ in the exponent of $a$ in equation (3). Then, by applying the rules of the form (E), $k(Y, a)$-times respectively, we obtain the term $\parallel_{Y \in \mathcal{Y}} \parallel_{a \in A} Y_a^{\#s(Y, a)+q(Y, a)}$ using that $q(Y, a) = q'(Y, a) + k(Y, a) \cdot r(Y, a) \cdot q(Y)$, for all $Y \in \mathcal{Y}$ and $a \in A$.

"$\supseteq$": We note that it is straightforward to prove by induction that $G \in \mathcal{L}_{Z_a}^c(\Gamma')$ only if $h_{G,A}(G) = a$, for all $a \in A$. Hence, $\mathcal{L}^c(\Gamma') \subseteq h_{C,A}^{-1}(B)$. Moreover, it is easy to verify that every complete derivation of $\Gamma'$ induces a complete derivation $\Gamma$ (in particular, every rule $X_b \to X_b \parallel Y_a^{\#q}$ in $\mathcal{R}'$ induces an $r$-fold application of $X \to X \parallel Y^{\#q}$ in $\mathcal{R}$, and every rule $X_b \to \parallel_{Y \in \mathcal{Y}} \parallel_{a \in A} Y_a^{\#s(Y, a)+q(Y, a)} \in \mathcal{R}'$ induces an application of $X \to \parallel_{Y \in \mathcal{Y}} \parallel_{Y^{\#q(Y)}} \in \mathcal{R}$ plus a $k_Y$-fold application of $X \to X \parallel Y^{\#q(Y)} \in \mathcal{R}$ for each $Y$, where $\sum_{a \in A} q(Y, a) = k_Y \cdot q(Y)$. Hence, $\mathcal{L}^c(\Gamma') \subseteq \mathcal{L}^c(\Gamma)$. Thus, we get $\mathcal{L}^c(\Gamma') \subseteq \mathcal{L}^c(\Gamma) \cap h_{C,A}^{-1}(B) = \mathcal{L}^c(\Gamma(A,B))$. $\square$

**Corollary 1:** Let $\mathcal{C}$ be a (aperiodic) universally stratified class and $\mathcal{L} \subseteq \mathcal{C}$ be a set recognizable in $\mathcal{C}$ (by an aperiodic recognizer). Then, there exists a (aperiodic) stratified grammar $\Gamma$ for $\mathcal{C}$ such that $\text{FP}(\Gamma) \subseteq \text{FP}(\Gamma_c)$ and $\mathcal{L} = \mathcal{L}^c(\Gamma)$.

[Proof of Corollary 1] Let $(A, B)$ be a $\mathcal{F}_C$-recognizer for $\mathcal{L}$, i.e., we have $\mathcal{L} = h_{C,A}^{-1}(B)$. Since $\mathcal{C}$ is universally stratified, there exists a stratified grammar $\Gamma_C$ for $\mathcal{C}$ such that $\mathcal{L}^c(\Gamma_C) = \mathcal{C}$. Then, $\mathcal{L} = \mathcal{C} \cap h_{C,A}^{-1}(B) = \mathcal{L}^c(\Gamma_C^{(A,B)})$, by Theorem 1. By Theorem 2, there exists a stratified grammar $\Gamma'$ such that $\text{FP}(\Gamma') \subseteq \text{FP}(\Gamma_C)$ and $\mathcal{L} = \mathcal{L}^c(\Gamma_C^{(A,B)}) = \mathcal{L}^c(\Gamma')$. Moreover, if $\Gamma_C$ is an aperiodic stratified grammar for $\mathcal{C}$ and $\mathcal{L}$ is recognized by an aperiodic recognizer, then $\Gamma'$ is an aperiodic stratified grammar for $\mathcal{C}$, by Theorem 2. $\square$

**Lemma 18:** Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ be a normalized stratified grammar. For each $X \in \mathcal{X}$ and multiset $m \in \text{mpow}(\mathcal{Y})$, we have $X \rightsquigarrow \Gamma m \iff X \rightsquigarrow \Gamma [m]_{\Gamma}$. $\square$

**Proof.** "$\Rightarrow$" Let $Y$ be a nonterminal. If $m(Y) = [m]_{\Gamma}(Y)$ there is nothing to prove, hence we assume

that $m(Y) > [m]_{\Gamma}(Y)$, i.e., $[m]_{\Gamma}(Y) = q(Y) + (m(Y) - q(Y)) \mod p(Y) = b(Y) + p(Y) + (m(Y) - q(Y)) \mod p(Y) < m(Y)$. Suppose, for a contradiction, that $\Gamma$ has no rule of the form $X \to Y^{\#q}$, for the chosen nonterminals $X$ and $Y$. In this case, $m(Y) = [m]_{\Gamma}(Y)$, contradiction. Hence, there exists a rule $X \to X \parallel Y^{\#q}(\dagger)$ and an integer $n \in \mathbb{N}$ such that $m(Y) = n \cdot p(Y) + [m]_{\Gamma}(Y)$. Because $\Gamma$ is normalized, the rule $(\dagger)$ is unique. Let $X \Rightarrow_{\Gamma}^* t$ be the derivation that witnesses $X \rightsquigarrow \Gamma m$. This derivation consists of one or more applications of the rule $(\dagger)$ and one or more rules of the form $X \to Y_1^{\#q_1} \parallel \dots \parallel Y_n^{\#q_n}$. By removing $nk$ occurrences of the rule $(\dagger)$, we obtain a derivation $X \Rightarrow_{\Gamma}^* u$, where $[m]_{\Gamma}(Y)$ is the number of occurrences of $Y$ in $u$ and $k \ge 1$ is an integer such that $p(Y) = kq$. This reduction is repeated for each $Y \in \mathcal{Y}$, until we obtain a derivation that witnesses $X \rightsquigarrow \Gamma [m]_{\Gamma}$. $\square$

"$\Leftarrow$" Let $Y$ be a nonterminal. If $m(Y) = [m]_{\Gamma}(Y)$ there is nothing to prove, hence we assume that $m(Y) > [m]_{\Gamma}(Y)$, i.e., $[m]_{\Gamma}(Y) = q(Y) + (m(Y) - q(Y)) \mod p(Y)$. Suppose, for a contradiction, that no rule $X \to X \parallel Y^{\#q}$ exists in $\Gamma$. In this case, $m(Y) = [m]_{\Gamma}(Y)$, contradiction. Then, let $X \to X \parallel Y^{\#q}$ be such a rule and $k \in \mathbb{N}$ be such that $p(Y) = kq$; by the definition of $p(Y)$, such a $k \in \mathbb{N}$ exists. We extend the derivation $X \Rightarrow_{\Gamma}^* u$ witnessing $X \rightsquigarrow [m]_{\Gamma}$ by adding $nk$ steps that apply the $(\dagger)$ rule to it, where $n \in \mathbb{N}$ is such that $m(Y) = n \cdot q(Y) + [m]_{\Gamma}(Y)$. By repeating this step for each $Y \in \text{supp}(m)$, we obtain a derivation that witnesses $X \rightsquigarrow \Gamma m$. $\square$

**Theorem 4:** Let $\mathcal{C}$ be one of the classes of trees, (disoriented) series-parallel graphs and graphs of tree-width at most 2. The problem "given $\mathcal{F}_C$-grammars $\Gamma$ and $\Gamma'$ such that $\Gamma'$ is regular, does $\mathcal{L}^c(\Gamma) \subseteq \mathcal{L}^c(\Gamma')$?" belongs to 2EXPTIME and is EXPTIME-hard, even if $\Gamma'$ is aperiodic.

[Proof of Theorem 4] Let $(A, B)$ be a recognizer for $\mathcal{L}^c(\Gamma')$. The existence of such a recognizer follows from the fact that $\Gamma'$ is regular for $\mathcal{C}$, where $\mathcal{C}$ is the class of either trees (Theorem 5), series-parallel graphs (Theorem 13), or graphs of tree-width 2 at most (Theorem 6). Moreover, we have $\text{card}(A) \in 2^{2^{\text{poly}(\text{size}(\Gamma'))}}$ and that each function $f^A$ can be computed in time $2^{\text{poly}(\text{size}(\Gamma'))}$, for each of the three classes considered. Then, $(A, A \setminus B)$ is a recognizer for the complement language $\mathcal{L}^c(\Gamma') \stackrel{\text{def}}{=} C \setminus \mathcal{L}^c(\Gamma')$. By Theorem 1, we obtain $\mathcal{L}^c(\Gamma^{(A,A\setminus B)}) = \mathcal{L}^c(\Gamma) \cap \mathcal{L}^c(\Gamma') = \mathcal{L}^c(\Gamma) \setminus \mathcal{L}^c(\Gamma')$. Hence $\mathcal{L}^c(\Gamma^{(A,A\setminus B)}) = \emptyset$ if and only if $\mathcal{L}^c(\Gamma) \subseteq \mathcal{L}^c(\Gamma')$. Since $\Gamma^{(A,A\setminus B)}$ can be computed in time:

$$ \mathcal{O} \left( \text{size}(\Gamma) \cdot \left( 2^{2^{\text{poly}(\text{size}(\Gamma'))}} \right)^{\text{size}(\Gamma)} \cdot \left( 2^{\text{poly}(\text{size}(\Gamma'))} \right)^{\text{size}(\Gamma)} \right) \in 2^{2^{\text{poly}(\text{size}(\Gamma)) + \text{size}(\Gamma')}$$

and the emptiness of a grammar can be checked in linear time, we obtain that the inclusion problem $\mathcal{L}^c(\Gamma) \subseteq \mathcal{L}^c(\Gamma')$ belongs to 2EXPTIME.

For the EXPTIME-hardness lower bound, we deal separately with the case of trees and series-parallel graphs. Since the class of graphs of tree-width 2 at most subsumes both trees
and series-parallel graphs, either result implies EXPTIME-hardness of the inclusion problem for the class of graphs of tree-width 2 at most.

We next prove the EXPTIME-hardness of the inclusion problem for trees (over a binary alphabet). We reduce from the inclusion problem between languages of nondeterministic bottom-up tree automata $A_i = (Q_i, I_i, \delta_i, F_i)$ over an arbitrary ranked alphabet $\mathbb{A}$, i.e., whose symbols $f \in \mathbb{A}$ have associated ranks $\#f \ge 0$, where $Q_i$ is a finite set of states, $I_i, F_i \subseteq Q_i$ are initial and final states and $\delta_i$ is a set of transitions of the form $f(q_1, \dots, q_{\#f}) \to q$, for $i = 1, 2$. The language $\mathcal{L}(A_i)$ is the set of ranked trees $t$ over $\mathbb{A}$ that can be labeled with states by the automaton $A_i$ such that the following hold:

- each subtree $f(t_1, \dots, t_{\#f})$ of $t$ is recursively labeled by $q$ if $t_j$ is labeled by $q_j$, for $j \in [1, \#f]$ and $f(q_1, \dots, q_{\#f}) \xrightarrow{a} q \in \delta_j$,

- the root of $t$ is labeled by a final state.

The problem “given nondeterministic bottom-up tree automata $A_1$ and $A_2$, does $\mathcal{L}(A_1) \subseteq \mathcal{L}(A_2)$?” is known to be EXPTIME-complete [8, Corollary 1.7.9].

We now state how tree automata can be encoded by regular tree grammars. For this we first fix some ranked alphabet $\mathbb{A}$. Let $m = \max\{\#a \mid a \in \mathbb{A}\}$. We define the alphabet $\mathbb{B}_{\mathbb{A}} = \{e_f \mid f \in \mathbb{A}\} \cup \{p_i \mid 1 \le i \le m\}$ for some fresh symbols $e_f$ and $p_i$, with $\#e_f = 2$ and $\#p_i = 2$ for all $f \in \mathbb{A}$ and $1 \le i \le m$. Let $\mathcal{C}$ be the class of trees over the alphabet $\mathbb{B}_{\mathbb{A}}$. We define the encoding $\mathrm{enc}(T)$ of a tree over the alphabet $\mathbb{A}$ by a tree over the alphabet $\mathbb{B}_{\mathbb{A}}$; the encoding is defined via the unique term $t$ such that $t^T = T$:

$$ \mathrm{enc}(T) \stackrel{\mathrm{def}}{=} \left\{ \begin{array}{ll} \mathbf{0}_{\{1\}}^{T}, & \text{if } t = \mathbf{0}_{\{1\}} \\ \mathrm{append}_{e_f}^{T}(\|_{i \in [1, \#f]}^{T} \mathrm{append}_{p_i}^{T}(\mathrm{enc}(t_i))), & \text{if } t = f(t_1, \dots, t_{\#f}), \ \#f = n \end{array} \right. $$

We now show how to encode some tree automaton $A = (Q, I, \delta, F)$ over the alphabet $\mathbb{A}$ by a regular tree grammar $\Gamma_A = (\mathcal{N}, \mathcal{R})$ over the alphabet $\mathbb{B}_{\mathbb{A}}$. We choose $\mathcal{N}$ as the union of the non-terminals $Y_{i,q}$, for all $1 \le i \le m$ and $q \in Q$, the non-terminals $X_{i,q,f}$, for all $1 \le i \le m$, $q \in Q$ and $f \in \mathbb{A}$, and the non-terminal $X$. For every transition $f(q_1, \dots, q_{\#f}) \to q$ of $A$ and $1 \le i \le m$, we add to $\mathcal{R}$ the rules

$$ \begin{aligned} Y_q &\to \mathrm{append}_{e_f}(X_{f,q}) \quad X_{f,q} \to Y_{1,q_1} \parallel \dots \parallel Y_{\#f,q_{\#f}} \\ Y_{i,q} &\to \mathrm{append}_{p_i}(X_q) \quad X_q \to Y_q \end{aligned} $$

The axioms of $\Gamma$ consist of the rules $\to Y_q$ such that $q \in \mathcal{I}$. It is easy to check that $\mathcal{L}^T(\Gamma_A) = \mathrm{enc}(\mathcal{L}(A))$ and that $\Gamma_A$ is aperiodic (actually, it has no rules of the form (A)). Then, given nondeterministic bottom-up automata $A_1$ and $A_2$, we have $\mathcal{L}(A_1) \subseteq \mathcal{L}(A_2)$ if and only if $\mathrm{enc}(\mathcal{L}(A_1)) \subseteq \mathrm{enc}(\mathcal{L}(A_2))$ if and only if $\mathcal{L}^T(\Gamma_{A_1}) \subseteq \mathcal{L}^T(\Gamma_{A_2})$. Since the time needed to compute $\Gamma_A$ is polynomial in the size of $A$, for any bottom-up tree automaton $A$, the inclusion problem for the class of trees over an alphabet containing only binary symbols, where the right-hand side is an aperiodic regular grammar, is EXPTIME-hard.

Now, let $\mathcal{C}$ be the class of SP graphs over an alphabet $\mathbb{A}$ of binary symbols. We reduce from the inclusion problem

for trees, where the right-hand side is an aperiodic regular grammar. To this end, we encode a tree $T$ over an alphabet $\mathbb{A}$ of binary symbols of binary edge labels as an SP graph $\mathbf{sp}(T)$ over the edge alphabet $\mathbb{B} = \mathbb{A} \cup \{e\}$, for some fresh edge label $e$, where $e$ is used to link the leaves of the tree to the 2-source of the SP graph; the 1-source is the root of the tree. It is clear that this encoding is injective, hence $\mathcal{L}^T(\Gamma) \subseteq \mathcal{L}^T(\Gamma')$ if and only if $\mathbf{sp}(\mathcal{L}^T(\Gamma)) \subseteq \mathbf{sp}(\mathcal{L}^T(\Gamma'))$, for any two $\mathcal{F}_{\mathcal{T}}$-grammars $\Gamma$ and $\Gamma'$.

First, given an arbitrary tree grammar $\Gamma$ over $\mathbb{A}$, we define the $\mathcal{F}_{\mathcal{SP}}$-grammar $\bar{\Gamma}$ having the same nonterminals as $\Gamma$ and the rules:

- $Z \to a_{1,2} \circ Z'$, for each rule $Z \to \mathrm{append}_{\alpha}(Z')$ of $\Gamma$, where $a \in \mathbb{A}$,

- $Z \to e_{1,2}$, for each rule $Z \to \mathbf{0}_{\{1\}}$ of $\Gamma$.

- $Z \to Z$, for each axiom $\to Z$ of $\Gamma$.

It is easy to check that $\mathbf{sp}(\mathcal{L}^T(\Gamma)) = \mathcal{L}^{\mathrm{SP}}(\bar{\Gamma})$: each term generated by $\Gamma$ corresponds to exactly one term generated by $\bar{\Gamma}$, starting from the same nonterminal, in which each subterm $\mathrm{append}_{\alpha}(x)$ is replaced by $a_{1,2} \circ x$ and each subterm $\mathbf{0}_{\{1\}}$ by $e_{1,2}$.

Second, given a regular tree grammar $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ over the alphabet $\mathbb{A}$, we define the regular series-parallel grammar $\tilde{\Gamma} = (\{P_X \mid X \in \mathcal{X} \cup \mathbb{B}\} \uplus \{S_Y \mid Y \in \mathcal{Y}\}, \mathcal{R})$ with rules:

$$ \begin{aligned} S_Y &\to P_a \circ P_X, P_X \to S_{Y_1} \parallel \dots \parallel S_{Y_n}, \\ \text{if } Y \to \mathrm{append}_a(X), X \to Y_1 \parallel \dots \parallel Y_n \in \mathcal{R} \text{ for } n \ge 2 \\ S_{Y_1} &\to P_a \circ S_{Y_2}, \text{ if } Y_1 \to \mathrm{append}_a(X), X \to Y_2 \in \mathcal{R} \\ S_Y &\to P_a \circ P_e, \text{ if } Y \to \mathrm{append}_a(X), X \to \mathbf{0}_{\{1\}} \in \mathcal{R} \\ P_b &\to b_{1,2}, \text{ if } b \in \mathbb{B} \\ &\to P_X, \text{ if } X \to X, X \to Y_1 \parallel \dots \parallel Y_n \in \mathcal{R}, \text{ for } n \ge 2 \\ &\to S_Y, \text{ if } X \to X, X \to Y \in \mathcal{R} \\ &\to P_e, \text{ if } X \to X, X \to \emptyset_{\{1\}} \in \mathcal{R} \end{aligned} $$

It is easy to see that $\tilde{\Gamma}$ is an aperiodic regular series-parallel grammar if $\Gamma$ is an aperiodic tree grammar and, moreover, $\mathbf{sp}(\mathcal{L}^T(\Gamma)) = \mathcal{L}^{\mathrm{SP}}(\bar{\Gamma})$.

Then, $\mathbf{sp}(\mathcal{L}^T(\Gamma)) \subseteq \mathbf{sp}(\mathcal{L}^T(\Gamma'))$ if and only if $\mathcal{L}^{\mathrm{SP}}(\bar{\Gamma}_1) \subseteq \mathcal{L}^{\mathrm{SP}}(\bar{\Gamma}_2)$, for any two $\mathcal{F}_{\mathcal{SP}}$-grammars $\Gamma$ and $\Gamma'$, such that $\Gamma'$ is regular. Since the time needed to compute both $\bar{\Gamma}_1$ and $\bar{\Gamma}_2$ is polynomial in the sum of the sizes of $\Gamma$ and $\Gamma'$, the inclusion problem for the series-parallel class, where the right-hand side is an aperiodic regular grammar, is EXPTIME-hard. $\square$

**Lemma 3:** Let $\Gamma_{\mathcal{T}} \stackrel{\mathrm{def}}{=} (\{X, Y\}, \mathcal{R})$ be the regular tree grammar having the following rules:

$$ \begin{aligned} Y &\to \mathrm{append}_a(X, \dots, X), \text{ for all } a \in \mathbb{A} \text{ (C)} \\ X &\to X \parallel Y \text{ (A)} \quad X \to \mathbf{0}_{\{1\}} \text{ (B)} \quad \to X \text{ (E)} \end{aligned} $$

Then, we have $\mathcal{L}^T(\Gamma_{\mathcal{T}}) = \mathcal{T}$.

[Proof of Lemma 3] “$\subseteq$” Obvious, as $\Gamma_{\mathcal{T}}$ uses only operations from $\mathcal{F}_{\mathcal{T}}$. “$\supseteq$”. Let $T \in \mathcal{T}$ be a tree. Let $t$ be an $\mathcal{F}_{\mathcal{T}}$-term with $t^T = T$. By a straight-forward induction on the structure of $t$ we can establish that $T \in \mathcal{L}^T(\Gamma_{\mathcal{T}})$. $\square$

**Lemma 4:** Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R})$ be a normalized regular tree grammar. Then, $\mathrm{card}(\mathcal{A}_{\Gamma}) \in 2^{\mathrm{size}(\Gamma)^{\mathrm{poly}(\mathrm{card}(\mathcal{Y}))}}$, $\mathrm{size}(a) \in \mathcal{O}(a)$.
size(Γ)$^{poly}$ (card( Y )), for each a ∈ A$_{Γ}$ and f A$_{Γ}$ ( a$_{1}$, . . . , a$_{#f}$ ) is computable in time size(Γ)$^{poly}$ (card( Y )), for each function symbol f ∈ F$_{T}$ and all a$_{1}$, . . . , a$_{#f}$ ∈ A$_{Γ}$.

[Proof of Lemma 4]We observe that:

$$
\begin{align*}
b(Y) &= \max\{q_i \mid X \to Y_1^{\sharp q_1} \parallel \dots \parallel Y_n^{\sharp q_n} \in \mathcal{R}, Y_i = Y\} \\
      &\le \text{size}(\Gamma),
\end{align*}
$$

$$
\begin{align*}
p(Y) &= \max\{1, \text{lcm}\{q \mid X \to X \parallel Y^{\sharp q} \in \mathcal{R}\}\} \\
      &\le \text{size}(\Gamma)^{\text{card}(\mathcal{Y})},
\end{align*}
$$

$$
\begin{align*}
q(Y) &= b(Y) + p(Y) \le \text{size}(\Gamma)^{\text{card}(\mathcal{Y})} + \text{size}(\Gamma) \\
     &\in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}
\end{align*}
$$

We then set $\mathcal{Q} \stackrel{\text{def}}{=} \max\{q(Y) \mid Y \in \mathcal{Y}\} \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$.
There are at most $\mathcal{Q}^{\text{card}(\mathcal{Y})} \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$ different
reduced multisets and hence at most $2^{\text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}}$ different
sets of reduced multisets, thus $\text{card}(\mathcal{A}) = 2^{\text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}}$.

We note that an element $a \in A$ is a set of reduced multisets and there are at most $\mathcal{Q}^{\text{card}(\mathcal{Y})} \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$ different reduced multisets $m$. We then observe that $\text{card}(m) \le \text{card}(\mathcal{Y}) \cdot \mathcal{Q} \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$. Hence, we obtain that $\text{size}(a) \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$.

We now compute an upper bound on the time needed to evaluate the function $f^A(a_1, \dots, a_n)$, for each function symbol $f \in \mathcal{F}_T$ of arity $\#f = n \ge 0$ and elements $a_1, \dots, a_n \in \mathcal{A}_\Gamma$:

- $\mathbf{0}^A = \{\emptyset_m\}$ requires constant time.

- $a_1 \parallel^A a_2$ requires computing $\lceil m_1 + m_2 \rceil$ for all $m_1 \in a_1$ and $m_2 \in a_2$. We first note that computing $\lceil m_1 + m_2 \rceil$ requires a constant number of arithmetic operations for every $Y \in \mathcal{Y}$. Hence, $\lceil m_1 + m_2 \rceil$ can be computed in $\text{poly}(\text{card}(\mathcal{Y}) \cdot \mathcal{Q}) \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$. As we have to do this computation for at most size$(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$ multisets $m_1 \in a_1$ and $m_2 \in a_2$, we get that $a_1 \parallel^A a_2$ can be computed in size$(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$.

- append$_b^A(a_1, \dots, a_{\#b-1})$ requires an iteration over all rules $Y \to$ append$_b(a_1, \dots, a_{\#b-1})$ of which there are at most size$(\Gamma)$ many and over all $m_i \in a_i$ of which there are at most size$(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$ many. We then need to check whether $X_i \rightsquigarrow \Gamma m_i$, for all $i \in [1, \#b - 1]$. This check can be done by going over all rules of the form (B) with some left-hand side $X_i$ and then performing a modulo computation w.r.t. the rules of the form (A) with left-hand size $X_i$ (we recall that in $\Gamma$ there is at most one such rule for every $Y \in \mathcal{Y}$. Most precisely, for each rule $X_j \to Y_1^{\sharp q_1} \parallel \dots Y_k^{\sharp q_k}$ and each $Y_\ell, \ell \in [1, k]$, one must check that $r(j, \ell)$ divides $m_i(Y_\ell) - q_\ell$, where $X_j \to X_j \parallel Y_\ell^{\sharp r(j, \ell)}$ is the unique rule of the form (A) for $X_j$ and $Y_\ell$. Since all numbers are encoded in unary, this check takes time at most $(m_i(Y_\ell) + q_\ell) \cdot r(j, \ell) \le (\mathcal{Q} + \text{size}(\Gamma)) \cdot \text{size}(\Gamma) \in \text{size}(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$. Then, append$_b^A(a_1, \dots, a_{\#b-1})$ can be computed in size$(\Gamma)^{\text{poly}(\text{card}(\mathcal{Y}))}$).

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

Lemma 5: For all $T_1, T_2 \in \mathbb{T}$, if $h_{\Gamma}(T_1) = h_{\Gamma}(T_2)$ then $T_1 \in \mathcal{L}^{\Gamma}(\Gamma) \iff T_2 \in \mathcal{L}^{\Gamma}(\Gamma)$.

[Proof of Lemma 5]We assume $T_1 \in \mathcal{L}^{\mathcal{T}}(\Gamma)$. Then, there is a $X$-derivation of $T_1$, for some axiom $\to X$ of $\Gamma$. Without loss of generality, each such derivation can be reordered such that it starts with zero or more rules of type (A), followed by a single rule of type (B). Let $m_1$ be the multiset of nonterminals from $\mathcal{Y}$ resulting from this prefix of the derivation, namely:

$$
X \Rightarrow_{\Gamma}^{*} \parallel_{Y \in \mathcal{Y}} Y^{\sharp m_1(Y)}
$$

By Definition 13, $m_1$ is a view of $T_1$, hence $\lceil m_1 \rceil \in h_{\Gamma}(T_1)$ and $\lceil m_1 \rceil \in h_{\Gamma}(T_2)$ follows from the equality $h_{\Gamma}(T_1) = h_{\Gamma}(T_2)$. Then, there exists a view $m_2$ of $T_2$ such that $\lceil m_1 \rceil = \lceil m_2 \rceil$. Since $X \rightsquigarrow \Gamma m_1$, we obtain $X \rightsquigarrow \Gamma \lceil m_1 \rceil_{\Gamma} = \lceil m_2 \rceil_{\Gamma}$ and $X \rightsquigarrow \Gamma m_2$, by Lemma 18. Because $m_2$ is a view of $T_2$ and $X \rightsquigarrow \Gamma m_2$, by Definition 13, there exists a complete $X$-derivation:

$$
X \Rightarrow_{\Gamma}^{*} \parallel_{Y \in \mathcal{Y}} Y^{\sharp m_2(Y)} \Rightarrow_{\Gamma}^{*} \parallel_{Y \in \mathcal{Y}, i \in [1, m_2(Y)]} v(Y, i)
$$

where $v(Y, i)$ is a ground term such that $Y_i \Rightarrow_{\Gamma}^{*} v(Y, i)$, for each $Y \in \mathcal{Y}$ and $i \in [1, m_2(Y)]$ and $T_2 = (\parallel_{Y \in \mathcal{Y}, i \in [1, m_2(Y)]} v(Y, i))^T$. Because $\to X$ is an axiom of $\Gamma$, we obtain $T_2 \in \mathcal{L}^T(\Gamma)$. The other direction is symmetric. $\square$

Lemma 6: $h_{\Gamma}$ is a homomorphism between $\mathcal{T}$ and $\mathcal{A}_{\Gamma}$.

[Proof of Lemma 6]We prove the following points:

$h_{\Gamma}(\mathbf{0}_{\{1\}}^{T}) = \mathbf{0}_{\{1\}}^{A_{\Gamma}}$: the tree having one vertex and no edges is an empty $\parallel$-composition of trees derived starting with nonterminals from $\mathcal{Y}$. Hence, $h_{\Gamma}(\mathbf{0}_{\{1\}}^{T}) = \{\emptyset_{m}\} = \mathbf{0}_{\{1\}}^{A_{\Gamma}}$, by the definition of $\mathbf{0}_{\{1\}}^{A_{\Gamma}}$.

$h_{\Gamma}(T_1 \parallel^T T_2) = h_{\Gamma}(T_1) \parallel^{A_{\Gamma}} h_{\Gamma}(T_2)$: “$\subseteq$” Let $m \in h_{\Gamma}(T_1) \parallel^T T_2$ be a reduced view. Then, by Definition 13, there is a view $m'$ with $m' = [m]_{\Gamma}$ such that for each $Y \in \mathcal{Y}$ and $i \in [1, m(Y)]$, there exists a complete derivation $Y \Rightarrow_{\Gamma}^{*} v(Y, i)$, where $v(Y, i)$ is a ground term, such that $T_1 \parallel^T T_2 = \parallel_{Y \in \mathcal{Y}, i \in [1, m'(Y)]} v(Y, i)^T$. By splitting the set of terms $\{v(Y, i) \mid Y \in \mathcal{Y}, i \in [1, m'(Y)]\}$ according to whether $v(Y, i)^T$ is a subtree of $T_1$ or $T_2$, we obtain multisets $m'_1, m'_2 \in \text{mpow}(\mathcal{Y})$ such that $m' = m'_1 + m'_2$ and $T_j = (\parallel_{Y \in \mathcal{Y}, i \in [1, m'_j(Y)]} v(Y, i))^T$, for $j = 1, 2$. Hence, $m'_i$ is a view of $T_i$, for $i = 1, 2$. Let $m_i \stackrel{\text{def}}{=} [m'_i]_{\Gamma}$ be reduced views of $T_i$, for $i = 1, 2$. By Lemma 2, we have $m = [m']_{\Gamma} = [m'_1 + m'_2]_{\Gamma} = [(m'_1]_{\Gamma} + [m'_2]_{\Gamma})_{\Gamma} = [m_1 + m_2]_{\Gamma}$. Then, $m = m_1 + m_2 \in h_{\Gamma}(T_1) \parallel^{A_{\Gamma}} h_{\Gamma}(T_2)$, by the definition of $\parallel^{A_{\Gamma}}$.

"$\supseteq$" Let $m \in h_{\Gamma}(T_1) \parallel^{A_{\Gamma}} h_{\Gamma}(T_2)$ be a reduced view. By the definition of $\parallel^{A_{\Gamma}}$, there exist reduced views $m_i \in h_{\Gamma}(T_i)$, for $i = 1, 2$, such that $m = [m_1 + m_2]_{\Gamma}$. Then, there exist views $m'_i$ of $T_i$, such that $m_i = [m'_i]_{\Gamma}$, for $i = 1, 2$. Hence, for each $Y \in \text{supp}(m'_j)$ and $i \in [1, m_j(Y)]$, there exists a complete derivation $Y \Rightarrow_{\Gamma}^{*} v(Y, i, j)$ such that $T_j = (\parallel_{Y \in \mathcal{Y}, i \in [1, m'_j(Y)]} v(Y, i, j))^T$, for $j = 1, 2$. We now define the ground terms $v(Y, i)$ as $v(Y, i, 1)$ for $1 \le i \le m'_1(Y)$, and as $v(Y, i - m'_1(Y), 2)$ for $m'_1(Y) + 1 \le i \le m'_1(Y) + m'_2(Y)$. With these definitions, we have complete derivations $Y \Rightarrow_{\Gamma}^{*} v(Y, i)$ for all $1 \le i \le m'_1(Y) + m'_2(Y)$ and $Y \in \text{supp}(m'_1 + m'_2)$.
Thus, $m'_1 + m'_2$ is a view of $T_1 \|^T T_2$. Since $[m'_1 + m'_2]_\Gamma = [\lceil m'_1 \rceil_\Gamma + \lceil m'_2 \rceil_\Gamma]_\Gamma = [m_1 + m_2]_\Gamma = m$, by Lemma 2, we obtain $m \in h_\Gamma(T_1 \|^T T_2)$.

$$ \frac{h_\Gamma(\text{append}_b^T(T_1, \dots, T_{\#b-1})) = \text{append}_b^{A_\Gamma}(h_\Gamma(T_1), \dots, h_\Gamma(T_{\#b-1}))}{\text{append}_b^{A_\Gamma}(h_\Gamma(T_1), \dots, h_\Gamma(T_{\#b-1}))} $$
“≤” Let $m \in \text{append}_b^{A_\Gamma}(h_\Gamma(T_1), \dots, h_\Gamma(T_{\#b-1}))$ be a multiset. By the definition of $\text{append}_b^{A_\Gamma}$, there exist reduced views $m_i \in h_\Gamma(T_i)$ and a rule $Y \to \text{append}_b(X_1, \dots, X_{\#b-1})$ in $\Gamma$ such that $X_i \rightsquigarrow \Gamma m_i$, for all $i \in [1, \#b-1]$, and $m = \{\{Y\}\}$. Then, for each $i \in [1, \#b-1]$, there exists a view $m'_i$ of $T_i$ for $\Gamma$ such that $m_i = \lceil m'_i \rceil_\Gamma$. By Lemma 18, we obtain $X_i \rightsquigarrow \Gamma m'_i$, hence there exists complete derivations:

$$ X_i \Rightarrow_{\Gamma}^{*} \|_{Y \in \mathcal{Y}} Y^{\sharp m_i}(Y) $$

for some view $m_i$ of $T_i$, for each $i \in [1, \#b-1]$. Then $[m_i]_\Gamma \in h_\Gamma(T_i)$, for each $i \in [1, \#b-1]$. Since $X_i \rightsquigarrow \Gamma m_i$, we obtain $X_i \rightsquigarrow \Gamma [m_i]_\Gamma$, by Lemma 18, hence $m = [m']_\Gamma = \{\{Y\}\} \in \text{append}_b^{A_\Gamma}(h_\Gamma(T_1), \dots, h_\Gamma(T_{\#b-1}))$, by the definition of $\text{append}_b^{A_\Gamma}$.

“≥” Let $m \in \text{append}_b^{A_\Gamma}(h_\Gamma(T_1), \dots, h_\Gamma(T_{\#b-1}))$ be a multiset. By the definition of $\text{append}_b^{A_\Gamma}$, there exist reduced views $m_i \in h_\Gamma(T_i)$ and a rule $Y \to \text{append}_b(X_1, \dots, X_{\#b-1})$ in $\Gamma$ such that $X_i \rightsquigarrow \Gamma m_i$, for all $i \in [1, \#b-1]$, and $m = \{\{Y\}\}$. Then, for each $i \in [1, \#b-1]$, there exists a view $m'_i$ of $T_i$ for $\Gamma$ such that $m_i = \lceil m'_i \rceil_\Gamma$. By Lemma 18, we obtain $X_i \rightsquigarrow \Gamma m'_i$, hence there exists complete derivations:

$$ X_i \Rightarrow_{\Gamma}^{*} \|_{Y \in \mathcal{Y}} Y^{\sharp m'_i}(Y) \Rightarrow_{\Gamma}^{*} \|_{Y \in \mathcal{Y}, j \in [1, m'_i(Y)]} v(Y, i, j) $$

where $v(Y, i, j)$ are ground terms such that $Y \Rightarrow_{\Gamma}^{*} v(Y, i, j)$ and $T_i = (\|_{Y \in \mathcal{Y}, j \in [1, \#b-1]} v(Y, i, j))^T$, for each $i \in [1, \#b-1]$. We combine these $X_i$-derivations with the rule $Y \to \text{append}_b(X_1, \dots, X_{\#b-1})$ to obtain a complete $Y$-derivation of a ground term that evaluates to $T \stackrel{\text{def}}{=} \text{append}_b^T(T_1, \dots, T_{\#b-1})$, hence $\{\{Y\}\}$ is a view of $T$ and $m = \lceil \{\{Y\}\} \rceil = \{\{Y\}\} \in h_\Gamma(T)$. □

**Lemma 7:** The algebra $\mathcal{A}_\Gamma$ is aperiodic if the regular tree grammar $\Gamma$ is aperiodic.

[Proof of Lemma 7] The regular grammar $\Gamma$ is aperiodic iff the modified grammar $\Gamma'$ obtained from Lemma 1 has $q = 1$ for each rule $X \to X \parallel Y^{\sharp q}$ of the form (A). If $\Gamma$ is aperiodic, we must have $p(Y) = 1$, for each nonterminal $Y \in \mathcal{Y}$, because $p$ is computed from $\Gamma'$. Then, for each multiset $m \in \text{mpow}(\mathcal{Y})$, we have:

$$ [m](Y) = \begin{cases} m(Y), & \text{if } m(Y) < q(Y) \\ q(Y), & \text{otherwise} \end{cases} $$

By [17, Lemma 5.11], it is sufficient to prove that the commutative semigroup $(M, \oplus)$ is aperiodic, where $M \subseteq \text{mpow}(\mathcal{Y})$ is the set of all reduced multisets and $m_1 \oplus m_2 \stackrel{\text{def}}{=} [m_1 + m_2]$. Now consider an element $m \in M$ and its idempotent power

idem($m$). By the definition of $[\cdot]$ and Lemma 2, we obtain that $\text{idem}(m)(Y)$ is either 0 or $q(Y)$, for each nonterminal $Y \in \mathcal{Y}$. Hence, $\text{idem}(m) \oplus m = \text{idem}(m)$. Since the choice of $m \in M$ was arbitrary, we obtain that $(M, \oplus)$ is a aperiodic. □

**Theorem 5:** The language of each (aperiodic) regular tree grammar $\Gamma$ is recognizable by an (aperiodic) recognizer $(A, B)$, where $\text{card}(A) \in 2^{2^{\text{poly}(\text{size}(\Gamma))}}$ and $f^A(a_1, \dots, a_{\#f})$ can be computed in time $2^{\text{poly}(\text{size}(\Gamma))}$, for each function symbol $f \in \mathcal{F}_\Gamma$ and all elements $a_1, \dots, a_{\#f} \in A$.

[Proof of Theorem 5] Let $\Gamma$ be a regular (aperiodic) tree grammar. Using Lemma 1, we obtain a normalized (aperiodic) grammar $\Gamma' = (\mathcal{X} \uplus \mathcal{Y}, \mathcal{R}')$. In particular, we have $\mathcal{L}^\Gamma(\Gamma') = \mathcal{L}^\Gamma(\Gamma)$ and $\text{size}(\Gamma') \in 2^{\text{poly}(\text{card}(\mathcal{X})+\text{card}(\mathcal{Y}))\cdot\log(\text{size}(\Gamma))}$. Note that $\Gamma$ and $\Gamma'$ have the same set of nonterminals. Then, we build the recognizer $\mathcal{A}_{\Gamma'}$ based on the grammar $\Gamma'$. By Lemma 5, we obtain $\mathcal{L}^\Gamma(\Gamma') = h_\Gamma^{-1}(B_{\Gamma'}')$, where $B_{\Gamma'} \stackrel{\text{def}}{=} \{h_{\Gamma'}(T) | T \in \mathcal{L}^\Gamma(\Gamma')\}$. By Lemma 6, $(\mathcal{A}_{\Gamma'}, B_{\Gamma'})$ is a recognizer for $\mathcal{L}^\Gamma(\Gamma')$. Because of $\mathcal{L}^\Gamma(\Gamma') = \mathcal{L}^\Gamma(\Gamma)$, $\mathcal{A}_{\Gamma'}$ is also a recognizer for the language of $\Gamma$. Moreover, $\mathcal{A}_{\Gamma'}$ is aperiodic if $\Gamma'$ is aperiodic, by Lemma 7. By Lemma 4, we further have that:

$$ \begin{aligned} \text{card}(\mathcal{A}_{\Gamma'}) &\in 2^{\text{size}(\Gamma')} \cdot \text{poly}(\text{card}(\mathcal{Y})) \\ &\in 2^{2^{\text{poly}(\text{card}(\mathcal{X})+\text{card}(\mathcal{Y}))\cdot\log(\text{size}(\Gamma))}} \cdot \text{poly}(\text{card}(\mathcal{Y})) \\ &\in 2^{2^{\text{poly}(\text{size}(\Gamma))}} \end{aligned} $$

Moreover, $f^{\mathcal{A}_{\Gamma'}}(a_1, \dots, a_n)$ can be computed in time:

$$ \begin{aligned} \text{size}(\Gamma')^{\text{poly}(\text{card}(\mathcal{Y}))} &\in 2^{\text{poly}(\text{card}(\mathcal{X})+\text{card}(\mathcal{Y}))\cdot\log(\text{size}(\Gamma))} \cdot \text{poly}(\text{card}(\mathcal{Y})) \\ &\in 2^{\text{poly}(\text{size}(\Gamma))} \end{aligned} $$

for each $f \in \mathcal{F}_\Gamma$ and $a_1, \dots, a_n \in \mathcal{A}_{\Gamma'}$. □

**Lemma 9:** Each connected graph with at least two vertices has only nontrivial blocks.

[Proof of Lemma 9] Suppose, for a contradiction, that $G$ is a connected graph with two or more vertices that has a trivial block $B$, consisting of one vertex $u \in V_G$. Then, $G$ has another vertex $v \in V_G \setminus \{u\}$. Because $G$ is connected, there is a path between $u$ and $v$, hence there is an edge $e$ attached to $u$ and some other vertex $w$ (possibly $w = v$). The graph with vertex set $\{u, w\}$ and edge set $\{e\}$ has no cutvertex and subsumes $B$, contradicting the fact that $B$ is a maximal subgraph of $G$ without a cutvertex. □

**Lemma 11:** Let $G$ be a connected graph of tree-width at most 2, $B$ be a nontrivial block of $G$ and $x$ be a vertex of $B$. Then, there exists another vertex $y$ of $B$ such that $B_{(x,y)}$ (the graph $B$ having 1-source $x$ and 2-source $y$) is a disoriented P-graph.

[Proof of Lemma 11] Let $(T, \beta)$ be a tree decomposition of $B$ such that $\text{wd}(T, \beta) = \text{tw}(B)$. The sets $\beta(n)$, $n \in V_T$ are called *bags*. If $m$ is the parent of $n$ in $T$, the set $\text{adh}_{T, \beta}(n) \stackrel{\text{def}}{=} \beta(m) \cap \beta(n)$ is the *adhesion* of $n$ in $(T, \beta)$ (by convention, $\text{adh}_{T, \beta}(n) = \emptyset$ if $n$ is the root of $T$).

Because $B$ is connected and has at least two vertices, there must be an edge from $x$ to some other vertex $y$ and there
must be some node whose bag contains both $x$ and $y$. We can w.l.o.g. assume that this node is the root of $T$ (otherwise we can reorient the edges of $T$ such that this node becomes the root). We can further assume w.l.o.g. that the bag of the root contains exactly $\{x, y\}$ (otherwise we add a new root node to the tree, connected to the old root, whose bag contains exactly $\{x, y\}$). Further, w.l.o.g, we can choose $(T, \beta)$ such that $\beta(n) \setminus \beta(m) \neq \emptyset$, for each pair $(m, n)$ of parent and child nodes of $T$ (if $\beta(n) \subseteq \beta(m)$ then the edge of $T$ between $m$ and $n$ can be contracted). Since $B$ has no cutvertex, it follows that $\text{card}(\text{adh}_{T, \beta}(n)) \geq 2$, for all non-root nodes $n \in V_T$. This is a consequence of the fact that the adhesion of each non-root node of $T$ is a separator of $B$, see e.g. [24, Lemma 11.3]. Since $\text{card}(\beta(n)) \leq 3$, the bag of each non-root node can be uniquely decomposed into its adhesion $\{u_1, u_2\}$ and a third element $v \notin \{u_1, u_2\}$. Where no confusion arises, we shall use the names $u_1, u_2$ (for the adhesion) and $v$ (for the remaining vertex) throughout the proof. Moreover, w.l.o.g, we can choose $(T, \beta)$ such that $\text{adh}_{T, \beta}(n) \neq \text{adh}_{T, \beta}(m)$ for each pair $(m, n)$ of parent and child of $T$; if $\text{adh}_{T, \beta}(n) = \text{adh}_{T, \beta}(m)$, then $n$ can be attached as a child to the parent of $m$. For every pair of vertices $u_1, u_2$ of $B$ we define the graph $B^{\{u_1, u_2\}}$ of sort $\{1, 2\}$ as the subgraph of $B$ consisting only of the vertices $u_1$ and $u_2$ and all the edges of $B$ between these two vertices. For every non-root node $n \in V_T$, with $\text{adh}_{T, \beta}(n) = \{u_1, u_2\}$, we denote by $B|_n^{\{u_1, u_2\}}$ the subgraph of $B$ of sort $\{1, 2\}$, with $u_1$ resp. $u_2$ as the first resp. second source, induced by $\bigcup \{\beta(p) \mid p \text{ is a descendant of } n\}$ minus the edges of $B^{\{u_1, u_2\}}$.

**Fact 2:** For every non-root node $n \in V_T$, with $\text{adh}_{T, \beta}(n) = \{u_1, u_2\}$, we have $B|_n^{\{u_1, u_2\}} \in \text{DSP}$.

**Proof.** By induction on the structure of the subtree $T|_n$ of $T$ rooted at $n$, where $\{u_1, u_2, v\} \stackrel{\text{def}}{=} \beta(n)$ and $\{u_1, u_2\} \stackrel{\text{def}}{=} \text{adh}_{T, \beta}(n)$. Let $p_1, \dots, p_k$ be the children of $n$ in $T$. Then, for each $i \in [1, k]$, $\text{adh}_{T, \beta}(p_i)$ is either $\{u_1, v\}$ or $\{u_2, v\}$. Let $P_{u_1, v} \uplus P_{v, u_2} = \{p_1, \dots, p_k\}$ be the sets such that $\text{adh}_{T, \beta}(p) = \{u_1, v\}$ resp. $\text{adh}_{T, \beta}(p) = \{u_2, v\}$, for all $p \in P_{u_1, v}$ resp. $p \in P_{v, u_2}$. We now observe that:

$$ B|_n^{(u_1, u_2)} = \left( \left( \left\|_{p \in P_{u_1, v}}^{\mathcal{G}} B|_p^{(u_1, v)} \right\|^{\mathcal{G}} B^{\{u_1, v\}} \right) \circ^{\mathcal{SP}} \left( \left\|_{p \in P_{v, u_2}}^{\mathcal{G}} B|_p^{(v, u_2)} \right\|^{\mathcal{G}} B^{\{v, u_2\}} \right) \right) \quad \square $$

Back to the proof, let $n$ be the root of $T$, and let $p_1, \dots, p_k$ be the children of $n$ in $T$. We recall that $\beta(n) = \{x, y\}$. We now observe that:

$$ B_{(x,y)} = B^{\{x,y\}} \|^{\mathcal{G}} \left( \|_{i \in [1,k]}^{\mathcal{G}} B|_{p_i}^{(x,y)} \right) $$

This establishes that $B_{(x,y)} \in \text{DSP}$. Now, we use the fact that $B$ is a block (i.e., has no cutvertex) to obtain that $B_{(x,y)}$ is $\circ$-atomic: Assume that $B_{(x,y)}$ is not $\circ$-atomic. Then, by Lemma 8, there are some graphs $G_1, G_2$ of sort $\{1, 2\}$ with $B_{(x,y)} = G_1 \circ G_2$. In particular, the 2-source of $G_1$ (which is equal to the 1-source of $G_2$) is a cutvertex of $B_{(x,y)}$. However, this contradicts the definition of a block, which cannot contain a cutvertex. $\square$

**Lemma 12:** Let $\Gamma_2 \stackrel{\text{def}}{=} (\{X, Y, P, S\}, \mathcal{R})$ be the regular tree-width 2 grammar with the below rules, for $b \in \mathbb{B}$ and $i = 1, 2$:

$$ \begin{array}{lclcl} \rightarrow & X & (\text{E}) & Y & \rightarrow & P \triangleright X & (\text{C}) & S & \rightarrow & b_{i,3-i} & (\text{C}) \\ X & \rightarrow & X & \parallel & Y & (\text{A}) & S & \rightarrow & \circ & (P, S, X) & (\text{C}) & P \rightarrow b_{i,3-i} & (\text{D}) \\ X & \rightarrow & \mathbf{0}_{\{1\}} & (\text{B}) & S & \rightarrow & \circ & (P, P, X) & (\text{C}) & P & P & \parallel & S & (\text{A}) \\ & & & & & & & & & P & S & \parallel & S & (\text{B}) \end{array} $$

The sets $\mathcal{L}_{\mathcal{G}_2}(\Gamma_2)$, $G_2^{\{1\}}$ and $\{G \in \mathcal{G} \text{ connected } | \text{tw}(G) \leq 2, \sigma(G) = \{1\}\}$ are equal.

[Proof of Lemma 12]"$\mathcal{L}_{\mathcal{G}_2}(\Gamma_2) \subseteq G_2^{\{1\}}$" Clearly, all graphs resulting from derivations of the $\mathcal{G}_2$-grammar $\Gamma_2$ belong to $G_2$ — the universe of the algebra $\mathcal{G}_2$. Further, all graphs resulting from the axiom $X$ have sort $\{1\}$ and hence belong to $G_2^{\{1\}}$. "$G_2^{\{1\}} \subseteq \{G \text{ connected } | \text{tw}(G) \leq 2, \sigma(G) = \{1\}\}$" Each graph $G \in \mathcal{L}_{\mathcal{G}_2}(\Gamma_2)$ has tree-width at most 2, because the grammar $\Gamma_2$ only uses operations from the derived algebra $\mathcal{G}_2$, whose function symbols are interpreted using operations from $G$ that involve at most 3 sources. Moreover, all these operations preserve connectivity and each $X$-derivation yields terms of sort $\{1\}$.

"$\{G \text{ connected } | \text{tw}(G) \leq 2, \sigma(G) = \{1\}\} \subseteq \mathcal{L}_{\mathcal{G}_2}(\Gamma_2)$" Let $G$ be a connected graph of tree-width at most 2 of sort $\{1\}$, and let $T$ be its block tree. In case the 1-source is a cutvertex, we can assume without loss of generality (by rotating the block tree), that the 1-source is the root of the block tree. In case the 1-source is not a cutvertex, we can assume without loss of generality (by rotating the block tree), that the block containing the 1-source is the root of the block tree; we then add the 1-source as the new root to the block tree. We introduce the following notation: For every node of the block tree consisting of a single vertex $v \in V_G$ (that is $v$ is either a cutvertex or the 1-source of $G$), we denote by $G_v$ the subgraph of $G$ that is induced by $v$ and its descendants in the block tree, where $G_v$ is considered as a graph of sort $\{1\}$ with 1-source $v$. Note that we have $G_v = G$ for the 1-source $v$ of $G$, because $v$ is the root of the block tree.

We will now prove that $G_v \in \mathcal{L}_{\mathcal{G}_2}^{\mathcal{G}_2}(\Gamma_2)$ for every node of the block tree consisting of a single vertex $v \in V_G$. Recall that this is sufficient to prove the claim because we also consider $G_v = G$ for the 1-source $v$ of $G$. If $G_v$ has one vertex and no edges, we obtain $G_v \in \mathcal{L}_{\mathcal{G}_2}^{\mathcal{G}_2}(\Gamma_2)$ by applying the rule $X \rightarrow \mathbf{0}_{\{1\}}$ from $\Gamma_2$. Else, by Lemma 9, each block of $G_v$ is nontrivial. Let $B_1, \dots, B_\ell$ be the blocks that are the children of $v$ in the block tree. For each $j \in [1, \ell]$, let $c_1^j, \dots, c_n^j$ be the vertices that are the children of $B_j$ in $T$. By the inductive hypothesis, there exist complete derivations $X \Rightarrow_{\Gamma_2}^* \gamma_{i,j}$ such that $\gamma_{i,j}^{\mathcal{G}_2} = G_{c_i^j}$, where each $G_{c_i^j}$ is of sort $\{1\}$, having $c_i^j$ as its 1-source. By Lemma 11, for each $j \in [1, \ell]$ there is some vertex $w_j$ of $B_j$, such that $(B_j)_{(v, w_j)}$, the graph $B_j$ considered as graph of sort $\{1, 2\}$, with $v$ (resp. $w_j$) as its 1-source (resp. 2-source), is a $\circ$-atomic disoriented series-parallel graph. By Lemma 24 (naturally extended to disoriented series-parallel graphs) there is a derivation $P \Rightarrow_{\Gamma_{DSP}}^* \beta_j$ of the universal series-parallel grammar $\Gamma_{DSP}$ that witnesses $(B_j)_{(v, w_j)} \in \mathcal{L}_{\Gamma_{DSP}}^{\text{DSP}}$ (we
recall that $\Gamma_{DSP}$ contains, in addition to the rules of $\Gamma_{SP}$, the rules $S \to b_{2,1}$ and $P \to b_{2,1}$, for each $b \in \mathbb{B}$).

We now take the derivations $P \Rightarrow_{\Gamma_{DSP}}^* \beta_j$, for every $1 \le j \le \ell$ and build modified derivations $P \Rightarrow_{\Gamma_2}^* \theta_j$ such that $\delta_{\Gamma_2}^j$ is the graph $(B_j)_{(v,w_j)}$ to which we attach all the graphs $G_j^{c_i}$ at the respective cutvertices $c_i^j$, for every $i$ such that $c_i^j \neq w_j$. We obtain the derivation $P \Rightarrow_{\Gamma_2}^* \theta_j$ from $P \Rightarrow_{\Gamma_{DSP}}^* \beta_j$ as follows:

- each step $S \Rightarrow_{\Gamma_{DSP}} P \circ S$ is replaced by the derivation:

* $S \Rightarrow_{\Gamma_2} \circ(P, S, X) \Rightarrow_{\Gamma_2}^* \circ(P, S, \gamma_{i,j})$, if the join vertex of the serial composition is the cutpoint $c_i^j$, for some $i \in [1, n_j]$, or

* $S \Rightarrow_{\Gamma_2} \circ(P, S, X) \Rightarrow_{\Gamma_2} \circ(P, S, \mathbf{0}_{\{1\}})$, otherwise.

- each step $S \Rightarrow_{\Gamma_{DSP}} P \circ P$ is replaced by the derivation:

* $S \Rightarrow_{\Gamma_2} \circ(P, P, X) \Rightarrow_{\Gamma}^* \circ(P, P, \gamma_{i,j})$, if the join vertex of the serial composition is the cutpoint $c_i^j$, for some $i \in [1, n_j]$, or

* $S \Rightarrow_{\Gamma_2} \circ(P, P, X) \Rightarrow_{\Gamma_2} \circ(P, P, \mathbf{0}_{\{1\}})$, otherwise.

For each $j \in [1, \ell]$, we build the complete derivation

$$Y \Rightarrow_{\Gamma_2} P \triangleright X \Rightarrow_{\Gamma_2}^* \theta_j \triangleright \delta_j,$$

where $\delta_j = \mathbf{0}_{\{1\}}$ in case that $c_i^j \neq w_j$ for all $i$, and $\delta_j = \gamma_{i,j}$ in case that $c_i^j = w_j$ for some $i$. Since $B_1, \dots, B_\ell$ are the children of $v$ in the block tree, each graph $G_j$ consisting of $B_j$ and all its descendants in the block tree is a graph of sort $\{1\}$ with $v$ as 1-source such that, moreover $G = G_1 \parallel G_2 \dots \parallel G_2 G_\ell = (\theta_1 \triangleright \delta_1 \parallel \dots \parallel \theta_\ell \triangleright \delta_\ell)^{G_2}$. We consider the complete derivation

$$X \Rightarrow_{\Gamma_2}^* X \parallel Y^{\parallel\ell} \Rightarrow_{\Gamma_2} \mathbf{0}_{\{1\}} \parallel Y^{\parallel\ell} \Rightarrow_{\Gamma_2}^* \mathbf{0}_{\{1\}} \parallel (\parallel_{j \in [1, \ell]} \theta_j \triangleright \delta_j),$$

Lemma 19: Let $S \in S$, $Q \in \mathcal{P} \uplus S$ and $X \in \mathcal{X}$ be non-terminals. Then, for every derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u, Q, X)$, there are non-terminals $P_1, \dots, P_n$ and $X_1, \dots, X_{n-1}$, derivations $P_i \Rightarrow_{\Gamma}^* v_i$ and $X_j \Rightarrow_{\Gamma}^* t_j$, and rules $S_i \to \circ(P_i, S_{i+1}, X_i)$, for $1 \le i < n-1$, with $S = S_1$, and a rule $S_{n-1} \to \circ(P_n, Q, X)$ such that $u \stackrel{a}{\sim} \circ(\dots \circ (v_1, v_2, t_1), \dots, v_n, t_{n-1})$.

Proof. We consider the derivation $S \Rightarrow_{\Gamma}^* t[Q, X]$, where $t[Q, X]$ is a term such that $t[Q, X] \stackrel{a}{\sim} \circ(u, Q, X)$. We note that the only rules of a regular tree-width 2 grammar that generate series compositions are the rules of shape $S_1 \to \circ(P, S_2, X)$ and $S \to \circ(P_1, P_2, X)$. Further, because $Q$ occurs at the rightmost position of a series-composition of terms, we must have (up to a reordering of the rule applications) that the derivation $S \Rightarrow_{\Gamma}^* t[Q, X]$ has the form

$$ \begin{align*} S_1 \Rightarrow_{\Gamma} \circ(P_1, S_2, X_1) &\Rightarrow_{\Gamma} \circ(P_1, \circ(P_2, S_3, X_2), X_1) \Rightarrow_{\Gamma} \\ &\dots \\ &\Rightarrow_{\Gamma} \circ(P_1, \circ(P_2, \circ(\dots, \circ(P_n, Q, X), \dots), X_2), X_1) \\ &\Rightarrow_{\Gamma}^* \circ(v_1, \circ(v_2, \circ(\dots, \circ(v_n, Q, X), \dots), t_2), t_1) \end{align*} $$

where $S = S_1$, and $P_i \Rightarrow_{\Gamma}^* v_i$, $X_j \Rightarrow_{\Gamma}^* t_j$ are derivations, for all $i \in [1, n]$ and $j \in [1, n-1]$. We obtain $t[Q, X] = \circ(v_1, \circ(v_2, \circ(\dots, \circ(v_n, Q, X), \dots), t_2), t_1) \stackrel{a}{\sim}$

$\circ(u, Q, X)$. Hence, $u \stackrel{a}{\sim} (\dots \circ (v_1, v_2, t_1), \dots, v_n, t_{n-1})$, see Figure 6 (b). $\square$

Lemma 20: Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus S, \mathcal{R})$ be a regular tree-width 2 grammar, $S \in S$ and $Q \in \mathcal{P} \uplus S$ be nonterminals, $G \in G_{\{1,2\}}$ be an S-graph and $K \in G_{\{1\}}$ be a graph. Then, for all graphs $G_1, G_2 \in G_{\{1,2\}}$ and $H \in G_{\{1\}}$ such that $G = \circ G_2(G_1, G_2, H)$, the following are equivalent:

1. there exists a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u, Q, X)$, where $u$ is a ground $\mathcal{F}_2$-term such that $u^{G_2} = G$,

2. there exists derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_1, S', w)$ and $S' \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_2, Q, X)$, for some nonterminal $S' \in \mathcal{Y}_{\{1,2\}}$ and ground $\mathcal{F}_2$-terms $u_1, u_2$ and $w$ such that $u_i^{G_2} = G_i$, for $i = 1, 2$ and $w^{G_2} = H$.

Proof. “(1) $\Rightarrow$ (2)” We assume that there exists a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u, Q, X)$, where $u$ is a ground $\mathcal{F}_{SP}$-term such that $u^{G_2} = G$. By Lemma 19, there are non-terminals $P_1, \dots, P_n$ and $X_1, \dots, X_{n-1}$, derivations $P_i \Rightarrow_{\Gamma}^* v_i$ and $X_j \Rightarrow_{\Gamma}^* t_j$, and rules $S_i \to \circ(P_i, S_{i+1}, X_i)$, for $1 \le i < n-1$, with $S = S_1$, and a rule $S_{n-1} \to \circ(P_n, Q, X)$ such that $u \stackrel{a}{\sim} (\dots \circ (v_1, v_2, t_1), \dots, v_n, t_{n-1})$. Since $u^{G_2} = \circ G_2(G_1, G_2, H)$, we must have:

$$ \begin{align*} G_1 &= (\circ(\dots \circ (v_1, v_2, t_1) \dots, v_i, t_{i-1}))^{G_2} \\ G_2 &= (\circ(\dots \circ (v_{i+1}, v_{i+2}, t_{i+1}) \dots, v_n, t_{n-1}))^{G_2} \\ H &= t_i^{G_2}, \text{ for some } i \in [1, n-1] \end{align*} $$

We define:

$$ \begin{align*} u_1 &\stackrel{\text{def}}{=} \circ (\dots \circ (v_1, v_2, t_1) \dots, v_i, t_{i-1}) \\ u_2 &\stackrel{\text{def}}{=} \circ (\dots \circ (v_{i+1}, v_{i+2}, t_{i+1}) \dots, v_n, t_{n-1}) \\ w_1 &\stackrel{\text{def}}{=} t_i \end{align*} $$

The existence of the derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_1, S_i, w_1)$ and $S_i \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_2, Q, X)$ follows from the decomposition of the above derivation up to and from $S_i$ onwards, modulo re-orderings via associativity of the subderivations.

“(2) $\Rightarrow$ (1)” We assume that there exist derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_1, S', w)$ and $S' \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_2, Q, X)$, where $u_i$ are ground $\mathcal{F}_{SP}$-terms such that $u_i^{G_2} = G_i$ and $w^{G_2} = H$. By Lemma 19, there are non-terminals $P_1, \dots, P_n$ and $X_1, \dots, X_{n-1}$, derivations $P_i \Rightarrow_{\Gamma}^* v_i$ and $X_j \Rightarrow_{\Gamma}^* t_j$, and rules $S_i \to \circ(P_i, S_{i+1}, X_i)$, for $1 \le i < n-1$, with $S = S_1$, $S' = S_k$, and $w = t_k$, and a rule $S_{n-1} \to \circ(P_n, Q, X)$ such that $u_1 \stackrel{a}{\sim} \circ(\dots \circ (v_1, v_2, t_1), \dots, v_i, t_{i-1})$ and $u_2 \stackrel{a}{\sim} \circ(\dots \circ (v_{i+1}, v_{i+2}, Q), \dots, v_n, t_{n-1})$. Hence, we obtain $\circ(u_1, u_2, w_1) \stackrel{a}{\sim} \circ(v_1, \circ(v_2, \circ(\dots, \circ(v_n, Q, X), \dots), t_2), t_1)$, which proves $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u_1, u_2, w), Q, X$. Since $G = \circ G_2(G_1, G_2, H) = \circ G_2(u_1^{G_2}, u_2^{G_2}, w^{G_2})$, we define $u \stackrel{\text{def}}{=} \circ(u_1, u_2, w)$, thus obtaining $S \stackrel{a}{\Rightarrow}_{\Gamma}^* \circ(u, Q, X)$. $\square$

Lemma 13: Let $\Gamma = (\mathcal{X} \uplus \mathcal{Y} \uplus \mathcal{P} \uplus S, \mathcal{R})$ be a normalized regular tree-width 2 grammar in alternative form. Then, $\text{card}(\mathcal{A}_{\Gamma}) \in 2^{\text{poly}(\text{size}(\Gamma))}$ and $\text{size}(a) \in 2^{\text{poly}(\text{size}(\Gamma))}$ for each $a \in \mathcal{A}_{\Gamma}$. Moreover, $f^{\mathcal{A}_{\Gamma}}(a_1, \dots, a_{\#f})$ can be computed in time $2^{\text{poly}(\text{size}(\Gamma))}$, for each function symbol $f \in \mathcal{F}_2$ and all elements $a_1, \dots, a_{\#f} \in \mathcal{A}_{\Gamma}$.
[Proof of Lemma 13]As in the proof of Lemma 4, we have at most size($\Gamma$)$^{poly}$($card(Y)$) reduced multisets in a profile of sort $\{1\}$ and at most size($\Gamma$)$^{poly}$($card(S)$) multisets in a P-profile of sort $\{1, 2\}$. Moreover, there are at most $card(S) \cdot (card(P) + card(S) \cdot card(X)$ triples of the form $(S, Q, X)$ and at most $card(S)$ pairs $(S, \perp)$ in an S-profile of sort $\{1, 2\}$. Thus, we obtain:

$$ \begin{aligned} \mathrm{card}(\mathcal{A}_{\Gamma}) &\in 2^{\mathrm{size}(\Gamma)^{\mathrm{poly}(\mathrm{card}(Y))}} + 2^{\mathrm{size}(\Gamma)^{\mathrm{poly}(\mathrm{card}(S))}} + \\ &\quad 2^{\mathrm{card}(S) \cdot (\mathrm{card}(P) + \mathrm{card}(S)) \cdot \mathrm{card}(X) + \mathrm{card}(S)} \\ &\in 2^{2^{\mathrm{poly}(\mathrm{size}(\Gamma))}} \end{aligned} $$

An element $a \in \mathcal{A}_\Gamma$ is a set of either reduced multisets from $mpow(Y)$ or $mpow(S)$, or a set of triples $(S, Q, X)$ and pairs $(S, \perp)$. As in the proofs of Lemmas 4 and 27, we then obtain $\mathrm{size}(a) \in \mathrm{size}(\Gamma)^{\mathrm{poly}(\mathrm{size}(\Gamma))}$ for each $a \in \mathcal{A}_\Gamma$.

We compute an upper bound on the time needed to evaluate the function $f^{\mathcal{A}_\Gamma}$, for each $f \in \mathcal{F}_2$:

- the cases $0_{\{1\}}^{\mathcal{A}_\Gamma}$, $b_{1,2}^{\mathcal{A}_\Gamma}$ and $a_1 \|^{\mathcal{A}} a_2$ have similar counterparts in the proofs of Lemmas 4 and 27, respectively.

- $a_1 \triangleright a_2$: since $a_1$ is a P-profile of sort $\{1, 2\}$, there are at most size($\Gamma$)$^{\mathrm{poly}(\mathrm{card}(S))}$ many multisets $m \in a_1$ and the check $P \rightsquigarrow \Gamma m$, for a given nonterminal $P$ and a multiset $m \in a_1$, takes size($\Gamma$)$^{\mathrm{poly}(\mathrm{card}(S))}$ time. Similarly, because $a_2$ is a profile of sort $\{1\}$, there are at most size($\Gamma$)$^{\mathrm{poly}(\mathrm{card}(Y))}$ multisets $k \in a_2$ and the check $X \rightsquigarrow k$, for a given multiset $k \in a_2$, takes time size($\Gamma$)$^{\mathrm{poly}(\mathrm{card}(Y))}$. Then, the application of the ($\triangleright$) inference rule from Figure 7, takes $2^{\mathrm{poly}(\mathrm{size}(\Gamma))}$ time.

- $\circ^{\mathcal{A}_\Gamma}(a_1, a_2, a_3)$: depending on the type of the profiles $a_1$ and $a_2$, the application of either of the inference rules ($P \circ^i P$), ($P \circ^i S$), ($S \circ^i P$) and ($S \circ^i S$) requires an iteration over the rules of $\Gamma$ and the evaluation of at most three conditions $P \rightsquigarrow \Gamma m$ (resp. $X \rightsquigarrow \Gamma k$) for some given nonterminal $P \in \mathcal{P}$ (resp. $X \in X$) and multiset $m \in a_i$, $i = 1, 2$ (resp. $k \in a_3$). Since these checks take time size($\Gamma$)$^{\mathrm{poly}(\mathrm{card}(S))}$ (resp. $\mathrm{size}(\Gamma)^{\mathrm{poly}(\mathrm{card}(Y))}$), the entire computation takes $2^{\mathrm{poly}(\mathrm{size}(\Gamma))}$ time.

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

**Lemma 14:** For all $G_1, G_2 \in G_2$, if $h_\Gamma(G_1) = h_\Gamma(G_2)$ then $G_1 \in \mathcal{L}^{G_2}(\Gamma) \iff G_2 \in \mathcal{L}^{G_2}(\Gamma)$.

[Proof of Lemma 14]We assume that $G_1 \in \mathcal{L}^{G_2}(\Gamma)$ and prove $G_2 \in \mathcal{L}^{G_2}(\Gamma)$ (the other direction is symmetric). Since $h_\Gamma(G_1) = h_\Gamma(G_2)$, we distinguish three cases:

$\sigma(G_1) = \sigma(G_2) = \{1\}$: the proof in this case is similar to the proof of Lemma 5.

$\sigma(G_1) = \sigma(G_2) = \{1, 2\}$ and $G_1, G_2$ are P-graphs: the proof in this case is similar to the proof of Lemma 28 in the case $G_1, G_2 \in \mathcal{SP}$ are both P-graphs.

$\sigma(G_1) = \sigma(G_2) = \{1, 2\}$ and $G_1, G_2$ are S-graphs: Since $G_1 \in \mathcal{L}^{G_2}(\Gamma)$, there exists a complete derivation $S \Rightarrow_{\Gamma}^* u_1$ such that $u_1^{G_2} = G_1$, for some axiom $\to S$ of $\Gamma$. By Definition 18 (3b), we obtain $(S, \perp) \in h_\Gamma(G_1)$, hence $(S, \perp) \in h_\Gamma(G_2)$, by the equality $h_\Gamma(G_1) = h_\Gamma(G_2)$. Again by Definition 18

(3b), we obtain a complete derivation $S \Rightarrow_{\Gamma}^* u_2$ such that $u_2^{G_2} = G_2$, hence $G_2 \in \mathcal{L}^{G_2}(\Gamma)$, because $\to S$ is an axiom. $\square$

**Lemma 15:** $h_\Gamma$ is a homomorphism between $G_2$ and $\mathcal{A}_\Gamma$.

[Proof of Lemma 15]We prove the following points, for all $b \in \mathbb{B}$, $1 \le i \le 2$ and $G_1, G_2 \in G_2$:

$h_\Gamma(0_{\{1\}}^{G_2}) = 0_{\{1\}}^{\mathcal{A}_\Gamma}$: this case is similar to the case $0_{\{1\}}^{\mathcal{T}}$ from the proof of Lemma 6.

$h_\Gamma(G_1 \|^{G_2} G_2) = h_\Gamma(G_1) \|^{\mathcal{A}_\Gamma} h_\Gamma(G_2)$, where $\sigma(G_1) = \sigma(G_2) = \{1\}$: this case is similar to the case of parallel composition from the proof of Lemma 6.

$h_\Gamma(b_{i,3-i}^{G_2}) = b_{i,3-i}^{\mathcal{A}_\Gamma}$: this case is similar to the case $b_{1,2}^{\mathcal{S}P}$ from the proof of Lemma 29.

$h_\Gamma(G_1 \triangleright G_2 G_2) = h_\Gamma(G_1) \triangleright^{\mathcal{A}_\Gamma} h_\Gamma(G_2)$: $\subseteq$ Since $G_1 \triangleright G_2 G_2$ is a graph of sort $\{1\}$, let $\{\mathcal{Y}\} \in h_\Gamma(G_1 \triangleright G_2 G_2)$ be a reduced view of $G_1 \triangleright G_2 G_2$. Because $G_1 \triangleright G_2 G_2$ is not a parallel composition of two or more graphs of sort $\{1\}$, any element of $h_\Gamma(G_1 \triangleright G_2 G_2)$ is a singleton multiset, for some nonterminal $Y \in \mathcal{Y}$. Then, by Definition 18 (1), there exists a complete derivation $Y \Rightarrow_{\Gamma}^* u$ such that $u^{G_2} = G_1 \triangleright G_2 G_2$. Without loss of generality, we can assume that this derivation has the form:

$$ Y \Rightarrow_{\Gamma} P \triangleright X \Rightarrow_{\Gamma}^* v_1 \triangleright X \Rightarrow_{\Gamma}^* v_1 \triangleright v_2 $$

for some ground $\mathcal{F}_2$-terms $v$ and $w$ such that $v_i^{G_2} = G_i$, for $i = 1, 2$. By a reordering of the steps, if necessary, we can consider that the derivation $P \Rightarrow_{\Gamma}^* v_1$ has the form:

$$ P \Rightarrow_{\Gamma}^{*} \|_{S \in \mathcal{S}} S^{\sharp m(S)} \Rightarrow_{\Gamma}^{*} \|_{S \in \mathcal{S}, i \in m(S)} w_1(S, i) $$

where $w_1(S, i)$ are ground $\mathcal{F}_2$-terms such that $G_1 = (\|_{S \in \mathcal{S}, i \in m(S)} w_1(S, i))^{G_2}$. Then $m$ is a view of $G_1$ such that $P \rightsquigarrow m$. We obtain $[m]_\Gamma \in h_\Gamma(G_1)$ and $P \rightsquigarrow [m]_\Gamma$, by Lemma 18. Similarly, by reordering the steps of the derivation $X \Rightarrow_{\Gamma}^* v_2$, we obtain a view $k$ of $G_2$ such that $X \rightsquigarrow k$, hence $[k]_\Gamma \in h_\Gamma(G_2)$ and $X \rightsquigarrow [k]_\Gamma$, by Lemma 18. We obtain $\{\mathcal{Y}\} \in h_\Gamma(G_1) \triangleright^{\mathcal{A}_\Gamma} h_\Gamma(G_2)$, by applying the inference rule ($\triangleright$) from Figure 7.

$\supseteq$ Let $\{\mathcal{Y}\} \in h_\Gamma(G_1) \triangleright^{\mathcal{A}_\Gamma} h_\Gamma(G_2)$ be a multiset. By the inference rule ($\triangleright$) from Figure 7, which defines $\triangleright^{\mathcal{A}_\Gamma}$, each element of $h_\Gamma(G_1) \triangleright^{\mathcal{A}_\Gamma} h_\Gamma(G_2)$ is a singleton multiset containing some nonterminal $Y \in \mathcal{Y}$. By the inference rule ($\triangleright$), there exists multisets $m \in h_\Gamma(G_1)$ and $k \in h_\Gamma(G_2)$ and a rule $Y \to P \triangleright X$ in $\Gamma$ such that $P \rightsquigarrow m$ and $X \rightsquigarrow k$. Then, we obtain complete derivations:

$$ P \Rightarrow_{\Gamma}^{*} \|_{S \in \mathcal{S}} S^{\sharp m(S)} \Rightarrow_{\Gamma}^{*} \|_{S \in \mathcal{S}, i \in m(S)} w_1(S, i) $$

$$ X \Rightarrow_{\Gamma}^{*} \|_{Y \in \mathcal{Y}} Y^{\sharp k(Y)} \Rightarrow_{\Gamma}^{*} \|_{Y \in \mathcal{Y}, i \in k(Y)} w_2(Y, i) $$

where $w_1(S, i)$ and $w_2(Y, i)$ are ground $\mathcal{F}_2$-terms such that $G_1 = (\|_{S \in \mathcal{S}, i \in m(S)} w_1(S, i))^{G_2}$ and $G_2 = (\|_{Y \in \mathcal{Y}, i \in k(Y)} w_2(Y, i))^{G_2}$. By composing these derivations with the rule $Y \to P \triangleright X$, we obtain a complete derivation $Y \Rightarrow_{\Gamma}^* u$ such
that $u^{G_2} = G_1 \triangleright^{G_2} G_2$. Since $G_1 \triangleright^{G_2} G_2 \in A_{\{1\}}$, we obtain $\{[Y]\} \in h_{\Gamma}(G_1 \triangleright^{G_2} G_2)$, by Definition 18 (1).

$h_{\Gamma}(G_1 \|^{G_2} G_2) = h_{\Gamma}(G_1) \|^{A_{\Gamma}} h_{\Gamma}(G_2)$, where $\sigma(G_1) = \sigma(G_2) = \{1, 2\}$: this case is similar to the case of parallel composition from the proof of Lemma 29.

$h_{\Gamma}(\sigma^{G_2}(G_1, G_2, H)) = \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$: Note that $G \stackrel{\text{def}}{=} \sigma^{G_2}(G_1, G_2, H)$ is an S-graph, hence $h_{\Gamma}(G)$ is an S-profile, whose elements are of the form $(S, Q, X)$ or $(S, \perp)$, where $S \in S$, $Q \in P \uplus S$ and $X \in \mathcal{X}$. In the following, we tackle the cases of elements of the form $(S, Q, X)$, the other cases being similar and left to the reader. Based on the types of $G_1$ and $G_2$, we distinguish the following cases:

- $G_1$ and $G_2$ are P-graphs: "$\subseteq$" Let $(S, Q, X) \in h_{\Gamma}(G)$ be a reduced view of $G$. By Definition 18 (3a), there exists a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u, Q, X)$, for some ground $\mathcal{F}_2$-term $u$ such that $G = u^{G_2}$. By Lemma 20, there exist derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$ and $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$, for some nonterminal $S_1 \in S$ and ground $\mathcal{F}_2$-terms $u_1, u_2$ and $w$ such that $u_i^{G_2} = G_i$, for $i = 1, 2$ and $w^{G_2} = H$. Then, by Lemma 19, and because $G_1$ and $G_2$ are P-graphs, there are rules $S \to \circ(P_1, S_1, X_1)$ and $S_1 \to \circ(P_2, Q, X)$, and complete derivations $P_i \stackrel{\sim}{\Rightarrow}_{\Gamma} u_i$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} w$, for some nonterminals $P_1, P_2$ and $X_1$. By reordering these derivations, if necessary, we obtain views $m_i$ of $G_i$ and $k$ of $H$ such that $P_i \stackrel{\sim}{\Rightarrow}_{\Gamma} m_i$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. By Lemma 18, we obtain $P_i \stackrel{\sim}{\Rightarrow}_{\Gamma} [m_i]_{\Gamma} \in h_{\Gamma}(G_i)$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} [k]_{\Gamma} \in h_{\Gamma}(H)$. Hence, we obtain $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$, by applying the inference rule $(\circ^1(P, P))$ from Figure 7. "$\supseteq$" Let $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$ be a triple. Since $h_{\Gamma}(G_1)$ and $h_{\Gamma}(G_2)$ are P-profiles, by the inference rule $(\circ^1(P, P))$ from Figure 7, we have rules $S \to \circ(P_1, S_1, X_1)$, $S' \to \circ(P_2, Q, X) \in \mathcal{R}$ and reduced views $m_i \in h_{\Gamma}(G_i)$ such that $P_i \stackrel{\sim}{\Rightarrow}_{\Gamma} m_i$, for $i = 1, 2$ and $k \in h_{\Gamma}(H)$ such that $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. Then, there exist views $m'_i$ of $G_i$, for $i = 1, 2$ and $k'$ of $H$. The existence of these views implies the existence of complete derivations $P_i \stackrel{\sim}{\Rightarrow}_{\Gamma} u_i$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} w$ such that $u_i^{G_2} = G_i$, for $i = 1, 2$ and $w^{G_2} = H$. Then, we obtain derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$ and $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$, hence there exists a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u, Q, X)$, for some ground $\mathcal{F}_2$-term $u$ such that $u^{G_2} = \sigma^{G_2}(G_1, G_2, H) = G$. Hence, $(S, Q, X) \in h_{\Gamma}(G)$, by Definition 18 (3a).

- $G_1$ is a P-graph and $G_2$ is an S-graph: "$\subseteq$" Let $(S, Q, X) \in h_{\Gamma}(G)$ be a reduced view of $G$. Similar to the previous case, we obtain derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$ and $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$, for some nonterminal $S_1 \in S$ and ground $\mathcal{F}_2$-terms $u_1, u_2$ and $w$ such that $u_i^{G_2} = G_i$, for $i = 1, 2$ and $w^{G_2} = H$. Then, by Lemma 19, and because $G_1$ is a P-graph, there is a rule $S \to \circ(P_1, S_1, X_1)$, and complete derivations $P_1 \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} u_1$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} w$, for some nonterminals $P_1$ and $X_1$. By reordering these derivations, if necessary, we obtain views $m_1$ of $G_1$ and $k$ of $H$ such that $P_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} m_1$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. By Lemma 18, we obtain $P_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} [m_1]_{\Gamma} \in h_{\Gamma}(G_1)$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} [k]_{\Gamma} \in h_{\Gamma}(H)$.

Moreover, since $G_2$ is an S-graph, we have $(S_1, Q, X) \in h_{\Gamma}(G_2)$, by Definition 18 (3a). Then, we obtain $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$, by applying the inference rule $(\circ^1(P, S))$ from Figure 7.

"$\supseteq$" Let $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$ be a triple. Since $h_{\Gamma}(G_1)$ is a P-profile and $h_{\Gamma}(G_2)$ is an S-profile, by the inference rule $(\circ^1(P, S))$ from Figure 7, we have a rule $S \to \circ(P, S_1, X_1) \in \mathcal{R}$ and reduced views $m_1 \in h_{\Gamma}(G_1)$, $(S_1, Q, X) \in h_{\Gamma}(G_2)$ and $k \in h_{\Gamma}(H)$, such that $P_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} m_1$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. Then, there exist views $m'_1$ of $G_1$ and $k'$ of $H$, from which we obtain complete derivations $P_1 \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} u_1$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} w$ such that $u_1^{G_2} = G_1$ and $w^{G_2} = H$. By combining these derivations with the rule $S \to \circ(P, S_1, X_1)$, we obtain a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w_1)$. Moreover, because $(S_1, Q, X)$ is a view of $G_2$, there exists a derivation $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$ such that $u_2^{G_2} = G_2$. By Lemma 20, we obtain a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u, Q, X)$ such that $u^{G_2} = G$, hence $(S, Q, X) \in h_{\Gamma}(G)$, by Definition 18 (3a).

- $G_1$ is an S-graph and $G_2$ is a P-graph: "$\supseteq$" Let $(S, Q, X) \in h_{\Gamma}(G)$ be a reduced view of $G$. Similar to the previous cases, we obtain derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$ and $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$, for some nonterminal $S_1 \in S$ and ground $\mathcal{F}_2$-terms $u_1, u_2$ and $w$ such that $u_i^{G_2} = G_i$, for $i = 1, 2$ and $w^{G_2} = H$. Because $G_1$ is an S-graph, we can assume w.l.o.g. that the derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$ is of the form:

$$S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, X_1) \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$$

for a complete derivation $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} w$ such that $w^{G_2} = H$. By a reordering of the steps of this derivation, if necessary, we obtain a view $k$ of $H$ such that $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. Moreover, by Lemma 18, we obtain $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} [k]_{\Gamma} \in h_{\Gamma}(H)$. Since $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, X_1)$, we have $(S, S_1, X_1) \in h_{\Gamma}(G_1)$, by Definition 18 (3a). Then, by Lemma 19, and because $G_2$ is a P-graph, there is a rule $S_1 \to \circ(P, Q, X)$, and a complete derivation $P \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} u_2$. By a reordering of the steps of this derivation, if necessary, we obtain a view $m$ of $G_2$ such that $P \stackrel{\sim}{\Rightarrow}_{\Gamma} m$. Moreover, by Lemma 18, we obtain $P \stackrel{\sim}{\Rightarrow}_{\Gamma} [m]_{\Gamma} \in h_{\Gamma}(G_2)$. Then, we obtain $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$, by applying the inference rule $(\circ^1(S, P))$ from Figure 7.

"$\supseteq$" Let $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$ be a triple. Since $h_{\Gamma}(G_1)$ is an S-profile and $h_{\Gamma}(G_2)$ is a P-profile, by the inference rule $(\circ^1(S, P))$ from Figure 7, we have a rule $S_1 \to \circ(P, Q, X) \in \mathcal{R}$ and reduced views $(S, S_1, X_1)$ of $G_1$, $m$ of $G_2$ and $k$ of $H$ such that $P \stackrel{\sim}{\Rightarrow}_{\Gamma} m$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. By Lemma 18, there exist views $m'$ of $G_2$ and $k'$ of $H$ such that $P \stackrel{\sim}{\Rightarrow}_{\Gamma} m$ and $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma} k$. Since $(S, S_1, X_1) \in h_{\Gamma}(G_1)$, by Definition 18 (3a), there exists a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, X_1)$ such that $u_1^{G_2} = G_1$. From the rule $S_1 \to \circ(P, Q, X)$ and the view $m'$ of $G_2$, we obtain a derivation $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$ such that $u_2^{G_2} = G_2$. From the view $k'$ of $H$ we obtain a derivation $X_1 \stackrel{\sim}{\Rightarrow}_{\Gamma}^{*} w$ such that $w^{G_2} = H$. By Lemma 20, there exists a derivation
$S \stackrel{a}{\rightharpoonup}_{\Gamma}^{*} \circ(u, Q, X)$ such that $u^{G_2} = \circ^{G_2}(G_1, G_2, H) = G$, hence $(S, Q, X) \in h_{\Gamma}(G)$, by Definition 18 (3a).

- $G_1$ and $G_2$ are S-graphs: "$\subseteq$" Let $(S, Q, X) \in h_{\Gamma}(G)$ be a reduced view of $G$. As in the previous case, there exist reduced views $(S, S_1, X_1) \in h_{\Gamma}(G_1)$ and $k \in h_{\Gamma}(H)$, such that $X_1 \rightsquigarrow \Gamma k$. Moreover, as in the previous case, we obtain a derivation $S_1 \stackrel{a}{\rightharpoonup}_{\Gamma}^{*} \circ(u, Q, X)$, for a ground $\mathcal{F}_2$-term $u$ such that $u^{G_2} = G_2$, hence $(S_1, Q, X) \in h_{\Gamma}(G_2)$, by Definition 18 (3a). Then, we obtain $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$, by applying the inference rule $(\circ^1(S, S))$ from Figure 7.

"$\supseteq$" Let $(S, Q, X) \in \circ^{A_{\Gamma}}(h_{\Gamma}(G_1), h_{\Gamma}(G_2), h_{\Gamma}(H))$ be a triple. Since both $h_{\Gamma}(G_1)$ and $h_{\Gamma}(G_2)$ are S-profiles, by the inference rule $(\circ^1(S, S))$ from Figure 7, we have reduced views $(S, S_1, X_1) \in h_{\Gamma}(G_1)$, $(S_1, Q, X) \in h_{\Gamma}(G_2)$ and $k \in h_{\Gamma}(H)$ such that $X_1 \rightsquigarrow \Gamma k$. By Lemma 18, there exists a view $k'$ of $H$ such that $X_1 \rightsquigarrow k'$ and a complete derivation $X_1 \stackrel{*}{\Rightarrow}_{\Gamma} w$ such that $w^{G_2} = H$. By Definition 18 (3a), we obtain derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, X_1)$ and $S_1 \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_2, Q, X)$ such that $u_1^{G_2} = G_1$, for $i = 1, 2$. By combining the derivations $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, X_1)$ and $X_1 \stackrel{*}{\Rightarrow}_{\Gamma} w$ we obtain $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u_1, S_1, w)$, hence a derivation $S \stackrel{a}{\Rightarrow}_{\Gamma}^{*} \circ(u, Q, X)$ such that $w^{G_2} = \circ^{G_2}(G_1, G_2, H) = G$, by Lemma 20. Then, $(S, Q, X) \in h_{\Gamma}(G)$, by Definition 18 (3a). □

**Theorem 6:** The language of each (aperiodic) regular tree-width 2 grammar $\Gamma$ is recognizable by an (aperiodic) recognizer $(A, B)$. Moreover, $\text{card}(A) \in 2^{2^{\text{poly}(\text{size}(\Gamma))}}$ and $f^A(a_1, \dots, a_{\#f})$ can be computed in time $2^{\text{poly}(\text{size}(\Gamma))}$, for each function symbol $f \in \mathcal{F}_{SP}$ and elements $a_1, \dots, a_n \in A$.

[Proof of Theorem 6] Let $\Gamma = (\mathcal{X} \oplus \mathcal{Y} \oplus \mathcal{P} \oplus \mathcal{S}, \mathcal{R})$ be a regular (aperiodic) tree-width 2 grammar. Using Lemma 1, we obtain a normalized (aperiodic) grammar $\Gamma' = (\mathcal{X} \oplus \mathcal{Y} \oplus \mathcal{P} \oplus \mathcal{S}, \mathcal{R}')$. We point out that $\Gamma$ and $\Gamma'$ have the same set of non-terminals. In particular, we have $\mathcal{L}^{G_2}(\Gamma') = \mathcal{L}^{G_2}(\Gamma)$ and $\text{size}(\Gamma') \in 2^{\text{poly}(\text{card}(\mathcal{X})+\text{card}(\mathcal{Y})+\text{card}(\mathcal{P})+\text{card}(\mathcal{S}))\cdot\log(\text{size}(\Gamma'))}$. We then consider the corresponding normalized regular grammar in alternative form $\hat{\Gamma}' = (\mathcal{X} \oplus \mathcal{Y} \oplus \mathcal{P} \oplus \hat{\mathcal{S}}, \hat{\mathcal{R}}')$. We recall that $\mathcal{L}^{G_2}(\hat{\Gamma}') = \mathcal{L}^{G_2}(\Gamma')$ and $\text{size}(\Gamma') = \Theta(\text{size}(\hat{\Gamma}'))$.

We build the recognizer $(A_{\hat{\Gamma}'}, B_{\hat{\Gamma}'})$ based on the grammar $\hat{\Gamma}'$. By Lemma 14, we obtain $\mathcal{L}^{G_2}(\hat{\Gamma}') = h_{\hat{\Gamma}'}^{-1}(B_{\hat{\Gamma}'})$, where $B_{\hat{\Gamma}'} \stackrel{\text{def}}{=} \{h_{\hat{\Gamma}'}(G) \mid G \in \mathcal{L}^{G_2}(\hat{\Gamma}')\}$. By Lemma 15, $(A_{\hat{\Gamma}'}, B_{\hat{\Gamma}'})$ is a recognizer for $\mathcal{L}^{G_2}(\hat{\Gamma}')$. Because of $\mathcal{L}^{G_2}(\hat{\Gamma}') = \mathcal{L}^{G_2}(\Gamma)$, $A_{\hat{\Gamma}'}$ is also a recognizer for the language of $\Gamma$ in $G_2$. Moreover, $A_{\hat{\Gamma}'}$ is aperiodic if $\hat{\Gamma}'$ is aperiodic, by the counterpart of Lemma 7 for $G_2$. We further recall that $\hat{\Gamma}'$ is aperiodic iff $\Gamma'$ is aperiodic. The complexity upper bounds follow in the same way as in the proof of Theorem 5. □

**Lemma 16:** Let $\mathcal{C}$ be a class. Each set $\mathcal{L} \subseteq \mathcal{P}_\mathcal{C}$ of parse trees is (aperiodic) recognizable in the parse tree algebra $\mathcal{P}_\mathcal{C}$ iff $\mathcal{L}$ is (aperiodic) recognizable in the tree algebra $\mathcal{T}(\mathcal{A}_\mathcal{C})$.

[Proof of Lemma 16] “$\Rightarrow$” Assume that $\mathcal{L} \subseteq \mathcal{P}_\mathcal{C}$ is (aperiodic) recognizable in $\mathcal{P}_\mathcal{C}$ and let $\mathcal{B} = (\{\mathcal{B}^\tau\}_{\tau \in \Sigma_\mathcal{C}}, \{f^\mathcal{B}\}_{f \in \mathcal{F}_\mathcal{C}})$ be a (aperiodic) locally finite $(\mathcal{F}_\mathcal{C}, \Sigma_\mathcal{C})$-algebra, such that $\mathcal{L} = h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}^{-1}(D)$, for some set $D \subseteq \mathcal{B}$. We define the locally finite

algebra $\overline{\mathcal{B}}$ having domain $\overline{\mathcal{B}}^{\{1\}} \stackrel{\text{def}}{=} \{(b, \tau) \mid b \in \mathcal{B}^{\tau}, \tau \in \Sigma_\mathcal{C}\} \cup \{\perp\}$ and a single sort $\{1\}$, that interprets each function symbol from $\mathcal{F}_{\mathcal{T}(\mathcal{A}_\mathcal{C})}$ as follows:

$$ \text{append}_{\overline{\mathcal{B}}}^{\overline{\mathcal{B}}}(\bar{b}_1, \dots, \bar{b}_{\#f}) \stackrel{\text{def}}{=} \left\{ \begin{array}{l} (f^{\overline{\mathcal{B}}}(b_1, \dots, b_{\#f}), \sigma(f)), \\ \text{if } \bar{b}_i = (b_i, \tau_i), \text{ for } i \in [1, \#f] \\ \text{and } \alpha(f) = \langle \tau_1, \dots, \tau_{\#f} \rangle \\ \perp, \text{ otherwise} \end{array} \right. \\ \\ (b_1, \tau_1) \parallel^{\overline{\mathcal{B}}} (b_2, \tau_2) \stackrel{\text{def}}{=} \left\{ \begin{array}{l} (b_1 \parallel^{\overline{\mathcal{B}}} b_2, \tau_1), \text{ if } \tau_1 = \tau_2 \\ \perp, \text{ otherwise} \end{array} \right. $$

We prove that $\mathcal{B}$ is aperiodic only if $\overline{\mathcal{B}}$ is aperiodic. Let $(b, \tau) \in \overline{\mathcal{B}}$ be an element. Then, $\text{idem}((b, \tau)) = (\text{idem}(b), \tau)$, by the definition of $\parallel^{\overline{\mathcal{B}}}$. By the aperiodicity of $\mathcal{B}$, we obtain $\text{idem}((b, \tau)) \parallel^{\overline{\mathcal{B}}} (b, \tau) = (\text{idem}(b) \parallel^{\overline{\mathcal{B}}} b, \tau) = (\text{idem}(b), \tau) = \text{idem}((b, \tau))$, thus $\overline{\mathcal{B}}$ is aperiodic, because the choice of $(b, \tau)$ was arbitrary. We define the set $\overline{\mathcal{D}} \stackrel{\text{def}}{=} \{(b, \tau) \mid b \in \mathcal{B}^{\tau} \cap D, \tau \in \Sigma_\mathcal{C}\}$ and the function $\overline{h} : \mathcal{T}(\mathcal{A}_\mathcal{C}) \to \overline{\mathcal{B}}$ as follows:

$$ \overline{h}(T) \stackrel{\text{def}}{=} (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T), \tau), \text{ for } T \in \mathcal{P}_\mathcal{C}^\tau $$

By the definition of $\overline{h}$ and $\overline{D}$, we have $h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T) \in D \iff \overline{h}(T) \in \overline{D}$, for each $T \in \mathcal{P}_\mathcal{C}$, hence $\mathcal{L} = h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}^{-1}(D) = \overline{h}^{-1}(\overline{D})$. We are left with proving that $\overline{h}$ a homomorphism between $\mathcal{T}(\mathcal{A}_\mathcal{C})$ and $\overline{\mathcal{B}}$, by showing the following points:

$$ \begin{align*} \overline{h}(\text{append}_{\overline{f}}^{\mathcal{T}(\mathcal{A}_\mathcal{C})}(T_1, \dots, T_{\#f})) &= \text{append}_{\overline{f}}^{\overline{\mathcal{B}}} (\overline{h}(T_1), \dots, \overline{h}(T_n)), \\ \text{for } f \in \mathcal{F}_\mathcal{C} \setminus \{\parallel_{\tau, \tau} | \tau \in \Sigma_\mathcal{C}\}: \text{ Assume that} \\ \alpha(f) &= \langle \sigma(T_1), \dots, \sigma(T_{\#f}) \rangle \text{ and } \tau = \sigma(f) = \\ \sigma(\text{append}_{\overline{f}}^{\mathcal{T}(\mathcal{A}_\mathcal{C})}(T_1, \dots, T_{\#f})). \text{ Using the definition of} \\ \text{append}_{\overline{f}}, \text{ we obtain:} \end{align*} $$

$$ \begin{align*} \overline{h}(\text{append}_{\overline{f}}^{\mathcal{T}(\mathcal{A}_\mathcal{C})}(T_1, \dots, T_{\#f})) \\ &= (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(\text{append}_{\overline{f}}^{\mathcal{T}(\mathcal{A}_\mathcal{C})}(T_1, \dots, T_{\#f})), \tau) \\ &= (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(f^{\mathcal{P}_\mathcal{C}}(T_1, \dots, T_{\#f})), \tau) \\ &= (f^{\mathcal{B}}(h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_1), \dots, h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_{\#f})), \tau) \\ &= \text{append}_{\overline{f}}^{\overline{\mathcal{B}}}((h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_1), \sigma(T_1)), \dots, (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_{\#f}), \sigma(f))) \\ &= \text{append}_{\overline{f}}^{\overline{\mathcal{B}}} (\overline{h}(T_1), \dots, \overline{h}(T_n)) \end{align*} $$

$$ \begin{align*} \overline{h}(T_1 \parallel^{\mathcal{T}(\mathcal{A}_\mathcal{C})} T_2) &= \overline{h}(T_1) \parallel^{\mathcal{T}(\mathcal{A}_\mathcal{C})} \overline{h}(T_1): \text{ Assume that we have} \\ \tau &\stackrel{\text{def}}{=} \sigma(T_1) = \sigma(T_2) \text{ for some } \tau \in \Sigma_\mathcal{C}. \text{ We compute, using the} \\ \text{definition of } \parallel^{\overline{\mathcal{B}}} \end{align*} $$

$$ \begin{align*} \overline{h}(T_1) \parallel^{\mathcal{T}(\mathcal{A}_\mathcal{C})} T_2) &= (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_1) \parallel^{\mathcal{T}(\mathcal{A}_\mathcal{C})} T_2), \tau) \\ &= (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_1) \parallel^{\mathcal{B}} h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_2), \tau) \\ &= (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_1), \tau) \parallel^{\overline{\mathcal{B}}} (h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}(T_2), \tau) \\ &= \overline{h}(T_1) \parallel^{\overline{\mathcal{B}}} \overline{h}(T_2) \end{align*} $$

“$\Leftarrow$” Assume that $\mathcal{L}$ is recognizable in $\mathcal{T}(\mathcal{A}_\mathcal{C})$ and let $\overline{\mathcal{B}} = (\mathcal{B}^{\{1\}}, \{\text{append}_{\overline{f}}^{\overline{\mathcal{B}}} f \}_{f \in \mathcal{F}_\mathcal{C}})$ be a locally-finite single-sorted algebra such that $\mathcal{L} = h_{\mathcal{P}_\mathcal{C}, \mathcal{B}}^{-1}(\overline{D})$, for some set $\overline{D} \subseteq \overline{\mathcal{B}}$. We de-
fine the domain $\mathbb{B}^\tau \stackrel{\text{def}}{=} \{(b, \tau) \mid b \in \bar{\mathbb{B}}\}$ of sort $\tau$, for each $\tau \in \Sigma_C$ and the $(\mathcal{F}_C, \Sigma_C)$-algebra $\mathcal{B} \stackrel{\text{def}}{=} (\{\mathbb{B}^\tau\}_{\tau \in \Sigma_C}, \{f^B\}_{f \in \mathcal{F}_C})$ such that, for each $f \in \mathcal{F}_C$:

$$ 
\begin{aligned}
f^B((b_1, \tau_1), \dots, (b_{\#f}, \tau_{\#f})) &\stackrel{\text{def}}{=} (\text{append}_{\bar{f}}^{\bar{\mathbb{B}}}(b_1, \dots, b_{\#f}), \sigma(f)), \\
\text{if } f \in \mathcal{F}_C \setminus \{\|_{\tau, \tau}| \tau \in \Sigma_C\}, \alpha(f) &= \langle \tau_1, \dots, \tau_{\#f} \rangle \\
(b_1, \tau) \|_{\tau, \tau}^{\mathcal{B}}(b_2, \tau) &\stackrel{\text{def}}{=} (b_1 \|^{\bar{\mathcal{B}}} \bar{b}_2, \tau), \text{ for all } \tau \in \Sigma_C
\end{aligned}
$$

We prove that $\bar{\mathbb{B}}$ is aperiodic only if $\mathcal{B}$ is aperiodic. Let $(b, \tau) \in \mathbb{B}$ be an element. Then, $\text{idem}((b, \tau)) = (\text{idem}(b), \tau)$, by the definition of $\|_{\tau, \tau}^{\mathcal{B}}$. By the aperiodicity of $\bar{\mathbb{B}}$, we obtain $\text{idem}((b, \tau)) \|_{\tau, \tau}^{\mathcal{B}}(b, \tau) = (\text{idem}(b) \|^{\bar{\mathcal{B}}} \bar{b}, \tau) = (\text{idem}(b), \tau) = \text{idem}((b, \tau))$.

We define the set $D \stackrel{\text{def}}{=} \{(b, \tau) \mid b \in \bar{D}, \tau \in \Sigma_C\}$ and the function $h: \mathcal{P}_C \to \mathbb{B}$ as $h(T) \stackrel{\text{def}}{=} (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T), \sigma(T))$. Then, we immediately obtain that $h(T) \in D \iff h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T) \in \bar{D}$, for each $T \in \mathcal{P}_C$, i.e., $\mathcal{L} = h_{\mathcal{T}(\hat{\mathcal{A}}_C), \bar{\mathbb{B}}}^{-1}(\bar{D}) = h^{-1}(D)$. We are left with proving that $h$ is a homomorphism between $\mathcal{P}_C$ and $\mathcal{B}$, by showing the following points:

$$ h(f^{\mathcal{P}_C}(T_1, \dots, T_{\#f})) = f^B(h(T_1), \dots, h(T_{\#f})), \text{ for } f \in \mathcal{F}_C \setminus \{\|_{\tau, \tau}| \tau \in \Sigma_C\}: \text{ Let } \tau \stackrel{\text{def}}{=} \sigma(h(f^{\mathcal{P}_C}(T_1, \dots, T_{\#f}))). \text{ We compute:} $$

$$ 
\begin{aligned}
& h(f^{\mathcal{P}_C}(T_1, \dots, T_{\#f})) \\
&= (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(f^{\mathcal{P}_C}(T_1, \dots, T_{\#f})), \tau) \\
&= (\text{append}_{\bar{f}}^{\bar{\mathbb{B}}}(h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_1), \dots, h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_{\#f}), \tau) \\
&= f^B((h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_1), \sigma(T_1)), \dots, (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_{\#f}), \sigma(f))) \\
&= f^B(h(T_1), \dots, h(T_{\#f}))
\end{aligned}
$$

$$ h(T_1 \|_{\tau, \tau}^{\mathcal{P}_C}, T_2) = h(T_1) \|_{\tau, \tau}^{\mathcal{B}} h(T_2): \text{ We denote } \sigma(T_1) = \frac{\sigma(T_2)}{\sigma(T_2) = \tau} \text{ and compute:} $$

$$ 
\begin{aligned}
h(T_1 \|_{\tau, \tau}^{\mathcal{P}_C}, T_2) &= (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_1 \|_{\tau, \tau}^{\mathcal{P}_C}, T_2), \tau) \\
&= (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_1) \|_{\tau, \tau}^{\bar{\mathcal{B}}}, h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_2), \tau) \\
&= (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_1), \tau) \|^{\mathcal{B}} (h_{\mathcal{T}(\hat{\mathcal{A}}_C)}, \bar{\mathbb{B}}(T_2), \tau) \\
&= h(T_1) \|^{\mathcal{B}} h(T_2)
\end{aligned}
\quad \square $$

**Proposition 1:** For every parse tree $T \in \mathcal{P}_C$ there is only one $\mathcal{F}_C$-term up to the associativity and commutativity of the operations $\|_{\tau, \tau}$, with $\tau \in \Sigma_C$, such that $T = t^{\mathcal{P}_C}$.

[Proof of Proposition 1] The proof is by induction on the size of $T$. Because every parse tree $T \in \mathbb{R}_C$ is representable, we have that $T = \|_{\tau, \tau}^{\mathcal{P}_C} f_i^{\mathcal{P}_C}(T_1^i, \dots, T_{\#f_i}^i)$ for some sort $\tau \in \Sigma_C$, function symbols $f_i \in \mathcal{F}_C \setminus \{\|_{\tau, \tau}| \tau \in \Sigma_C\}$ and parse trees $T_j^i$. We note that the choice of the function symbols $f_i$ is unique up to reordering because these are all the edges that are attached to the root of the parse tree. By the inductive hypothesis, we have that there are some terms $t_j^i$ such that $T_j^i = (t_j^i)^{\mathcal{P}_C}$, which are unique up to the associativity and commutativity of the operations $\|_{\tau, \tau}$. Hence, $t = \|_{\tau, \tau} f_i(T_1^i, \dots, T_{\#f_i}^i)$ is a term with $T = t^{\mathcal{P}_C}$ that is unique up to the associativity and commutativity of the operations $\|_{\tau, \tau}$. $\square$

**Proposition 2:** For each class $\mathcal{C}$, the function $\text{val}_\mathcal{C}$ is a parameterless definable transduction.

[Proof of Proposition 2] Let $k \ge 1$ be the minimum integer such that each sort that occurs in some function symbol from $\mathcal{F}_C$ is a subset of $[1, k+1]$. Since $\mathcal{F}_C$ is finite, such an integer exists. Let $h: \mathcal{P}_C \to \mathcal{P}_{\mathcal{G} \le k}$ be homomorphism that replaces each $\bar{f}$-labeled edge of a parse tree for $\mathcal{C}$ with the parse tree corresponding to the $\mathcal{F}_{\mathcal{G}}^{\le k}$-term $t_f$ that interprets the function symbol $f$ in $\mathcal{G}^{\le k}$. Since each such term is finite, the $h$ function is a definable transduction. By Theorem 9, $\text{val}_\mathcal{C} = h \circ \text{val}_{\mathcal{G} \le k}$ is a definable transduction, because $\text{val}_{\mathcal{G} \le k}$ is a definable transduction, by [2, Proposition 7.48]. $\square$

**Lemma 17:** Let $\mathcal{C}$ be a class and $\mathcal{L} \subseteq \mathcal{C}$ be a set of graphs. Then, $\mathcal{S} \stackrel{\text{def}}{=} \text{val}_{\mathcal{C}}^{-1}(\mathcal{L})$ is (aperiodic) recognizable in $\mathcal{P}_C$ if and only if $\mathcal{L}$ is (aperiodic) recognizable in $\mathcal{C}$.

[Proof of Lemma 17] “⇒” We assume that $\mathcal{S} = \text{val}_{\mathcal{C}}^{-1}(\mathcal{L})$ is recognizable and let $(\mathcal{I}, J)$ be a $(\mathcal{F}_C, \Sigma_C)$-recognizer such that $\mathcal{S} = h_{\mathcal{P}_C, \mathcal{I}}^{-1}(J)$. By Lemma 22, the algebra $\mathcal{P}_C \approx_S$ is locally finite and there exists a surjective homomorphism $g$ from $\mathcal{I}$ to $(\mathcal{P}_C)_{\approx_S}$ such that $h_{\approx_S} = g \circ h_{\mathcal{P}_C, \mathcal{I}}$. By Lemma 23, the algebras $(\mathcal{P}_C)_{\approx_S}$ and $\mathcal{C}_{\approx_L}$ are isomorphic, hence $\mathcal{C}_{\approx_L}$ is locally finite, thus $\mathcal{L}$ is recognizable in $\mathcal{C}$, witnessed by the homomorphism $h_{\approx_L}$. We assume now that $\mathcal{I}$ is an aperiodic algebra and prove that $(\mathcal{P}_C)_{\approx_S}$ is aperiodic. Provided that $(\mathcal{P}_C)_{\approx_S}$ is aperiodic, the aperiodicity of $\mathcal{C}_{\approx_L}$ follows from the isomorphism between $(\mathcal{P}_C)_{\approx_S}$ and $\mathcal{C}_{\approx_L}$. Let $a \in \mathcal{P}_C$. By the surjectivity of $g$, there exists $i \in \mathcal{I}$ such that $g(i) = [a]_{\approx_S}$ and let $\tau$ be the sort of $i$, which is also the sort of $[a]_{\approx_S}$. Hence, $g(\text{idem}(i)) = \text{idem}([a]_{\approx_S})$ and we compute: $\text{idem}([a]_{\approx_S}) \|_{\tau, \tau}^{(\mathcal{P}_C)_{\approx_S}} [a]_{\approx_S} = g(\text{idem}(i)) \|_{\tau, \tau}^{(\mathcal{P}_C)_{\approx_S}} g(i) = g(\text{idem}(i)) \|_{\tau, \tau}^{\mathcal{I}} i = g(\text{idem}(i)) = [a]_{\approx_S}$. Since the choice of $a \in \mathcal{P}_C$ was arbitrary, we obtain that $(\mathcal{P}_C)_{\approx_S}$ is aperiodic.

“⇒” We assume that $\mathcal{L}$ is recognizable and let $(\mathcal{I}, J)$ be a $(\mathcal{F}_C, \Sigma_C)$-recognizer such that $\mathcal{L} = h_{\mathcal{C}, \mathcal{I}}^{-1}(J)$. Using a similar argument as for the previous direction, we obtain that $\mathcal{C}_{\approx_L}$ is a locally finite algebra that, moreover, is aperiodic if $\mathcal{I}$ is aperiodic. Since $(\mathcal{P}_C)_{\approx_S}$ and $\mathcal{C}_{\approx_L}$ are isomorphic, by the argument from the previous direction, we obtain that $(\mathcal{P}_C)_{\approx_S}$ is locally finite and, moreover, aperiodic if $\mathcal{C}_{\approx_L}$ is aperiodic. Then, $\mathcal{S}$ is (aperiodic) recognizable, witnessed by $h_{\approx_S}$. $\square$

**Theorem 11:** The classes SP and DSP are parsable.

[Proof of Theorem 11] We first describe the parsing transduction $\pi_{SP}$ for the SP class. The parsing transduction for the DSP class will be the composition $\pi_{SP} \circ \delta_{rev}$ of a transduction $\delta_{rev}$ that reverses an arbitrarily chosen set of edges and $\pi_{SP}$. Note that the output of $\delta_{rev}$ is rejected by SP if it does not belong to SP.

We recall the following definitions from [3, Section 6]. Let $G \in \text{SP}$ be an (oriented) series-parallel graph and $x, y \in V_G$ be (not necessarily distinct) vertices of $G$.

1. $x \le y$ iff there exists an oriented path from $x$ to $y$ in $G$ and $x < y$ iff $x \le y$ and $x \ne y$.

2. for $x < y$, $G[x, y]$ is the subgraph of $G$ consisting of all vertices $x \le z \le y$ and all edges between them.
3. $\tilde{V}_G$ is the set of vertices of $G$ that are not on some path from $\xi_G(1)$ to $\xi_G(2)$. Note that every vertex from $V_G$ is on some path from $\xi_G(1)$ to $\xi_G(2)$, however the vertices from $\tilde{V}_G$ are avoided by at least one such path.

4. for each $x \in \tilde{V}_G$ and $y \in V_G$, we define left($x$) $\stackrel{\text{def}}{=} y$ (resp. right($x$) $\stackrel{\text{def}}{=} y$) iff the following hold:

(a) $y < x$ (resp. $x < y$).

(b) every path from $\xi_G(1)$ to $\xi_G(2)$ that crosses $x$ also crosses $y$.

(c) there is some path from $\xi_G(1)$ to $\xi_G(2)$ that crosses $y$ but not $x$.

(d) any vertex $y'$ that satisfies conditions (4a-4c) for $x$ is such that $y' \le y$ (resp. $y \le y'$).

5. $G[x] \stackrel{\text{def}}{=} G[\text{left}(x), \text{right}(x)]$, for each vertex $x \in \tilde{V}_G$. The existence and unicity of left($x$) and right($x$) is proved in [3, Lemma 6.6].

6. $G[e] \stackrel{\text{def}}{=} G[v_G(e, 1), v_G(e, 2)]$, for each edge $e \in E_G$.

7. $G_e$ is the graph consisting of the edge $e$ and vertices $v_G(e, 1)$ and $v_G(e, 2)$, for each edge $e \in E_G$. Note that $G[e]$ and $G_e$ are not the same, e.g., if $G = (b_{1,2} \parallel b_{1,2})^{\text{SP}}$. Moreover, each $G[e]$, resp. $G_e$, is a P-component of $G$.

We call a P-component of $G$ any $\circ$-atomic subgraph of $G$, i.e., either a single-edge graph or a parallel compositions of at least two other subgraphs. An S-component of $G$ is a subgraph $C$ of $G$ that is a serial composition of at least two other subgraphs of $G$ such that $C \circ^{\text{SP}} K$ or $K \circ^{\text{SP}} C$ are not subgraphs of $G$ for any other graph $K$. By the corrected<fnref n="12" /> statement of [3, Lemma 6.7], the set of P-components of some series-parallel subgraph of $G$ equals $\{G[x] \mid x \in E_G \cup \tilde{V}_G\} \cup \{G_e \mid e \in E_G\}$. Moreover, the functions left, right : $\tilde{V}_G \to V_G$ are definable using MSO.

To prove that the class $\text{SP}$ is parsable, we describe a definable transduction $\pi_{\text{SP}}$ that builds from each input graph $G$ (i.e., $G \in G$ is any graph, not just some series-parallel graph) a parse tree $T \in \text{P}_{\text{SP}}$ such that $\text{val}_{\text{SP}}(T) = G$. First, the input graph $G$ is rejected if $G \notin \text{SP}$. The latter condition can be checked by encoding the conditions of [3, Lemma 6.1] using MSO formulæ. The transduction uses a parameter $X$ that is assigned to a subset of $\tilde{V}_G \cup E_G$ having the following MSO-definable properties (we abuse notation and write $x \in X$ whenever $x$ belongs to the valuation of $X$):

- $G[x] \neq G[y]$, for all $x \neq y \in X$,

- for each $x \in \tilde{V}_G \cup E_G$ there exists $y \in X$ such that $G[x] = G[y]$.

The transduction $\pi_{\text{SP}}$ uses $k = 4$ layers. We denote by $(x, i)$ an element $x \in X$ taken from the layer $i$. The nodes of the output parse tree $T$ are the vertices $x \in X$ from the 1st layer. The edges of $T$ are elements from the 3rd and 4th layers, i.e., $(x, 3)$ for $x \in X$ represent ternary serial composition $\bar{\circ}$-edges, and $(x, 4)$ for $x \in X \cap E_G$ represent unary $\bar{b}_{1,2}$-labeled edges. The 2nd layer is used only for the additional vertices used by the edges that encode serial composition subterms.

<figure><img src="image_9.png" /><figcaption>Fig. 9. Chaining of $\bar{\circ}$ edges in the $\text{SP}$ parse tree of a graph $G[x_{j,1}] \parallel^{\text{SP}} (G[x_{i,1}] \circ^{\text{SP}} \dots \circ^{\text{SP}} G[x_{i,n_i}])$, for some $i \neq j$, where we assume that the graph $G[x_{j,1}]$ as well as all the graphs $G[x_{i,1}], \dots, G[x_{i,n_i}]$ consist of a single edge. The nodes of the parse tree are shown in red and the edges in black.</figcaption></figure>

The distinction between $G[e]$ and $G_e$, for some edge $e \in E_G$ is mirrored by the distinction between $(e, 1)$ (i.e., a node of $T$) and $(e, 4)$ (i.e., an edge of $T$). The parse tree $T$ of $G$ (i.e., the result of $\pi_{\text{SP}}(G)$ for the given valuation of $X$) is defined as follows:

- $V_T \stackrel{\text{def}}{=} \{(x, 1), (x, 2) \mid x \in X\}$,

- $E_T$ consists of either:

* ternary $\bar{\circ}$-labeled edges correspond to the P-components of $G$ that occur in some S-component. More specifically, for each $x \in X$, we have $G[x] = C_1 \parallel^{\text{SP}} \dots \parallel^{\text{SP}} C_m$, where $C_i = G[x_{i,1}] \circ^{\text{SP}} \dots \circ^{\text{SP}} G[x_{i,n_i}]$ and $x_{i,j} \in X$, for all $i \in [1, m]$ and $j \in [1, n_i]$. Then, for each $i \in [1, m]$ and $j \in [1, n_i]$, $T$ has a $\bar{\circ}$-labeled edge $(x_{i,j}, 3)$ attached to the following vertices (see Figure 9 for an illustration):

$$ 
\begin{align*}
v_T((x_{i,j}, 3), 1) &\stackrel{\text{def}}{=} \begin{cases} (x, 1), & \text{if } j = 1 \\ (x_{i,j-1}, 2), & \text{if } 2 \le j \le n_i - 1 \end{cases} \\
v_T((x_{i,j}, 3), k) &\stackrel{\text{def}}{=} (x_{i,j}, k-1), \quad \text{for } 1 \le j < n_i - 1, k = 2, 3 \\
v_T((x_{i,n_i-1}, 3), 2) &\stackrel{\text{def}}{=} (x_{i,n_i-1}, 1) \\
v_T((x_{i,n_i-1}, 3), 3) &\stackrel{\text{def}}{=} (x_{i,n_i}, 1)
\end{align*}
$$

Note that the relation “$G[x_{i,j}]$ is to the left of $G[x_{i,l}]$ in the S-component $C_i$”, for all $1 \le j < l \le n_i$, can be defined in MSO, thus the distinction between the two cases in the definition of $v_T((x_{i,j}, 3), 1)$ above is MSO-definable.

* unary $\bar{b}_{1,2}$-labeled edges $(x, 4)$, attached to a single vertex, for each $x \in X \cap E_G$. These edges correspond to the P-components of $G$ of the form $G_e$, for $e \in E_G$. The choice of the vertex $v_T((x, 4), 1)$ depends on the position of the single-edge graph $G_x$, namely:

(i) $G_x$ occurs alone or on the 1st position on some S-component of $G$, in which case $v_T((x, 4), 1) = (y, 1)$, where $y$ is the representative of the innermost enclosing P-component of that S-component,

(ii) $G_x$ occurs on some S-component, but not on the first or last position, in which case $v_T((x, 4), 1) = (x, 1)$,

(iii) $G_x$ occurs on the last position on some S-component, in which case $v_T((x, 4), 1) = (y, 2)$,

<footnote n="12">¹²The original statement of [3, Lemma 6.7] considers only $\{G[x] \mid x \in E_G \cup \tilde{V}_G\}$ and ignores $\{G_e \mid e \in E_G\}$.</footnote>