Database Reference
In-Depth Information
The algorithm that we shall present is based heavily on the ideas developed in the algo-
rithm for building solutions in XML data exchange, see
Chapter 12
. In particular, we shall
use the notion of a
kind
, which was central to that algorithm (see
Definitions 12.9
on page
164
and
12.17
on page
169
).
To justify the reordering of the quantifiers, we would need to show that for every two
target trees
T
1
and
T
2
there is a
π
-union
tree
T
such that whenever
T
1
|
π
(
a
,
c
) or
T
2
|
=
=
π
(
a
,
c
),then
T
π
(
a
,
c
). As we have learned in
Chapter 12
, this need not be true in
general, but can be guaranteed by assuming that
T
1
and
T
2
are of the same kind.
A single kind usually cannot provide solutions to all source trees. For instance, for
|
=
M
=
π
(
x
), saying “there is an
a
-node
storing
x
whose next sibling is a
b
-node”, and a target kind fixes the value in the
a
node
to some
d
, a tree of this kind can only be a solution for source trees that store the same
d
in the last
a
-node. Thus source documents have to be split into subsets admitting solutions
of a single kind. It turns out that the latter is guaranteed by closure under π -unions, which
means that we can also use kinds to split the source documents.
Based on this we reformulate the absolute consistency condition as:
a
∗
b
∗
}
ab
∗
}
−→
π
(
x
)
(
{
r
→
,
{
r
→
,
{
π
(
x
)
}
) with
π
(
x
)=
for every
source kind
K
there exists
atargetkind
K
such that
for every a b
such that
(
a
,
b
) is satisfiable in a tree of kind
K
,
π
π
(
a
,
c
) is satisfiable in a tree of kind
K
,
there exists c
such that
which ultimately leads to an algorithm working in exponential space.
Theorem 18.8 A
B
C
ONS
(
⇓
,
⇒
,
∼
)
is in
E
XPSPACE
.
Proof
We present the algorithm as a two-round game between two players,
∀
and
∃
.In
each round,
∀
moves first. Moves are made by the choice of an object of size exponential
in
during the second round. The
winning condition, a polynomial time property of the moves, is defined so that
M
during the first round, and polynomial in
M
∃
has a
winning strategy if
is absolutely consistent.
The existence of a strategy for
M
in a game of such form can be easily tested
in E
XPSPACE
by exhaustive search. The algorithm simply iterates over all possible
(exponential-size) objects that can be played by
∃
∀
and
∃
in the first round, and checks
if
. To test if an object
Y
is a winning
answer to an object
X
, the algorithm iterates over all (polynomial-size) objects that can be
played in the second round and checks if
∃
has a winning answer for each object played by
∀
∃
has a winning answer to each object played by
∀
, which only requires testing the (polynomial) winning condition for the four objects.
Let us now describe the game. The rules reflect the reformulated absolute consistency
condition: in the first round
∀
states what kind of tree is a counter-example to absolute
consistency, while
chooses the kind of tree that gives a solution to the purported counter-
example; in the second round
∃
∀
picks a tree of the declared kind and a tuple witnessing that
the solutions fail, and
∃
tries to respond with a tree and a tuple that would prove
∀
wrong.
