Database Reference
In-Depth Information
@
where
,
from Propositi
on
39
,
g
E
=
ν(X)
◦[
_
]:
X
→
T
P
(X)
,
s
E
=
E
◦[
_
]
:
X
→
T
∞
,
f
=
T
◦
s
E
and
B
P
=
S
×
B
P
.
Proof
This commutative diagram is obtained from the commutative diagram in
Proposition
39
where the square diagram (4) is substituted by equivalent square di-
agram (6), with an added bijection
DB
and the set of
DB
subcategories
Sub(
DB
)
,
−
DB
◦
DB
=
, so that
f
=
T
◦
E
−
DB
◦
DB
◦
and by considering that
id
D
P
S
@
@
[
_
]
=
T
◦
E
◦[
_
]
=
T
◦
s
E
.
7.5.1 DB-Mappings Denotational Semantics and Structural
Operational Semantics
In the description of the syntax (algebras) and the semantics (coalgebras) used pre-
viously, we used both of them and hence we correlated them by the commutative di-
agrams representing the adequacy of the denotational semantics for the operational
semantics.
But we can consider the algebraic and coalgebraic structures in different hierar-
chic layers. For example, we can start with certain algebras describing one's appli-
cation domain. On top of these one can have certain dynamic systems (processes)
as coalgebras, involving such algebras (e.g., as codomains of attributes). And such
coalgebraic systems may exist in an algebraic processes.
A concrete example of such layering of coalgebra on top of an algebra is given by
Plotkin's so-called structural operational semantics (SOS) [
35
]. It involves a transi-
tion system (a coalgebra) describing the operational semantics of some language, by
giving the transition rules by induction on the structure of the terms of the language.
The later means that the set of terms of the language is used as an (initial) algebra.
Differently from the DB-denotational semantics where the carrier set of the de-
notational model (a
(X
Σ)
-algebra) is the set of ground terms representing the
objects (i.e., instance-databases) in base
DB
category, the carrier set in the SOS-
denotational semantics is the
D
P
S
=
gfp(
S
×
B
P
)
of the 'behavior functor
B
P
',
i.e., the set of LTS trees with the states in
and actions (i.e., transitions) in
Act
.In
[
39
], both Functorial Operational semantics (FOS) (which starts with the syntactical
monad
S
T
P
and then derives its
operational model
) and its dual Functorial Denota-
tional Semantics (FDS) which starts from the observational comonad
D
P
and then
derives its
denotational model
are presented.
In general [
39
], given a (Cartesian) category
Set
and arbitrary notions of program
constructs
Σ
P
and behavior
B
P
on
Set
, with
Σ
P
freely generating the syntax monad
(
T
P
,η,μ)
, one can define a corresponding
abstract
notion of
operational rules
as
the natural transformations
:
B
P
T
P
, and then derive the
Σ
P
(Id
×
B
P
)
B
P
T
P
. By duality
T
P
:
natural transformations
=
B
P
μ
◦
Σ
P
(
T
P
×
B
P
T
P
)
[
39
] from the comonad
D
P
,ε,δ
, in the same way, from the natural transformations
B
P
(Id
ρ
:
ρ
D
P
◦
Σ
P
D
P
Σ
P
)
we can derive the natural transformations
ρ
=
B
P
(
:
Σ
P
D
P
D
P
Σ
P
D
P
)
.
Σ
P
δ
