Database Reference
In-Depth Information
P
SPACE
is contained in E
XPTIME
. Thus, most likely (barring some unexpected collapse re-
sults in complexity theory), compositions of mappings that do not use data comparisons
still cannot be expressed with SO tgds.
12
23
Theorem 19.17
There
are
mappings
M
and
M
in
SM(
⇓
,
⇒
)
such
that
C
OMPOSITION
(
M
12
,
M
23
)
is
E
XPTIME
-complete.
Proof
We will reduce from the nonuniversality problem for bottom-up nondeterministic
automata on binary trees, modifying the reduction given in
Proposition 18.3
.
First, define
D
3
over
{
r
,
label
,
state
,
nontr
,
reject
}
as
state
∗
label
∗
nontr
∗
state
→
reject
?
label
,
state
:@
attr
nontr
:@
left
,
@
right
,
@
label
,
@
up
.
r
→
A tree conforming to
D
3
is meant to encode an automaton. It stores the alphabet in the
label
-nodes, state space in the
state
-nodes (we assume that the initial state is stored as
first, just after
), and the
complement
of the transition relation. The reason we store the
complement is that we do not have negation. We do not have to enforce anything on such a
tree, since we will be constructing it ourselves based on a given automaton, when preparing
input for the composition membership algorithm. In particular, we will make sure that all
states, labels, and nontransitions are stored correctly.
Next, let
D
2
over
{
r
,
node
,
label
,
state
,
leaf
,
yes
,
no
}
be given by
r
→
node
node
→
label
state
∗
(
nodenode
|
leaf
)
state
→
yes
|
no
state
,
label
:@
attr
.
A tree conforming to
D
2
is meant to encode a rejecting run of the corresponding power
set automaton. This time we will need to ensure that it really is a correct rejecting run
with the st-tgds, since this is precisely the tree that will be produced by the composition
membership algorithm.
Finally, we define
D
1
simply as
r
→
ε
. The only tree conforming to
D
1
will be used as
astub.
Let us now describe
Σ
23
, which will enforce the correctness of the run. First, we make
sure that
label
-nodes store labels,
//
label
(
x
)
−→
r
/
label
(
x
)
.
Second, we need to check that for each
node
-node, each state is stored in exactly one
state
-node, and that nothing else is stored there,
+
state
(
y
)]
+
state
(
y
)]
.
//
node
[
state
(
x
)
→
−→
r
[
state
(
x
)
→
