Database Reference
In-Depth Information
Lemma 12.24
Let
λ
be a run over K with margins of size m. For all T
1
,
T
2
,...,
T
n
∈
L
(
K
)
and every pattern
π
of size at most m,
T
1
⊕
m
T
2
⊕
m
···⊕
m
T
n
|
=
π
(
a
)
whenever
T
i
|
=
π
(
a
)
for some i
.
Before giving the proof, we show how
Lemmas 12.23
and
12.24
lead to a general
solution-building algorithm.
Algorithm 12.4 Building solutions for SM(
⇓
,
⇒
,
∼
)
Require:
M
=(
S
s
,
S
t
,
Σ
)
∈
SM(
⇓
,
⇒
,
∼
),
T
|
=
S
s
,and
S
t
=(
A
,
Attr
)
compute
Δ
T
,M
m
:= max
δ
∈
Δ
T
,M
δ
n
:=
A
A
+max
δ
∈
Δ
T
,M
δ
D
:=
d
d
is used in
T
∪{⊥
0
,⊥
1
,...,⊥
n
}
for all
A
-kinds
K
of height and branching at most (2
m
+ 1)
A
, data values in
D
,
admitting an accepting run with margins of size
m
do
for all δ
∈
Δ
T
,M
do
find
S
δ
∈
L
(
K
) with data values in
D
and a witnessing substitution of forests and
contexts of height and branching at most
A·
(2+
δ
), satisfying
S
δ
|
=
δ
end for
if all
S
δ
found then return
δ
∈
Δ
T
,M
S
δ
end for
if no success for each
K
return '
T
has no solution with respect to
M
'
Theorem 12.25
For each mapping
)
,
Algorithm 12.4
computes a solu-
tion for a source tree T (or determines that it does not exist) in polynomial time.
M ∈
SM(
⇓
,
⇒
,
∼
Proof
Let
m
be the maximal size of target side patternsin
. The only modification
needed in the argument in
Theorem 12.21
is that we only consider kinds admitting runs
with margins of size
m
, the operation
M
⊕
is replaced by
⊕
m
,and
Lemmas 12.19
and
12.20
are replaced by
Lemmas 12.24
and
12.23
, respectively.
It remains to prove
Lemma 12.24
. From the point of view of a single
T
i
,thetree
T
1
⊕
m
T
2
⊕
m
···⊕
m
T
n
is obtained from
T
i
by extending the forests/contexts substituted at the
ports, according to some rules. An
m-safe extension
of
T
at port
u
is obtained by replacing
T
u
with any compatible
forest of the form
F
+
T
u
+
F
,if
u
is a forest port;
•
T
u
,if
u
is a tree port;
•
·
tree of the form
C
T
u
·
C
,if
u
is a context port.
•
context of the form
C
·
Atree
T
∈
L
(
K
) is an
m-safe extension
of
T
∈
L
(
K
) if it is obtained from
T
by simultane-
ous
m
-safe extensions at different ports.
