Database Reference
In-Depth Information
nonempty for some
σ
∈
Γ
. We speak of strongly connected components (SCCs) of
B
or
A
meaning SCCs of
G
B
and
G
A
, respectively.
The pumping properties of SCCs of
depend on their internal structure. We say that an
SCC is
nontrivial
if it contains an edge (it might have only one vertex though). A nontrivial
SCC
X
of
A
X
such that
Q
∗
p
1
Q
∗
p
2
Q
∗
∩
δ
A
is
branching
if there exist
p
,
p
1
,
p
2
∈
(
p
,
σ
) is
nonempty for some
. If this is not the case,
X
is
nonbranching
.
In the automata version of the notion of kind, which we are about to define, ports come
in three flavors, corresponding to pumpable trees, contexts, and forests. The additional
requirements forests or contexts that can be substituted is given in terms of the UNFTA's
states.
σ
Definition 12.17 Let
A
be an UNFTA. An
A
-kind K
is a multicontext in which each
port belongs to one of the following categories:
•
p-port
, a leaf port decorated with a state
p
contained in a branching SCC of
A
;
p
,
p
-port
, an internal port with a single child, decorated with states
p
,
p
contained in
the same nonbranching SCC of
•
A
;
q
,
q
-port
, a leaf port decorated with states
q
,
q
contained in the same SCC of one of
A
•
's horizontal automata.
By
L
(
K
) we denote the set of trees that
agree
with
K
, i.e., can be obtained from
K
by
com-
patible substitutions
, i.e., by substituting
p
-trees at
p
-ports,
p
,
p
-contexts at
p
,
p
-ports,
and
q
,
q
-forests at
q
,
q
-ports. We refer to the three kinds of ports above as
tree
,
context
,
and
forest
ports.
Trees agreeing with a kind can be combined in a natural way, just like trees conforming
to a nested-relational DTD. Like before, for
T
L
(
K
) there is witnessing substitution
T
u
,
u
ranging over the ports of
K
, such that if we substitute at each port
u
of
K
the forest or
context
T
u
, we obtain
T
. Unlike for nested-relational DTDs, we cannot guarantee that there
is a unique witnessing substitution (
Exercise 16.3
), but as we shall see in
Lemma 12.19
,
this is not a problem. In order to combine
S
,
T
∈
∈
L
(
K
) into a single tree
S
⊕
T
∈
L
(
K
)
we perform the following substitutions at ports of
K
:
if
u
is a
q
,
q
-port
u
, substitute
S
u
+
F
+
T
u
for some
q
,
q
-forest
F
;
•
if
u
is a
p
,
p
-port, substitute
S
u
·
T
u
for some
p
,
p
-context
C
;
•
C
·
•
if
u
is a
p
-port, substitute
M
(
S
u
,
T
u
) for some
p
,
p
,
p
-multicontext
M
.
Multifold
⊕
is performed from left to right, i.e.,
T
1
⊕
T
2
⊕···⊕
T
n
=(
...
(
T
1
⊕
T
2
)
⊕
...
)
⊕
T
n
.
The result of the operation
depends on the choice of
F
,
C
,
M
. The existence of small
F
,
C
,
M
is guaranteed by the following lemma. In this lemma and elsewhere we shall be
talking of “single-exponential” objects (e.g., forests or multicontexts); the meaning of this
⊕
