Database Reference
In-Depth Information
B
P
(
That is, every natural transformation
ρ
:
Σ
P
D
P
D
P
Σ
P
D
P
)
de-
fines coinductively a lifting
D
ρ
of the comonad
D
P
to the
Σ
P
-algebras: given
a
Σ
P
-algebra ('assumption')
k
:
Σ
P
S
→
S
, the structure (
Σ
P
-algebra)
D
ρ
(k)
:
Σ
P
(
D
P
S
)
→
D
P
S
can be seen as the
denotational model
on the set of global be-
D
P
S
:
Σ
P
D
P
haviors (trees)
. In fact, for a given natural transformation
ρ
B
P
(
D
P
Σ
P
D
P
)
and a set
S
, there is a morphism
ρ
S
:
Σ
P
D
P
(
S
→
B
P
(
D
P
)
Σ
P
D
P
)(
S
:
Σ
P
S
→
S
S
×
B
P
)
-coalgebra
)
and for a given
Σ
P
-algebra
k
,the
(
[
◦
]
[
snd
S
,ρ
S
]:
D
P
S
Σ
P
D
P
S
→
S
×
B
P
(
D
P
S
Σ
P
D
P
S
ε
s
,k
Σ
P
(ε
s
)
,
)
, with
the unique arrow
f
to the final
(
=[
◦
]
S
×
B
P
)
-coalgebra from a di-
ε
s
,k
Σ
P
(ε
s
)
agram (4a)
The unique 'parameter' in this commutative diagram is the arrow
k
(all
other arrows have fixed semantics). The arrow
f
(which is the unique coinductive
extension of
:
Σ
P
S
→
S
[
snd
S
,ρ
S
]
along
[
ε
S
,k
◦
Σ
P
(ε
S
)
]
) is composed of two components, the
identity
id
D
P
S
:
D
P
S
→
D
P
S
and the component denoted by
D
ρ
(k)
:
Σ
P
D
P
S
→
f
that uniquely defines the ar-
D
P
S
, with
[
id
,
D
ρ
(k)
]=
=[
ε
S
,k
◦
Σ
P
(ε
S
)
]
D
P
S
row
D
ρ
(k)
for any given arrow
k
, so that the diagram (4d) above can be reduced to
the following commutative subdiagram
Consequently, the 'lifting' comonad
D
ρ
maps a
Σ
P
-algebra
(
S
,k
:
Σ
P
S
→
S
)
into
the
Σ
P
-algebra
(
D
P
S
,
D
ρ
(k)
:
Σ
P
D
P
S
→
D
P
S
)
called SOS-denotational
Σ
P
-