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:
Search WWH ::




Custom Search