Information Technology Reference
In-Depth Information
For each of the operations defined above on sets, there are analogous ones on
functions. Let
f
:
X
→
Y
,
f
1
:
X
→
Y
and
f
2
:
Z
→
W
. We define the following
operations:
+
f
2
:
X
+
Z
+
W
f
1
×
f
2
:
X
×
Z
→
Y
×
W
f
1
→
Y
(
f
1
×
f
2
)(
x, z
f
1
(
x
)
,f
2
(
z
)
(
f
1
+
f
2
)(
c
)=
c, c
∈{⊥
,
}
)=
f
A
:
X
A
Y
A
→
(
f
1
+
f
2
)(
κ
i
(
x
)) =
κ
i
(
f
i
(
x
))
,i
∈{
1
,
2
}
f
A
(
g
)=
f
◦
g
Note that here we are using the same symbols that we defined above for the
operations on sets. It will always be clear from the context which operation is
being used.
In our definition of non-deterministic functors we will use constant sets
equipped with an information order. In particular, we will use join-semilattices.
A (bounded) join-semilattice is a set
B
equipped with a binary operation
∨
B
and
a constant
⊥
B
∈
B
, such that
∨
B
is commutative, associative and idempotent.
The element
⊥
B
is neutral with respect to
∨
B
.Asusual,
∨
B
gives rise to a partial
ordering
b
1
∨
B
b
2
=
b
2
.Everyset
S
can be
mapped into a join-semilattice by taking
B
to be the set of all finite subsets of
S
with union as join.
≤
B
on the elements of
B
:
b
1
≤
B
b
2
⇔
Coalgebras.
A coalgebra is a pair (
S, g
:
S
→
G
(
S
)), where
S
is a set of states
and
, together with the function
g
,
determines the
transition structure
(or dynamics) of the
G
:
Set
→
Set
is a functor. The functor
G
G
-coalgebra [13].
Definition 1 (Bisimulation).
Let
(
S, f
)
and
(
T,g
)
be two
G
-coalgebras. We
call a relation
R
⊆
S
×
T
a
bisimulation
[7] iff
(
s, t
)
∈
R
⇒
f
(
s
)
,g
(
t
)
∈
G
(
R
)
G
(
R
)
is defined as
G
(
R
)=
{
G
(
π
1
)(
x
)
,
G
(
π
2
)(
x
)
|
x
∈
G
(
R
)
}
where
.
We write
s
∼
G
t
whenever there exists a bisimulation relation containing (
s, t
)
∼
G
the bisimilarity relation. We shall drop the subscript
G
and we call
whenever
G
the functor
is clear from the context.
Polynomial functors.
They are functors
G
:
Set
→
Set
, built inductively from
)
A
:
the identity, and constants, using
×
,
+ and (
−
+
A
(1)
where
B
is a (non-empty) finite join-semilattice and
A
is a finite set. Typical
examples of polynomial functors include
PF
G
::=
Id
|
B
|
G
G
|
G
×
G
|
G
=(
B
×
Id
)
A
,
R
=
B
×
Id
,
M
D
=
×
Id
A
+
Id
)
A
. These functors represent, respectively, the type
of Mealy, deterministic and partial deterministic automata.
2
and
Q
=(1
R
-bisimulation is
stream equality, whereas
-bisimulation coincides with language equivalence.
Next, we give the definition of the ingredient relation, which relates a poly-
nomial functor
D
with its
ingredients
,
i.e.
the functors used in its inductive
construction. We shall use this relation later for typing our expressions.
G
Search WWH ::
Custom Search