Database Reference
In-Depth Information
model
B
P
-colagebra (i.e., 'assumption')
m
:
X
→
B
P
(X)
, the structure (
B
P
-
colagebra)
T
P
X)
can be seen as the
operational model
on the
set of terms (with the process variables) in
T
(m)
:
T
P
X
→
B
P
(
T
P
X
. In fact, for a given natural trans-
formation
and a set
X
, there is a morphism
X
:
T
P
X
×
B
P
T
P
X)
→
B
P
T
P
X
Σ
P
(
defined by:
1.
nil
Act
;
2.
((t,Y),i)
→{
(a
i
,a
k
.t
k
)
|
(a
k
,t
k
)
∈
Y
}
→∅
, and
a
→∅
for each
a
∈
if
|
Y
|≥
1
;∅
otherwise;
3.
((t
1
,Y
1
),...,(t
n
,Y
n
))
→
1
≤
i
≤
n
Y
i
.
For a given
B
P
-coalgebra
m
:
X
→
B
P
X
, there is a
(X
Σ
P
)
-algebra
η
X
,
m
,
h,
X
]
:
B
P
(η
X
)
◦
[
X
Σ
P
(
T
P
X
×
T
P
X
×
B
P
T
P
X)
→
B
P
T
P
X,
with the unique arrow
[
id
T
P
X
,
T
(m)
]
from the initial 'syntax'
(X
Σ
P
)
-algebra,
so that the following diagram commutes
The unique parameter in this commutative diagram is the arrow
m
:
X
→
B
P
X
(all other arrows have fixed semantics). The mapping
T
(m)
is a component of the
unique arrow from the initial
(X
Σ
P
)
-algebra, so that the diagram above can be
reduced to the following interesting commutative component:
Thus, for any 'parameter' (coalgebra structure)
m
:
X
→
B
P
X
, its
conservative ex-
T
(m)
:
T
P
X
→
B
P
(
T
P
X)
is uniquely recur-
tension
to all terms with variables
sively determined (notice that for all variables
p
k
∈
⊆
T
P
X
,
T
(m)(p
k
)
=
X
m(p
k
)
)
by:
1.
p
k
→
m(p
k
)
(note that it can be the empty set
∅
as well);
2.
nil
Act
;
3.
a.t
→{
(a,a
i
.t
i
)
|
(a
i
,t
i
)
∈
T
(m)(t)
}
→∅
, and
a
→∅
for each
a
∈
if
|
T
(m)(t)
|≥
1
;∅
otherwise;
n
(t
1
,...,t
n
)
→
1
≤
i
≤
n
T
(m)(t
i
)
.
Thus, the injective function
η
X
:
X
→
T
P
X
'lifts' to the coalgebra mapping (dia-
gram (8))
η
X
:
4.
(X,m)
→
(
T
P
X,
T
(m))
for every coalgebra structure
m
on
X
.
