Database Reference
In-Depth Information
F(μ
X
)
1
T
P
X
T
P
(φ)(t
i
)
=
λ
≤
i
≤
n
F(μ
X
)
λ
T
P
X
T
P
(φ)(t
i
)
=
1
≤
i
≤
n
=
φ
#
(t
i
)
1
≤
i
≤
n
φ
#
n
(t
1
,...,t
n
)
.
=
Thus,
φ
#
=
F(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)
.
Note that in this representation of the (unique) solution of a guarded recursive
specification
φ
T
P
X)
we do not use the non-final semantics construction
of the commutative diagram (12b) used in [
6
] and [
19
], so that we do not need
to involve the mapping
β
λ
:
T
P
(gfp(F))
:
X
→
F(
gfp(F)
. Moreover, we do not need to
use
λ
-bialgebras in this representation: what we need is only the distribution law
λ
with its multiplication and unit axioms. Thus, this new minimalist approach is more
rational and use the standard final semantics for
F
-coalgebras.
→
Lemma 14
℘
.
Then we obtain that φ
#
is equal to the conservative extension
(
lifting
)
of ℘
,
that is
,
φ
#
=
T
(℘)
.
Let us consider Proposition
45
when F
=
B
P
and φ
=
B
P
(η
X
)
◦
Proof
Let as consider the definition of the mapping
φ
#
given in the proof of Propo-
sition
45
. It is enough to show that
φ
#
=
T
(℘)
for the variables
p
k
∈
X
. In fact,
φ
#
(p
k
)
=
φ(p
k
)
=
B
P
(η
X
)
◦
℘(p
k
)
=
℘(p
k
)
=
T
(℘)(p
k
)
.
Hence, from this lemma we obtain that the non-guarded specification of behavior
φ
#
:
T
P
→
B
P
(
T
P
X)
(the unique extension of the recursive guarded specification
φ
=
B
P
(η
X
)
◦
℘
:
X
→
B
P
(
T
P
X)
) is equal to conservative extension
T
(℘)
of the
non-recursive but guarded specification
℘
→
B
P
X
.
Based on Proposition
45
and Lemma
14
, we obtain the following results:
:
X
Corollary 25
The general Proposition
45
,
in the case when the endofunctor F is
equal to the abstract behavior
B
P
,
can be applied to
th
e final database-mapping
sem
an
tics based on the general behavior endofunctor
B
P
=
S
×
B
P
with
D
P
S
=
gfp(
B
P
) and a guarded recursive specification φ
=
B
P
(η
X
)
◦
℘
.
We obtain the following commutative diagram of the fin
al
B
P
-coalgebra seman-
tics for the guarded non-recur
siv
e specification
[
_
]:
X
→
B
P
(X)
(
external square
of this diagram
),
based on the
B
P
-coalgebra semanti
cs
for its derived non-guarded
g
E
,φ
#
:
T
P
X
recursive specification ψ
=
ass
◦
→
B
P
(
T
P
X)
(
in internal square
diagram
(14))
where φ
#
=
T
(℘)
=
B
P
(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)
,
