Database Reference
In-Depth Information
•
each
p
-port is evaluated to
p
;
the only child of each
p
,
p
-port
u
is evaluated to
p
,and
u
evaluates to
p
;
•
if
u
is a
q
,
q
-port, the horizontal automaton arrives at
u
in state
q
and leaves in state
q
.
•
More precisely, we assume that each port
u
is labeled with a unique label
◦
u
and we con-
sider an accepting run of
A
extended with the following transition rules for each
u
:
δ
(
p
,
◦
u
)=
ε
if
u
is a
p
-port,
(
p
,
if
u
is a
p
,
p
-port,
δ
◦
u
)=
p
q
if
u
is a
q
,
q
-port,
δ
(
p
u
,
◦
u
)=
ε
and
q
,
p
u
→
where
p
u
is a fresh state.
Thus, if a tree
T
is obtained from
K
by substituting compatible forests or contexts, an
accepting run of
A
over
T
can be obtained by combining an accepting run over
K
with
runs witnessing compatibility. In consequence, if
K
admits an accepting run of
A
,then
L
(
K
)
⊆
L
(
A
).
Lemma 12.20
Every T
∈
L
(
A
)
agrees with some
A
-kind K of branching and size
bounded by
A
, admitting an accepting run.
Proof
Fix an accepting run
on
T
, together with witnessing runs of the horizontal
automata. Prune
T
introducing ports as stubs according to the following rules.
First, each maximal forest such that the witnessing horizontal run in its roots stays within
some (horizontal) SCC is replaced with a
q
,
q
-port, where
q
,
q
are the first and the last
state of the corresponding fragment of the run.
Next, all maximal subtrees that evaluate to a state
p
, which is contained in a branching
SCC of
λ
of
A
, are replaced with a
p
-port.
Finally, for each nonbranching SCCs
X
, consider the maximal paths of length at least
2 where the run stays in
X
.Since
X
is nonbranching, the paths are disjoint. Replace the
subtree rooted at the top end of the path with a
p
,
p
-port for suitable
p
,
p
, and under it put
the subtree originally rooted at the bottom end of the path.
Note that the result of this procedure depends on the order in which the nonbranching
SCCs are processed.
Let
K
be the resulting kind. By construction
T
A
L
(
K
). The bounds on the height and
branching of
K
follow from the observation that no state and no SCC occurs more than
once in a sequence of children, or a branch.
∈
+
, ,
) is just like for the case of SM
nr
(
The solution-building algorithm for SM(
↓
∼
⇓
,
∼
),
except that we use
A
-kinds admitting an accepting run of
A
instead of
D
t
-kinds, where
A
is the UNFTA underlying the target schema.
+
, ,
Theorem 12.21
For each mapping
)
,
Algorithm 12.3
computes a solu-
tion for a source tree T (or determines that it does not exist) in polynomial time.
M ∈
SM(
↓
∼
