Database Reference
In-Depth Information
where the
β
λ
in diagram (12) is a unique
F
-homomorphism into the final
F
-
coalgebra, and hence
β
λ
gfp(F)
F
F(gfp(F))
is just the final
λ
-bialgebra. It was demonstrated [
6
] that for a given distributive law
λ
, for any
guarded recursive mapping given by a
F
T
P
(gfp(F))
T
P
-coalgebra
φ
:
X
→
F(
T
P
X)
, there is
a unique “solution”
φ
@
gfp(F)
(so-called
λ
-coiterative arrow induced by
φ
)
such that the following diagram commutes:
:
X
→
=
−
F
◦
so that,
φ
@
T
P
(φ
@
)
◦
◦
:
→
gfp(F)
.
It is an interesting consideration in [
19
] that the uniqueness of the solution
φ
@
,
for a given guarded recursive mapping
φ
, is a based on the fact that there is a bijec-
tive representation of
φ
by the
λ
-bialgebra
F(β
λ
)
F
φ
X
μ
X
φ
#
T
P
X
F(
2
T
P
X
T
P
X)
, where
φ
#
=
◦
λ
T
P
X
◦
T
P
(φ)
, (and, vice versa, for each
λ
-bialgebra
F(μ
X
)
μ
X
g
2
T
P
X
F(
T
P
X)
T
P
X
its corresponding guarded recursive mapping
φ
is equal to
g
◦
η
X
), so that there is a
unique homomorphism into the final
λ
-bialgebra
T
P
gfp(F)
F
gfp(F)
.
β
λ
gfp(F)
F
However, here we will present a more simple and direct representation, based on the
standard final
F
-coalgebra semantics:
Proposition 45
For each guarded recursive specification φ
:
X
→
F(
T
P
X)
,
there
exists a unique solution φ
@
φ
#
◦
gfp(F) such that φ
#
:
→
(gfp(F),
F
) is the unique F -coalgebra homomorphism into the final F -coalgebra
,
=
η
X
:
→
T
P
X, φ
#
)
X
(
