Database Reference
In-Depth Information
such that for each query q(
x
)
∈
L
G
,
x
,
α
∗
MakeOperads
∀
x
unf
q(
x
)
⇒
r
q
(
x
)
M
α
∗
MakeOperads
∀
x
q(
x
)
⇒
r
q
(
x
)
Tf
OP
=
in
◦
◦
f
in
:
D
→
TD
is a morphism in
DB
.
Here f
M
and f
in
are obtained by a functorial translation of the mapping
M
and of
the integrity constraints Σ
tgd
G
as specified in Corollary
15
.
Proof
Let us define for a query
q(
x
)
over the global schema
, based on Defini-
tion
17
(for queries), the following morphisms in
DB
(for the original, the expanded
and successively unfolded queries, respectively):
1.
h
q
={
f,q
⊥
}=
α
∗
(MakeOperads(
{∀
G
x
(q(
x
)
⇒
r
q
(
x
))
}
))
,
α
∗
(MakeOperads(
2.
h
q
E
={
f
E
,q
⊥
}=
{∀
⇒
}
x
(exp
(q(
x
))
r
q
(
x
))
))
,
G
α
∗
(MakeOperads(
3.
h
q
U
={
))
.
Then, by the query-rewriting theorem, the images of the functions
f,f
E
and
f
U
are
equal to the same computed certain query answer, that is,
f
U
,q
⊥
}=
{∀
x
(unf
(exp
(q(
x
)))
⇒
r
q
(
x
))
}
M
G
r
q
(
x
)
.
im(f )
=
im(f
E
)
=
im(f
U
)
=
Hence, the following diagrams in
DB
(on the right) based on the composition of
T-coalgebra homomorphisms
−→
ret(
,D),h
q
E
and
f
M
:
(D,h
q
U
)
I
f
in
:
ret(
,D),h
q
E
→
can(I,
),h
q
I
D
commute: