Database Reference
In-Depth Information
The final coalgebra isomorphism
B
:
D
P
S
→
S
×
B
P
(
D
P
S
)
splits into two
epic projections (i.e., surjective functions)
B
=
fst
S
, snd
S
, where for a given LTS
@
=[
p
k
]
=
tree
t
with the root state
ass(p
k
)
,
fst
S
restitutes its root state, i.e.,
fst
S
(t)
@
,
ass(p
k
)
, while
snd
S
restitutes the trees obtained by division of all subtrees of
[
A
]
a
1
a
n
t
1
,...,
t
n
}={
(a
1
,t
1
),...,(a
n
,t
n
)
}∈
P
fin
(Act
snd
S
(t)
={
×
D
P
S
)
=
B
P
(
D
P
S
)
where
t
i
∈
D
P
S
,
1
≤
i
≤
n
are the subtrees of
t
if we eliminate its root
state
ass(p
k
)
, and
n
≥
1 is the number of branches that come from the root
ass(p
k
)
.
Consequently, for a set
X
and
(
S
×
B
)
-coalgebra
(X,
[
_
]
)
in the category
Set
of all
(
S
×
B
P
)
-coalgebras, there is a unique coalgebra homomorphism
B
@
[
_
]
:
(X,
[
_
]
)
−→
(gfp(
S
×
B
P
),
B
)
from this
(
S
×
B
P
)
-coalgebra to the final
@
(
S
×
B
P
)
-coalgebra such that the diagram above in
Set
commutes, where
[
_
]
:
−→
S
×
B
P
)
is a 'coinductive' extension of the arrow
[
]:
−→
S
×
B
P
(X)
X
gfp(
_
X
such that for any process
p
k
∈
X
at the state
ass(p
k
)
∈
S
, we obtain
@
@
)
•[
p
k
]
(ass(p
k
),
{
(a
i
,
[
p
k
+
i
]
|
(a
i
,p
k
+
i
)
∈
℘
S
(s
k
)
}
)
if
℘(p
k
)
=∅
;
ass(p
k
)
, otherwise,
which is a labeled (possibly infinite) tree with the root in the state (instance database)
A
∈
S
⊆
D
P
S
@
=
ass(p
k
)
∈
S
⊆
Ob
DB
. That is,
[
p
k
]
is an LTS tree
L
A
with the root state
A
=
Ob
DB
.
One of the properties of Aczel's coinductive semantics for CCS (similar to this
one) is that it maps two processes
p
k
and
p
m
to the same set if they are observation-
ally equivalent (it is denoted by
p
k
∼
ass(p
k
)
composed of states in
S
and transitions in
Act
⊆
p
m
):
@
@
.
(BSM) p
k
∼
p
m
iff
[
p
k
]
=[
p
m
]
That is, the coinductive extension of the operational model
[
_
]:
X
−→
S
×
B
P
(X)
does preserve
B
P
bisimulation and, conversely, it can be “pulled back” to form the
largest
B
P
-bisimulation relation.
The above is a property which holds in general for every coinductive extension of
coalgebras of endofunctors
S
×
B
P
preserving categorical (weak) pullbacks. Thus,
one does not need to work with non-well founded sets, as we did.
A condition which well-behaved operational semantics should satisfy is
compo-
sitionality
: To every behavior
B
P
there corresponds a notion of observational equiv-
alence called
_
)
cor-
responds to Milner's strong bisimulation—the finest notion of observational equiv-
alence for transition relations). If this observational equivalence is a congruence
(as in our case) w.r.t. the construct of the syntax, then the operational semantics
is compositional. This means that programs with the same observable behavior
can be interchanged in any context without affecting the overall observable behav-
ior.
The construction of coalgebraic operational semantics can be done by using the
duality property between algebras and coalgebras: instead of the set of variables
X
,
by duality we use the corresponding set of states
B
P
-bisimulation [
3
] (which for the behavior
B
P
=
P
fin
(Act
×
S
; instead of
Σ
P
syntax endofunc-
tor, we use the behavior endofunctor
B
P
; instead of coproduct (disjoint union)
,
