Database Reference
In-Depth Information
so that λ is a natural transformation. It is easy to verify that it satisfies the unit and
multiplication axioms.
We have introduced the abstract notion of operational rules as the natural trans-
formations : Σ P (Id
B P T P , and hence derive the natural transforma-
× B P )
B P T P . The natural transformation
T P :
tions
= B P μ
Σ P (
T P × B P T P )
Σ P B P T P B P T P is a component of the natural transforma-
tion that represents the Σ P -actions on the observables, so that for each set X its
component ϑ X is defined by:
1. nil
(i.e., germ ) ϑ
:
→∅
, and for any a
Act , a
→∅
;
2. (Y,i) →{ (a i ,a k .t k ) | (a k ,t k ) Y }
if n =| Y |≥
1;
otherwise;
3. (Y 1 ,...,Yt n ) 1 i n Y i .
Thus, there is a unique Σ P -homomorphism
B P (
T P X), B P X ),ϑ X
λ X :
(
B P X,
P )
from the initial algebra, with
P =[
inl
B P X , inr
B P X ]=[ η B P X , inr
B P X ]
such that
the following diagram commutes
Consequently, it is easy to verify that the λ X in this lemma is well defined.
For example, for S
={
(a 1 ,p k 1 ),...,(a n ,p k n )
}∈ B P (X) , from point 3 above,
λ X (a.S)
={
(a,a 1 .p k 1 ),...,(a,a n .p k n )
}∈ B P (
T P X) , with λ X (a.
{
(a 1 ,p k 1 )
}
)
=
{ (a,a 1 .p k 1 ) }
, and λ X (a. ) =∅
.Or,for S i B P (X) , i =
1 , 2 , 3 , 4 and t 1 = S 1 ,t 2 =
a 2 .S 2 ,t 3 = a 3 .S 3 ,t 4 = S 4 , from point 4,
λ X
4 (t 1 ,t 2 ,t 3 ,t 4 )
4 (S 1 ,a 2 .S 2 ,a 3 .S 3 ,S 4 )
= (a 2 ,a i .p k i )
λ X
=
S 2 (a 3 ,a i .p k i )
S 3
|
(a i ,p k i )
|
(a i ,p k i )
S 1
S 4 .
The associate notion of a model is a so-called λ -bialgebra that consists of an object
(a set) X with a pair of maps
β
γ
X
FX , where β is a T P -algebra
T P X
(Eilenberg-Moore monadic algebra such that β
η X =
id X and β
μ x =
β
T P (β) ),
that is, β is a F -homomorphism from (
T P X, λ X T P (β)) into F -coalgebra (X,γ )
such that the following two diagrams commute:
Search WWH ::




Custom Search