Information Technology Reference
In-Depth Information
ε
1
:
F G
ε
2
:
F G
ε
1
⊕ ε
2
:
F G
is represented by the equation
ε
1
⊕
ε
2
:
F
G
=
ε
1
:
F
G
∧
ε
2
:
F
G
.Forthe
sake of notation, algebraically we write
ε
:
F
G
to represent expressions of type
F
.
The structured expressions
σ
G
∈
F
(
Exp
G
)aregivenbythesetof
Σ
-terms of
sort
ExpStruct
, such that
)=
true
(here : is the extension of
the type-checking operator to structured expressions). Algebraically, we write
σ
:
E
G
σ
:
F
(
Exp G
(
Exp
G
).
The function
δ
G
, which provides the coalgebraic structure of
F
(
Exp
G
)todenotethat
σ
is an element of
F
G
-expressions,
has the algebraic correspondent
δ
∈
Σ
, a function parameterized with the functor
ingredients.
Recall from Section 2 that a relation
R⊆
Exp
G
G
×
Exp
G
G
is a bisimulation
if and only if (
s, t
)
∈R⇒
δ
G
G
(
s
)
,δ
G
G
(
t
)
∈
G
(
R
). In order to enable the
algebraic framework to decide bisimilarity of
G
-expressions, we define a new
entailment relation for polynomial functors
PF
(the definitions of
G
and
PF
are closely related).
Definition 6.
The entailment relation
with the fol-
lowing inference rules, which allow a restricted contextual reasoning over the
frozen equations of structured expressions:
PF
is the extension of
σ
1
=
σ
1
σ
2
=
σ
2
E
G
PF
E
G
PF
(5)
σ
1
,σ
2
E
G
PF
σ
1
,σ
2
=
E
G
PF
σ
=
σ
(6)
E
G
PF
k
i
(
σ
) =
k
i
(
σ
) (
i
= 1
,
2)
E
G
PF
f
(
a
) =
g
(
a
)
,
for all
a
∈
A
(7)
E
G
PF
f
=
g
Let
G
be a polynomial functor, and
R
a binary relation on the set of
G
-
expressions. We will make use of the conventions:
-
R
id
=
R∪{
(
ε, ε
)
|E
G
ε
:
G
G
=
true
}
-
cl
(
R
) is the closure of
R
under transitivity, symmetry and reflexivity
=
e∈R
{
R
e
}
R
-
(application of the freezing operator to all elements of
)
ε
=
ε
(
ε, ε
)
-
E
G
∪ R
is a shorthand for (
S, Σ, E
∪{
|
∈R}
)
-
δ
G
G
(
ε
=
ε
) denotes the equation
δ
G
G
(
ε
)=
δ
G
G
(
ε
)
-
σ, σ
∈
G
) is a shorthand for: (
σ, σ
)isanelementoftheset
S
,where
(
R
E
G
G
(
R
)=
S
(here,
G
(
R
)
⊆T
Σ,
ExpStruct
×T
Σ,
ExpStruct
)
The following theorem and corollary correspond to the equivalences (
i
), and
respectively (
ii
), in Fig. 1. Theorem 2 formalizes the connection between the
inductive definition of
PF
(on the algebraic side),
hence enabling the definition of bisimulations in algebraic terms, in Corollary 1.
G
(on the coalgebraic side) and
Search WWH ::
Custom Search