Database Reference
In-Depth Information
Theorem 11
Let us define
,
for a given database schema
A
and its category of
programs
P
,
a constant functor K
A
:
P
A
→
Cat
such that for every program P
∈
A
DB
Sch
(G(
A
))
and for each arrow P
Ob
P
A
,
K
A
(P )
Mor
P
A
,
K
A
(P
=
◦
_
∈
◦
_) is
DB
Sch
(G(
A
))
.
Then there is a “transaction” natural transformation τ
T
:
DB
Sch
(G(
A
))
equal to the identity functor Id
:
→
R
M
→
K
A
such that
DB
Sch
(G(
A
))
with
:
for each program P
,
we obtain a functor T
P
=
τ
T
(P )
:
R
P
→
1.
For any object st
(k) in the category
R
P
,
T
P
(st
(k))
α
∗
such that
=
Out
DB
st
k
μy
t
2
st
(k
y)
∗
t
3
st
(k
y)
+
1
−
0
.
α
∗
(
A
)
=
−
−
−
1
=
st
(k)
st
(m) in the category
R
P
,
:
→
2.
Fo r a n y a r row g
T
P
st
(k)
T
P
st
(m)
M
⇒
T
P
(g)
=
===
such that
if T
P
(st
(k))
T
P
(st
(m))
M
P
NOP
=
;
M
=
M
P
i
n
◦···◦
P
i
1
otherwise,
where P
i
n
◦···◦
P
i
1
is the sequential composition of ordered list of
RA
-arrows
,
considered as the programs of
M
R
,
between the states st
(k
1
) and st
(m
1
)
,
for k
1
=
μy(t
2
(st
(k
(t
3
(st
(k
k
−
−
y))
∗
−
y))
+
1
)
−
1
=
0
) and m
1
=
m
−
μy(t
2
(st
(m
(t
3
(st
(m
0
)
,
such that the
RA
-arrows be-
tween any two consecutive synchpoints st
(j
1
) and st
(j
2
)
,
k
1
≤
−
y))
∗
−
y))
+
1
)
−
1
=
j
1
<j
2
≤
m
1
,
T
P
(st
(j
1
)) are not considered
.
This functor is such that for its image
,
Im(T
P
)
with T
P
(st
(j
2
))
=
DB
Sch
(G(
A
))
is the
set of all transactions between the models of the database schema
⊆
Mod(G(
A
))
⊆
A
.
Proof
Notice that if
t
2
(st
(k))
(t
3
(st
(k))
μy(t
2
(st
(k
∗
+
1
)
−
1
=
0 then
j
=
−
(t
3
(st
(k
y))
∗
−
y))
+
1
)
−
1
=
0
)
=
0(
j
≥
1 otherwise). From the definition in
T
P
(st
(k))
is an object (a functor) in
DB
Sch
(G(
A
))
such that it is a model of schema
point 1, for every
st
(k)
,
α
∗
=
A
(i.e., it satisfies all integrity constraints in
A
).
st
(m)
,
T
P
(g)
is a composed transaction, in which the
intermediate identity transactions (and all arrows between two synchpoints
st
(j
1
)
and
st
(j
2
)
, with
k
1
≤
st
(k)
:
→
For any arrow
g
m
1
, where in the second synchpoint
st
(j
2
)
the
ROLLBACK operation was executed) are eliminated between two models of
j
1
<j
2
≤
.
Thus such a composed transaction, obtained by the sequential composition
P
i
n
◦
···◦
A
P
i
1
, corresponds to an arrow in
DB
Sch
(G(
A
))
between two models of
A
. Thus,
DB
Sch
(G(
A
))
.
Let us show that
T
P
is a well-defined functor from
R
P
into
DB
Sch
(G(
A
))
:
1. For each identity arrow NOP
Im(T
P
)
⊆⊆
Mod(G(
A
))
⊆
st
(k)
st
(k)
we obtain the identity arrow
:
→
M
P
NOP
⇒
T
P
(st
(k))
.
α
∗
====
α
∗
where
α
∗
=
