Database Reference
In-Depth Information
A
t
be the UNFTAs underlying the source and target
schemas, and let
m
be the maximum over the sizes of all patterns used in
To make the rules precise, let
A
s
,
M
.
A
s
-kind
K
∀
and an accepting run with margins of size
m
,
such that the height and branching of
K
is bounded by (2
m
+ 1)
In the first round
∀
plays an
. The data values
used in
K
are to represent an equality type, so it is enough to choose them from
C
=
{
A
s
1
,
2
,...,
|
K
∀
|}
. The response
K
∃
of
∃
is similar except that
A
s
is replaced by
A
t
,andsome
of the nodes can store nulls taken from a fixed set
{⊥
1
,
⊥
2
,...,
⊥
|
K
∃
|
}
.
π
(
x
,
z
) and tuples
a
,
b
In the second round,
∀
chooses a dependency
π
(
x
,
y
)
−→ ∃
z
(
a
,
b
) can be realized
(
without
nulls) together with a polynomial object witnessing that
π
in a tree agreeing with
K
∀
(
Lemma 12.29
). The player
∃
then responds with a tuple
c
π
(
a
,
c
) can be realized in a tree
(possibly
including
nulls) and a polynomial witness that
agreeing with
K
∃
.
A player loses if he fails to make a move complying with the rules. If all moves are
made,
wins.
Let us verify that
∃
∃
M
has a winning strategy if and only if
is absolutely consistent.
's strategy in the first round is to choose an XML tree
T
for which no solution exists and play
K
∀
such that
T
If
M
is not absolutely consistent,
∀
∈
L
(
K
∀
) (see
Lemma 12.23
). In the
π
(
x
,
z
) and tuples
a
,
b
such that
T
(
a
,
b
),
second round,
∀
chooses an std
π
(
x
,
y
)
−→ ∃
z
|
=
π
π
(
a
,
c
) can be realized in a tree agreeing with
K
∃
. Some suitable
std and
a
,
b
exist, as otherwise for all choices of
but there is no
c
such that
∀
there would be
c
and a tree in
L
(
K
∃
)
π
(
a
,
c
);by
Lemma 12.24
we would then be able to combine all these trees into
atree
T
∈
satisfying
π
(
a
,
c
), i.e., a solution for
T
.
L
(
K
∃
) satisfying all
's strategy in the first round is to choose
K
∃
so that for every tree agreeing with
K
∀
there exists a solution agreeing with
K
∃
.Inthe
second round, whatever
a
,
b
was played,
Assume that
|M|
is absolutely consistent.
∃
π
(
a
,
c
) can be realized in a tree from
L
(
K
∃
) for
some
c
;
's strategy is simply to choose suitable
c
and a witness.
It remains to see that such
K
∃
can be produced, provided that
∃
is absolutely consistent.
First let us see that each tree in
L
(
K
∀
) has a solution agreeing with some
K
∃
.Let
N
=
(2
m
+1)
M
A
t
(2
m
+1)
A
t
,
T
L
(
K
∀
) and let
A
be the set of data values used in
T
that
are not elements of
C
.Let
A
0
,
A
1
,...,
A
k
be sets of data values such that
∈
|
A
i
|
=
|
A
|
for each
i
and
C
,
A
0
,
A
1
,...,
A
k
are pairwise disjoint. For each
i
fix
f
i
:
A
∪
C
→
A
i
∪
C
such that
f
i
restricted to
C
is the identity, and
f
i
restricted to
A
is a bijection
A
A
i
.Let
T
i
=
f
i
(
T
) be
obtained by renaming the data values according to
f
i
. Since values in
C
are not changed,
T
i
∈
→
L
(
K
∀
) for all
i
.Using
Lemma 12.24
, we combine
T
i
's into a tree
T
∈
L
(
K
∀
) which
satisfies all the valuations of source side patterns satisfied by any of the
T
i
's. In particular,
whenever
T
(
a
,
b
),
T
|
(
f
i
(
a
)
,
f
i
(
b
)) for each
i
.As
is absolutely consistent,
T
has a solution, say
S
.By
Lemma 12.23
,
S
agrees with some
|
M
=
π
=
π
A
t
-kind
K
of height and
branching bounded by (2
m
+ 1)
, admitting an accepting run with margins of size
m
(but not necessarily using only data values from
C
or nulls). Since
K
has at most
k
nodes, there is
i
0
such that
K
contains no data values from
A
i
0
.Let
f
(
c
)=
c
for
c
∈
C
,
f
(
a
)=
f
−
1
i
0
A
t
∈
A
i
0
∪
C
. Then,
f
(
S
) agrees with
(
a
) for
a
∈
A
i
0
,and
f
(
a
)=
⊥
a
for all
a
/
