Database Reference
In-Depth Information
1, we obtain the case described by Definition
41
for
the sequential composition on non-concurrent programs.
The sequential composition
P
2
=
In the case when
n
=
m
=
(P
0
(
1
)
|···|
P
0
(m))
◦
(P
1
(
1
)
|···|
P
1
(n))
means
that the execution of all concurrent programs
P
1
(i),
1
n
has to be finished
before the beginning of the execution of the set of concurrent programs
P
0
(i),
1
≤
i
≤
≤
i
≤
m
.
Consequently, the definitions of the functors
U
M
:
P
A
→
Cat
and
R
M
:
P
A
→
R
M
in Corol-
Cat
with the “embedding” natural transformation
τ
E
:
U
M
lary
20
are valid also for the concurrent programs
P
=
P(
1
)
|···|
P(n),n
≥
1.
In fact, for any arrow
P
0
◦
_
:
P
1
→
P
2
, with
P
1
=
(P
1
(
1
)
|···|
P
1
(n)),n
≥
1, and
P
0
=
(P
0
(
1
)
|···|
P
0
(m)),m
≥
1, in
P
, with
P
2
=
P
◦
P
1
,wehavethefollowing
A
commutative diagram of functors in
Cat
:
Notice that the concept of the atomic transaction for the concurrent RDB machine
M
RC
is equal to that defined for the machine
M
R
, given by Definition
42
. The only
difference is that such atomic transactions can be generated by different concurrent
programs, while for
M
R
they are generated by only one host program.
Consequently, we have the same definition of the constant functor
K
A
:
P
A
→
Cat
and the same “transaction” natural transformation
τ
T
:
R
M
→
K
A
such that
1,
K
A
(P )
DB
Sch
(G(
A
))
. Thus, we ob-
for each program
P
=
P(
1
)
|···|
P(n),n
≥
=
DB
Sch
(G(
A
))
as it was specified by Theorem
11
and hence, the image of this functor
im(T
P
)
⊆
tain a functor
T
P
=
τ
T
(P )
:
R
P
→
DB
Sch
(G(
A
))
is the
set of all transactions generated by the concurrent programs, between the models
of database schema
Mod(G(
A
))
⊆
(the object component
T
P
generates all instance-databases
modified by the concurrent programs, while the arrow component
T
P
A
generates the
transactions between them).
Thus, also for the concurrent time-sharing execution of the programs in
M
UC
and
M
RC
, we obtain the following vertical composition
τ
T
•
K
A
of
τ
E
:
U
M
R
M
and of the “transaction”
the “embedding” natural transformation
τ
E
:
U
M
K
A
,
natural transformation
τ
T
:
R
M
