Database Reference
In-Depth Information
where φ
#
F(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)
.
It is represented by the following commutative
diagram
:
In particular
,
it is valid for the case when F
=
B
P
=
P
fin
(Act
×
_)
:
Set
→
Set
.
Proof
We have to show that for a general recursive specification
φ
#
:
T
P
X
→
F(
T
P
X)
, given by
φ
#
F(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)
, its reduction to the variables
X
⊆
T
P
X
, expressed by the arrow
φ
#
◦
η
X
:
X
→
F(
T
P
X)
,is
equal
to the given
guarded
recursive specification
φ
. In fact,
φ
#
◦
η
X
=
η
X
from the natural transformation
η
F(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)
◦
T
P
applied to arrow
λ
X
:
Id
=
◦
λ
T
P
X
◦
η
F
T
P
X
◦
φ
from the 'unit-
λ
' property when
X
substituted by
F(μ
X
)
T
P
X
=
F(μ
X
)
◦
F(η
T
P
X
)
◦
φ
(from the monad property
I
d
=
μ
◦
T
P
η
)
=
φ.
By using the natural transformation (a germ)
ϑ
:
Σ
P
F
T
P
F
T
P
, in the proof
of Lemma
13
, it is easy to see by the following initial
Σ
P
-algebra commutative
diagram that, for any
φ
:
X
→
F
T
P
X
, the mapping
φ
#
is its
unique
extension:
From this commutative diagram we obtain that this unique function
φ
#
is defined
recursively (based on the mapping
ϑ
X
defined in the proof of Lemma
13
)bythe
following mapping: