Database Reference
In-Depth Information
st
(k)
st
(m)
,
f
st
(m)
st
(l)
, with
T
P
(f )
2. For any two arrows
g
:
→
:
→
=
M
P
j
N
◦···◦
P
j
1
⇒
(T
P
(st
(m))
T
P
(st
(l)))
we obtain that
=======
M
P
j
N
◦···◦
P
j
1
◦
P
i
n
◦···◦
P
i
1
⇒
=
T
P
st
(k)
==============
T
P
st
(l)
T
P
(f
◦
g)
M
P
j
N
◦···◦
P
j
1
⇒
=
T
P
st
(m)
=======
T
P
st
(l)
◦
T
P
st
(k)
M
P
i
n
◦···◦
P
i
1
⇒
T
P
st
(m)
=======
T
P
(f )
T
P
(g).
=
◦
The following commutative diagram demonstrates that
τ
T
is a natural transfor-
mation, for any arrow
P
1
◦
:
→
, where
P
2
=
P
1
◦
_
P
P
2
in
P
A
P
is sequential
composition of the programs
P
and
P
1
:
In fact, from point 1, for any
st
(k)
∈
Ob
R
P
⊆
Ob
R
P
2
,
T
P
2
st
(k)
=
Out
DB
st
k
μy
t
2
st
(k
y)
−
−
∗
t
3
st
(k
y)
+
1
−
0
−
1
=
T
P
st
(k)
.
=
st
(k)
→
st
(m))
∈
Mor
R
P
2
,
T
P
2
(g)
=
T
P
(g)
,
And for any arrow
(g
:
Mor
R
P
⊆
and hence the diagram above commutes.
K
A
Consequently, we have the following vertical composition
τ
T
•
τ
E
:
U
M
R
M
and of the “transac-
of the “embedding” natural transformation
τ
E
:
U
M
K
A
,
tion” natural transformation
τ
T
:
R
M
