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: