Database Reference
In-Depth Information
This ensures that for each state we either have a
yes
-node or a
no
-node.
Next, we make sure that the
yes
/
no
nodes are properly assigned in the leaves, and then
properly propagated up the tree,
//
node
[
state
(
x
)
/
no
,
label
(
u
)
,
leaf
]
−→
−→ ∃
y
r
[
→
state
(
y
)
,
nontr
(
y
,
y
,
u
,
x
)]
,
//
node
[
state
(
x
)
/
no
,
label
(
u
)
,
node
/
state
(
y
)
/
yes
→
node
/
state
(
z
)
/
yes
]
−→
−→
r
/
nontr
(
y
,
z
,
u
,
x
)
.
Finally, check that the run is rejecting,
r
/
node
/
state
(
x
)
/
yes
−→
r
/
state
(
x
)
/
reject
.
Let us see that membership in the composition of
M
12
=(
D
1
,
D
2
,
0) and
M
23
=
(
D
2
,
D
3
,
Σ
23
) is indeed E
XPTIME
-hard.
Take an automaton
A
=
Γ
,
Q
,
δ
,
q
0
,
F
with
Γ =
{
a
1
,
a
2
,...,
a
m
}
and
Q
=
{
q
0
,
q
1
,...,
q
n
}
. Without
loss of general-
ity we may assume that
F
=
{
q
k
,
q
k
+1
,...,
q
m
}
.Let
Q
×
Q
×
Γ
×
Q
\
δ
=
{
. Encode
A
as a tree
T
A
defined as
r
,
state
(
q
0
)
/
reject
,
state
(
q
1
)
/
reject
,...,
state
(
q
k
−
1
)
/
reject
,
state
(
q
k
)
,
state
(
q
k
+1
)
,...,
state
(
q
n
)
,,
label
(
a
1
)
,
label
(
a
2
)
,...,
label
(
a
m
)
,,
nontr
(
p
1
,
r
1
,
b
1
,
s
1
)
,
nontr
(
p
2
,
r
2
,
b
2
,
s
2
)
,...,
nontr
(
p
,
r
,
b
,
s
)
.
Proving that
A
rejects some tree if and only if (
r
,
T
A
)
(
p
1
,
r
1
,
b
1
,
s
1
)
,
(
p
2
,
r
2
,
b
2
,
s
2
)
,...,
(
p
,
r
,
b
,
s
)
}
23
∈
M
12
◦
M
is straightforward.
Summing up, if we want to guarantee that the composition is expressible with SO tgds,
we need to further restrict the class of mappings. In the following section we shall in-
vestigate this issue in more detail and isolate a fairly natural class of mappings closed by
composition.
19.5 Tractable XML composition
Finding a formalism capable of expressing compositions of XML mappings is much harder
than for relational mappings. We have seen that allowing data comparisons in mappings
can lead to undecidable compositions, and even if we forbid data comparisons altogether,
we cannot hope to show that SO tgds can express XML compositions without disproving
a long-standing conjecture in complexity theory. In this section we pursue a dual goal: we
shall try to find out when a composition of mappings can be expressed with SO tgds.
Let us first formally define SO tgds in the XML context. Recall that in XML data
exchange, we used dependencies of the form
π
∧
α
,
π
∧
α
−→ ∃
z
