Database Reference
In-Depth Information
Thus, from definition of
F
P
,
F
P
(g)
st
(k
st
(k
=
NOP
:
+
1
)
→
+
1
)
, and we
obtain
F
P
(g
F
P
(f )
F
P
(f )
F
P
(g)
F
P
(f )
.
◦
f)
=
=
NOP
◦
=
◦
n
, then, from definition of
F
P
,
4. If
j
≤
l
and
l
2
≤
j
+
st
(k)
st
(k)
F
P
(g
F
P
(g)
F
P
(f )
◦
f)
=
=
=
NOP
:
→
and hence
F
P
(g
F
P
(g)
F
P
(f )
.
◦
=
◦
f)
5. If
l
2
=
j
+
n
+
1 and
l
1
=
j
+
n
then we define
st
(k
st
(m).
F
P
(g
F
P
(g)
◦
f)
=
RETURN
◦
Ap
n
:
+
1
)
→
Thus, from definition of
F
P
,
F
P
(f )
st
(k
st
(k
=
:
+
→
+
NOP
1
)
1
)
and hence
F
P
(g
F
P
(g)
F
P
(g)
F
P
(g)
F
P
(f )
.
◦
=
=
◦
=
◦
f)
NOP
6. If
l
=
j
+
n
and
l
1
=
j
+
n
+
1 then we define
st
(k
st
(m).
F
P
(g
F
P
(f )
◦
=
◦
Ap
n
:
+
→
f)
RETURN
1
)
Thus, from definition of
F
P
,
F
P
(g)
st
(m)
st
(m)
and hence
F
P
(g
=
NOP
:
→
◦
F
P
(f )
.
7. (Repetition of point 1, for the new idle (wait) state
st
(m)
of
M
R
)If
l>j
F
P
(f )
F
P
(f )
F
P
(g)
f)
=
=
NOP
◦
=
◦
+
n
and
l
2
<j
where
∂(g)
=
st(j
)
and
g
∈{
COMMIT
,
ROLLBACK
,
CALL
,n
}
then, from definition of
F
P
,
F
P
(g
F
P
(g)
F
P
(f )
st
(m)
st
(m)
◦
f)
=
=
=
NOP
:
→
F
P
(f )
.
The functor
F
P
is well defined: each identity arrow in
U
P
is mapped into the identity
arrow (NOP) in
U
P
. From the compositional property for the atomic arrows, for the
composition of
all
arrows
F
P
(g
and hence
F
P
(g
F
P
(g)
◦
f)
=
◦
F
P
(g)
F
P
(f )
is valid.
◦
=
◦
f)
Notice that the functor
F
P
, represented in Fig.
6.4
, “forgets” all transitions of the
host program of
M
U
which are not a part of the synchronized conversations between
the universal host machine and RDB categorial machine
M
R
.
Let
Inst
U
:
Time
be two mapping that define
the time-instance when a given state is achieved during the execution of the source
program
P
of the machines
M
U
and
M
R
, respectively. From the fact that the states
are progressively enumerated during the execution of this program,
Inst
U
st(j)
≤
Ob
U
P
→
Time
and
Inst
R
:
Ob
R
P
→
Inst
U
st(m)
iff
j
≤
m,
(6.3)
and, analogously, for the states
st
(k)
of
M
R
.
Let
WS
Ob
R
P
be the subset of idle wait-states of
M
U
. We have that be-
fore the beginning of execution of the program
P
,the
M
R
is in one of this idle
wait-states
st
(k
0
)
⊂
∈
WS
. Consequently, for each state
st(j)
,
j
≥
0, in
ATrS
U
,
Inst
R
(st
(k
0
))
. For example, in Fig.
6.3
, Sect.
6.2
,
st
(k), st
(m)
≥
∈
Inst
U
(st(j))
Inst
R
(st
(k))
for
i
≤
j
+
n
, and
Inst
U
(st(i))
≥
Inst
R
(st
(m))
WS
, with
Inst
U
(st(i))
≥
for
i
≥
j
+
n
+
1.
