Database Reference
In-Depth Information
T
(℘) is the unique extension of the behavior to all terms with variables and
,
by
Proposition
39
and Corollary
23
,
f
@
→ T
∞
is the
adequate
DB-denotational semantics
,
that is
,
the mapping whose results are represented as a
composed objects in the
DB
category
.
=
T
◦
E
◦[
]
:
_
X
@
Proof
From Corollary
24
,
f
#
=
Abs
◦[
#
.
From the commutative diagram (4c) in Proposition
43
, in the case when
_
]
S
=
1
×
B
P
(
T
P
X)
can be substituted by (isomorphic
is a terminal object in
Set
, so that
1
to it) the set
B
P
(
T
P
X)
, and
1
×
B
P
(
D
P
(
1
))
can be substituted by (isomorphic to
g
E
0
it) the set
B
P
(
D
P
(
1
))
. Thus, the constant mapping
ass
◦
:
T
P
X
→
1
={⊥
}
can
be eliminated, by extending this simplified (4c) diagram with the bijection
Abs
:
D
P
(
1
)
→T
∞
, and we obtain the following commutative diagram
that composes the diagram (11) of this proposition.
In this setting, a denotational model is adequate w.r.t. an operational semantics
when its
(X
Σ
P
)
-algebra homomorphism
f
#
:
T
P
X,
I
)
→
T
∞
,
[
]
(
(
f,h
)
is equal
to the final
B
P
-coalgebra homomorphism
#
:
T
P
X,
T
(℘)
→
@
Abs
◦[
_
]
(
T
∞
,
DB
).
Thus, in particular, the DB-semantic domain
T
∞
(the objects in
DB
category) is the
carrier of the final
B
P
-coalgebra of the behavior
B
P
.
Consequently, for each term
t
∈
T
P
X
with the database-mapping process vari-
@
ables,
f
#
(t)
=
Abs
(
[
_
]
#
(t))
.
7.5.2 Generalized Coinduction
The conventional coiteration schema, used in Sect.
7.4
for the operational semantics,
assigns infinite behaviors to the processes of a set
X
by specifying for each element
in
X
a direct observation and successor states (processes). Since the successors are
taken from
X
again, the same specification applied to them reveals the second layer
of the behavior, and so on.
A different approach is taken by the
λ
-coiteration schema [
6
], which is parame-
terized by the
s
yntax monad
T
P
and a distributive law
λ
of
T
P
over general behavior
endofunctor
B
P
=
S
×
B
P
. It allows the successor states (processes) to be taken
