Database Reference
In-Depth Information
Proof
Let us consider the root database schema
A
∈
V
G
for a given mapping-
interpretation
α
A
∈
DB
Sch
(G)
(not necessarily a model) of the sketch
Sch
(G)
such that
A
=
α
∗
(
A
)
is a model of
Int(G)
⊆
after the insertion of a number of
tuples in this database. The fact that
A
is a model of
A
can be verified in the
DB
category by the fact that the integrity-constraint arrow
T
AA
={
A
v
1
·
q
A,
1
,...,v
n
·
q
A,n
,
1
r
∅
}:
A
→
A
in
Sch
(G)
is satisfied by
α
∗
, that is,
α(v
i
)
for
i
=
1
,...,n
are
the injective functions (see Corollary
4
and Example
12
in Sect.
2.4.1
).
That is,
A
α
∗
(
,α
∗
)
)
=
A
)
∈
Ob
DB
(denoted alternatively by a state-pair
s
=
(
A
is a model of the schema
A
and, consequently, the root state in this LTS. Then, an
atomic action for a mapping
M
AB
:
A
→
B
in
E
G
is given by
Δ
α, MakeOperads(
M
AB
)
∈
P
fin
(
Υ
),
a
=
M
AB
⇒
for the insertion transition
α
∗
===
α
1
(in Proposition
32
). The final transition step
state of this action
a
is
s
=
B
=
(
B
,α
1
)
, where
α
1
∈
DB
Sch
(G)
is a new
Int(G)
⊆
interpretation obtained from
α
1
by changing only an extension of
B
in the way that
B
is a new obtained model of the database schema
B
after the transferring of the in-
formation flux
Flux(α, MakeOperads(
=
Ta
from the instance database
A
into this database
B
. In the case of Strong
Data Integration,
α
1
M
AB
))
=
T(Δ(α,MakeOperads(
M
AB
)))
M
AB
after the transition
satisfies the inter-schema mapping
M
AB
⇒
α
∗
==
α
1
(see the vertical arrow in the right ellipse of the diagram in Sect.
7.2.2
).
Consequently, we have the atomic state-transition
(
a
(
,α
∗
)
,α
1
)
or,
A
B
B
, caused by the insertion-transition
α
∗
==
M
AB
a
⇒
α
1
, which cor-
responds in
DB
to the
atomic
morphism
f
=
α
∗
(MakeOperads(
M
AB
))
:
A
→
B
with the information flux
f
equivalently,
A
=
Ta
(in the case of Strong Data Integration, the inter-
is satisfied by the final interpretation
α
1
).
By following this
forward-chaining
process, from the initial root and its interpre-
tation
α
∗
, for a given graph
G
, we obtain that an LTS is a tree where the states are
the models of the database schemas and transitions are labeled by actions that are
the kernels of the information fluxes of the inter-schema mappings.
We consider the class of cyclic database mapping graphs
G
as well, and hence
such a tree can be also infinite.
It is easy to verify that there is a correspondence between atomic actions in
Act
and atomic morphisms in
DB
category, given by mapping
schema mapping
M
AB
:
A
→
B
→
f
=
B
T
(f )
|
f
is an atomic morphism in
DB
T
:
Act
=
f
, where
f
such that for any
a
=
Δ(α,
M
AB
)
∈
Act
,
Ta
=
Flux(α,
M
AB
)
=
α
∗
(
M
AB
)
:
α
∗
(
A
)
→
α
∗
(
B
)
is a mapping morphism in
DB
.
Analogous considerations can be provided in the case when some tuples in the
root database
are
deleted
. In this case, we will have the
backward-chaining
pro-
cess that will propagate in the inverted graph
G
OP
and hence will delete the tuples
in another databases in
G
as well (as explained in Sect.
7.2.1
for the transitions
α
∗
===
A
OP
BA
⇒
M
α
1
).
