Database Reference
In-Depth Information
The diagram (e1) represents the diagram for naming the roots of the trees in
D
P
S
composed of the
Σ
P
signature. From this diagram we obtain the denotation
relationship
fst
S
◦
D
ρ
(k)
=
k
◦
Σ
P
(fst
S
),
g
E
=
◦
◦
:
Σ
P
S
→
S
where
k
is corresponding to
fst
S
, in the way that deter-
mines the name of the root of composed trees by operations in
Σ
P
and the denota-
tional model
ass
κ
D
ρ
(k)
.
From the fact that
fst
S
◦ :
T
P
X
is the unique homomorphism (external
square of the diagrams (1a) and (e1)), it must be equal to
ass
#
, and from
ass
→
S
=
fst
S
◦◦
g
E
.
The diagram (e2) represents the generalization of the behavior from the
flattened
guarded behavior
g
E
:
X
→
S
, we obtain that
ass
=
ass
#
◦
[
_
]=
ass,℘
:
X
→
S
×
B
P
(X)
into the general guarded behav-
g
E
,
ior
ass,
T
(℘)
◦
g
E
=
ass
◦
T
(℘)
◦
g
E
:
X
→
S
×
B
P
(
T
P
X)
, which will be
analyzed in next section.
Consequently,
℘
represents the correspondence between
the abstract behavior
℘
and the general behavior
T
(℘)
◦
g
E
=
B
P
(
g
E
)
◦
T
(℘)
, and between the abstract
behavior
℘
and the program equations defined by
g
E
.
Consequently, the relationship between the abstract SOS-denotational semantics
and the DB-denotational semantics is given by the following corollary:
@
Corollary 23
For any given behavior
[
_
]
,
its unique coinductive extension
[
_
]
→
T
P
(X)
(
in Proposition
39
)
and
g
E
(
in Proposition
34
),
the relationship between the
adequate
SOS-denotational seman-
tics
(
with a denotational model
and derived from them
g
E
=
ν(X)
◦[
_
]:
X
g
E
D
ρ
(k) in Proposition
43
,
where k
=
ass
◦
◦
κ
:
Σ
P
S
→
S
)
and the
adequate
DB-denotational semantics are represented by the fol-
lowing commutative diagram between (X
Σ
P
)-algebras
@
where f
=
T
◦
s
E
=
T
◦
E
◦[
_
]
:
X
→T
∞
is the corresponding DB-mapping
@
for the solution mapping
[
_
]
:
X
→
D
P
S
=
gfp(
S
×
B
P
)
.
