11institutetext: Technische Universtität Wien, Vienna, Austria
11email<EMAIL_ADDRESS>Université
Grenoble Alpes, Grenoble, France
22email<EMAIL_ADDRESS>
# Tree-Verifiable Graph Grammars

Mark Chimes 11 Radu Iosif 22 Florian Zuleger 11

###### Abstract

Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order
to extend the notion of context-free sets from words andtrees to graphs of
bounded tree-width. While for words and trees thesyntactic restrictions that
guarantee that the associated languages ofwords resp. trees are regular - and
hence, MSO-definable - are known,the situation is far more complicated for
graphs. Here, Courcelleproposed the notion of regular graph grammars, a
syntactic restrictionof HR grammars that guarantees the definability of the
associatedlanguages of graphs in Counting Monadic Second Order Logic
($\mathsf{CMSO}$).However, these grammars are not complete in the sense that
not every$\mathsf{CMSO}$-definable set of graphs of bounded tree-width can be
generatedby a regular graph grammar. In this paper, we introduce a
newsyntactic restriction of HR grammars, called tree-verifiable graphgrammars,
and a new notion of bounded tree-width, called embeddablebounded tree-width,
where the later restricts the trees of atree-decomposition to be a subgraph of
the analyzed graph. The mainproperty of tree-verifiable graph grammars is that
their associatedlanguages are $\mathsf{CMSO}$-definable and that the have
bounded embeddabletree-width. We show further that they strictly generalize
the regulargraph grammars of Courcelle. Finally, we establish a
completenessresult, showing that every language of graphs that is
$\mathsf{CMSO}$-definableand of bounded embeddable tree-width can be generated
by atree-verifiable graph grammar.

##  0.1 Introduction

The notion of _regular_ word and tree languages is one of the pillars of the
theory of formal languages because many equivalent representations of regular
languages are known.In particular, we have that Monadic Second Order Logic
(MSO) over words resp. trees defines exactly the class of regular word resp.
tree languages.On the other hand, regular word resp. tree languages are a
subset of the context-free word resp. tree languages, and regular word resp.
tree grammars can be seen as syntactic restrictions of context-free grammars
that ensure the regularity of the generated languages.Regular languages enjoy
many desirable properties, in particular, the following problems are known to
be decidable:  (1) _emptiness_ : is the language empty? (2) _membership_ :
does a given word resp. tree belong to the language?  (3) _inclusion_ : given
two languages, is the firstincluded in the second? Because of the importance
of regular languages and their decidability properties, it would be highly
desirable to lift the connection between regular grammars and MSO to graphs,
which are important for many branches of computing, such as e.g.,static
analysis [19], databases and knowledgerepresentation [1], concurrency[7] and
aspects of machinelearning, such as neural networks [20].In this paper, we
study graph languages that lie at the intersectionof  (i) HR-_context-free_
and (ii) $\mathsf{CMSO}$-_definable_ classes. The sets of graphs in this class
are,at the same time  (i) least solutions of a system of recursive equations
usingoperations that substitute a hyper-edge of a graph by another graph,and
(ii) models of a formula that uses (quantification over) variablesdenoting
combined sets of vertices and edges and relation symbols(from a fixed finite
signature) describing the incidence relation ofa graph. In particular,
$\mathsf{CMSO}$ is the extension of MSO with atomicpropositions that express
constraints on the cardinality of a set,modulo a constant. This intersection
class has nice algorithmic properties, becauseemptiness, membership and
inclusion are all decidable. In particular,the decidability of inclusion
follows from a celebrated theorem provedby Courcelle, stating that the
satisfiability of a $\mathsf{CMSO}$ formula isdecidable over graphs of bounded
tree-width, a parameter that,intuitively speaking, measures the difference
between a graph and atree encoding of that graph [5].We recall that the MSO-
definability of a word language defined by a context-free grammar is, in
general, undecidable [10].Hence, as for words and trees, we will put syntactic
restrictions on HR-grammars in order to ensure $\mathsf{CMSO}$-definability.An
important precursor of our work is the class of _regulargraph grammars_
introduced byCourcelle [6] as a graph counterpart to the left- or right-
recursive word grammars, which define regular, and, hence, MSO-definable [3]
word languages.Regular graph grammars are a subclass of HR-grammars.In order
to state some intuition on regular graph grammars, we first recall the HR-
grammars.We note that HR-grammars generalize context-free word and tree
grammars to graphs of bounded tree-width.HR-grammars describe the construction
of graphs, using zero ormore distinguished vertices, called _sources_ ,
labeled by numbers$1,\ldots,n$.A _substitution operation_ replaces a
_nonterminal edge_ attached to vertices $v_{1},\ldots,v_{n}$ in agraph $H$ by
a disjoint graph $K$ with sources $1,\ldots,n$, suchthat the $i$-th source of
$K$ is glued with $v_{i}$, for each$i=1,\ldots,n$ and this is the only
overlapping between the twographs.A _parallel composition_ is a special
substitution thatglues the $i$-th sources of two graphs, for
$i=1,\ldots,n$.The rules of a regular graph grammar use two disjoint sets
ofnonterminals, called _recursive_ and _non-recursive_. Intuitively, a
recursive nonterminal can becomposed in parallel with any number of
occurrences of the samenon-recursive terminal in a derivation, but a
substitution may only generate non-recursive terminals. The rules of a regular
graph grammar are defined by twosyntactic conditions:  (i) each two vertices
of a graph $H$ in a substitution operation areconnected by a path that crosses
only terminal edges and internal(i.e., non-source) vertices, except for
endpoints, and (ii) the parallel composition involves at most one
recursivenonterminal. The graphs generated by regular graph grammars have the
property thateach parse tree from the derivation of a graph lies embedded in
thestructure of the graph and can be extracted by an MSO-definablerelation
between the relational structures that representgraphs. Then, for each set of
graphs defined by the grammar thereexists an MSO formula that defines it. This
formula is obtainedfrom  (i) the MSO definition of the set of parse trees, the
existence ofwhich is guaranteed by the alternation between recursive andnon-
recursive nonterminals in the derivation, and (ii) the definition (i.e., tuple
of MSO formulæ) of therelation that extracts the parse tree from the graph. A
natural question that arises is whether each set of graphs that is both MSO-
definable and HR-context-free can be defined by a regular graph grammar.

### Our contributions

In this paper, we give this question a negative answer and suggest an
alternative class that lies at the intersection of $\mathsf{CMSO}$-definable
and HR-context-free classes, by introducing _tree-verifiable grammars_.We
demonstrate that tree-verifiable grammars strictly generalize the regular
graph grammars of Courcelle, and establish a characterization result:We show
that a language of graphs is $\mathsf{CMSO}$-definableand of bounded
embeddable tree-width, a notion we introduce below, if and only if this
language can be generated by a tree-verifiable graph grammar.The syntactic
condition that defines tree-verifiable grammars is that each rule maps a
nonterminal $u$ to agraph operation, which is either  (A) a substitution
described by a graph with asingle terminal hyper-edge attached to an internal
_root_ nodeand several _future roots_ that are distributed among
thenonterminal edges (in this case $u$ is anon-recursive nonterminal), (B) a
parallel composition of $u$ with severaloccurrences of the same non-recursive
nonterminal, or (C) a parallel composition of non-recursivenonterminals ($u$
is a recursive nonterminal in the(B) and (C) cases). We define the _embeddable
tree-width_ of a graph to be theminimal width of a tree decomposition whose
backbone is isomorphic tosome spanning tree of the graph. The embeddable tree-
width of a graphis, in general, greater than its tree-width, i.e., there are
graphsfor which the optimal tree decomposition is not isomorphic to aspanning
tree.We show that this stronger notion allows us to precisely capture that
class of graphs generated by tree-verifiable grammars:We establish that a
language of graphs is $\mathsf{CMSO}$-definableand of bounded embeddable tree-
width if and only if this language can be generated by a tree-verifiable graph
grammar.In the special case of trees (i.e., graphs obtained by restricting the
parallel composition to graphs with one root source) tree-verifiable grammars
define precisely the $\mathsf{CMSO}$-definable unranked sets of
trees.Moreover, if all the repetition counts from the rules(B) equal one,
tree-verifiable grammars are the same as the MSO-definable unranked sets of
trees.This settles positively another question relative to the definition of
associative-commutative (AC) tree grammars of Courcelle [6, Definition 3.7],
namely whether AC grammars define all the MSO-definable sets of unranked
trees.

### Related work

The intersection of the $\mathsf{CMSO}$-definable and HR-context-free sets
ofgraphs has been investigated in the seminal paper ofCourcelle [6] that
introduced regulargraph grammars [6, §5] and proves thatthe set of series-
parallel (i.e., graphs with sources $1$ and $2$ thatcan be either serialized
or composed in parallel) belongs to thisclass graphs [6, §6]. More
recently,Doumane refined this result by developping a language of
regularexpressions that describes the class of $\mathsf{CMSO}$-definable
graphs thatcan be built using at most twosources [8]. An interesting question
thatremains open, for the time being, is whether the sets of graphsdefined by
these regular expressions have bounded embeddabletree-width. It is known that
their optimal tree decompositions can beextracted from the structure of the
graphs in a canonical fashion, butthese canonical decompositions do not
correspond to spanning trees.Substructural logics [17] are first-order logics
extendedwith a non-idempotent _separating conjunction_ operator thatdecomposes
logical structures. A distinguished substructural logic isSeparation Logic
(SL) [12, 18], that isinterpreted over finite partial functions of fixed
arity, called _heaps_. With heaps one can model certain graphs of
boundeddegree, i.e., where the number of edges attached to a vertex is bounded
by a constant.Another model of composition, used in Graph Logic (GL)
ofCardelli et al [4] or the Separation Logic ofRelations [15], splits graphs
intosubgraphs with disjoint sets of edges. These logics are more generalthan
SL, because they describe classes of graphs of unboundeddegree (e.g., stars
and unranked sets of trees). Used in combinationwith recursive definitions,
the separating conjunction becomes apowerful means to describe shape-related
graph properties (lists,trees, stars, etc.).One of the first fragments of SL
with recursive definitionshaving a decidable entailment problem used an ad-hoc
translation intoequivalent MSO formulæ, together with a syntactic guarantee
oftree-width boundedness [11].In subsequent work, a decision procedure, not
based on MSO, for the entailment problem in this SL fragment was proposed and
implemented [14, 13] and the complexity of this entailment problem was
established [9, 16].The ideas used in the definition of the SL fragment
motivated the definition of tree-verifiable grammars in this paper.In
particular, considering substitutionoperations described by graphs with a
single edge that connects theroot to the future roots is similar to the
_connectivity_ condition from [11]. Moreover, distributingthe future roots
among the nonterminals guarantees that each futureroot will eventually become
the root of a subgraph, which correspondsto the _establishment_ conditionof
[11]. These conditions guarantee thatthe SL-defined heaps of [11] havebounded
embeddable tree-width.We note that the fragment of [11] is restricted to
degree-bounded heaps and that [11] did not attempt to achieve any completeness
resp. characterization result that corresponds to the proposed syntactic
restriction.

##  0.2 Preliminaries

The set of natural numbers is denoted by ${\rm Nature}$. Given $i,j\in{\rm
Nature}$,we write $[{i},{j}]$ for the set $\\{{i,i+1,\ldots,j}\\}$, assumedto
be empty if $i>j$. The cardinality of a finite set $A$ is denotedby
$\mathrm{card}({A})$. For a set $A$, we denote by $\mathrm{pow}({A})$ its
powerset,$A^{0}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\\{{\epsilon}\\}$,
$A^{i+1}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}A^{i}\times
A$, for all$i\geq 0$,
$A^{*}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\bigcup_{i\geq
0}A^{i}$ and
$A^{+}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\bigcup_{i\geq
1}A^{i}$, where $\times$ is the Cartesian product and$\varepsilon$ denotes the
empty sequence. Intuitively, $A^{*}$(resp. $A^{+}$) denotes the set of
possibly empty (resp. nonempty)sequences of elements from $A$. The length of a
sequence $\alpha\in A^{*}$ is denoted by $\mathrm{len}({\alpha})$ and its
$i$-th element by$\alpha_{i}$, for $i\in[{1},{\mathrm{len}({\alpha})}]$. For a
function $f:A\rightarrow B$, we denote its _domain_ by $\mathrm{dom}({f})=A$
and itsimage by
$\mathrm{img}({f})\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\\{{b\in
B\mid f(a)=b\text{ for some }a\in A}\\}$. The domain-restriction of a function
$f$ to a set $C$ isdenoted as
${f}\\!\\!\downharpoonleft_{\scriptscriptstyle{C}}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\\{{(a,f(a))\mid
a\in C}\\}$.

### Graphs

in this paper are multigraphs consisting of edges of arity one ormore. Let
$\mathbb{A}$ be a finite alphabet of edge labels, rangedover by $a$ and
equipped with arities ${\\#{a}}\geq 1$.

######  Definition 1.

A _concrete graph (c-graph) of type $n\geq 0$_ is a tuple
$G=\langle{V_{\scriptscriptstyle{G}},{E}_{\scriptscriptstyle{G}},\lambda_{\scriptscriptstyle{G}},\upsilon_{\scriptscriptstyle{G}},\xi_{\scriptscriptstyle{G}}}\rangle$,
where:

  * •

$V_{\scriptscriptstyle{G}}$ is a finite set of _vertices_ ,

  * •

${E}_{\scriptscriptstyle{G}}$ is a finite set of _edges_ , such
that$V_{\scriptscriptstyle{G}}\cap{E}_{\scriptscriptstyle{G}}=\emptyset$,

  * •

$\lambda_{\scriptscriptstyle{G}}:{E}_{\scriptscriptstyle{G}}\rightarrow\mathbb{A}$
is amapping that defines the labels of the edges,

  * •

$\upsilon_{\scriptscriptstyle{G}}:{E}_{\scriptscriptstyle{G}}\rightarrow
V_{\scriptscriptstyle{G}}^{+}$ is a mapping that associates each edge a
nonemptysequence of vertices attached to the edge, such
that${\\#{(\lambda_{\scriptscriptstyle{G}}(e))}}=\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(e)})$,
foreach $e\in{E}_{\scriptscriptstyle{G}}$,

  * •

$\xi_{\scriptscriptstyle{G}}:[{1},{n}]\rightarrow V_{\scriptscriptstyle{G}}$is
an injective mapping that designates $n$ distinct _sources_. The vertex
$\xi_{\scriptscriptstyle{G}}(i)$ is the _$i$ -th source_ of $G$.A vertex $v\in
V_{\scriptscriptstyle{G}}$ is _internal_ if
$v\not\in\mathrm{img}({\xi_{\scriptscriptstyle{G}}})$.By
$\mathsf{intern}({G})=V_{\scriptscriptstyle{G}}\setminus\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in[1,n]\\}$ we denote the internal nodes of $G$.For simplicity, we omit the
sources for graphs of type $0$.

We denote by ${\mathcal{G}^{\scriptscriptstyle{\mathbb{A}}}}{}$ the set of
c-graphs with edgelabels from $\mathbb{A}$.

For example, Fig. 1 (a,b) shows severalc-graphs with (numbered) sources
depicted in black and internalvertices in white. A _path_ from $v_{1}$ to
$v_{k+1}$ in a c-graph$G$ is a sequence of tuples:

$\langle{v_{1},i_{1},e_{1},v_{2},j_{1}}\rangle,\langle{v_{2},i_{2},e_{2},v_{3},j_{2}}\rangle,\ldots,\langle{v_{k},i_{k},e_{k},v_{k+1},j_{k}}\rangle$

where $v_{1},\ldots,v_{k+1}\in V_{\scriptscriptstyle{G}}$,
$e_{1},\ldots,e_{k}\in{E}_{\scriptscriptstyle{G}}$ and $v_{\ell}$ and
$v_{\ell+1}$ are the$i_{\ell}$-th and $j_{\ell}$-th vertices attached to
$e_{\ell}$,respectively, for all $\ell\in[{1},{k}]$.A set $C\subseteq
V_{\scriptscriptstyle{G}}$ is _connected_ in $G$iff for any $u,v\in C$ there
exists a path from $u$ to $v$ in $G$containing only vertices from $C$.Two
c-graphs are _disjoint_ iff their sets of vertices and edgesare disjoint,
respectively. Two c-graphs are _isomorphic_ iffthere exists a bijection
between their vertices and edges thatpreserves the edge labels, the sequences
of vertices attached to edgesand the sources. A _graph_ is the equivalence
class of a c-graphfor isomorphism. For any graph $G$ we denote by$\widehat{G}$
the graph of type $0$ that is obtained from$G$ by removing its sources. A
language $\mathcal{L}$ of graphs issome set of graphs. We say $\mathcal{L}$ is
of type $n$ if all graphs$G\in\mathcal{L}$ are of type $n$. By
$\widehat{\mathcal{L}}=\\{\widehat{G}\mid G\in\mathcal{L}\\}$ we denote
thelanguage of type $0$ that is obtained by removing the sources of thegraphs
of $\mathcal{L}$.

### Graph Operations and Grammars.

If $G$ is a c-graph, $e\in{E}_{\scriptscriptstyle{G}}$ is an edge such
that${\\#{\lambda_{\scriptscriptstyle{G}}}}(e)=m$ and $H$ is a c-graph of type
$m$disjoint from $G$, then the _substitution_ $G[e/H]$deletes the edge $e$
from $G$, adds $H$ to $G$ and joins the$i$-th vertex from
$\upsilon_{\scriptscriptstyle{G}}(e)$ with the $i$-th source of$H$, for all
$i\in[{1},{m}]$. The sources and type of$G[e/H]$ are the same as for $G$. Fig.
1 (a)shows an example of substitution, formally defined below:

$3$$b$$2$$1$$\longrightarrow$$c$$b$$b$$a$$a$$c$$b$$1$$2$$1$$2$(a)$e$$H$$(G,e)$$G[e/H]$$a$$b$$2$$3$$1$$\longrightarrow$$\parallel_{3}$$a$$c$$b$$a$$b$$2$$3$$c$$b$$a$$2$$3$$1$$1$(b)

Figure 1: Graph operations: substitution (a) parallel composition (b)

######  Definition 2 (Substitution).

Let $G$ be a c-graph of type $n$, $e\in{E}_{\scriptscriptstyle{G}}$ is anedge
such that
$\upsilon_{\scriptscriptstyle{G}}(e)=\langle{v_{1},\ldots,v_{m}}\rangle$and
$H$ is a c-graph of type $m$ disjoint from $G$. Let$\sim\
\subseteq(V_{\scriptscriptstyle{G}}\cup V_{\scriptscriptstyle{H}})^{2}$ be the
leastequivalence relation such that $v_{i}\sim\xi_{\scriptscriptstyle{H}}(i)$
for all$i\in[1,m]$. We denote by $[u]_{\sim}$ the $\sim$-equivalence classof
$u\in V_{\scriptscriptstyle{G}}\cup V_{\scriptscriptstyle{H}}$. Then
$G^{\prime}=G[e/H]$ is defined by setting:

  * •

$V_{\scriptscriptstyle{G^{\prime}}}=\\{[u]_{\sim}\mid u\in
V_{\scriptscriptstyle{G}}\cup V_{\scriptscriptstyle{H}}\\}$,

  * •

${E}_{\scriptscriptstyle{G^{\prime}}}={E}_{\scriptscriptstyle{G}}\setminus\\{e\\}\cup{E}_{\scriptscriptstyle{H}}$,

  * •

$\lambda_{\scriptscriptstyle{G^{\prime}}}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}{(\lambda_{\scriptscriptstyle{G}})}\\!\\!\downharpoonleft_{\scriptscriptstyle{({E}_{\scriptscriptstyle{G}}\setminus\\{{e}\\})}}\cup~{}\lambda_{\scriptscriptstyle{H}}$,

  * •

$\upsilon_{\scriptscriptstyle{G^{\prime}}}(e^{\prime})\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\langle{[u_{1}]_{\sim},\ldots,[u_{k}]_{\sim}}\rangle$,
for all $e^{\prime}\in{E}_{\scriptscriptstyle{G}}\setminus\\{e\\}$with
$\upsilon_{\scriptscriptstyle{G}}(e^{\prime})=\langle{u_{1},\ldots,u_{k}}\rangle$,resp.
all $e^{\prime}\in{E}_{\scriptscriptstyle{H}}$ with
$\upsilon_{\scriptscriptstyle{H}}(e^{\prime})=\langle{u_{1},\ldots,u_{k}}\rangle$,

  * •

$\xi_{\scriptscriptstyle{G^{\prime}}}(i)\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}[\xi_{\scriptscriptstyle{G}}(i)]_{\sim}$,
for all $i\in[{1},{n}]$.

The substitution $G[e/H]$ is lifted from c-graphs to graphs(one can always
chose c-graphs that are isomorphic to $G$ and $H$ and are disjoint).Then, the
graph $G[e/H]$ is defined as the isomorphism class of the c-graph thatresults
from the substitution involving these c-graphs.

The graph operation $(G,e_{1},\ldots,e_{k})$, where
$e_{1},\ldots,e_{k}\in{E}_{\scriptscriptstyle{G}}$ are pairwise distinct
edges, takes pairwisedistinct c-graphs $H_{1},\ldots,H_{k}$ of
types${\\#{\lambda_{\scriptscriptstyle{G}}(e_{1})}},\ldots,{\\#{\lambda_{\scriptscriptstyle{G}}(e_{k})}}$,respectively,
and returns the c-graph $G[e_{1}/H_{1},\ldots,e_{k}/H_{k}]$, where the
substitutions can be done in any order. Againthis operation can be lifted from
concrete graphs to graphs.We now introduce an important special case of a
graph operation:The _parallel composition_ $\parallel_{n}$ denotes the
operation$(G,e_{1},e_{2})$, where $G$ has exactly $n$ vertices, all ofwhich
are sources, and $e_{1}$ and $e_{2}$ are the only edges of $G$,both of arity
$n$ and attached to all $n$ sources.Intuitively, $G_{1}\parallel_{n}G_{2}$
denotes the graphs that can be obtained from two graphs $G_{1}$ and$G_{2}$ of
type $n$ by merging their sources. Fig. 1(b) shows an example of parallel
composition. Note that thecomposition operation $\parallel_{n}$ is both
commutative andassociative.

(c)$2$$3$$a$(a)$1$(1)(2)(3)(3)(2)(1)$u$$u$$u\rightarrow$(b)$a$$1$$3$$u\rightarrow$$2$

Figure 2: Graph Grammar for Trees with Linked Leaves

A _graph grammar_ is a pair $\Gamma=(\mathcal{U},\mathcal{R})$,
where$\mathcal{U}$ is a set of _nonterminals_ distinct from
$\mathbb{A}$,ranged over $u,v,w$ with associated arities ${\\#{u}}\geq 1$,
and$\mathcal{R}$ is a finite set of rules of one of the following forms,
with$u,v,w\in\mathcal{U}$:

  1. 1.

$u\rightarrow v_{1}\parallel_{n}\ldots\parallel_{n}v_{k}$,
where$u,v_{1},\ldots,v_{k}\in\mathcal{U}$ are nonterminals of arity $n$,

  2. 2.

$u\rightarrow{G}[{e_{1}}({v_{1}}),\ldots,{e_{k}}({v_{k}})]$,
where$u,v_{1},\ldots,v_{k}\in\mathcal{U}$ are nonterminals
and${G}[{e_{1}}({v_{1}}),\ldots,{e_{k}}({v_{k}})]$ denotes the graph
operation$(G,e_{1},\ldots,e_{k})$, for some c-graph $G$ of type${\\#{u}}$,
such that
$\mathrm{img}({\lambda_{\scriptscriptstyle{G}}})\subseteq\mathbb{A}\cup\\{{v_{1},\ldots,v_{k}}\\}$
and $\lambda_{\scriptscriptstyle{G}}(e)=v_{i}\iff e=e_{i}$, for all
$e\in{E}_{\scriptscriptstyle{G}}$; if
$\lambda_{\scriptscriptstyle{G}}(e)\in\mathcal{U}$ (resp.
$\lambda_{\scriptscriptstyle{G}}(e)\in\mathbb{A}$), we say that $e$is a
nonterminal (resp. terminal) edge of $G$,

  3. 3.

$\rightarrow u$, for some nonterminal $u\in\mathcal{U}$, iscalled an _axiom_.

We note that in rules of shape 1., we explicitly allow $k=0$.With this we
denote the rule $u\rightarrow\overline{\mathbf{1}}_{n}$, where
$\overline{\mathbf{1}}_{n}$ denotes the graph of type $n$ that consists of $n$
vertices (all of which are sources), and that has no edges.The nonterminal on
the left-hand side of $\rightarrow$ in a non-axiomrule is called the _head_ of
that rule. The _language of $\Gamma$ associated with nonterminal $u$_ is the
set$\mathcal{L}_{\Gamma}({u})$ of graphs corresponding to $u$ in the
uniqueleast solution111By Tarski’s fixpoint theorem, since the graphoperations
are monotonic (w.r.t. to inclusion of sets) andcontinuous (w.r.t. infinite
unions of sets), the system of recursiveequations defined by the grammar has a
unique least solution. ofthe system of recursive equations defined by the
grammar rules, withnonterminals interpreted as sets, operations lifted to sets
and$\rightarrow$ interpreted as the right-to-left set inclusion$\supseteq$.
Note that each $\mathcal{L}_{\Gamma}({u})$ is a language oftype ${\\#{u}}$.
The _language of $\Gamma$_, denoted by$\mathcal{L}({\Gamma})$, is the union of
the sets$\widehat{\mathcal{L}_{\Gamma}({u})}$ for all axioms $\rightarrow u$
of$\Gamma$. Note that $\mathcal{L}({\Gamma})$ is a language of type $0$. Aset
$\mathcal{L}$ of graphs is _hyperedge-replacement_ (HR)
iff$\mathcal{L}=\mathcal{L}({\Gamma})$ for some graph grammar $\Gamma$.

######  Example 1.

Fig. 2 shows a graph grammar with a single nonterminal$u$, of arity $3$, and
two rules. The first rule (a) is of the form
$u\rightarrow{G}[{e_{1}}({u}),{e_{2}}({u})]$, where $G$ is ac-graph with a
(grey-filled) terminal edge labeled by $a$, where${\\#{a}}=3$, and two
nonterminal (unfilled) edges $e_{1}$ and $e_{2}$,both labeled by $u$. The
order of the vertices attached to theseedges is (1) middle, (2) left and (3)
right. The second rule (b) is ofthe form $u\rightarrow G$, where $G$ consists
of a singleterminal edge labeled by $a$. The language of this grammar consists
ofall graphs of the form depicted in Fig. 2 (c).

### Monadic Second Order Logic with Counting

($\mathsf{CMSO}$) is the set of formulæ written in the syntax fromFig. 3 (a)
using a set $\mathcal{V}=\\{{x,y,\ldots}\\}$ of _first-order variables_ , a
set $\mathcal{X}=\\{{X,Y,\ldots}\\}$ of _second-order variables_ and relation
symbols $\mathsf{edg}_{a}$ ofarity ${\\#{a}}+1$, for all $a\in\mathbb{A}$. By
MSO we denotethe subset of $\mathsf{CMSO}$ formulæ consisting of formulæ that
do notcontain atomic subformulæ of the form $\mathsf{card}_{{q},{p}}({X})$,
alsocalled _cardinality constraints_. A variable is _free_ ifit occurs outside
the scope of any quantifier. The set of freevariables of a formula $\psi$ is
denoted by $\mathrm{fv}({\psi})$. A _sentence_ is a formula without free
variables.

$\psi:=x=y\mid\mathsf{edg}_{a}(x_{1},\ldots,x_{{\\#{a}}+1})\mid\mathsf{card}_{{q},{p}}({X})\mid
X(x)\mid\neg\psi\mid\psi\wedge\psi\mid\exists x~{}.~{}\psi\mid\exists
X~{}.~{}\psi$

(a) $\mathsf{CMSO}$ Syntax

$\begin{array}[]{rclcl}G&\models^{\mathfrak{s}}&x=y&\iff&\mathfrak{s}(x)=\mathfrak{s}(y)\\\
G&\models^{\mathfrak{s}}&\mathsf{edg}_{a}(x_{1},\ldots,x_{{\\#{a}}+1})&\iff&\mathfrak{s}(x_{1})\in{E}_{\scriptscriptstyle{G}},~{}\lambda_{\scriptscriptstyle{G}}(\mathfrak{s}(x_{1}))=a\text{
and
}\upsilon_{\scriptscriptstyle{G}}(\mathfrak{s}(x_{1}))=\langle{\mathfrak{s}(x_{2}),\ldots,\mathfrak{s}(x_{{\\#{a}}+1})}\rangle\\\
G&\models^{\mathfrak{s}}&\mathsf{card}_{{q},{p}}({X})&\iff&\mathrm{card}({\mathfrak{s}(X)})=kq+p\text{
for some }k\in{\rm Nature}\\\
G&\models^{\mathfrak{s}}&X(x)&\iff&\mathfrak{s}(x)\in\mathfrak{s}(X)\\\
G&\models^{\mathfrak{s}}&\neg\phi&\iff&G\not\models^{\mathfrak{s}}\phi\\\
G&\models^{\mathfrak{s}}&\phi_{1}\land\phi_{2}&\iff&G\models^{\mathfrak{s}}\phi_{1}\text{
and }G\models^{\mathfrak{s}}\phi_{2}\\\ G&\models^{\mathfrak{s}}&\exists
x~{}.~{}\psi&\iff&G\models^{\mathfrak{s}[x\leftarrow u]}\psi\text{, for an
element }u\in V_{\scriptscriptstyle{G}}\cup{E}_{\scriptscriptstyle{G}}\\\
G&\models^{\mathfrak{s}}&\exists
X~{}.~{}\psi&\iff&G\models^{\mathfrak{s}[X\leftarrow U]}\psi\text{, for a set
}U\subseteq
V_{\scriptscriptstyle{G}}\cup{E}_{\scriptscriptstyle{G}}\end{array}$

(b) $\mathsf{CMSO}$ Semantics

Figure 3: Monadic Second Order Logic with Counting ($\mathsf{CMSO}$)

We define the semantics of $\mathsf{CMSO}$, for graphs of type $0$, by
asatisfaction relation $G\models^{\mathfrak{s}}\psi$ between graphs
andformulæ, where the valuation
$\mathfrak{s}:\mathcal{V}\cup\mathcal{X}\rightarrow
V_{\scriptscriptstyle{G}}\cup{E}_{\scriptscriptstyle{G}}\cup\mathrm{pow}({V_{\scriptscriptstyle{G}}\cup{E}_{\scriptscriptstyle{G}}})$
maps each variable $x\in\mathcal{V}$ to a vertex or and edge,
i.e.,$\mathfrak{s}(x)\in
V_{\scriptscriptstyle{G}}\cup{E}_{\scriptscriptstyle{G}}$, and each variable
$X\in\mathcal{X}$ to a finite subset of vertices and edges,
i.e.,$\mathfrak{s}(X)\subseteq
V_{\scriptscriptstyle{G}}\cup{E}_{\scriptscriptstyle{G}}$. Thesatisfaction
relation is defined inductively on the structure offormulæ in Fig. 3 (b).If
$\psi$ is a sentence, the satisfaction relation does not depend on the
variablemapping and we write $G\models\psi$ instead of
$G\models^{\mathfrak{s}}\psi$.A language $\mathcal{L}$ of graphs of type $0$
is _$\mathsf{CMSO}$ -definable_ iff there exists a $\mathsf{CMSO}$ sentence
$\psi$ suchthat ${\mathcal{G}}=\\{{G\mid G\models\psi}\\}$.We define the
formula$e\in{E}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigvee_{a\in\mathbb{A}}\exists
x_{1},\ldots,x_{{\\#{a}}}.\ \mathsf{edg}_{a}(e,x_{1},\ldots,x_{{\\#{a}}})$,
which denotes that $e$ is an edge, and the formula $v\in
V\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigvee_{a\in\mathbb{A}}\exists
e,x_{1},\ldots,x_{{\\#{a}}}.\
\mathsf{edg}_{a}(e,x_{1},\ldots,x_{{\\#{a}}})\wedge\bigvee_{1\leq
i\leq{\\#{a}}}x_{i}=v$, which denotes that $v$ is a vertex.As usual we define
$\phi\rightarrow\psi\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\neg\phi\lor\psi$
and
$\phi\leftrightarrow\psi\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\phi\rightarrow\psi\wedge\psi\rightarrow\phi$.For
$\Delta={E},V$, we further define $\forall
x\in\Delta~{}.~{}\psi(x)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
x~{}.~{}x\in\Delta\rightarrow\psi(x)$, $\exists
x\in\Delta~{}.~{}\psi(x)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
x~{}.~{}x\in\Delta\wedge\psi(x)$,
$\exists!x\in\Delta~{}.~{}\psi(x)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
x\in\Delta~{}.~{}\psi(x)\wedge\forall y\in\Delta~{}.~{}\psi(y)\rightarrow
y=x$, and $\exists
X\subseteq\Delta~{}.~{}\psi\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
X~{}.~{}\left(\forall x~{}.~{}X(x)\rightarrow x\in\Delta\right)\wedge\psi$.

### Recognizable Sets of Graphs.

A congruence relation on graphs is an equivalence relation $\cong$ suchthat
(1) any two equivalent graphs are of the same type, and (2) for every graph
$H$, for every edge $e$ of $H$, for every graph$G$ of type
${\\#{(\lambda_{\scriptscriptstyle{H}}(e))}}$, and every $G^{\prime}\cong G$,
one has $H[e/G]\cong H[e/G^{\prime}]$. Such a congruence is called _locally-
finite_ iff it has finitelymany equivalence classes of each type (by the
definition ofcongruences, each equivalence class consists of graphs of the
sametype). A set of graphs $\mathcal{L}$ is _recognizable_ iff thereexists a
locally-finite congruence $\cong$ such that $G\cong G^{\prime}$ only if
$G\in\mathcal{L}$ iff $G^{\prime}\in\mathcal{L}$.

### Trees.

We introduce trees as a subset of the set of graphs of type 1, whoseonly
source denotes the root. We consider the following restrictedgraph operations.
Let $\overline{\mathbf{1}}$ be the graph that consists of asingleton vertex,
which is also its only source, and that has no edges.For an edge label
$a\in\mathbb{A}$ and $1\leq i\leq{\\#{a}}$denote by
$\overline{\mathbf{a}}^{i}$ the
operation$(G,e_{1},\ldots,e_{i-1},e_{i+1},\ldots,e_{{\\#{a}}})$, where$G$ is a
c-graph that consists of a singleton edge $e$ labelledby $a$ attached to
pairwise distinct vertices$v_{1},\ldots,v_{{\\#{a}}}$, such that
$\xi_{\scriptscriptstyle{G}}(1)=v_{i}$ andthe other vertices
$v_{1},\ldots,v_{i-1},v_{i+1},\ldots,v_{{\\#{a}}}$ are attached to distinct
edges $e_{1},\ldots,e_{i-1},e_{i+1},\ldots,e_{{\\#{a}}}$ labeled with unary
symbols,respectively.
Intuitively,$\overline{\mathbf{a}}^{i}(G_{1},\ldots,G_{i-1},G_{i+1},\ldots,G_{{\\#{a}}})$
is obtained by taking the disjoint unionof the graphs
$G_{1},\ldots,G_{i-1},G_{i+1},\ldots,G_{{\\#{a}}}$ and adding a new edge
labelled by $a$with sequence of vertices
$(\xi_{\scriptscriptstyle{G_{1}}}(1),\ldots,\xi_{\scriptscriptstyle{G_{i-1}}}(1),v,\xi_{\scriptscriptstyle{G_{i+1}}}(1),\ldots,\xi_{\scriptscriptstyle{G_{{\\#{a}}}}}(1))$,
where $v$ is a new vertex thatbecomes the only source of the resulting graph.
This operation isdepicted in Fig. 4 (a). The parallel compositionoperation for
trees is $\parallel_{1}$, depicted in Fig. 4(b).The set of trees over
$\mathbb{A}$ is defined as the least set closedunder the operations
$\overline{\mathbf{1}}$, $\parallel_{1}$ and $\overline{\mathbf{a}}^{i}$,for
all $a\in\mathbb{A}$ and $1\leq i\leq{\\#{a}}$. We retrievethe standard
terminology for trees from this definition. The verticesof a tree $T$ are
called _nodes_. For an edge $e\in{E}_{\scriptscriptstyle{T}}$ introduced by an
operation $\overline{\mathbf{a}}^{i}$, we say
that$\upsilon_{\scriptscriptstyle{T}}(i)$ is the _parent_ of
$\upsilon_{\scriptscriptstyle{T}}(1),\ldots,\upsilon_{\scriptscriptstyle{T}}(i-1),\upsilon_{\scriptscriptstyle{T}}(i+1),\ldots,\upsilon_{\scriptscriptstyle{T}}({\\#{a}})$
and the latter nodes are the _children_ of the former. Note that the trees we
consider in thispaper are _unordered_ , i.e., the relative order of the
edgesattached to a node is not important, and _unranked_ , i.e., thereis no
bound on the number of children of a node.

$G_{1}$$G_{{\\#{a}}}$$G_{i-1}$$G_{i+1}$$G_{1}$$G_{{\\#{a}}}$$G_{i-1}$$G_{i+1}$$1$$a$$e_{1}$$e_{i-1}$$e_{{\\#{a}}}$$e_{i+1}$$1$$1$$\parallel_{1}$$\longrightarrow$$1$(b)(a)$\longrightarrow$$1$$a$$1$$1$$1$$\overline{\mathbf{a}}^{i}$

Figure 4: Tree operations: substitution (a) parallel composition (b)

##  0.3 Tree Grammars

This section is concerned with unranked trees, whose nodes may have unbounded
numbers ofchildren, the order of which is not important.We are interested in
HR sets of trees, generated by _tree grammars_ , which are graph grammars,
whose rules use only tree operations.In general, HR sets of trees are not
$\mathsf{CMSO}$-definable.For instance, the grammar with rules
$u\rightarrow\overline{\mathbf{a}}^{1}\parallel_{1}\overline{\mathbf{b}}^{1}\parallel_{1}u$
and $u\rightarrow\overline{\mathbf{1}}$, where $a$ and $b$ are binary edge
labels, defines theset of trees of height one, whose root has the same number
of $a$\- and$b$-labeled edges. Since $\mathsf{CMSO}$ cannot describe sets of
equalcardinality (see, e.g., [5, Proposition3.9]), this set is not
$\mathsf{CMSO}$-definable.This motivates the quest for trees grammars defined
by easy-to-checksyntactic restrictions, that guarantee the
$\mathsf{CMSO}$-definability of theirlanguages. The following definition
introduces such a class of treegrammars. In the rest of this section, we prove
that the languages ofthe grammars that conform with the following definition
coincide withthe $\mathsf{CMSO}$-definable tree languages.

######  Definition 3.

A tree grammar $\Gamma=(\mathcal{U},\mathcal{R})$ is _regular_ iffthere exists
a set $\mathcal{W}\subseteq\mathcal{U}$ of nonterminalssuch that the rules in
$\mathcal{R}$ are of one of the following forms,either:

  1. A.

$w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})$, for some
$a\in\mathbb{A}$ and $1\leq i\leq{\\#{a}}$, where $w\in\mathcal{W}$and
$u_{1},\ldots,u_{{\\#{a}}-1}\in\mathcal{U}$,

  2. B.

$u\rightarrow u\parallel_{1}w^{q}$, for some $q\in{\rm Nature}$, where
$u\in\mathcal{U}\setminus\mathcal{W}$ and $w\in\mathcal{W}$,

  3. C.

$u\rightarrow w_{1}\parallel_{1}\cdots\parallel_{1}w_{k}$, where
$u\in\mathcal{U}\setminus\mathcal{W}$ and
$w_{1},\ldots,w_{k}\in\mathcal{W}$;this rule becomes
$u\rightarrow\overline{\mathbf{1}}$, in case $k=0$.

We further require that the axioms are of the form $\rightarrow u$,for some
$u\in\mathcal{U}\setminus\mathcal{W}$.

We call a set $\mathcal{L}$ of trees _regular_ iff there is a regulartree-
grammar $\Gamma$ and such that $\mathcal{L}=\mathcal{L}({\Gamma})$. Theshape
of regular tree-grammars as given inDefinition 3 is inspired by the AC-
treegrammars introduced byCourcelle [6, Section 3]. However,Courcelle’s
definition of AC-grammars considers $q=1$ in allrules of the form rules B
inDefinition 3. In this section, we showthat the languages of these grammars
coincide with the MSO-definabletree languages. Hence, the AC-grammars are not
complete wrt$\mathsf{CMSO}$-definablility, because there are tree languages
that are$\mathsf{CMSO}$-definable but not MSO-definable, see e.g., [5,
Corollary6.6].First, we prove that the $\mathsf{CMSO}$-definable tree-
languages are exactlythe regular tree languages. For this we will make use of
the followinglemma:Given a regular tree-grammar
$\Gamma=(\mathcal{U},\mathcal{R})$ with aset $\mathcal{W}$ as in Definition
3,we can build a regular tree-grammar
$\Gamma^{\prime}=(\mathcal{U}^{\prime},\mathcal{R}^{\prime})$ with
$\mathcal{L}({\Gamma})=\mathcal{L}({\Gamma^{\prime}})$, suchthat, for each
pair of non-terminals $u\in\mathcal{U}\setminus\mathcal{W}$ and
$w\in\mathcal{W}$, there is atmost one rule $u\rightarrow u\parallel_{1}w^{q}$
of shapeB in $\mathcal{R}^{\prime}$ .Let $u$ and $w$ be fixed nonterminals,
with $u\in\mathcal{U}\setminus\mathcal{W}$ and $w\in\mathcal{W}$ and
$u\rightarrow u\parallel_{1}w^{q_{1}}$, $\ldots$, $u\rightarrow
u\parallel_{1}w^{q_{k}}$ be the set of rules of shape B of$\mathcal{R}$, for
the given nonterminals. Let $d\geq 1$ be the gcd of theintegers
$q_{1},\ldots,q_{k}\geq 1$. By Schur’s theorem, there existsa computable
integer $n\geq 1$ such that for each integer $x\geq n$there exist
$x_{1},\ldots,x_{k}\in{\rm Nature}$ such that
$dx=q_{1}x_{1}+\ldots+q_{k}x_{k}$. We further observe that the set
$M\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\\{{q_{1}x_{1}+\ldots+q_{k}x_{k}\mid
x_{1},\ldots,x_{k}\in{\rm Nature}}\\}\cap[{1},{dn-1}]$ iscomputable. Let
$u^{\prime},u^{\prime\prime}$ be fresh nonterminals, not in $\mathcal{U}$.
Wedefine
$\mathcal{U}^{\prime}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\mathcal{U}\cup\\{{u^{\prime},u^{\prime\prime}}\\}$.We
now obtain the set of rules $\mathcal{R}^{\prime}$ from $\mathcal{R}$ as
follows:For every rule
$w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})$ with some
$u_{j}=u$ we replace this rule by two copies, one where we replace $u_{j}$
with $u^{\prime}$ and one where we replace $u_{j}$ with $u^{\prime\prime}$.We
keep all the rules
$w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})$ with
$u_{j}\neq u$ for all $j$.We remove the rules $u\rightarrow
u\parallel_{1}w^{q_{1}},\ldots,u\rightarrow u\parallel_{1}w^{q_{k}}$ and add
the rule $u^{\prime\prime}\rightarrow
u^{\prime\prime}\parallel_{1}w^{q}$.Further, we replace every rule
$u\rightarrow w_{1}\parallel_{1}\cdots\parallel_{1}w_{k}$ with the rules
$u^{\prime}\rightarrow
w_{1}\parallel_{1}\cdots\parallel_{1}w_{k}\parallel_{1}w^{m}$ for all $m\in M$
and the rule $u^{\prime\prime}\rightarrow
w_{1}\parallel_{1}\cdots\parallel_{1}w_{k}\parallel_{1}w^{dn}$.Then
$\Gamma^{\prime}=(\mathcal{U}^{\prime},\mathcal{R}^{\prime})$ is a regular
tree grammar, forthe set $\mathcal{W}\subseteq\mathcal{U}^{\prime}$,
where$u^{\prime},u^{\prime\prime}\not\in\mathcal{W}$. Moreover, it is
immediate to show that eachderivation of $\Gamma$ can be simulated by a
derivation of$\Gamma^{\prime}$ with the same outcome, and vice-versa.As we can
iteratively perform the above transformation for every pair ofnon-terminals
$u\in\mathcal{U}\setminus\mathcal{W}$ and $w\in\mathcal{W}$, the claim
follows.The first direction of the equivalence between regular
and$\mathsf{CMSO}$-definable tree languages is given by the following
theorem:Let $\mathcal{L}$ be a regular tree language. Then, $\mathcal{L}$
is$\mathsf{CMSO}$-definable.Let $\Gamma=(\mathcal{U},\mathcal{R})$ be a
regular tree grammar suchthat $\mathcal{L}({\Gamma})=\mathcal{L}$. Let
$\mathcal{W}\subseteq\mathcal{U}$ be the set that partitions $\mathcal{U}$ as
required by thedefinition of a regular tree-grammar. By Lemma 0.3,we can
assume that for each pair of non-terminals $u,w\in\mathcal{U}$, there is at
most one rule $u\rightarrow u\parallel_{1}w^{q}$ of shape B in $\mathcal{R}$.
We now build a$\mathsf{CMSO}$-sentence $\phi$ such that $\mathcal{L}=\\{{G\mid
G\models\phi}\\}$.Let $\mathcal{A},\mathcal{B},\mathcal{C}$ be the set of
rules of theform shape A,B, C in$\mathcal{R}$, respectively, where by
$n_{\mathcal{A}}=\mathrm{card}({\mathcal{A}})$and
$n_{\mathcal{C}}=\mathrm{card}({\mathcal{C}})$ we denote the number of rulesof
the respective form. For each of the rules $A\in\mathcal{A},C\in\mathcal{C}$
we will use a set variable $\underline{A},\underline{C}$. Further, we will use
a first-order variable $r$for the root of the tree. Below we state a formula
$\psi$ with freevariables $r$ and
$\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}$
such that $G\models^{\mathfrak{s}}\psi$ implies that $G$ is a tree with
root$r$ whose edges can be partitioned into the
sets$\underline{A}_{1}\ldots\underline{A}_{n_{A}}$ and whose vertices can
bepartitioned into sets $\underline{C}_{1}\ldots\underline{C}_{n_{C}}$
suchthat the rules denoted by these sets together with some applicationsof
rules $B\in\mathcal{B}$ constitute a derivation of $G$(note that this
derivation does not necessarily need to start withan axiom). Then, we define
the formula:

$\phi\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
r,\underline{A}_{1},\ldots,\underline{A}_{n_{A}},\underline{C}_{1},\ldots,\underline{C}_{n_{C}}.\left(\psi\wedge\bigvee_{C\in\mathcal{C},C\text{
has head }u,\text{ axiom }\rightarrow u\in\Gamma}\underline{C}(r)\right).$

As we will require that every edge is labelled by somerule $A\in\mathcal{A}$
of shape $w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})$,
we will call $i$ the _root position_ of this rule, and say that a vertex $v$
is _at the root position_ of some edge $\epsilon$, if we
have$\underline{A}(\epsilon)$ for some
$A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}$
and$\mathsf{edg}_{a}(\epsilon,v_{1},\ldots,v_{i-1},v,v_{i+1},\ldots,v_{{\\#{a}}})$for
some vertices$v_{1},\ldots,v_{i-1},v_{i+1},\ldots,v_{{\\#{a}}}$.The formula
$\psi$ is the conjunction of the sentencesbelow:

  * •

$\phi_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigvee_{A\in\mathcal{A}}\underline{A}(e)\land\bigwedge_{A_{1}\neq
A_{2}\in\mathcal{A}}\neg(\underline{A}_{1}(e)\land\underline{A}_{2}(e))$.
Thisformula states that every edge of the tree is labelled by exactlyone rule
of shape A.

  * •

$\phi_{2}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in V.\bigvee_{C\in\mathcal{C}}\underline{C}(v)\land\bigwedge_{C_{1}\neq
C_{2}\in\mathcal{C}}\neg(\underline{C}_{1}(v)\land\underline{C}_{2}(v))$.
Thisformula states that every vertex of the tree is labelled by exactlyone
rule of shape C.

  * •

$\phi_{3}$ is the conjunction of the formulae $\phi_{3a}$,$\phi_{3b}$,
$\phi_{3c}$, and $\phi_{3d}$, and states that the graphis a tree with root
$r$, where:

    * –

$\phi_{3a}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigwedge_{a\in\mathbb{A}}\forall
e\in{E}.\forall x_{1}\ldots x_{{\\#{a}}}\in V.\
\mathsf{edg}_{a}(e,x_{1},\ldots,x_{{\\#{a}}})\rightarrow\bigwedge_{1\leq
i<j\leq{\\#{a}}}x_{i}\neq x_{j}$ states thatfor every edge the vertices
incident to that edge are pairwisedifferent.

    * –

The formula

$\phi_{3b}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\\\
\bigwedge_{A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}}\left(\underline{A}(e)\rightarrow\forall
x_{1}\ldots x_{{\\#{a}}}\in
V.\mathsf{edg}_{a}(e,x_{1},\ldots,x_{{\\#{a}}})\rightarrow\bigwedge_{1\leq
t\leq{\\#{a}},t\neq i}x_{t}\neq r\right)$

states that the root $r$ is only incident to some edge $\epsilon$, if $r$ isat
the root position of $\epsilon$.

    * –

The formula

$\phi_{3c}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in V.v\neq r\rightarrow\exists!e\in{E}.\\\
\bigvee_{A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}}\left(\underline{A}(e)\land\exists
x_{1}\ldots x_{{\\#{a}}}\in
V.\mathsf{edg}_{a}(e,x_{1},\ldots,x_{{\\#{a}}})\land\bigvee_{1\leq
t\leq{\\#{a}},t\neq i}x_{t}=v\right)$

states that for every vertex $v\neq r$ there is exactly one edge $\epsilon$
such that $v$ is incident to $\epsilon$ and $v$ is not at the root position of
$\epsilon$.

    * –

$\phi_{3d}$ states that every vertex in the graph is reachablefrom the root
(as this formula is standard we omit it forbrevity).

  * •

$\phi_{4}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}\;.\;\bigwedge_{A\in\mathcal{A}}\left(\underline{A}(e)\rightarrow\psi^{A}_{4}(e)\right)$
states that every edge $\epsilon$ labelled by some
rule$A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{i-1},u_{i+1},\ldots,u_{{\\#{a}}})\in\mathcal{A}$
needs to satisfy the formula

$\psi^{A}_{4}(e)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in V\;.\;\bigwedge_{1\leq t\leq{\\#{a}},t\neq
i}\left(\mathsf{at}_{t}(e,v)\rightarrow\bigvee_{C\in\mathcal{A},\ C\text{ has
head }u_{t}}\underline{C}(v)\right),$

which states that the vertices attached to $\epsilon$ that arenot at position
$i$ are labelled by some rule whose headagrees with the required non-terminal,
where the auxiliaryformula $\mathsf{at}_{t}(e,v)$ denotes that $v$ is at the
$t$-thposition of edge $\epsilon$, i.e.,

$\mathsf{at}_{t}(e,v)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigvee_{a\in\mathbb{A}}\exists
x_{1},\ldots,x_{t-1},x_{t+1},\ldots,x_{{\\#{a}}}\in
V.\mathsf{edg}_{a}(e,x_{1}\ldots x_{t-1},\;v,\;x_{t+1},\ldots,x_{{\\#{a}}}).$

  * •

$\phi_{5}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in
V.\bigwedge_{C\in\mathcal{C}}\underline{C}(v)\rightarrow\left(\bigwedge_{w\in\mathcal{W}}\psi^{C}_{w}(v)\right)$
statesthat each vertex labelled by some rule $C=u\rightarrow
w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}\in\mathcal{C}$satisfies the formula
$\psi^{C}_{w}$ for every $w\in\mathcal{W}$. This formula is obtained as
follows: Let usconsider some $w\in\mathcal{W}$. Let $p$ be the number oftimes
$w$ appears among the $w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}$. Let $q$ be
the number such that thereis a rule $u\rightarrow
u\parallel_{1}w^{q}\in\mathcal{B}$(we recall that there is at most one rule of
this shape), andlet $q=0$, otherwise. We now define the formula

$\psi^{C}_{w}(v)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
X\subseteq{E}\;.\;\mathsf{card}_{{q},{p}}({X})\wedge\forall e\;.\;e\in
X\leftrightarrow\bigvee_{A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}}\left(\underline{A}(e)\wedge\mathsf{at}_{i}(e,v)\right),$

which states that there are exactly $kq+p$ edges $\epsilon$,for some $k\in{\rm
Nature}$, such that $v$ is the root of$\epsilon$, i.e., such that $\epsilon$
is labelled by somerule
$w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}$
and $v$ is incident to $\epsilon$ at position $i$.

  * •

$\phi_{6}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigwedge_{A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}}\underline{A}(e)\rightarrow\exists
x_{1}\ldots x_{{\\#{a}}}\in V.\ \mathsf{edg}_{a}(e,x_{1},\ldots x_{{\\#{a}}})$
states that if edge $\epsilon$ is labelled by somerule
$A=w\rightarrow\overline{\mathbf{a}}^{i}(u_{1},\ldots,u_{{\\#{a}}-1})\in\mathcal{A}$,
then$\epsilon$ is labelled $a$.

We now prove that $\mathcal{L}=\\{{G\mid G\models\phi}\\}$.We begin by proving
$\mathcal{L}\subseteq\\{{G\mid G\models\phi}\\}$.For this it is sufficient to
prove for every $u\in\mathcal{U}\setminus\mathcal{W}$ that
$G\in\mathcal{L}_{\Gamma}({u})$implies $G\models\phi(u)$, where we introduce
the
formula$\phi(u)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
r,\underline{A}_{1},\ldots,\underline{A}_{n_{A}},\underline{C}_{1},\ldots,\underline{C}_{n_{C}}.\left(\psi\wedge\bigvee_{C\in\mathcal{C},C\text{
has head }u}\underline{C}(r)\right)$. We proceed by induction on the heightof
the tree $G$.We consider some $G\in\mathcal{L}_{\Gamma}({u})$ for some
$u\in\mathcal{U}\setminus\mathcal{W}$. Then, the derivation of $G$starts with
zero or more applications of rules $B\in\mathcal{B}$of form $u\rightarrow
u\parallel_{1}w^{q}$. At some point thereis an application of a rule
$C\in\mathcal{C}$ of form $u\rightarrow
w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}$.Then,indexing by $m$, for each
non-terminal $w_{m}$, the derivation continueswith an application of some rule
$A\in\mathcal{A}$ of form
$w_{m}\rightarrow\overline{\mathbf{a_{m}}}^{i_{m}}(u^{m}_{1},\ldots,u^{m}_{i_{m}-1},u^{m}_{i_{m}+1},\ldots
u^{m}_{n_{m}})$. Let us now assume that for each $u^{m}_{j}$ wehave derived a
tree $G^{m}_{j}\in\mathcal{L}_{\Gamma}({u^{m}_{j}})$. Then,we obtain

$\displaystyle
G=\overline{\mathbf{a_{1}}}^{i_{1}}(G^{1}_{1},\ldots,G^{1}_{i_{1}-1},G^{1}_{i_{1}+1},\ldots
G^{1}_{n_{1}})\parallel_{1}\cdots\parallel_{1}\overline{\mathbf{a_{m}}}^{i_{m}}(G^{m}_{1},\ldots,G^{m}_{i_{m}-1},G^{m}_{i_{m}+1},\ldots
G^{m}_{n_{m}})\parallel_{1}\cdots$
$\displaystyle\qquad\qquad\parallel_{1}\overline{\mathbf{a_{k}}}^{i_{k}}(G^{k}_{1},\ldots,G^{k}_{i_{k}-1},G^{k}_{i_{k}+1},\ldots
G^{k}_{n_{k}}).$

Let $e_{m}$ be the edge of $G$ that is generated by the operation
$\overline{\mathbf{a_{m}}}^{i_{m}}(G^{m}_{1},\ldots,G^{m}_{i_{m}-1},G^{m}_{i_{m}+1},\ldots
G^{m}_{n_{m}})$, i.e., the edge that connects the roots of the graphs
$G^{m}_{j}$.We now note that each of the subtrees $G^{m}_{j}$ is of smaller
height than $G$.Hence, we can apply the induction assumption and obtain that
$G^{m}_{j}\models\phi(u^{m}_{j})$.In particular, each of the $\phi(u^{m}_{j})$
begins with the quantifier prefix$\exists
r^{m,j},\underline{A}_{1}^{m,j},\ldots,\underline{A}_{n_{A}}^{m,j},\underline{C}_{1}^{m,j},\ldots,\underline{C}_{n_{C}}^{m,j}$,meaning
that we can choose valuations for these variables that witness the
satisfaction of the formula $\psi$.We will below use these valuations in order
to assign values to
$r,\underline{A}_{1},\ldots,\underline{A}_{n_{A}},\underline{C}_{1},\ldots,\underline{C}_{n_{C}}$
and argue these values witness$G\models\phi(u)$.Let $r$ be the root of $G$.For
each edge $e_{m}$, let $A^{m}\in\mathcal{A}$ be the rule that was used to
derive this edge.Further, let $C\in\mathcal{C}$ be the rule that was used in
the beginning of the derivation of $G$ (after some applications of rules
$B\in\mathcal{B}$).We now set
$\underline{A}_{t}=\bigcup_{m,j}\underline{A}^{m,j}_{t}\cup\bigcup_{m}\\{e_{m}\mid
A^{m}=A_{t}\\}$ for all $1\leq t\leq n_{A}$,
$\underline{C}_{t}=\bigcup_{m,j}\underline{C}^{m,j}_{t}$ for all $1\leq t\leq
n_{C}$ with $C_{t}\neq C$, and
$\underline{C}_{t}=\bigcup_{m,j}\underline{C}^{m,j}_{t}\cup\\{r\\}$,
otherwise.We now verify that $G\models\phi(u)$:

  * •

$\phi_{1}$:Each edge $e$ is either part of some subgraph$G^{m}_{j}$, or is
equal to some edge $e_{m}$.The way we defined the sets $\underline{A}_{t}$
still partitions all the edges in $G$.

  * •

$\phi_{2}$: Each vertex is either part of some subgraph or equals the root
$r$.The way we defined the sets $\underline{C}_{t}$ above still partitions all
the vertices in $G$.

  * •

$\phi_{3}$: Since $\Gamma$ is a tree grammar, $G$ is a tree.

  * •

$\phi_{4}$: Clearly, this property holds for all edges of $G^{m}_{j}$.We have
that the root $r^{m}_{j}$ of every $G^{m}_{j}$ is labeled by some rule with
head $u^{m}_{j}$.Hence, the property holds for all edges $e_{m}$.

  * •

$\phi_{5}$: Clearly, this property holds for all vertices of$G^{m}_{j}$. We
now consider the root $r$. We recall thatthe root is labelled by some rule
$C=u\rightarrow w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}\in\mathcal{C}$. Let
$w\in\mathcal{U}\setminus\mathcal{W}$ be some non-terminal. Let $p$ bethe
number of times $w$ appears among the
$w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}$. Let $q$ be the number such that
there is arule $u\rightarrow u\parallel_{1}w^{q}\in\mathcal{B}$ (we recallthat
there is at most one rule of this shape), and let $q=0$,otherwise. It is now
easy to verify that there are at least $p$edges, which are labelled by rules
with head $w$, and the number ofthese edges equals $p$ modulo $q$. As this
holds for every $w\in\mathcal{U}\setminus\mathcal{W}$, the property holds for
the root$r$.

  * •

$\phi_{6}$: Clearly, this property holds for all edges of $G^{m}_{j}$.The
property further holds for the edges $e_{m}$.

We now prove that $\mathcal{L}\supseteq\\{{G\mid G\models\phi}\\}$.For this it
is sufficient to prove that $G\models\phi(u)$ implies that
$G\in\mathcal{L}_{\Gamma}({u})$ for all
$u\in\mathcal{U}\setminus\mathcal{W}$.We now consider some graph
$G\models\phi(u)$ for some non-terminal
$u\in\mathcal{U}\setminus\mathcal{W}$.We note that $G\models\phi(u)$ implies
that $G$ is a tree.This allows us to proceed by induction on the height of the
tree.Let $r$ be the root of $G$, and let $e_{1},\ldots,e_{k}$ be the edges to
which $r$ is incident.Let
$A^{m}=w^{m}\rightarrow\overline{\mathbf{a_{m}}}^{i_{m}}(u_{1}^{m},\ldots,u_{{\\#{a}}-1}^{m})\in\mathcal{A}$
be the rule such that $\underline{A}^{m}(e_{m})$ and let
$\upsilon_{\scriptscriptstyle{G}}(e_{m})=r^{m}_{1}\ldots r^{m}_{n_{m}}$ be the
incident vertices, for $1\leq m\leq k$.We note that $G\models\phi(u)$ implies
that $r=r^{m}_{i^{m}}$ and $a_{m}=\lambda_{\scriptscriptstyle{G}}(e_{m})$ for
all $1\leq m\leq k$.For each vertex $r^{m}_{j}\neq r$, define $G^{m}_{j}$ as
the subtree starting with root $r^{m}_{j}$ (note that such a subtree can be
defined because there is exactly one edge, namely $e_{m}$, to which
$r^{m}_{j}$ is incident and where $r^{m}_{j}$ is not at the root position of
this edge).Thus, we have

$\displaystyle
G=\overline{\mathbf{a_{1}}}^{i_{1}}(G^{1}_{1},\ldots,G^{1}_{i_{1}-1},G^{1}_{i_{1}+1},\ldots
G^{1}_{n_{1}})\parallel_{1}\cdots\parallel_{1}\overline{\mathbf{a_{m}}}^{i_{m}}(G^{m}_{1},\ldots,G^{m}_{i_{m}-1},G^{m}_{i_{m}+1},\ldots
G^{m}_{n_{m}})\parallel_{1}\cdots$
$\displaystyle\qquad\qquad\parallel_{1}\overline{\mathbf{a_{k}}}^{i_{k}}(G^{k}_{1},\ldots,G^{k}_{i_{k}-1},G^{k}_{i_{k}+1},\ldots
G^{k}_{n_{k}})\quad(*).$

Because of $G\models\phi(u)$, there are sets
$\underline{A}_{1},\ldots,\underline{A}_{n_{A}},\underline{C}_{1},\ldots,\underline{C}_{n_{C}}$
thatwitness the satisfaction of $\psi$. We now choose the
sets$\underline{A}_{1}^{m,j},\ldots,\underline{A}_{n_{A}}^{m,j},\underline{C}_{1}^{m,j},\ldots,\underline{C}_{n_{C}}^{m,j}$
as the restrictionof the above sets to the vertices and edges of graph
$G^{m}_{j}$. Itis now routine to verify that
$G^{m}_{j}\models\phi(u^{m}_{j})$.Hence, we can apply the induction assumption
and obtain that$G^{m}_{j}\in\mathcal{L}_{\Gamma}({u^{m}_{j}})$. Let
$C=u\rightarrow w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}\in\mathcal{C}$
bethe rule such that $\underline{C}(r)$.Let
$w\in\mathcal{U}\setminus\mathcal{W}$ be some non-terminal. Let $p$ be the
number of times $w$appears among the
$w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}$. Let$q$ be the number such that
there is a rule $u\rightarrow u\parallel_{1}w^{q}\in\mathcal{B}$ (we recall
that there is at mostone rule of this shape), and let $q=0$, otherwise.
Because of$G\models\phi(u)$ there are at least $p$ edges among
the$e_{1},\ldots,e_{k}$, which are labelled by rules with head $w$, and
thenumber of these edges equals $p$ modulo $q$. As this holds for
every$w\in\mathcal{U}\setminus\mathcal{W}$, we can apply zero or moretimes
rules $B\in\mathcal{B}$, followed by a single applicationof rule
$C=u\rightarrow w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}\in\mathcal{C}$, in
order to obtain a partial derivation that can besummarized as $u\rightarrow
w_{1}\parallel_{1}\cdots\parallel_{1}w_{k}$,where $w_{m}$ is the head of the
rule $A^{m}\in\mathcal{A}$. Then,we continue the derivation by applying the
rule $A^{m}$ for every$m\in[1,k]$ in order to obtain the partial derivation

$\displaystyle
u\rightarrow\overline{\mathbf{a_{1}}}^{i_{1}}(u^{1}_{1},\ldots,u^{1}_{i_{1}-1},u^{1}_{i_{1}+1},\ldots
u^{1}_{n_{1}})\parallel_{1}\cdots\parallel_{1}\overline{\mathbf{a_{m}}}^{i_{m}}(u^{m}_{1},\ldots,u^{m}_{i_{m}-1},u^{m}_{i_{m}+1},\ldots
u^{m}_{n_{m}})\parallel_{1}\cdots$
$\displaystyle\qquad\qquad\parallel_{1}\overline{\mathbf{a_{k}}}^{i_{k}}(u^{k}_{1},\ldots,u^{k}_{i_{k}-1},u^{k}_{i_{k}+1},\ldots
u^{k}_{n_{k}}).$

This partial derivation together with (*) and
$G^{m}_{j}\in\mathcal{L}_{\Gamma}({u^{m}_{j}})$ then establishes
$G\in\mathcal{L}_{\Gamma}({u})$.In order to establish the completeness of
regular tree-grammars, weuse the already known equivalence between
$\mathsf{CMSO}$-definable andrecognizable languages of unranked trees [5,
Theorem5.3]:

######  Theorem 1 ([5]).

Let $\mathcal{L}$ be a language of trees.Then, $\mathcal{L}$ is
$\mathsf{CMSO}$-definable iff $\mathcal{L}$ is recognizable.

The dual direction of the equivalence between regular tree languagesand
$\mathsf{CMSO}$-definable tree languages is given by the following result:Let
$\mathcal{L}$ be a $\mathsf{CMSO}$-definable tree language. Then,
$\mathcal{L}$ is aregular tree language.By Theorem 1, $\mathcal{L}$ is
recognizable.Hence, there is a locally-finite congruence relation $\cong$ that
recognizes $\mathcal{L}$.Let $A$ be the finite set of equivalence classes of
graphs of type 1 (as all trees are graphs of type 1, these are the only
relevant equivalence classes).We now observe that $\cong$ induces
operations$\parallel_{1}$ and $\overline{\mathbf{a}}^{i}$ on $A$.In
particular, we note that $A$ and $\parallel_{1}$ form a finite commutative
monoid.Let $n=\mathrm{card}({A})$ be the cardinality of $A$.Because $A$ is
finite, we have for every $a\in A$ that there are some indices $0\leq d<n$ and
$1\leq q\leq n$ such that $a^{d}=a^{d+q}$ (*), where $a^{q}$ denotes the
$q$-fold composition of $a$ with itself wrt the operation $\parallel_{1}$.We
set $\mathsf{stem}(a)=d$ and $\mathsf{lasso}(a)=q$ for the least such $d$ and
$q$ and note that they are unique.We now create non-terminals $u_{a}$ and
$w_{a}$ for all elements $a\in A$, and define a grammar $\Gamma$ by the
following rules:

  1. A.

$w_{b}\rightarrow\overline{\mathbf{a}}^{i}(u_{a_{1}},\ldots,u_{a_{{\\#{a}}-1}})$
iff$b=\overline{\mathbf{a}}^{i}(a_{1},\ldots,a_{{\\#{a}}-1})$

  2. B.

$u_{b}\rightarrow u_{b}\parallel_{1}w_{a}^{q}$ iff $b=b\parallel_{1}a^{q}$ for
some $1\leq q\leq n$

  3. C.

$u_{b}\rightarrow
w_{a_{1}}^{p_{1}}\parallel_{1}\ldots\parallel_{1}w_{a_{n}}^{p_{n}}$ iff
$b=a_{1}^{p_{1}}\parallel_{1}\cdots\parallel_{1}a_{n}^{p_{n}}$ for some $0\leq
p_{i}<2n$

We finally add axioms $\rightarrow u_{a}$ for all $a\in A$ such that there is
some tree $G$ with $G\in a\subseteq\mathcal{L}$.We now prove that
$\mathcal{L}=\mathcal{L}({\Gamma})$:We first verify for all non-terminals
$u_{a},w_{a}\in\mathcal{U}$ that $G\in\mathcal{L}_{\Gamma}({u_{a}})$ resp.
$G\in\mathcal{L}_{\Gamma}({w_{a}})$ implies that $G\in a$;this by done by a
straightforward induction on the length of the derivation.In particular, this
implies that $\mathcal{L}\supseteq\mathcal{L}({\Gamma})$.We now prove that
$G\in a$ implies $G\in\mathcal{L}_{\Gamma}({u_{a}})$ and
$G\in\mathcal{L}_{\Gamma}({w_{a}})$ in case of
$G=\overline{\mathbf{a}}^{i}(G_{1},\ldots,G_{i-1},G_{i+1},\ldots,G_{{\\#{a}}})$
for some trees $G_{1},\ldots,G_{i-1},G_{i+1},\ldots,G_{{\\#{a}}}$.We prove the
claim by induction on the size of $G$.We first assume that
$G=\overline{\mathbf{a}}^{i}(G_{1},\ldots,G_{i-1},G_{i+1},\ldots,G_{{\\#{a}}})$
for some trees$G_{1},\ldots,G_{i-1},G_{i+1},\ldots,G_{{\\#{a}}}$. Let
$w_{j}\in A$ be the equivalenceclass such that $G_{j}\in w_{j}$. Then, we have
that
$a=\overline{\mathbf{a}}^{i}(w_{1},\ldots,w_{i-1},w_{i+1},\ldots,w_{{\\#{a}}})$.
Byinduction assumption, we have that $G_{j}\in\mathcal{L}_{\Gamma}({w_{j}})$.
Now, we can apply a rule ofshape A and deduce that
$G\in\mathcal{L}_{\Gamma}({w_{a}})$ and a rule of shape C,that is the rule
$u_{a}\rightarrow w_{a}$, in order to deduce
that$G\in\mathcal{L}_{\Gamma}({u_{a}})$. Note that the rule $u_{a}\rightarrow
w_{a}$ exists as a special case of rules of shape C.We now assume that
$G=G_{1}\parallel_{1}G_{2}\parallel_{1}\cdots$ for some sequence of trees
$G_{j}$ such that for all $j$ we have
$G_{j}=\overline{\mathbf{a_{j}}}^{i_{j}}(G_{1}^{j},\ldots,G_{i-1}^{j},G_{i+1}^{j},\ldots,G_{{\\#{a_{j}}}}^{j})$
for some trees
$G_{1}^{j},\ldots,G_{i-1}^{j},G_{i+1}^{j},\ldots,G_{{\\#{a_{j}}}}^{j}$.Let
$a_{i}\in A$ be the equivalence class such that $G_{i}\in a_{i}$.Note that we
have that $a=a_{1}\parallel_{1}a_{2}\parallel_{1}\cdots$.Now, because
$\parallel_{1}$ is associative and commutative, we can represent this product
as$a=a_{1}^{l_{1}}\parallel_{1}\cdots\parallel_{1}a_{n}^{l_{n}}$ for some
enumeration $a_{1},\ldots,a_{n}$ of the equivalence classes of $A$ and
$l_{i}\in{\rm Nature}$.By (*), we have
$a=a_{1}^{p_{1}}\parallel_{1}\cdots\parallel_{1}a_{n}^{p_{n}}$ for some $0\leq
p_{i}<2n$ such that $l_{i}=\mathsf{lasso}(a_{i})k_{i}+p_{i}$ for some
$k_{i}\in{\rm Nature}$, and $a=a\parallel_{1}a_{i}^{\mathsf{lasso}(a_{i})}$
for every $a_{i}$ with $l_{i}\geq 2n$.Now we obtain that
$G\in\mathcal{L}_{\Gamma}({u_{a}})$, using that
$G_{j}\in\mathcal{L}_{\Gamma}({w_{j}})$ by induction assumption and then
applying rules of shape B as often as needed followed by a single application
of a rule of shape C.In the rest of this section, we characterize the class
ofMSO-definable tree languages by tree grammars. We show that theMSO-definable
tree language are exactly the languages produced by thetree grammars having
$q=1$ in each rule of the form(B).Let $\mathcal{L}$ be a tree language such
that $\mathcal{L}=\mathcal{L}({\Gamma})$ forsome regular tree grammar $\Gamma$
such that $q=1$ for allrules of the form (B). Then, $\mathcal{L}$ isMSO-
definable.The proof agrees with the proof ofTheorem 0.3, except for asmall
modification. Because of $q=1$ for all rules ofshape B, we are able to replace
theconstraints $\mathsf{card}_{{q},{p}}({X})$ in the proof ofTheorem 0.3. We
recognizethat the formula $\mathsf{card}_{{q},{p}}({X})$ is equivalent to
theMSO-formula $\mathsf{card}({X})\geq p$ for $q=1$,
and$\mathsf{card}({X})\geq p\wedge\neg(\mathsf{card}({X})\geq p+1)$ for $q=0$,
where $\mathsf{card}({X})\geq
k\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
x_{1},\ldots,x_{k}.\ \bigwedge_{1\leq i\leq k}x_{i}\in X\wedge\bigwedge_{1\leq
i<j\leq k}x_{i}\neq x_{j}$.Let $\mathcal{L}$ be a MSO-definable tree language.
Then, there existssome regular tree grammar $\Gamma$ with
$\mathcal{L}=\mathcal{L}({\Gamma})$such that $q=1$ for all rules of the
form(B).The proof agrees with the proof of Theorem 0.3, except for one
additional argument:Again we use that $\mathcal{L}$ is recognizable by Theorem
1.Thus, there is a locally-finite congruence relation $\cong$ that recognizes
$\mathcal{L}$.Let $A$ be the finite set of equivalence classes of type 1.We
recall that $\cong$ induces an operation$\parallel_{1}$ on $A$.In particular,
we note that $A$ and $\parallel_{1}$ form a finite commutative monoid.We
recall that a monoid $A$ is called _aperiodic_ iff $\mathsf{lasso}(a)=1$ for
all elements $a\in A$.We now use that a set of trees is MSO-definable iff the
monoid $(A,\parallel_{1})$ is aperiodic, see Theorem 5.10 from Bojanczyk
[2].We conclude by observing that the rules resulting from the proof of
Theorem 0.3 have the required form.

##  0.4 Tree Verifiable Graph-Grammars

In this section, we introduce a syntactic restriction on HR graph grammars,
that ensures the $\mathsf{CMSO}$-definability of the generated graph
languages.The restriction is given in terms of easy-to-check syntactic
conditions on the rules of theHR grammar.Like in the case of regular tree
grammars, we partition the set of nonterminals in two alternating subsets.The
crucial restriction is then on the shape of the graphs $G$ in the rules of the
form $w\leftarrow{G}[{e_{1}}({v_{1}}),\ldots,{e_{k}}({v_{k}})]$, where we
require $G$ to consist of a single terminal edge $e$, which needs to contain
at least some source and some vertex of each $e_{i}$.Some additional
conditions ensures that these edges and vertices give rise to a spanning tree
of the generated graph that witnesses the bounded embeddable tree-width of the
graph (see Definition 6 and Proposition 0.4 below).The spanning tree property
also underlies our proof of $\mathsf{CMSO}$-definability, which motivates the
term _tree-verifiable_.As we shall argue next (§0.5), tree-verifiable grammars
define an expressive class of graph languages, as they strictly subsume the
regular graph grammars of Courcelle [6, §5].

######  Definition 4.

A graph grammar $\Gamma=(\mathcal{U},\mathcal{R})$ is _tree-verifiable_ iff
there exist two functions:

  * •

$\mathsf{rt}:\mathcal{U}\rightarrow{\rm Nature}$ mappingeach non-terminal $u$
to an index$\mathsf{rt}({u})\in[{1},{{\\#{u}}}]$, called the _root_ of$u$,

  * •

$\mathsf{fut}:\mathcal{U}\rightarrow\mathrm{pow}({{\rm Nature}})$ mapping
eachnon-terminal $u$ to a subset
$\mathsf{fut}({u})\subseteq[{1},{{\\#{u}}}]\setminus\\{{\mathsf{rt}({u})}\\}$,
called the _future roots_ of $u$,

and a set $\mathcal{W}\subseteq\mathcal{U}$ of nonterminals, suchthat the
rules in $\mathcal{R}$ are of one of the following forms,either:

  1. A.

$w\rightarrow{G}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]$, for some
$w\in\mathcal{W}$and $u_{1},\ldots,u_{k}\in\mathcal{U}\setminus\mathcal{W}$,
where$G$ has exactly one terminal edge $e$, the
vertices$\\{{\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({w}))}\\}\cup\\{{\upsilon_{\scriptscriptstyle{G}}(e_{i})_{\mathsf{rt}({u_{i}})}}\\}_{i\in[{1},{k}]}$
are pairwise distinct and attached to $e$, and

$\mathsf{intern}({G})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w})\\}=\biguplus_{i=1..k}\\{\upsilon_{\scriptscriptstyle{G}}(e_{i})_{j}\mid
j\in\\{\mathsf{rt}({u_{i}})\\}\cup\mathsf{fut}({u_{i}})\\}$

i.e., the internal nodes of $G$ plus the future roots associated to $w$ can
bepartitioned into the roots and future roots associated to all the non-
terminals$u_{i}$.

  2. B.

$u\rightarrow u\parallel_{n}w^{q}$, for some $q\in{\rm Nature}$, where
$u\in\mathcal{U}\setminus\mathcal{W}$, $w\in\mathcal{W}$
with${\\#{u}}={\\#{w}}=n$, such that $\mathsf{rt}({w})=\mathsf{rt}({u})$and
$\mathsf{fut}({w})=\emptyset$, i.e., the roots of $u$ and $w$agree and,
moreover, $w$ has no future roots,

  3. C.

$u\rightarrow w_{1}\parallel_{n}\cdots\parallel_{n}w_{k}$, where
$u\in\mathcal{U}\setminus\mathcal{W}$, $w_{1},\ldots,w_{k}\in\mathcal{W}$
with${\\#{u}}={\\#{w_{i}}}=n$, such that
$\mathsf{rt}({u})=\mathsf{rt}({w_{i}})$ and
$\mathsf{fut}({u})=\biguplus_{i=1..k}\mathsf{fut}({w_{i}})$, i.e., the roots
associated to the non-terminals ofthe right-hand side agree with the root of
the left-hand side andthat future roots of the left-hand side are partitioned
into thefuture roots of the non-terminals of the right-hand side.

Furthermore, the axioms are of the shape $\rightarrow u$ for some
$u\in\mathcal{U}\setminus\mathcal{W}$ with
$[1,{\\#{u}}]=\\{\mathsf{rt}({u})\\}\cup\mathsf{fut}({u})$, i.e., for every
start non-terminal$u$ every source must be a root or future root.

A set of graphs $\mathcal{L}$ is said to be _tree-verifiable_ iffthere is a
tree-verifiable graph-grammar $\Gamma$ such
that$\mathcal{L}=\mathcal{L}({\Gamma})$. The following example states a tree-
verifiable grammar for the trees with linked leaves from Example 1 plus an
additional binary edge from the bottom-right node of the tree to the root of
the tree (see the left of Fig. 6 for the depiction of such a graph)222We note
that we chose to add the binary edge as the easiest way of setting up a tree-
verifiable grammar (with axioms) that meets the requirements of Def.
4.However, one can also state a slightly more complicated tree-verifiable
grammar that exactly produces the trees with linked leaves from Example 1.:

$v_{\mathit{axiom}}(\overline{1})\rightarrow$$u$$u$$a$$1$$(\overline{1})$$(\underline{2})$(3)(3)$(\underline{2})$$(\overline{1})$$w_{\mathit{axiom}}(\overline{1},2)\rightarrow$$u(\overline{1},\underline{2},3)\rightarrow
w(\overline{1},\underline{2},3)$$w(\overline{1},\underline{2},3)\rightarrow$$a$$1$$3$$(\overline{1})$$v$$2$$u$$u$$a$$1$$(\overline{1})$$(\underline{2})$(3)(3)$(\underline{2})$$(\overline{1})$$3$$2$$w(\overline{1},\underline{2},3)\rightarrow$$v(\overline{1})\rightarrow\overline{\mathbf{1}}$$z_{\mathit{axiom}}(\overline{1},2)\rightarrow
w_{\mathit{axiom}}(\overline{1},2)$$\rightarrow
u_{\mathit{axiom}}(\overline{1})$$u_{\mathit{axiom}}(\overline{1})\rightarrow
v_{\mathit{axiom}}(\overline{1})$$z_{\mathit{axiom}}$$1$$e$$(2)$$(\overline{1})$

Figure 5: Tree-Verifiable Grammar for Trees with Linked Leaves

######  Example 2.

Let us consider the tree-verifiable grammar fromFig. 5, with the set of non-
terminals$\mathcal{U}=\\{{u_{\mathit{axiom}},v_{\mathit{axiom}},z_{\mathit{axiom}},w_{\mathit{axiom}},u,v,w}\\}$
anddistinguished non-
terminals$\mathcal{W}=\\{{v_{\mathit{axiom}},w_{\mathit{axiom}},w}\\}$, with
arities, rootsand future roots, as follows:

  * •

${\\#{u_{\mathit{axiom}}}}={\\#{v_{\mathit{axiom}}}}=1$,$\mathsf{rt}({u_{\mathit{axiom}}})=\mathsf{rt}({v_{\mathit{axiom}}})=1$,$\mathsf{fut}({u_{\mathit{axiom}}})=\mathsf{fut}({v_{\mathit{axiom}}})=\emptyset$,

  * •

${\\#{z_{\mathit{axiom}}}}={\\#{w_{\mathit{axiom}}}}=2$,$\mathsf{rt}({z_{\mathit{axiom}}})=\mathsf{rt}({w_{\mathit{axiom}}})=1$,$\mathsf{fut}({z_{\mathit{axiom}}})=\mathsf{fut}({w_{\mathit{axiom}}})=\emptyset$,

  * •

${\\#{u}}={\\#{w}}=3$,
$\mathsf{rt}({u})=\mathsf{rt}({w})=1$,$\mathsf{fut}({u})=\mathsf{fut}({w})=\\{{2}\\}$,

  * •

${\\#{v}}=1$, $\mathsf{rt}({v})=1$, $\mathsf{fut}({v})=\emptyset$.

We write the indices $1,\ldots,{\\#{n}}$ enclosed inparenthesis next to each
nonterminal $n\in\mathcal{U}$, where$\mathsf{rt}({n})$ is overlined and
$\mathsf{fut}({n})$ are underlined.Internal nodes are drawn as black circles
and sources are whitenumbered circles. Binary terminal edges are drawn with
solid linesand binary nonterminal edges are dashed. Ternary terminal edges
arefilled with grey and ternary nonterminal edges are unfilled.

The first result is that tree-verifiable graph grammars
produce$\mathsf{CMSO}$-definable sets of graphs:Let $\mathcal{L}$ be a tree-
verifiable graph language. Then, $\mathcal{L}$ is$\mathsf{CMSO}$-definable.Let
$\Gamma=(\mathcal{U},\mathcal{R})$ be a tree-verifiable grammar such that
$\mathcal{L}({\Gamma})=\mathcal{L}$.Let $\mathcal{W}\subseteq\mathcal{U}$ be
the set that partitions $\mathcal{U}$ as required by thedefinition of a tree-
verifiable graph grammar.By Lemma 0.3, whose proof also applies to tree-
verifiable grammars,we can assume that for each pair of non-terminals
$u,w\in\mathcal{U}$, there is at most one rule $u\rightarrow
u\parallel_{1}w^{q}$ of shape B in $\mathcal{R}$.Let
$\mathcal{A},\mathcal{B},\mathcal{C}$ be the set of rules of theform shape
A,B, C in$\mathcal{R}$, respectively, where by
$n_{\mathcal{A}}=\mathrm{card}({\mathcal{A}})$and
$n_{\mathcal{C}}=\mathrm{card}({\mathcal{C}})$ we denote the number of rulesof
the respective form. For each of the rules $A\in\mathcal{A},C\in\mathcal{C}$
we will use a set variable $\underline{A},\underline{C}$.For any
$u\in\mathcal{U}\setminus\mathcal{W}$, we below state a formula $\psi(u)$ with
free first-order variables $y_{1},\ldots,y_{{\\#{u}}}$ and free monadic
variables
$\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}$,
which has the following property:Given a graph $G$ of type ${\\#{u}}$, let
$\mathfrak{s}$ be the valuation defined by
$\mathfrak{s}(y_{i})=\xi_{\scriptscriptstyle{G}}(i)$ for all
$i\in[1,{\\#{u}}]$.Then,
$\widehat{G}\models^{\mathfrak{s}}\exists\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}.\
\psi(u)$ iff $G\in\mathcal{L}_{\Gamma}({u})$.We can use these formulae
$\psi(u)$ to build a $\mathsf{CMSO}$-sentence $\phi$ such that
$\mathcal{L}=\\{{G\mid G\models\phi}\\}$:

$\phi\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigvee_{\text{axiom
}\rightarrow u\in\Gamma}\exists
y_{1},\ldots,y_{{\\#{u}}},\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}.\
\psi(u).$

We next introduce some notation that will be useful in the definition of the
formulae $\psi(u)$, in particular, it will allow us to conveniently access the
spanning tree that underlies every derivation of a tree-verifiable grammar.We
consider some rule
$A=w\rightarrow{G}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]\in\mathcal{A}$.Let
$e$ be the single terminal edge of $G$.We denote by
$\mathsf{rpos}(A)=j\in[1,\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(e)})]$
the index such that
$\upsilon_{\scriptscriptstyle{G}}(e)_{j}=\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({w}))$,
by
$\mathsf{cpos}(A,i)=j\in[1,\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(e)})]$
the index such that
$\upsilon_{\scriptscriptstyle{G}}(e)_{j}=\upsilon_{\scriptscriptstyle{G}}(e_{i})_{\mathsf{rt}({u_{i}})}$
and by $\mathsf{cpos}(A)=\\{\mathsf{cpos}(A,i)\mid i\in[1,k]\\}$ the set of
these indices (we recall that the definition of a tree-verifiable grammar
requires all those vertices to be attached to $e$).We also define
$\lambda(A)=\lambda_{\scriptscriptstyle{G}}(e)$ as the label of the edge $e$,
$\mathsf{vtx}(A,i)=\upsilon_{\scriptscriptstyle{G}}(e)_{i}$ as the $i$-th
vertex attached to the edge $e$, and write $\mathsf{graph}(A)=G$ for the graph
of rule $A$.We call $\mathsf{rpos}(A)$ the _root position_ of $A$ and
$\mathsf{cpos}(A)$ the _positions_ of the _children_ of $A$.We say that a
vertex $v$ is _at the root position_ of some edge $\epsilon$, if
$\underline{A}(\epsilon)$ for some $A\in\mathcal{A}$ and
$v=\upsilon_{\scriptscriptstyle{G}}(\epsilon)_{\mathsf{rpos}(A)}$, and we say
that $v$ is _at child position_ $\mathsf{cpos}(A,i)$ of $\epsilon$, if
$\underline{A}(\epsilon)$ for some $A\in\mathcal{A}$ and
$v=\upsilon_{\scriptscriptstyle{G}}(\epsilon)_{i}$.Further, for a rule
$C=u\rightarrow w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}\in\mathcal{C}$ we
denote its head by $\mathsf{hd}(C)=u$.We now consider some non-terminal
$u^{\circ}\in\mathcal{U}\setminus\mathcal{W}$.Let
$\mathsf{nrts}({u^{\circ}})=[1,{\\#{u^{\circ}}}]\setminus(\mathsf{fut}({u^{\circ}})\cup\\{\mathsf{rt}({u^{\circ}})\\})$
be the indices that are neither the root nor the future roots of
$u^{\circ}$.The formula $\psi(u^{\circ})$ is the conjunction of the
sentencesbelow:

  * •

$\phi_{0}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigwedge_{1\leq
i<j\leq{\\#{u^{\circ}}}}y_{i}\neq y_{j}$ states that all sources of the graph
are pairwise different.

  * •

$\phi_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigvee_{A\in\mathcal{A}}\underline{A}(e)\land\bigwedge_{A_{1}\neq
A_{2}\in\mathcal{A}}\neg(\underline{A}_{1}(e)\land\underline{A}_{2}(e))$.
Thisformula states that every edge is labelled by exactlyone rule of shape A.

  * •

$\phi_{2}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in
V.\left(\bigvee_{C\in\mathcal{C}}\underline{C}(v)\leftrightarrow\bigwedge_{i\in\mathsf{nrts}({u^{\circ}})}y_{i}\neq
v\right)\land\bigwedge_{C_{1}\neq
C_{2}\in\mathcal{C}}\neg(\underline{C}_{1}(v)\land\underline{C}_{2}(v)$.This
formula states that every vertex is labelled by a rule of shape C iff this
vertex is neither the root nor a future root of $u^{\circ}$, and that every
vertex is labelled by at most one such rule.

  * •

$\phi_{3}$ is the conjunction of the formulae $\phi_{3a}$,$\phi_{3b}$,
$\phi_{3c}$, and $\phi_{3d}$, and states that the graph contains a spanning
tree with root $y_{\mathsf{rt}({u^{\circ}})}$, where the spanning tree is
constructed using only the root and child positions of every edge:

    * –

The formula

$\phi_{3a}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigwedge_{A\in\mathcal{A}}\underline{A}(e)\rightarrow\forall
x_{1}\ldots x_{{\\#{\lambda(A)}}}\in
V.\mathsf{edg}_{\lambda(A)}(e,x_{1},\ldots,x_{{\\#{\lambda(A)}}})\rightarrow\\\
\bigwedge_{i\neq j\in\mathsf{cpos}(A)\cup\\{\mathsf{rpos}(A)\\}}x_{i}\neq
x_{j}$

states that for every edge the vertices at its root and child positions are
pairwise different.

    * –

The formula

$\phi_{3b}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigwedge_{A\in\mathcal{A}}\underline{A}(e)\rightarrow\forall
x_{1}\ldots x_{{\\#{\lambda(A)}}}\in
V.\mathsf{edg}_{\lambda(A)}(e,x_{1},\ldots,x_{{\\#{\lambda(A)}}})\rightarrow\\\
\bigwedge_{i\in\mathsf{cpos}(A)}x_{i}\neq y_{\mathsf{rt}({u^{\circ}})}$

states that the root $y_{\mathsf{rt}({u^{\circ}})}$ is only incident to an
edge $\epsilon$, if $y_{\mathsf{rt}({u^{\circ}})}$ is not at a child position
of $\epsilon$.

    * –

The formula

$\phi_{3c}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in V.v\neq y_{\mathsf{rt}({u^{\circ}})}\rightarrow\exists!e\in{E}.\\\
\bigvee_{A\in\mathcal{A}}\left(\underline{A}(e)\land\exists x_{1}\ldots
x_{{\\#{\lambda(A)}}}\in
V.\mathsf{edg}_{a}(e,x_{1},\ldots,x_{{\\#{\lambda(A)}}})\land\bigvee_{i\in\mathsf{cpos}(A)}x_{i}=v\right)$

states that for every vertex $v\neq y_{\mathsf{rt}({u^{\circ}})}$ there is
exactly one edge $\epsilon$ such that $v$ is at a child position of
$\epsilon$.

    * –

$\phi_{3d}$ states that every vertex, except for the vertices
$(y_{i})_{i\in\mathsf{nrts}({u^{\circ}})}$, is reachable from
$y_{\mathsf{rt}}({u^{\circ}})$ using only the root and child positions of
every edge (as this formula is standard we omit it for brevity).

  * •

$\phi_{4}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}\;.\;\bigwedge_{A\in\mathcal{A}}\left(\underline{A}(e)\rightarrow\psi^{A}_{4}(e)\right)$
states that every edge $\epsilon$ labelled by some
rule$A=w\rightarrow{G}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]\in\mathcal{A}$
needs to satisfy the formula

$\psi^{A}_{4}(e)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in V\;.\;\bigwedge_{1\leq i\leq
k}\left(\mathsf{at}_{\mathsf{cpos}(A,i)}(e,v)\rightarrow\bigvee_{C\in\mathcal{A},\mathsf{hd}(C)=u_{i}}\underline{C}(v)\right),$

which states that every vertex attached to $\epsilon$ at some child position
$\mathsf{cpos}(A,i)$, is labelled by some rule with head $u_{i}$, where the
auxiliaryformula $\mathsf{at}_{t}(e,v)$ denotes that $v$ is at the
$t$-thposition of edge $\epsilon$, i.e.,

$\mathsf{at}_{t}(e,v)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\bigvee_{a\in\mathbb{A}}\exists
x_{1},\ldots,x_{t-1},x_{t+1},\ldots,x_{{\\#{a}}}\in
V.\mathsf{edg}_{a}(e,x_{1}\ldots x_{t-1},\;v,\;x_{t+1},\ldots,x_{{\\#{a}}}).$

  * •

$\phi_{5}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in
V.\bigwedge_{C\in\mathcal{C}}\underline{C}(v)\rightarrow\left(\bigwedge_{w\in\mathcal{W}}\psi^{C}_{w}(v)\right)$
statesthat each vertex labelled by some rule $C=u\rightarrow
w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}\in\mathcal{C}$satisfies the formula
$\psi^{C}_{w}$ for every $w\in\mathcal{W}$. This formula is obtained as
follows: Let usconsider some $w\in\mathcal{W}$. Let $p$ be the number oftimes
$w$ appears among the $w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}$. Let $q$ be
the number such that thereis a rule $u\rightarrow
u\parallel_{1}w^{q}\in\mathcal{B}$(we recall that there is at most one rule of
this shape), andlet $q=0$, otherwise. We now define the formula

$\psi^{C}_{w}(v)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists
X\subseteq{E}\;.\;\mathsf{card}_{{q},{p}}({X})\wedge\forall e\;.\;e\in
X\leftrightarrow\bigvee_{A\in\mathcal{A},A\text{ has head
}w}\left(\underline{A}(e)\wedge\mathsf{at}_{\mathsf{rpos}(A)}(e,v)\right),$

which states that there are exactly $kq+p$ edges $\epsilon$,for some $k\in{\rm
Nature}$, such that $\epsilon$ is labelled by somerule $A\in\mathcal{A}$ with
head $w$ and such that $v$ is incident to $\epsilon$ at position
$\mathsf{rpos}(A)$.

  * •

$\phi_{6}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigwedge_{A\in\mathcal{A}}\underline{A}(e)\rightarrow\exists
x_{1}\ldots x_{{\\#{\lambda(A)}}}\in V.\
\mathsf{edg}_{\lambda(A)}(e,x_{1},\ldots x_{{\\#{\lambda(A)}}})$ states that
$\underline{A}(\epsilon)$ for some rule $A\in\mathcal{A}$, then the edge
$\epsilon$ is labelled by $\lambda(A)$.

  * •

The formula

$\phi_{7}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigwedge_{A\in\mathcal{A}}\underline{A}(e)\rightarrow\forall
x_{1}\ldots x_{{\\#{\lambda(A)}}}\in V.\
\mathsf{edg}_{\lambda(A)}(e,x_{1},\ldots x_{{\\#{\lambda(A)}}})\rightarrow\\\
\bigwedge_{i\in[1,{\\#{\lambda(A)}}])}\left(\bigvee_{j\in\mathsf{nrts}({u^{\circ}})}x_{i}=y_{j}\wedge\mathsf{equal}_{j,\mathsf{vtx}(A,i)}(y_{\mathsf{rt}({u^{\circ}})},e)\right)\vee\left(\bigvee_{C\in\mathcal{C}}\underline{C}(x_{i})\wedge\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),\mathsf{vtx}(A,i)}(x_{i},e)\right)$

states for every vertex $x_{i}$ incident to some edge $\epsilon$ that this
vertex needs to be propagated according to the rules of the grammar.This
propagation can be implemented by a finite state machine, and we provide an
explicit MSO formula that implements this finite state machine.In case $x_{i}$
is not part of the spanning tree, $x_{i}$ needs to be equal to some vertex
$y_{j}$ that is neither a root nor a future root of $u^{\circ}$.Then, we
require that the source number $j$ for the non-terminal $u^{\circ}$ agrees
with vertex $\mathsf{vtx}(A,i)$ as propagated by the rules of the grammar.This
is expressed by the formula
$\mathsf{equal}_{j,\mathsf{vtx}(A,i)}(y_{\mathsf{rt}({u^{\circ}})},e)$.In case
$x_{i}$ is part of the spanning tree, there is some rule $C\in\mathcal{C}$
such that $\underline{C}(x_{i})$ holds.Then, we require that source
$\mathsf{rt}({\mathsf{hd}(C)})$ agrees with vertex $\mathsf{vtx}(A,i)$ as
propagated by the rules of the grammar.This is expressed by the formula
$\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),\mathsf{vtx}(A,i)}(x_{i},e)$.We
give the details on the construction of the formula
$\mathsf{equal}_{i,z}(v,e)$ below.

  * •

The formula

$\phi_{8}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in V.\bigwedge_{C\in\mathcal{C}}\underline{C}(v)\rightarrow\\\
\bigwedge_{i\in[1,{\\#{\mathsf{hd}(C)}}]}\bigvee_{j\in\mathsf{nrts}({u^{\circ}})}\mathsf{equal}_{j,i}(y_{\mathsf{rt}({u^{\circ}})},v)\vee\exists
x.\bigvee_{C^{\prime}\in\mathcal{C}}(\underline{C}^{\prime}(x)\wedge\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C^{\prime})}),i}(x,v))$

states for every vertex $v$ in the spanning tree, i.e., for every vertex $v$
with $\underline{C}(v)$ for some $C\in\mathcal{C}$, that every source
$i\in[1,{\\#{\mathsf{hd}(C)}}]$ needs to be propagated according to the rules
of the grammar.This propagation can be implemented by a finite state machine,
and we provide explicit an MSO formula that implements this finite state
machine.In particular, the $i$-th source of $\mathsf{hd}(C)$ must be equal to
a vertex $x$ that is part of the spanning tree or to a vertex $y_{j}$ that is
neither a root nor future root of $u^{\circ}$.For a vertex $x$ that is part of
the spanning tree there must be some $C^{\prime}\in\mathcal{C}$ with
$\underline{C}^{\prime}(x)$.Then, being equal to source $i$ of
$\mathsf{hd}(C)$ can be expressed by the formula
$\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C^{\prime})}),i}(x,v)$.For a vertex
$y_{j}$ that is neither a root nor a future root of $u^{\circ}$, being equal
to source $i$ of $\mathsf{hd}(C)$ can be expressed by the formula
$\mathsf{equal}_{j,i}(y_{\mathsf{rt}({u^{\circ}})},v)$.We give the details on
the construction of the formula $\mathsf{equal}_{i_{1},i_{2}}(v_{1},v_{2})$
below.

The formulae $\mathsf{equal}_{i,z}(v,e)$ and
$\mathsf{equal}_{i_{1},i_{2}}(v_{1},v_{2})$ are both defined in terms of a
formula $\rho$, which we define first.The formula $\rho$ uses monadic
predicates $K_{z}$ for $z\in V_{\scriptscriptstyle{\mathsf{graph}(A)}}$ and
$A\in\mathcal{A}$, and $L_{k}$ for $k\in[1,{\\#{u}}]$ and
$u\in\mathcal{U}\setminus\mathcal{W}$, in order to track vertices that are
equal according to the propagation by the rules of the grammar.$\rho$ also
uses the monadic predicates $M$ and $N$ (these two predicates are going to be
used as blank symbols, i.e., they do not carry any information).$\rho$ is
given as the conjunction of the following formulae:

  * •

$\rho_{1}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigvee_{P\in\mathcal{P}}P(e)\land\bigwedge_{P\neq
Q\in\mathcal{P}}\neg(P(e)\land Q(e))$ for $\mathcal{P}=\\{K_{z}\mid z\in
V_{\scriptscriptstyle{\mathsf{graph}(A)}},A\in\mathcal{A}\\}\cup\\{M\\}$
states that the predicates $K_{z}$ and $M$ partition the edges.

  * •

$\rho_{2}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
e\in{E}.\bigwedge_{A\in\mathcal{A}}\underline{A}(e)\rightarrow\bigvee_{P\in\\{K_{z}\mid
z\in V_{\scriptscriptstyle{\mathsf{graph}(A)}}\\}\cup\\{M\\}}P(e)$ states that
every edge labelled by some $\underline{A}$ for some $A\in\mathcal{A}$ must be
labelled by $M$ or by $K_{z}$ for some $z\in
V_{\scriptscriptstyle{\mathsf{graph}(A)}}$.

  * •

$\rho_{3}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in
V.\left(\bigvee_{P\in\mathcal{P}}P(e)\leftrightarrow\bigwedge_{i\in\mathsf{nrts}({u^{\circ}})}y_{i}\neq
v\right)\land\bigwedge_{P\neq Q\in\mathcal{P}}\neg(P(e)\land Q(e))$ for
$\mathcal{P}=\\{L_{i}\mid
i\in[1,{\\#{\mathsf{hd}(C)}}],C\in\mathcal{C}\\}\cup\\{N\\}$ states that the
predicates $L_{i}$ and $N$ partition the vertices, except for the vertices
$(y_{i})_{i\in\mathsf{nrts}({u^{\circ}})}$, which are not labelled by any
predicate.

  * •

$\rho_{4}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in
V.\bigwedge_{C\in\mathcal{C}}\underline{C}(v)\rightarrow\bigvee_{P\in\\{L_{i}\mid
i\in[1,{\\#{\mathsf{hd}(C)}}]\\}\cup\\{N\\}}P(e)$ states that every vertex
labelled by some $\underline{C}$ for some $C\in\mathcal{C}$ must be labelled
by $N$ or by $L_{i}$ for some $i\in[1,{\\#{\mathsf{hd}(C)}}]$.

  * •

The formula

$\rho_{5}\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\forall
v\in
V,e\in{E}.\bigwedge_{A=w\rightarrow{G}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]\in\mathcal{A}}\underline{A}(e)\rightarrow\forall
x_{1}\ldots x_{{\\#{\lambda(A)}}}\in
V.\mathsf{edg}_{\lambda(A)}(e,x_{1},\ldots
x_{{\\#{\lambda(A)}}})\rightarrow\\\
\bigwedge_{i\in[1,{\\#{w}}]}L_{i}(x_{\mathsf{rpos}(A)})\leftrightarrow
K_{\xi_{\scriptscriptstyle{G}}(i)}(e)\wedge\bigwedge_{1\leq j\leq k,1\leq
i\leq{\\#{u_{j}}}}L_{i}(x_{\mathsf{cpos}(A,j)})\leftrightarrow
K_{\upsilon_{\scriptscriptstyle{G}}(e_{j})_{i}}(e)$

states that if edge $\epsilon$ is labelled by
$A=w\rightarrow{G}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]\in\mathcal{A}$,then
the vertex $v$ at the root position of $\epsilon$ is labelled by $L_{i}$ iff
$\epsilon$ is labelled by $K_{\xi_{\scriptscriptstyle{G}}(i)}$, and the vertex
$v$ at the position $\mathsf{cpos}(A,j)$ of $\epsilon$ is labelled by $L_{i}$
iff $\epsilon$ is labelled by
$K_{\upsilon_{\scriptscriptstyle{G}}(e_{j})_{i}}$.This formula is the core of
the propogation mechanism and ensures that we track vertices that are equal
according to the rules of the grammar.

  * •

$\rho_{6}$ states that the vertices and edges labelled by $L_{i}$ resp.
$K_{z}$ are connected, using only the root and child positions of every edge
(as this formula is standard we omit it for brevity).

We can then set

$\mathsf{equal}_{i,z}(v,e)\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists(K_{z})_{z},(L_{i})_{i},M,N.\
\rho\wedge L_{i}(v)\wedge K_{z}(e)$

and

$\mathsf{equal}_{i_{1},i_{2}}(v_{1},v_{2})\stackrel{{\scriptstyle\scriptscriptstyle{\mathsf{def}}}}{{\iff}}\exists(K_{z})_{z},(L_{i})_{i},M,N.\
\rho\wedge L_{i_{1}}(v_{1})\wedge L_{i_{2}}(v_{2}).$

We now consider some $u\in\mathcal{U}\setminus\mathcal{W}$, a graph $G$ of
type ${\\#{u}}$, and a valuation $\mathfrak{s}$ with
$\mathfrak{s}(y_{i})=\xi_{\scriptscriptstyle{G}}(i)$ for all
$i\in[1,{\\#{u}}]$.We prove that
$\widehat{G}\models^{\mathfrak{s}}\exists\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}.\
\psi(u)$ iff $G\in\mathcal{L}_{\Gamma}({u})$.We first assume
$G\in\mathcal{L}_{\Gamma}({u})$ and show that
$\widehat{G}\models^{\mathfrak{s}}\psi(u)$ for some valuation of
$\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}$.We
proceed by induction on the number of rules by which $G$ was derived.Then, the
derivation of $G$ starts with zero or more applications of rules
$B\in\mathcal{B}$ of form $u\rightarrow u\parallel_{1}w^{q}$.At some point
there is an application of a rule $C=u\rightarrow
w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}\in\mathcal{C}$.Then, indexing by
$m$, for each non-terminal $w_{m}$, the derivation continues with an
application of some rule
$A^{m}=w_{m}\rightarrow{G^{m}}[{e_{1}^{m}}({u_{1}^{m}}),\ldots,{e_{k}^{m}}({u_{k}^{m}})]\in\mathcal{A}$.Let
$e_{m}$ be the single terminal edge of the graph $G^{m}$.Let us now assume
that for each $u^{m}_{j}$ we have derived a graph
$G^{m}_{j}\in\mathcal{L}_{\Gamma}({u^{m}_{j}})$.Then,we obtain

$\displaystyle
G=G^{1}[e_{1}^{1}/G_{1}^{1},\ldots,e_{n_{1}}^{1}/G_{n_{1}}^{1}]\cdots\parallel_{1}G^{m}[e_{1}^{m}/G_{1}^{m},\ldots,e_{n_{m}}^{m}/G_{n_{m}}^{m}]\parallel_{1}\cdots$
$\displaystyle\qquad\qquad\parallel_{1}G^{k}[e_{1}^{k}/G_{1}^{k},\ldots,e_{n_{k}}^{k}/G_{n_{k}}^{k}].$

We note that each of the graphs $G^{m}_{j}$ is derived by less rule
applications than $G$.We define the valuation $\mathfrak{s}^{m}_{j}$ by
setting $\mathfrak{s}^{m}_{j}(y_{i}^{m,j})=\xi_{\scriptscriptstyle{G}}(i)$ for
all $i\in[1,{\\#{u^{m}_{j}}}]$.By the induction assumption, we have that
$\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$ for some
sets
$\underline{A}_{1}^{m,j},\ldots,\underline{A}_{n_{A}}^{m,j},\underline{C}_{1}^{m,j},\ldots,\underline{C}_{n_{C}}^{m,j}$.We
now set
$\underline{A}_{t}=\bigcup_{m,j}\underline{A}^{m,j}_{t}\cup\bigcup_{m}\\{e_{m}\mid
A^{m}=A_{t}\\}$ for all $1\leq t\leq n_{A}$,
$\underline{C}_{t}=\bigcup_{m,j}\underline{C}^{m,j}_{t}$ for all $1\leq t\leq
n_{C}$ with $C_{t}\neq C$, and
$\underline{C}_{t}=\bigcup_{m,j}\underline{C}^{m,j}_{t}\cup\\{\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u}))\\}$,
otherwise.We now verify that $\widehat{G}\models^{\mathfrak{s}}\psi(u)$:

  * •

$\phi_{0}$: This formula holds as we require sources to be pairwise distinct.

  * •

$\phi_{1}$:Each edge $e$ is either part of some subgraph $G^{m}_{j}$, or is
equal to some edge $e_{m}$.The way we defined the sets $\underline{A}_{t}$
still partitions all the edges in $G$.

  * •

$\phi_{2}$: Each vertex is either a source of $G$, an internal node of
$G^{m}$, or belongs to $G^{m}_{j}$.We note that for a vertex $v$ of $G$ that
is neither a source of $G$ nor an internal node of $G^{m}$, there is exactly
one graph $G^{m}_{j}$ such that $v\in V_{\scriptscriptstyle{G^{m}_{j}}}$ and
we get from $\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$
that there is exactly one rule $C\in\mathcal{C}$ with
$\underline{C}^{m,j}(v)$.Further, for every internal vertex
$v\in\mathsf{intern}({G^{m}})$, there is exactly one $u^{m}_{j}$ with
$v=\mathfrak{s}^{m}_{j}(y^{m,j}_{i})$ for some $i\in\mathsf{fut}({u^{m}_{j}})$
because of the
condition$\mathsf{intern}({G^{m}})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w^{m}})\\}=\biguplus_{j=1..n_{m}}\\{\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i}\mid
i\in\\{\mathsf{rt}({u^{m}_{j}})\\}\cup\mathsf{fut}({u^{m}_{j}})\\}$.Hence, we
get from $\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$
that there is exactly one rule $C\in\mathcal{C}$ with
$\underline{C}^{m,j}(v)$.We now consider a vertex
$v=\xi_{\scriptscriptstyle{G}}(i)$ for some $i\in\mathsf{fut}({u})$.Then,
because of the condition
$\mathsf{fut}({u})=\biguplus_{i=1..k}\mathsf{fut}({w_{i}})$ of $C$ and the
conditions $\mathsf{intern}({G^{m}})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w^{m}})\\}=\biguplus_{j=1..n_{m}}\\{\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i}\mid
i\in\\{\mathsf{rt}({u^{m}_{j}})\\}\cup\mathsf{fut}({u^{m}_{j}})\\}$, there is
exactly one $u^{m}_{j}$ with $v=\mathfrak{s}^{m}_{j}(y^{m,j}_{i^{\prime}})$
for some $i^{\prime}\in\mathsf{fut}({u^{m}_{j}})$.Hence, we get from
$\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$ that there
is exactly one rule $C\in\mathcal{C}$ with $\underline{C}^{m,j}(v)$.Finally,
for the root $\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u}))$ we have set
$\underline{C}(\mathfrak{s}(y_{\mathsf{rt}({u})}))$ for the rule
$C\in\mathcal{C}$ that was applied in the beginning of the derivation (after
zero or more applications of rules $B\in\mathcal{B}$).

  * •

$\phi_{3}$:We get from
$\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$ that there
is a spanning tree of $G^{m}_{j}$ with root
$\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u^{m}_{j}}))$ that uses only the
root and child position of each edge.We then observe that adding the edges
$e_{1},\ldots,e_{m},\ldots,e_{k}$ gives a spanning tree of $G$ with root
$\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u}))$ that uses only the root and
child position of each edge.

  * •

$\phi_{4}$:We get from
$\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$ that this
property holds for all edges of graph $G^{m}_{j}$.We have that the root
$\xi_{\scriptscriptstyle{G^{m}_{j}}}(\mathsf{rt}({u^{m}_{j}}))$ of every
$G^{m}_{j}$ is labeled by some rule with head $u^{m}_{j}$.Hence, the property
holds for all edges $e_{m}$.

  * •

$\phi_{5}$: We get from
$\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\psi(u^{m}_{j})$ that this
property holds for all vertices of$G^{m}_{j}$. We now consider the root
$y_{\mathsf{rt}({u})}$. We recall thatthe root is labelled by some rule
$C=u\rightarrow w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}\in\mathcal{C}$. Let
$w\in\mathcal{U}\setminus\mathcal{W}$ be some non-terminal. Let $p$ bethe
number of times $w$ appears among the
$w_{1}\parallel_{1}\ldots\parallel_{1}w_{k}$. Let $q$ be the number such that
there is arule $u\rightarrow u\parallel_{1}w^{q}\in\mathcal{B}$ (we recallthat
there is at most one rule of this shape), and let $q=0$,otherwise. It is now
easy to verify that there are at least $p$edges, which are labelled by rules
with head $w$, and the number ofthese edges equals $p$ modulo $q$. As this
holds for every $w\in\mathcal{U}\setminus\mathcal{W}$, the property holds for
the root$y_{\mathsf{rt}({u})}$.

  * •

$\phi_{6}$: Clearly, this property holds for all edges of $G^{m}_{j}$.The
property further holds for the edges $e_{m}$.

  * •

$\phi_{7}$:We consider some edge $\epsilon$ that is part of some $G^{m}_{j}$
labelled by some $A\in\mathcal{A}$, and some vertex
$v=\upsilon_{\scriptscriptstyle{G^{m}_{j}}}(i)$ for
$i\in[1,\mathrm{len}({\upsilon_{\scriptscriptstyle{G^{m}_{j}}}(\epsilon)})]$.We
get from $\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\phi_{7}$ that
either we have$v=\xi_{\scriptscriptstyle{G^{m}_{j}}}(l)$ and
$\mathsf{equal}_{l,\mathsf{vtx}(A,i)}(\xi_{\scriptscriptstyle{G^{m}_{j}}}(\mathsf{rt}({u^{m}_{j}})),\epsilon)$
for some $l\in\mathsf{nrts}({u^{m}_{j}})$, or there is some $C\in\mathcal{C}$
with $\underline{C}(v)$ and
$\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),\mathsf{vtx}(A,i)}(v,\epsilon)$.In
the later case, the property continues to hold for $G$ because $G^{m}_{j}$ is
a subgraph of $G$.Hence, we only need to consider
$v=\xi_{\scriptscriptstyle{G^{m}_{j}}}(l)$ and
$\mathsf{equal}_{l,\mathsf{vtx}(A,i)}(\xi_{\scriptscriptstyle{G^{m}_{j}}}(\mathsf{rt}({u^{m}_{j}})),\epsilon)$
for some $l\in\mathsf{nrts}({u^{m}_{j}})$.We first consider the case
$v\in\mathsf{intern}({G^{m}})$.Then, we must have
$v=\xi_{\scriptscriptstyle{G^{m}_{j^{\prime}}}}(l^{\prime})$ for some $1\leq
j^{\prime}\leq n_{m}$ and
$l^{\prime}\in\\{\mathsf{rt}({u^{m}_{j^{\prime}}})\\}\cup\mathsf{fut}({u^{m}_{j^{\prime}}})$
because of the condition
$\mathsf{intern}({G^{m}})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w^{m}})\\}=\biguplus_{j=1..n_{m}}\\{\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i}\mid
i\in\\{\mathsf{rt}({u^{m}_{j}})\\}\cup\mathsf{fut}({u^{m}_{j}})\\}$.Now, we
get from
$\widehat{G^{m}_{j^{\prime}}}\models^{\mathfrak{s}^{m}_{j^{\prime}}}\phi_{8}$
that there is some vertex $v^{\prime}$ with $\underline{C}(v^{\prime})$ for
some $C\in\mathcal{C}$ such that
$\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),l^{\prime}}(v^{\prime},\xi_{\scriptscriptstyle{G^{m}_{j^{\prime}}}}(\mathsf{rt}({u^{m}_{j^{\prime}}})))$.Together
with
$\mathsf{equal}_{l,l^{\prime}}(\xi_{\scriptscriptstyle{G^{m}_{j}}}(\mathsf{rt}({u^{m}_{j}})),\xi_{\scriptscriptstyle{G^{m}_{j^{\prime}}}}(\mathsf{rt}({u^{m}_{j^{\prime}}})))$,because
of
$v=\xi_{\scriptscriptstyle{G^{m}_{j}}}(l)=\xi_{\scriptscriptstyle{G^{m}_{j^{\prime}}}}(l^{\prime})$,we
get that
$G\models^{\mathfrak{s}}\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),\mathsf{vtx}(A,i)}(v^{\prime},\epsilon)$.We
now assume that $v=\xi_{\scriptscriptstyle{G}}(t)$ for some $1\leq
t\leq{\\#{u}}$.In case of $t\in\mathsf{nrts}({u})$, there is nothing to
show.In case of $v=\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u}))$, the claim
follows from the fact
that$\mathsf{equal}_{l,\mathsf{rt}({u})}(\xi_{\scriptscriptstyle{G^{m}_{j}}}(\mathsf{rt}({u^{m}_{j}})),\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u})))$.Hence,
it remains to deal with $t\in\mathsf{fut}({u})$.We note that because of the
conditions $\mathsf{fut}({u})=\biguplus_{i=1..k}\mathsf{fut}({w_{i}})$ and
$\mathsf{intern}({G^{m}})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w^{m}})\\}=\biguplus_{j=1..n_{m}}\\{\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i}\mid
i\in\\{\mathsf{rt}({u^{m}_{j}})\\}\cup\mathsf{fut}({u^{m}_{j}})\\}$ we must
have $v=\xi_{\scriptscriptstyle{G^{m^{\prime}}_{j^{\prime}}}}(l^{\prime})$ for
some $1\leq m^{\prime}\leq k$, $1\leq j^{\prime}\leq n_{m^{\prime}}$ and
$l^{\prime}\in\\{\mathsf{rt}({u^{m}_{j^{\prime}}})\\}\cup\mathsf{fut}({u^{m^{\prime}}_{j^{\prime}}})$.We
can then conclude similarly as in the case of
$v\in\mathsf{intern}({G^{m}})$.We finally consider some edge $e_{m}$.We note
that the claim follows by arguments similar to the above.

  * •

$\phi_{8}$: This property can be proven similarly to property $\phi_{7}$.

We now assume $\widehat{G}\models^{\mathfrak{s}}\psi(u)$ for some valuations
of
$\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}$.We
will show that $G\in\mathcal{L}_{\Gamma}({u})$.We proceed by induction on the
height of the spanning tree, whose existence is ensured by subformula
$\phi_{3}$ of $\psi(u)$.Let $r=\mathfrak{s}(y_{\mathsf{rt}({u})})$ be the root
of the spanning tree, and let $\epsilon_{1},\ldots,\epsilon_{k}$ be the edges
of $G$ such that $r$ is at the root position of each $\epsilon_{i}$.Let
$A^{m}=w_{m}\rightarrow{G^{m}}[{e_{1}^{m}}({u_{1}^{m}}),\ldots,{e_{n_{m}}^{m}}({u_{n_{m}}^{m}})]\in\mathcal{A}$
be the rule such that $\underline{A}^{m}(\epsilon_{m})$ and let
$\upsilon_{\scriptscriptstyle{G}}(\epsilon_{m})=r^{m}_{1}\ldots
r^{m}_{\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(\epsilon_{m})})}$ be the
incident vertices, for $1\leq m\leq k$.We note that
$G\models^{\mathfrak{s}}\psi(u)$ implies that $r=r^{m}_{\mathsf{rpos}(u_{m})}$
and $\lambda(A^{m})=\lambda_{\scriptscriptstyle{G}}(\epsilon_{m})$ for all
$1\leq m\leq k$.Moreover, $j=\mathsf{cpos}(A,i)$, for some $i\in[1,n_{m}]$,
implies that $\underline{C}(r^{m}_{j})$, for some rule $C\in\mathcal{C}$ with
$\mathsf{hd}(C)=u^{m}_{j}$.For each $j\in\mathsf{cpos}(A^{m})$, we are now
going to define a subgraph $G^{m}_{j}$ of $G$:We first define its sources.For
this, we are going to use that $\widehat{G}\models^{\mathfrak{s}}\phi_{8}$.We
instantiate $\phi_{8}$ with $v=r^{m}_{j}$ and $i\in[1,{\\#{u^{m}_{j}}}]$, and
set $\xi_{\scriptscriptstyle{G^{m}_{j}}}(i)=\mathfrak{s}(y_{l})$ in case of
$\widehat{G}\models^{\mathfrak{s}}\mathsf{equal}_{l,i}(r,r^{m}_{j})$ for some
$l\in\mathsf{nrts}({u})$, or we set $\xi_{\scriptscriptstyle{G^{m}_{j}}}(i)$
as the value of $x$ in case of $\widehat{G}\models^{\mathfrak{s}}\exists
x.\bigvee_{C^{\prime}\in\mathcal{C}}(\underline{C}^{\prime}(x)\wedge\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C^{\prime})}),i}(x,r^{m}_{j})$.
We note that these values are unique.We then consider the subtree rooted in
$r^{m}_{j}$ of the spanning tree with root $r$.Let $V$ resp. $E$ be the
vertices that appear in this subtree.We then set
$V_{\scriptscriptstyle{G^{m}_{j}}}=V\cup\\{\xi_{\scriptscriptstyle{G^{m}_{j}}}(i)\mid
i\in[1,{\\#{u^{m}_{j}}}]\\}$, ${E}_{\scriptscriptstyle{G^{m}_{j}}}=E$ and
$\lambda_{\scriptscriptstyle{G^{m}_{j}}}={\lambda_{\scriptscriptstyle{G}}}\\!\\!\downharpoonleft_{\scriptscriptstyle{E}}$.We
now choose the sets
$\underline{A}_{1}^{m,j},\ldots,\underline{A}_{n_{A}}^{m,j},\underline{C}_{1}^{m,j},\ldots,\underline{C}_{n_{C}}^{m,j}$
as the restriction of the sets
$\underline{A}_{1}\ldots\underline{A}_{n_{A}},\underline{C}_{1}\ldots\underline{C}_{n_{C}}$
to the vertices and edges of graph $G^{m}_{j}$.It can now be verified that
$\widehat{G^{m}_{j}}\models^{\mathfrak{s}^{m}_{j}}\phi(u^{m}_{j})$ for the
valuation $\mathfrak{s}^{m}_{j}$ defined by
$\mathfrak{s}^{m}_{j}(y_{i}^{m,j})=\xi_{\scriptscriptstyle{G}}(i)$ for all
$i\in[1,{\\#{u^{m}_{j}}}]$.By the induction assumption we then obtain
that$G^{m}_{j}\in\mathcal{L}_{\Gamma}({u^{m}_{j}})$.We now argue for every
edge $\epsilon_{m}$ and
$l\in[1,\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(\epsilon_{m})})]$ that
$r^{m}_{l}=\mathfrak{s}(y_{i})$ for some $i\in[1,{\\#{u}}]$ or that
$r^{m}_{l}=\xi_{\scriptscriptstyle{G^{m}_{j}}}(i)$ for some
$i\in[1,{\\#{u^{m}_{j}}}]$ and $1\leq j\leq n_{m}$ (#).For this, we are going
to use that $\widehat{G}\models^{\mathfrak{s}}\phi_{7}$.We consider some
$l\in[1,\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(\epsilon_{m})})]$ with
$r^{m}_{l}\neq\mathfrak{s}(y_{i})$ for all $i\in[1,{\\#{u}}]$.Hence,
$\mathsf{vtx}(A^{m},l)\in\mathsf{intern}({G^{m}})$.Because of
$\mathsf{intern}({G^{m}})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w^{m}})\\}=\biguplus_{j=1..n_{m}}\\{\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i}\mid
i\in\\{\mathsf{rt}({u^{m}_{j}})\\}\cup\mathsf{fut}({u^{m}_{j}})\\}$ we have
that there is an $j\in[1,n_{m}]$
with$\mathsf{vtx}(A^{m},l)=\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i}$
for $i\in\\{\mathsf{rt}({u^{m}_{j}})\\}\cup\mathsf{fut}({u^{m}_{j}})$.This
means that
$\widehat{G}\models^{\mathfrak{s}}\mathsf{equal}_{i,\mathsf{vtx}(A^{m},l)}(r^{m}_{j},\epsilon_{m})$
(+).Because of $\widehat{G}\models^{\mathfrak{s}}\phi_{7}$ we must have
$\widehat{G}\models^{\mathfrak{s}}\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),\mathsf{vtx}(A^{m},l)}(r^{m}_{l},\epsilon_{m})$
for the rule $C\in\mathcal{C}$ such that $\underline{C}(r^{m}_{l})$.With (+)
this establishes
$\widehat{G}\models^{\mathfrak{s}}\mathsf{equal}_{\mathsf{rt}({\mathsf{hd}(C)}),i}(r^{m}_{l},r^{m}_{j})$.Hence,
we have $\xi_{\scriptscriptstyle{G^{m}_{j}}}(i)=r^{m}_{l}$ by the definition
of the sources of $G^{m}_{j}$.By similar arguments, we establish that
$\xi_{\scriptscriptstyle{G}}(i)=r^{m}_{l}$ iff
$\xi_{\scriptscriptstyle{G^{m}}}(i)=\mathsf{vtx}(A^{m},l)$, and that
$\xi_{\scriptscriptstyle{G}}(i)=\xi_{\scriptscriptstyle{G^{m}_{j}}}(i^{\prime})$
iff
$\xi_{\scriptscriptstyle{G^{m}}}(i)=\upsilon_{\scriptscriptstyle{G^{m}}}(e^{m}_{j})_{i^{\prime}}$.With
(#), we then get

$\displaystyle
G=G^{1}[e_{1}^{1}/G_{1}^{1},\ldots,e_{n_{1}}^{1}/G_{n_{1}}^{1}]\cdots\parallel_{1}G^{m}[e_{1}^{m}/G_{1}^{m},\ldots,e_{n_{m}}^{m}/G_{n_{m}}^{m}]\parallel_{1}\cdots$
$\displaystyle\qquad\qquad\parallel_{1}G^{k}[e_{1}^{k}/G_{1}^{k},\ldots,e_{n_{k}}^{k}/G_{n_{k}}^{k}](*).$

Now, let $C=u\rightarrow
w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}\in\mathcal{C}$ be the rule such
that $\underline{C}(r)$.Let $w\in\mathcal{U}\setminus\mathcal{W}$ be some non-
terminal. Let $p$ be the number of times $w$ appears among the
$w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}$.Let $q$ be the number such that
there is a rule $u\rightarrow u\parallel_{1}w^{q}\in\mathcal{B}$ (we recall
that there is at most one rule of this shape), and let $q=0$, otherwise.
Because of $\widehat{G}\models\psi(u)$ there are at least $p$ edges among the
$e_{1},\ldots,e_{k}$, which are labelled by rules with head $w$, and the
number of these edges equals $p$ modulo $q$.As this holds for every
$w\in\mathcal{U}\setminus\mathcal{W}$, we can apply zero or more times rules
$B\in\mathcal{B}$, followed by a single application of rule $C=u\rightarrow
w_{1}\parallel_{1}\ldots\parallel_{1}w_{n}\in\mathcal{C}$, in order to obtain
a partial derivation that can be summarized as $u\rightarrow
w_{1}\parallel_{1}\cdots\parallel_{1}w_{k}$,where $w_{m}$ is the head of the
rule $A^{m}\in\mathcal{A}$. Then, we continue the derivation by applying the
rule $A^{m}$ for every $m\in[1,k]$ in order to obtain the partial derivation

$\displaystyle
u\rightarrow{G^{1}}[{e_{1}^{1}}({u_{1}^{1}}),\ldots,{e_{n_{1}}^{1}}({u_{n_{1}}^{1}})]\parallel_{1}\cdots\parallel_{1}{G^{1}}[{e_{1}^{m}}({u_{1}^{m}}),\ldots,{e_{n_{m}}^{m}}({u_{n_{m}}^{m}})]\parallel_{1}\cdots$
$\displaystyle\qquad\qquad\parallel_{1}{G^{1}}[{e_{1}^{k}}({u_{1}^{k}}),\ldots,{e_{n_{k}}^{k}}({u_{n_{k}}^{k}})].$

This partial derivation together with (*) and
$G^{m}_{j}\in\mathcal{L}_{\Gamma}({u^{m}_{j}})$ then establishes
$G\in\mathcal{L}_{\Gamma}({u})$.The rest of this section is concerned with
proving a partialcompleteness result. We define a parameter, called
_embeddable tree-width_ , which is an over-approximation of the standardtree-
width of a graph. We show that the class of $\mathsf{CMSO}$-definable setsof
graphs, for which the embeddable tree-width is bounded, coincideswith the
class of tree-verifiable graph languages.Before defining embeddable tree-width
formally, we recall the standarddefinitions of _tree decomposition_ and
_treewidth_ of ac-graph, by considering trees over an alphabet of edge labels
thatconsists of a single binary element:

######  Definition 5.

A _tree decomposition_ of a c-graph $G$ of type $n$ is a pair$(T,\beta)$,
where $T$ is a tree, called _backbone_ , and
$\beta:V_{\scriptscriptstyle{T}}\rightarrow\mathrm{pow}({V_{\scriptscriptstyle{G}}})$
maps the vertices of $T$ intosets of vertices from $G$, such that:

  1. 1.

for each
$e\in{E}_{\scriptscriptstyle{G}}$,$\upsilon_{\scriptscriptstyle{G}}(e)=\langle{v_{1},\ldots,v_{k}}\rangle$,
there exists$n\in V_{\scriptscriptstyle{T}}$ such that
$v_{1},\ldots,v_{k}\in\beta(n)$,

  2. 2.

for each $v\in V_{\scriptscriptstyle{G}}$the set $\\{{n\in
V_{\scriptscriptstyle{T}}\mid v\in\beta(n)}\\}$ isnonempty and connected in
$T$.

The _width_ of the tree decomposition is
$0pt{T,\beta}\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\max_{n\in
V_{\scriptscriptstyle{T}}}\mathrm{card}({\beta(n)})-1$.The _tree-width_ of $G$
is
$\mathrm{tw}({G})\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\min\\{{0pt{T,\beta}\mid(T,\beta)\text{
tree decomposition of }G}\\}$.The tree-width of a graph is the tree-width of
some c-graph from it333Isomorphic c-graphs have equal tree-widths..A set
${\mathcal{G}}$ of graphs has _bounded tree-width_ iff
$\\{{\mathrm{tw}({G})\mid G\in{\mathcal{G}}}\\}$ is a finite set.

We refine the above definition by considering only backbones that arespanning
trees of the graph. The spanning trees considered cover boththe vertices and
the edges of the graph:

######  Definition 6.

An _embeddable_ tree-decomposition of a c-graph $G$ is atuple
$(T,\beta,\gamma,\delta)$ such that $(T,\beta)$ is atree-decomposition of $G$,
and there is some subset $W\subseteq V_{\scriptscriptstyle{T}}$ of the nodes
of $T$ suchthat:

  * •

the root of $T$ does not belong to $W$,

  * •

for every node $u\in V_{\scriptscriptstyle{T}}$ and every child $w\in
V_{\scriptscriptstyle{T}}$ of $u$, we have $w\in W$ iff $u\not\in W$, i.e.,the
membership in $W$ alternates for the nodes on every path of$T$,

Moreover, $\gamma:V_{\scriptscriptstyle{T}}\setminus W\rightarrow
V_{\scriptscriptstyle{G}}$ is a bijective mapping of the nodes
from$V_{\scriptscriptstyle{T}}\setminus W$ to the vertices of $G$,
and$\delta:W\rightarrow{E}_{\scriptscriptstyle{G}}$ is a bijective mapping
ofthe vertices in $W$ to the edges of $G$, satisfying theconditions:

  1. 1.

for all $u\in V_{\scriptscriptstyle{T}}\setminus W$ we have that
$\gamma(u)\in\beta(u)$, and

  2. 2.

for all $w\in W$ and $e=\delta(w)$ we have

     * •

if $w$ is the child of $u$ in $T$ then there is some
$i\in[{1},{{\\#{\lambda_{\scriptscriptstyle{G}}(e)}}}]$ such
that$\upsilon_{\scriptscriptstyle{G}}(e)_{i}=\gamma(u)$,

     * •

for every child $v$ of $w$ in $T$ there is adistinct
$j\in[{1},{{\\#{\lambda_{\scriptscriptstyle{G}}(e)}}}]\setminus\\{{i}\\}$
suchthat $\upsilon_{\scriptscriptstyle{G}}(e)_{j}=\gamma(v)$,

     * •

$\upsilon_{\scriptscriptstyle{G}}(e)_{i}\in\beta(w)$ for all $1\leq
i\leq\mathrm{len}({\upsilon_{\scriptscriptstyle{G}}(e)})$.

The _embeddable tree-width_ of $G$ is
$\mathrm{etw}({G})\stackrel{{\scriptstyle\scalebox{0.5}{$\mathsf{def}$}}}{{=}}\min\\{0pt{T,\beta}\mid(T,\beta,\gamma,\delta)\text{
is an embeddable tree decomposition of }G\\}$. Theembeddable tree-width of a
graph is the embeddable tree-width ofsome c-graph from it. A set
${\mathcal{G}}$ of graphs has _boundedembeddable tree-width_ iff
$\\{{\mathrm{etw}({G})\mid G\in{\mathcal{G}}}\\}$ is a finite set.

For example, Fig. 6 shows a graph that is generated by the tree-verifiable
grammar from Example 2 and an embeddable tree decomposition of this graph(this
tree decomposition is the tree decomposition that underlies the proof of
Proposition 0.4).The nodes from the inverseimage of $\gamma$ (resp. $\delta$)
are depicted by filled circles(resp. rectangles).The sets in the image of
$\beta$ (called _bags_) associated with the nodes of the tree decomposition
are stated next to the tree nodes.

$\\{v_{7},v_{11},v_{12}\\}$$v_{5}$$v_{8}$$v_{9}$$v_{10}$$v_{11}$$v_{12}$$v_{2}$$v_{3}$$v_{4}$$v_{7}$$v_{1}$$v_{6}$$e_{1}$$e_{2}$$e_{3}$$e_{4}$$e_{5}$$e_{6}$$e_{7}$$\\{v_{9}\\}$$\\{v_{10}\\}$$\\{v_{11}\\}$$\\{v_{3},v_{10},v_{12}\\}$$\gamma^{-1}(v_{1})$$\delta^{-1}(e_{1})$$\gamma^{-1}(v_{2})$$\gamma^{-1}(v_{3})$$\delta^{-1}(e_{2})$$\delta^{-1}(e_{3})$$\gamma^{-1}(v_{4})$$\gamma^{-1}(v_{6})$$\gamma^{-1}(v_{10})$$\gamma^{-1}(v_{7})$$\delta^{-1}(e_{7})$$\gamma^{-1}(v_{11})$$\\{v_{5},v_{9},v_{10}\\}$$\delta^{-1}(e_{6})$$\delta^{-1}(e_{5})$$\gamma^{-1}(v_{5})$$\delta^{-1}(e_{4})$$\\{v_{6},v_{10},v_{11}\\}$$e_{0}$$\gamma^{-1}(v_{12})$$\delta^{-1}(e_{0})$$\\{v_{3},v_{6},v_{7},v_{10},v_{11},v_{12}\\}$$\\{v_{2},v_{8},v_{10}\\}$$\\{v_{2},v_{4},v_{5},v_{8},v_{9},v_{10}\\}$$\\{v_{4},v_{8},v_{9}\\}$$\\{v_{7},v_{11},v_{12}\\}$$\\{v_{1},v_{2},v_{3},v_{8},v_{10},v_{12}\\}$$\\{v_{1},v_{12}\\}$$\\{v_{1},v_{12}\\}$$\\{v_{12}\\}$$\\{v_{8}\\}$$\gamma^{-1}(v_{8})$$\gamma^{-1}(v_{9})$$\\{v_{4},v_{8},v_{9}\\}$$\\{v_{5},v_{9},v_{10}\\}$$\\{v_{6},v_{10},v_{11}\\}$

Figure 6: Embeddable Tree Decomposition

The following variation ofDef. 6 will be useful forworking with the notion of
an embeddable tree-decomposition inanalyzing graph grammars and for conducting
inductive proofs aboutgraph grammars:

######  Definition 7.

Let $G$ be c-graph $G$ of type $n$ and let $z\in[{1},{n}]$ and
$\pi\subseteq[{1},{n}]\setminus\\{{z}\\}$. We consider a tuple
$(T,\beta,\gamma,\delta)$and subset $W\subseteq V_{\scriptscriptstyle{T}}$
such that the conditions ofDef. 6 are satisfied, exceptfor the bijectivity
requirement on $\gamma$, and the requirementthat the root of $T$ does not
belong to $W$. Let $r$ be theroot of $T$. We now call
$(T,\beta,\gamma,\delta)$ a _$(z,\pi)$ -embeddable tree-decomposition_ of
$G$iff the following hold:

  1. 1.

$\xi_{\scriptscriptstyle{G}}(i)\in\beta(r)$ for all $i\in[{1},{n}]$,

  2. 2.

$\gamma:V_{\scriptscriptstyle{T}}\setminus
W\rightarrow\mathsf{intern}({G})\cup A$ is a bijective mapping of the
verticesin $V_{\scriptscriptstyle{T}}\setminus W$ to the internal vertices
of$G$ plus the set $A=\pi$ in case of $r\in W$ and $A=\\{z\\}\cup\pi$
otherwise,

  3. 3.

if $r\in W$ then there is some
$i\in[{1},{{\\#{\lambda_{\scriptscriptstyle{G}}(\delta(r))}}}]$ such
that$\upsilon_{\scriptscriptstyle{G}}(\delta(r))_{i}=\xi_{\scriptscriptstyle{G}}(z)$
and$\gamma(u)\neq\xi_{\scriptscriptstyle{G}}(z)$ for every child $u$ of$r$,

  4. 4.

else ($r\in V_{\scriptscriptstyle{T}}\setminus W$) we have
that$\gamma(r)=\xi_{\scriptscriptstyle{G}}(z)$.

We call the tree-decomposition _pointed_ , if $r\in W$, and _non-pointed_ ,
otherwise.

To begin with, we note that tree-verifiable graph grammars are set upsuch that
the resulting languages always have bounded embeddabletree-width:Let
$\mathcal{L}$ be a tree-verifiable set of graphs.Then, $\mathcal{L}$ has
bounded embeddable tree-width.In more detail, given a tree-verifiablegraph-
grammar $\Gamma=(\mathcal{U},\mathcal{R})$, let $k$ be the maximum of
$\mathrm{card}({V_{\scriptscriptstyle{G}}})$ for the graphs $G$appearing in
$\mathcal{R}$ of shape A and the maximum of $\\#{u}$ for all non-terminals
$u\in\mathcal{U}$;then we have $\mathrm{etw}({G})\leq k$ for all
$G\in\mathcal{L}({\Gamma})$.Let $\Gamma=(\mathcal{U},\mathcal{R})$ be some
tree-verifiablegraph-grammar such that $\mathcal{L}=\mathcal{L}({\Gamma})$,
with $\mathcal{W}\subseteq\mathcal{U}$ for some subset of the non-terminals.
Let $k$be the maximum of $\mathrm{card}({V_{\scriptscriptstyle{G}}})$ for the
graphs $G$appearing in $\mathcal{R}$ ofshape A and the maximum of $\\#{u}$ for
all non-terminals $u\in\mathcal{U}$.We now prove for every$v\in\mathcal{U}$
and $G\in\mathcal{L}_{\Gamma}({v})$ that there isa
$(\mathsf{rt}({v}),\mathsf{fut}({v}))$-embeddable tree-decomposition withwidth
$\leq k$. Further, this tree-decomposition is pointed iff $v\in\mathcal{W}$.
The proof proceeds by induction on the length ofthe derivation of
$G\in\mathcal{L}_{\Gamma}({v})$.We first consider a nonterminal
$u\in\mathcal{U}\setminus\mathcal{W}$ and a graph
$G\in\mathcal{L}_{\Gamma}({v})$. Let $n={\\#{u}}$. We have that the derivation
of $G\in\mathcal{L}_{\Gamma}({u})$ starts with several applications of rules
ofshape $u\rightarrow u\parallel_{n}w^{q}$, followed by oneapplication of
shape $u\rightarrow w_{1}\parallel_{n}\ldots\parallel_{n}w_{k}$. In summary,
we have $G=G^{1}\parallel_{n}G^{2}\parallel_{n}\dots$ for some graphs
$G^{j}\in\mathcal{L}_{\Gamma}({w_{j}})$ and non-terminals
$w_{j}\in\mathcal{W}$.In particular, we can assume that the edges of the
graphs $G^{j}$are disjoint and that the only common vertices of $G^{j}$
areamong the vertices $[1,n]$. By induction assumption we have thatthere is a
pointed $(\mathsf{rt}({w_{j}}),\mathsf{fut}({w_{j}}))$-embeddabletree-
decomposition $(T^{j},\beta^{j},\gamma^{j},\delta^{j})$ of$G^{j}$ with width
$\leq k$ and a corresponding subset $W^{j}\subseteq
V_{\scriptscriptstyle{T^{j}}}$. We now construct a tree $T$ byadding a fresh
root vertex $r$ that we connect to the roots $r^{j}$ ofthe trees $T^{j}$, and
we set $W=\bigcup_{j}W^{j}$,
$\beta=\\{r\mapsto\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in[1,{\\#{u}}]\\}\\}\cup\bigcup_{j}\beta^{j}$,
$\gamma=\\{r\mapsto\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({u}))\\}\cup\bigcup_{j}\gamma^{j}$
and $\delta=\bigcup_{j}\delta^{j}$. It is now easy to verify
that$(T,\beta,\gamma,\delta)$ is a non-pointed
$(\mathsf{rt}({u}),\mathsf{fut}({u}))$-embeddable tree-decomposition with
width $\leq k$; wenote that the bijectivity requirement of $\gamma$ is
satisfiedbecause of the side-conditions $\mathsf{rt}({w})=\mathsf{rt}({u})$
and$\mathsf{fut}({w})=\emptyset$ of the rules ofshape B and theside-conditions
$\mathsf{rt}({u})=\mathsf{rt}({w_{i}})$ and
$\mathsf{fut}({u})=\biguplus_{i=1..l}\mathsf{fut}({u_{i}})$ of the rules
ofshape C.We now consider a nonterminal $w\in\mathcal{W}$ and a
graph$G\in\mathcal{L}_{\Gamma}({w})$. We have that there is anapplication of
some rule $w\rightarrow{G^{\circ}}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]$,
for some $u_{1},\ldots,u_{k}\in\mathcal{U}\setminus\mathcal{W}$. Let $e$ be
the single terminaledge of $G^{\circ}$. We have that there are some
graphs$G^{j}\in\mathcal{L}_{\Gamma}({u_{j}})$ such that
$G=G^{\circ}[e_{1}/G^{1},\ldots,e_{k}/G^{k}]$. In particular, wecan assume
that the edges of the graphs $G^{j}$ are disjoint andthat the only common
vertices of $G^{j}$ are among the$V_{\scriptscriptstyle{G^{\circ}}}$. By
induction assumption we have that thereis a non-pointed
$(\mathsf{rt}({u_{j}}),\mathsf{fut}({u_{j}}))$-embeddabletree-decomposition
$(T^{j},\beta^{j},\gamma^{j},\delta^{j})$ of$G^{j}$ with width $\leq k$ and a
corresponding subset $W^{j}\subseteq V_{\scriptscriptstyle{T^{j}}}$. We now
construct a tree $T$ byadding a fresh root vertex $r$ that we connect to the
roots $r^{j}$ ofthe trees $T^{j}$, and we set
$W=\\{r\\}\cup\bigcup_{j}W^{j}$,$\beta=\\{r\mapsto
V_{\scriptscriptstyle{G^{\circ}}}\\}\cup\bigcup_{j}\beta^{j}$,
$\gamma=\bigcup_{j}\gamma^{j}$ and $\delta=\\{r\mapsto
e\\}\bigcup_{j}\delta^{j}$. It isnow easy to verify that
$(T,\beta,\gamma,\delta)$ is anon-pointed
$(\mathsf{rt}({u}),\mathsf{fut}({u}))$-embeddabletree-decomposition with width
$\leq k$; we note that the bijectivityrequirement of $\gamma$ is satisfied
because of the side-
condition$\mathsf{intern}({G^{\circ}})\cup\\{\xi_{\scriptscriptstyle{G^{\circ}}}(i)\mid
i\in\mathsf{fut}({w})\\}=\biguplus_{i=1..k}(\\{\mathsf{rt}({u_{i}})\\}\uplus\\{\upsilon_{\scriptscriptstyle{G^{\circ}}}(u_{i})_{j}\mid
j\in\mathsf{fut}({u_{i}})\\})$ ofthe rules of shape C.We finally consider some
axiom $\rightarrow u$ for some $u\in\mathcal{U}\setminus\mathcal{W}$ with
$[1,{\\#{u}}]=\\{\mathsf{rt}({u})\\}\cup\mathsf{fut}({u})$ (*) and some graph
$G\in\mathcal{L}_{\Gamma}({u})$. By the above we have that there is
some$(\mathsf{rt}({u}),\mathsf{fut}({u}))$-embeddable tree-
decomposition$(T,\beta,\gamma,\delta)$ with width $\leq k$ for $G$.Because of
(*) we have that $\gamma:V_{\scriptscriptstyle{T}}\setminus W\rightarrow
V_{\scriptscriptstyle{G}}$ is a bijective mapping of the verticesin
$V_{\scriptscriptstyle{T}}\setminus W$ to the vertices of $G$.
Hence,$(T,\beta,\gamma,\delta)$ is an embeddable tree-
decomposition$(T,\beta,\gamma,\delta)$ and we have
established$\mathrm{etw}({G})\leq k$.We now prove the existence of a tree-
verifiable grammar that generatesall graphs with embeddable treewidth $\leq n$
for some given $n\in{\rm Nature}$. While the existence of such a grammar is an
interesting resulton its own, we will build on this result in our partial
completenessproof (Theorem 0.4), wherewe pair the non-terminals of this
grammar with the equivalence classesof some congruence relation.For each
finite alphabet $\mathbb{A}$ of edge labels and each $n\in{\rm Nature}$, there
exists a tree-verifiable grammar $\Gamma$, such
that$\mathcal{L}({\Gamma})=\\{{G\in{\mathcal{G}^{\scriptscriptstyle{\mathbb{A}}}}{}\mid
G\text{ has type }0\text{ and }\mathrm{etw}({G})\leq n}\\}$.We consider the
set of non-terminals

$\mathcal{U}=\\{u^{z,\pi,m},w^{z,\pi,m}\mid m\in[0,n],z\in[1,m]\text{ and
}\pi\subseteq[1,m]\setminus\\{z\\}\\},$

with${\\#{x^{z,\pi,m}}}=m$ for all $x\in\\{u,w\\}$, $m\in[0,n]$, $z\in[1,m]$
and $\pi\subseteq[1,m]\setminus\\{z\\}$. Then, we
set$\mathcal{W}=\\{w^{z,\pi,m}\mid m\in[0,n],i\in[1,m]\text{ and
}\pi\subseteq[1,m]\\}$, aswell as $\mathsf{rt}({x^{z,\pi,m}})=z$
and$\mathsf{fut}({x^{z,\pi,m}})=\pi$ for all $x\in\\{u,w\\}$, $m\in[0,n]$,
$z\in[1,m]$ and $\pi\subseteq[1,m]\setminus\\{z\\}$. We define thetree-
verifiable graph grammar $\Gamma=(\mathcal{U},\mathcal{R})$ bythe following
rules:

  1. A.

$w\rightarrow{G}[{e_{1}}({u_{1}}),\ldots,{e_{k}}({u_{k}})]$, for
some$w\in\mathcal{W}$ and
$u_{1},\ldots,u_{k}\in\mathcal{U}\setminus\mathcal{W}$, where $G$ has exactly
one terminal edge $e$,$\mathrm{card}({V_{\scriptscriptstyle{G}}})\leq n$,
vertex $\xi_{\scriptscriptstyle{G}}(\mathsf{rt}({w}))$ is incident to
$e$,vertex $\upsilon_{\scriptscriptstyle{G}}(e_{i})_{\mathsf{rt}({u_{i}})}$ is
incident to$e$ for every non-terminal $u_{i}$, and we have:

$\displaystyle\mathsf{intern}({G})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\mathsf{fut}({w})\\}=\biguplus_{i=1..k}(\\{\upsilon_{\scriptscriptstyle{G}}(e_{i})_{j}\mid
j\in\\{\mathsf{rt}({u_{i}})\\}\cup\mathsf{fut}({u_{i}}))$

  2. B.

$u\rightarrow u\parallel_{m}w$, where
$u\in\mathcal{U}\setminus\mathcal{W}$,$w\in\mathcal{W}$ with
${\\#{u}}={\\#{w}}=m$, suchthat $\mathsf{rt}({w})=\mathsf{rt}({u})$ and
$\mathsf{fut}({w})=\emptyset$,

  3. C.

$u\rightarrow w_{1}\parallel_{m}\ldots\parallel_{m}w_{k}$, where
$u\in\mathcal{U}\setminus\mathcal{W}$, $w_{1},\ldots,w_{k}\in\mathcal{W}$with
${\\#{u}}={\\#{w_{i}}}=m$, such that $\mathsf{rt}({u})=\mathsf{rt}({w_{i}})$,
$\mathsf{fut}({u})=\biguplus_{i=1..k}\mathsf{fut}({u_{i}})$and
$\mathsf{fut}({u_{i}})\neq\emptyset$ for all $i\in[2,k]$.

We further add axioms of the shape $\rightarrow u^{z,\pi,m}$ for all
$m\in[0,n]$, $z\in[1,m]$ and $\pi=[1,m]\setminus\\{z\\}$.First, we prove that
$\mathcal{R}$ is finite. There are only finitelymany rules of shape A because
of $\mathrm{card}({V_{\scriptscriptstyle{G}}})\leq n$, there are only finitely
many non-terminals $\mathcal{U}$ and finitely many different edge labels
$a\in\mathbb{A}$ for $e$, and we have
$k<{\\#{a}}={\\#{\lambda_{\scriptscriptstyle{G}}(e)}}$ because of
therequirement that the roots of all non-terminals must be pairwise
different.There clearly are only finitely many rules ofshape B because there
are onlyfinitely many non-terminals $\mathcal{U}$. There are only finitelymany
rules of shape C becausethere are only finitely many non-terminals
$\mathcal{U}$ and theconstraint
$\mathsf{fut}({u})=\biguplus_{i=1..k}\mathsf{fut}({u_{i}})$ requiresthe
partitioning of $\mathsf{fut}({u})$ into sets $\mathsf{fut}({u_{i}})$,
whichneed to be non-empty for all $i\in[2,k]$, and there are onlyfinitely many
ways to partition a finite set into non-empty subsets.We now prove that
$\mathcal{L}({\Gamma})$ consists of all graphs over $\mathbb{A}$ with
embeddable tree-width $\leq n$.We first observe that $\mathrm{etw}({G})\leq n$
for all $G\in\mathcal{L}({\Gamma})$, by Proposition 0.4.We now show that
$\Gamma$ can indeed generate all graphs with embeddable tree-width $\leq n$.In
order to do so, we prove the following more general
statement:Let$(T,\beta,\gamma,\delta)$ be a $(z,\pi)$-embeddabletree-
decomposition, with width $\leq n$, of graph $G$ with type$m$. Then,
$G\in\mathcal{L}_{\Gamma}({w^{z,\pi,m}})$ in case thetree-decomposition is
pointed, and $G\in\mathcal{L}_{\Gamma}({u^{z,\pi,m}})$ otherwise. The
proofproceeds by induction on the height of the tree-
decomposition$(T,\beta,\gamma,\delta)$. Let $r$ be the root of $T$. Forevery
child $r^{j}$ of $r$ we consider the induced
tuple$(T^{j},\beta^{j},\gamma^{j},\delta^{j})$, where $T^{j}$ is thesubtree of
$T$ rooted in $r_{j}$, and $\beta^{j},\gamma^{j},\delta^{j}$are obtained by
restricting the functions $\beta,\gamma,\delta$ tothe vertices of $T^{j}$.We
first assume that the tree-decomposition is pointed. Then, wehave
$\delta(r)=e\in{E}_{\scriptscriptstyle{G}}$ such that for every child$r^{j}$
of $r$ in $T$ that there is some
$i\in[1,{\\#{\lambda_{\scriptscriptstyle{G}}(e)}}]$ with
$\upsilon_{\scriptscriptstyle{G}}(e)_{i}=\gamma(r)$. Let $k$ be the number of
children $r_{j}$ of $r$ (we notethat
$k<{\\#{\lambda_{\scriptscriptstyle{G}}(e)}}$ because of the requirementthat
children are attached to pairwise different vertices). Let
$V=\beta(r)\cup\bigcup_{j\in[1,k]}\beta(r^{j})$ be the verticesassociated to
the bags of $r$ and the $r_{j}$ in thetree-decomposition. Let
$m^{j}=\mathrm{card}({\beta(r^{j})})$. Let$v_{1}^{j},\ldots,v_{m^{j}}^{j}$ be
some fixed enumeration of thevertices of the bag $\beta(r^{j})$. We consider
the graph $G^{j}$that is obtained by restricting $G$ to the images of
$\gamma^{j}$and $\delta^{j}$ and whose sources are defined by
setting$\xi_{\scriptscriptstyle{G^{j}}}(i)=v_{i}^{j}$ for all $i\in[1,m^{j}]$.
Let$z^{j}\in[1,m^{j}]$ be the index such that $v_{i}^{j}=\gamma(r_{j})$ and
let $\pi^{j}=\\{i\in[1,m^{j}]\mid
v_{i}^{j}\in\mathrm{img}({\gamma^{j}})\\}\setminus\\{z^{j}\\}$ be the subset
of theindices whose associated vertices appear in the image of $\gamma^{j}$.We
now recognize that $(T^{j},\beta^{j},\gamma^{j},\delta^{j})$ is anon-pointed
$(z^{j},\pi^{j})$-embeddable tree-decomposition of$G^{j}$. By induction
assumption we have that
$G^{j}\in\mathcal{L}_{\Gamma}({u^{z^{j},\pi^{j},m^{j}}})$. We now definethe
graph $G^{\circ}$ to consist of the vertices $V_{G}$, the samesources as $G$
(i.e., we set
$\xi_{\scriptscriptstyle{G^{\circ}}}(i)=\xi_{\scriptscriptstyle{G}}(i)$ for
all $i\in[1,m]$), the single terminaledge $e$, and some non-terminal edges
$e_{1},\ldots,e_{k}$,
with$\upsilon_{\scriptscriptstyle{G^{\circ}}}(e_{j})=\left\langle
v_{1}^{j},\ldots,v_{\mathrm{card}({\beta(r^{j})})}^{j}\right\rangle$, labelled
by the non-
terminals$u^{z^{1},\pi^{1},m^{1}},\ldots,u^{z^{k},\pi^{k},m^{k}}$.We note that
we have $G=G^{\circ}[e_{1}/G^{1},\ldots,e_{k}/G^{k}]$. We further notethat we
have $\mathsf{intern}({G^{\circ}})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\pi\\}=\biguplus_{j=1..k}(\\{\upsilon_{\scriptscriptstyle{G}}(e_{j})_{i}\mid
i\in\\{z^{j}\\}\cup\pi^{j}),$ because of
$V=\beta(r)\cup\bigcup_{j\in[1,k]}\beta(r^{j})$,
$\beta(r)=\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in[1,m]\\}$,$\gamma=\bigcup_{j\in[1,k]}\gamma^{j}$ and
$\gamma:V_{\scriptscriptstyle{T}}\setminus
W\rightarrow\mathsf{intern}({G})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in\pi)\\}$ is a bijectivefunction. Hence, we can infer
$G\in\mathcal{L}_{\Gamma}({w^{z,\pi,m}})$ by an application of arule of shape
A.We now assume that the tree-decomposition is non-pointed. Weconsider the
graph $G^{j}$ that is obtained by restricting$G$ to the images of $\gamma^{j}$
and $\delta^{j}$ and that has thesame sources as $G$, i.e., we set
$\xi_{\scriptscriptstyle{G^{j}}}(i)=\xi_{\scriptscriptstyle{G}}(i)$ for all
$i\in[1,m]$. We note that$\\{\xi_{\scriptscriptstyle{G^{j}}}(i)\mid
i\in[1,m]\\}=\beta^{j}(r^{j})$because we have that $\beta^{j}(r^{j})=\beta(r)$
and$\\{\xi_{\scriptscriptstyle{G}}(i)\mid i\in[1,m]\\}=\beta(r)$ from
theassumption that $(T,\beta,\gamma,\delta)$ is a $(z,\pi)$-embeddable tree-
decomposition of $G$. We now
set$\pi^{j}=\\{i\in[1,m]\mid\xi_{\scriptscriptstyle{G^{j}}}(i)\in\mathrm{img}({\gamma^{j}})\\}$
as the subset of the sources that appear in theimage of $\gamma^{j}$. We now
recognize that$(T^{j},\beta^{j},\gamma^{j},\delta^{j})$ is a
pointed$(z,\pi^{j})$-embeddable tree-decomposition of $G^{j}$.By induction
assumption we have that $G^{j}\in\mathcal{L}_{\Gamma}({w^{z,\pi^{j},m}})$. We
note that wehave $\pi=\biguplus_{j}\pi^{j}$ because
$\gamma:V_{\scriptscriptstyle{T}}\setminus
W\rightarrow\mathsf{intern}({G})\cup\\{\xi_{\scriptscriptstyle{G}}(i)\mid
i\in(\\{z\\}\cup\pi)\\}$ is abijective function and we have the following
partitioning
$\gamma=\\{r\mapsto\xi_{\scriptscriptstyle{G}}(z)\\}\cup\bigcup_{j}\gamma^{j}$.Hence,
we can infer $G\in\mathcal{L}_{\Gamma}({u^{z,\pi,m}})$ by applying rules
ofshape B as often as neededfollowed by a single application of a rule ofshape
C.We finally consider some graph $H$ of type $0$ for which there is an
embeddable tree-decomposition$(T,\beta,\gamma,\delta)$ of width $\leq n$. Let
$m=\mathrm{card}({\beta(r)})$ for the root $r$ of $T$. Note that $m\leq n$.
Let $v_{1},\ldots,v_{m}$ be some fixed enumeration of$\beta(r)$. We now define
the $G$ of type $m$ as theextension of $H$ with the sources $[1,m]$ by
setting$\xi_{\scriptscriptstyle{G}}(i)=v_{i}$ for all $i\in[1,m]$. We
nowchoose $z\in[1,m]$ such that $\gamma(r)=v_{z}$. Wefurther set
$\pi=[1,m]\setminus\\{z\\}$. We nowrecognize that $(T,\beta,\gamma,\delta)$ is
a $(z,\pi)$-embeddable tree-decomposition of graph $G$. By theabove, we get