Database Reference
In-Depth Information
Let us show that for
Z
=T
∞
the DB-denotational semantics
Σ
P
-algebra,
[
f,h
]:
T
∞
T
∞
)
X
(in the commutative diagram represented in the proof of
Proposition
37
in Sect.
7.3.2
is defined a mapping
h
), for
f
Σ
P
(
,
is adequate for the final coalgebra semantics of the database-mapping programs,
given by the following commutative diagrams (1) and (2):
=
(
T
◦
s
E
)
:
X
→T
∞
Proposition 38
The DB-denotational semantics (X
Σ
P
)-algebra with the car-
rier set
T
∞
is
adequate
for the final coalgebra semantics
(
with
the same
carrier
set
)
of the database-mapping process-programs expressed by a guarded system of
equations
g
E
(
flattened or not
)
when f
=
T
◦
s
E
,
so that the following diagram
commutes
The commutative square diagram
(1)
is obtained from the
initial algebra
semantics
where
→
T
P
(X) is the
initial algebra
isomorphism for the Σ
P
abstract signature
,
with the DB-denotational semantics algebra
I
:
X
Σ
P
(
T
P
(X))
[
f,h
]:
X
Σ
P
(
T
∞
)
T
∞
.
The commutative square diagram
(
composed of two triangles
(3)
and
(2))
is ob-
tained from the
final coalgebra
semantics
(
in Proposition
37
).
Proof
The assignment to process variables
f
=
T
◦
s
E
is just the
solution
for the
system of flattened equations for a database mapping process-program
P
(Proposi-
tion
37
, where the mapping
h
is specified in its proof).
Let us demonstrate that if
f
=
T
◦
s
E
then diagram (3) commutes: It is enough
to show that for each variable
p
A
∈
f(p
A
)
. In fact, from the defi-
nition of the set of flattened equations
E
of a database-mapping process-program, in
Proposition
34
,wehavethat
X
is just the set of variables in
E
, and for each equation
(p
A
=
X
,
f
#
◦
g
E
(p
A
)
=
∈
∈
T
P
X
,
g
E
(p
A
)
=
t
and hence
f
#
◦
=
=
t)
E
, where
p
A
,t
g
E
(p
A
)
f
#
(t)
(by replacing
t
with
p
A
(from the fact that they are equal)
=
f
#
(p
A
)
=
f(p
A
)
(be-
cause the restriction of
f
#
to the variables
X
⊆
T
P
X
is
equal
to
f
(from the initial-
algebra semantics (diagram (1) above),
f
#
is the unique inductive extension of
h
along the mapping
f
with
f
=
f
#
◦
inl
X
). Thus, we can replace
inl
X
with
g
E
in
