Database Reference
In-Depth Information
The semantics of a programming language is called
compositional
when the
meaning of compound programs can be derived from the meaning of their subcom-
ponents. A complete account of the meaning of programming language requires
both an operational and denotational semantics:
•
Denotational semantics
is the mathematical interpretation which is better suited
for reasoning about
programs
because of its
modularity
. The programs from the
initial
Σ
P
-algebra, where
Σ
P
is the signature of the language corresponding
to the basic constructs, and the corresponding unique homomorphism from the
programs to the
denotational model
is called
initial algebra semantics
[
17
].
•
Operational semantics
of a programming language accounts for a formal de-
scription of its executable
behaviors
which should be
observable
.The
seman-
tic domain
, carrier of the denotational model, is the final
B
P
-coalgebra of the
B
P
(final solution of a domain equation
X
=
B
P
(X)
).
Intended operational model
of a language based on the transition relation may
also be seen as a
'behavior' endofunctor
B
P
-coalgebra: the unique homomorphism from this intended
operational model (
B
P
-coalgebra) to the semantic domain (final
B
P
-coalgebra)
is called the
final coalgebra semantics
[
2
,
36
].
•
Semantic adequateness
. Both kinds of semantics should be related in such a way
that one should be able to infer from the denotational semantics the operational
behavior of the programs when the initial algebra and the final coalgebra seman-
tics coincide [
36
]. The mathematical
structural
approach to operational seman-
tics [
35
] is that every structural operational semantics (SOS) coinduces a deno-
tational semantics, i.e., every SOS is
compositional
: This is achieved by defining
operational semantics in terms of abstract, mathematical notions of
syntax
and
behavior
.
Bridging the gap between the operational and the denotational aspects of semantics
is based on a suitable interplay between the standard
induction
principle and the dual
coinduction
principle (note that both principles are supported by the
DB
category,
as demonstrated in the next chapter, Sects.
8.3.1
and
8.3.2
, respectively).
The idea of coupling the initial algebra with coalgebra semantics was used in [
36
]
to systematically derive denotational models from structural operational seman-
tics [
35
]: the notion of observational equivalence (strong bisimulation) is a
con-
gruence
if suitable restrictions are imposed on the syntactic format of the rules:
among the rules in this format, 'abstract GSOS' rules and (negative) tree rules are
known best. It was proven [
39
] that the structural rules correspond to the germ of an
inductive functorial semantics, that is, they can be seen as an
action
of the syntax on
the composite functor
B
P
◦
T
P
, for abstract notions of
syntax
T
P
(a monad freely
generated by signature
Σ
P
) and
behavior
B
P
.
The fundamental results of this functorial operational semantics (FOS), created
for the base
Set
category, are used to develop a new abstract FODS (functorial oper-
ational database-mapping semantics) concepts based on the denotational semantics
of the database category
DB
.
Any given nonempty set of states in
S
and a given set of atomic actions in
Act
can be used to define a labeled transition system (LTS), used in structural operational
semantics, as follows:
