Database Reference
In-Depth Information
Fig. 6.4
Embedding: functorial semantics
Consequently, we are able to define a function
:
Ob
R
U
→
κ
Ob
R
P
(6.4)
st
(k)
with
such that for any
st(j)
∈
Ob
R
U
,
κ(st(j))
=
max
i
WS
and
Inst
R
st
(i)
≤
Inst
U
st(j)
.
st
(i)
k
=
|
∈
It is easy to verify that for each state
st(i)
∈
ATrS
U
F
P
st(i)
=
In
∗
ER
Out
U
st(i),κ
st(i)
=
λIn
∗
ER
(Out
U
st(i)
κ
st(i)
.
(6.5)
Let us consider the one synchronized conversation cycle in Fig.
6.3
, Sect.
6.2
,
where:
1. For
i
≤
j
−
1,
λIn
∗
ER
(Out
U
(st(i)))
=
λIn
∗
ER
(
{}
)
=
id
and hence
F
P
st(i)
=
id
κ
st(i)
=
κ
st(i)
=
st
(k).
