Database Reference
In-Depth Information
data memory of
M
R
: this changing of the extension of the schema
A
we will denote
M
P
n
⇒
α
1
.
by a transition
α
∗
===
Notice that
α
1
(
A
)
is always consistent for the reduced schema
A
=
(S
A
,
∅
)
(and
hence the R-algebra
α
1
is a model of
A
). However, it may be inconsistent for the
original database schema
).
In order to be able to consider the sequences of such transitions for a given
schema
A
=
(S
A
,Σ
A
)
(thus,
α
1
is not necessarily a model of
A
A
, we introduce a category of such transitions, as follows:
Proposition 30
Fo r
a
g iv e n
s k e t c h
Sch
(G(
A
)) of a schema
A
=
(S
A
,Σ
A
)
,
the category of interpretations of
A
is the subcategory of functors Int(G(
A
))
⊆
DB
Sch
(G(
A
))
,
from Proposition
16
(
and Proposition
17
in Sect
.
4.1.3
),
where
:
1.
Each object is an R-algebra
(
a mapping interpretation
)
α
∗
:
Sch
(G(
A
))
→
DB
,
which is functor such that for the identity schema mapping
M
AA
=
1
r
i
∈
S
A
∪{
O(r
i
,r
i
)
|
r
i
∈
1
r
∅
}:
A
→
A
,
we obtain the identity morphism α
∗
(
M
AA
)
α
∗
(
:
A
→
A for A
=
A
)
.
If Σ
A
=∅
,
then for
M
A
A
={
1
r
,
1
r
∅
}:
A
→
A
,
we obtain the iden-
tity morphism α
∗
(
M
A
A
)
α
∗
(
:
A
T
→
A
T
for A
T
=
A
)
={
R
=
,
⊥}
,
and for
α
∗
(
T
AA
)
the sketch arrow
T
AA
:
A
→
A
,
we obtain f
Σ
A
=
:
A
→
A
T
with
0
(
by Proposition
15
in Sect
.
4.1.1
).
2.
Each atomic arrow is a natural transformation η
P
n
:
f
Σ
A
=⊥
α
∗
α
1
,
denoted by
M
P
n
⇒
α
1
,
where
a transition α
∗
===
M
P
n
:
A
→
A
is the schema mapping
(
by
Proposition
26
,
Sect
.
5.3
)
such that α
1
(
A
) is an instance-database obtained from
the instance-database α
∗
(
A
) by execution of an arrow P
n
in
RA
,
such that
:
α
∗
(
α
1
(
2.1.
η
P
n
(
A
)
:
A
)
→
A
) is defined by Corollary
17
as an arrow in
,
specified in Example
34
for the cases when P
n
is obtained
from '
UPDATE...
'
,
'
INSERT...
'or'
DELETE. . .
'
,
SQL statements
,
re-
spectively
.
2.2.
η
P
n
(
{
f
U
,f
I
,f
D
}
A
T
.
The compositions of the arrows in Int(G(
A
)
=
id
A
T
:
A
T
→
DB
Sch
(G(
A
))
satisfy the following
A
))
⊆
property
:
α
1
===
α
2
◦
α
∗
===
α
1
=
α
∗
====
α
2
.
M
P
k
⇒
M
P
k
◦
P
n
⇒
M
P
n
⇒
Proof
Let us show that this category of functors, for a given schema
A
,iswell
defined:
1. The fact that each arrow in
Int(G(
DB
Sch
(G(
A
))
is a natural transformation
A
))
⊆
α
∗
α
1
η
P
n
:
holds from the following commutative diagram on the right:
