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