Database Reference
In-Depth Information
is that the size of such an object is at most single-exponential in the size of the automaton
that gives rise to it.
Lemma 12.18
Let
A
be an UNFTA.
Fo r a l l s t a t e s q
,
q
from the same SCC of one of
•
A
's horizontal automata, there exist a
single exponential q
,
q
-forest.
Fo r a l l s t a t e s p
,
p
from the same SCC of
, there exists a single exponential p
,
p
-
•
A
context.
•
Fo r a l l s t a t e s p
,
p
,
p
from the same branching SCC of
A
, there exists a single expo-
nential p
,
p
,
p
-multicontext.
Proof
Assume that
q
,
q
belong to the same SCC of a horizontal automaton
B
. Then there
starting in
q
and ending in
q
. For each
i
we can find a single exponential
r
i
-tree
S
i
: branching can be bounded by the
maximal number of states of the horizontal automata, and paths' lengths need not exceed
the number of states of
is a sequence of states
r
1
r
2
...
r
m
of
A
that admits a run of
B
.Then
S
1
S
2
...
S
m
is a
q
,
q
-forest of single exponential size.
A
p
,
p
-context can be constructed as follows. If there is an edge (
p
,
p
) in
G
A
,then
r
1
r
2
...
r
k
pr
k
+1
r
k
+2
...
r
m
A
(
p
,
∈
δ
and some states
r
1
,
r
2
,...,
r
m
. Hence,
σ
) for some
σ
,
S
k
+1
,
S
k
+2
,...,
S
m
] is a
p
,
p
-context if only
S
i
is an
r
i
-tree for all
i
.Inthe
general case, let the path from
p
to
p
in
G
A
be
r
1
r
2
...
r
m
, with
r
1
=
p
,
r
m
=
p
.A
p
,
p
-
context is obtained by taking
C
1
C
2
...
C
m
−
1
,where
C
i
is an
r
i
,
r
i
+1
-context constructed like
above.
If
X
is a branching SCC, there are
p
0
,
p
1
,
p
2
∈
σ
[
S
1
,
S
2
,...,
S
k
,
◦
X
such that
Q
∗
p
1
Q
∗
p
2
Q
∗
∩
δ
(
p
0
,
σ
)
is nonempty for some
. Hence, a
p
1
,
p
2
,
p
0
-multicontext
M
of exponential size can be
constructed in the same way as above. To obtain a
p
,
p
,
p
-multicontext for arbitrary
p
,
p
,
p
∈
σ
M
(
C
1
,
C
2
),where
C
1
is a
p
,
p
1
-context,
C
2
is a
p
,
p
2
-context, and
X
,take
C
·
C
is a
p
0
,
p
-context.
Regardless of the chosen
F
,
C
,
M
, and the witnessing substitutions, the operation pre-
serves satisfiability of patterns that do not use
+
.
↓
,
→
and
→
+
, ,
Lemma 12.19
Fo r a l l T
1
,
T
2
,...,
T
n
∈
L
(
K
)
and every
π
∈
Π
(
↓
∼
)
,
T
1
⊕
T
2
⊕···⊕
T
n
|
=
π
(
a
)
whenever
T
i
|
=
π
(
a
)
for some i
.
Proof
does not break the descendant relation:
if a node
w
is a descendant of
v
in
T
i
, the corresponding nodes in
T
1
⊕
It is enough to observe that the operation
⊕
T
2
⊕···⊕
T
n
will
also be in this relation.
Based on the above lemma, we can effectively build solutions for mappings that do not
use
+
. The last missing ingredient is to show that one can cover all target trees
with small kinds. Towards this end we need to distinguish kinds that produce only trees
accepted by the UNFTA.
An
accepting run
of
↓
,
→
and
→
-kind
K
must satisfy the usual conditions for ordinary
nodes, and the following rules for the ports:
A
over an
A