Database Reference
In-Depth Information
7.4.2 Duality and Database-Mapping Programs: Specification
Versus Solution
Let us consider the following initial-final duality for the database-mapping process-
programs expressed by a guarded
and flattened
system
E
of equations: the initial
(X
Σ
P
)
-algebra homomorphism
g
E
:
(
T
P
X,
I
)
→
(X,
[
id
X
,h
X
]
)
(defined in
the Proposition
35
with the mappings
h
X
:
X
represented by the initial-
algebra diagram
(I
1
)
. Note that in general case of the guarded, but not flattened
system of equations, the commutativity of (I1) in Proposition
35
does not hold.
Dual
(
Σ
P
(X)
→
@
S
×
B
P
)
-coalgebra homomorphism
[
_
]
:
(X,
ass,℘
)
→
(
D
P
S
,
B
)
is
represented by the final-coalgebra diagram (4),
The commutative diagram
(I
1
)
of the unique initial algebra homomorphism
id
X
#
=
g
E
)
represents the database-mapping process-
program
specification
by a set of flattened guarded equations
E
with
E
⊆
(p
k
=
t)
|
t
∈
T
P
X
with
p
k
=
:
(
T
P
X,
I
)
→
(X,
[
id
X
,h
X
]
g
E
(t)
,
while the commutative diagram (4) of the unique final coalgebra homomorphism
[
@
B
)
represents the
solution
of this previously specified
database-mapping process-program.
From the final-coalgebra diagram (4), we obtain
ass
_
]
:
(X,
[
_
]
)
→
(
B
P
S
,
@
.
It is easy to verify that the
kernel
of this unique coalgebra homomorphism into
the final
(
=[
_
]
:
X
→
D
P
S
S
×
B
P
)
-coalgebra,
ass
:
(X,
ass,℘
)
→
(
D
P
S
,
B
)
, defined by
=
(p
k
,p
m
)
ass
(p
m
)
X
2
ass
(p
k
)
∈
|
=
K
ass
is a
bisimulation relation
of the program specified by
g
E
(a set of guarded flattened
equations
E
in Proposition
34
) as defined previously in (BSM). In fact,
p
k
∼
p
m
,
i.e.,
(p
k
,p
m
)
∈
K
ass
iff
@
.
Dually, from the initial-algebra diagram
(I
1
)
, we obtain the unique homomor-
phism
id
X
#
=
@
[
p
k
]
=[
p
m
]
g
E
:
(
T
P
X,
I
)
→
(X,
[
id
X
,h
X
]
)
from the initial
(X
Σ
P
)
-algebra.
It is easy to verify that the kernel of the unique
(X
Σ
P
)
-algebra homomorphism
