Database Reference
In-Depth Information
First, DTD
D
=(
d, r
) is defined as follows.
d
(
r
)=
x,
d
(
x
)=(
E
x
|x
)(
x|B
c
|E
x
)
,
d
(
B
c
)=
cc,
d
(
c
)=(
T
c
|F
c
)(
c|E
c
)
,
d
(
E
x
)=
d
(
E
x
)=
d
(
E
c
)=
d
(
T
c
)=
d
(
F
c
)=
.
Note that
D
is independent of
φ
since
D
is fixed. In contrast,
D
depends on
φ
in the proof of Theorem 1 in Ref. [10].
Second, query
q
is defined as follows.
m
q
=
/r
/x/
···
/x /E
x
(1)
/ ↑
::
x/P
m
/ ↑
::
x/P
m−
1
/ ↑
::
x/ ···/ ↑
::
x/P
1
/ ↑
::
x/ ↑
::
r
(2)
/Q
1
/Q
2
/ ···/Q
n
,
(3)
where
P
m
,P
m−
1
, ··· ,P
1
in (2) and
Q
1
,Q
2
, ··· ,Q
n
in (3) are subqueries defined
later. In short, according to
φ
subqueries (1) and (2) plot a tree
t
showninFig.1,
and then subquery (3) checks whether
φ
is satisfiable over
t
.Eachsubquery
P
i
plots the “subtree”
P
i
in
t
, as shown in Fig. 1. Formally,
P
i
is defined as follows
(1
≤ i ≤ m
).
m−i
+1
/x/E
x
/ ↑
::
x/ ···/x/E
x
/ ↑
P
i
=
::
x/B
c
(4)
/c/T
i,
1
/ ↑
::
c/c/T
i,
2
/ ↑
::
c/ ···/c/T
i,n−
1
/ ↑
::
c/c/T
i,n
/ ↑
::
c
(5)
n
+1
/ ↑
::
c/ ···/ ↑
::
c/B
c
(6)
/c/F
i,
1
/ ↑
::
c/c/F
i,
2
/ ↑
::
c/ ···/c/F
i,n−
1
/ ↑
::
c/c/F
i,n
/ ↑
::
c
(7)
n
+1
/ ↑
::
c/ ···/ ↑
::
c/B
c
(8)
n
+1
/c/ ···/c /T
c
/ ↑
n
+1
::
c/E
c
/ ↑
::
c/ ···/ ↑
::
c/↑
::
B
c
(9)
n
+1
/c/ ···/c /F
c
/ ↑
n
+1
::
c/E
c
/ ↑
::
c/ ···/ ↑
::
c/↑
::
B
c
(10)
m−i
+1
/ ↑
::
x/ ···/ ↑
::
x.
(11)
Starting from the
x
-node at position
x
i
in
t
(Fig. 1), the context node goes down
to
B
c
by (4). Then subquery (5) sets the value of
T
i,j
for 1
≤ j ≤ n
and subquery
(7) sets those of
F
i,j
for 1
≤ j ≤ n
,where