Information Technology Reference
In-Depth Information
Note that, throughout the paper, we will use streams as a basic example to
illustrate the definitions. It should be remarked that the framework is general
enough to include more complex examples, such as deterministic automata, au-
tomata on guarded strings or Mealy machines. The latter will be used as example
in Section 4.1.
3 An Algebraic View on the Coalgebra of Generalized
Regular Expressions
We now have a (theoretical) framework which, given a functor
G
, allows for the
uniform derivation of 1) a language
Exp
G
for specifying behaviors of
G
-systems,
and 2) a coalgebraic structure on
Exp
G
, which provides an operational semantics
to the set of expressions. In the rest of the paper, we will extend and adapt the
framework of the previous section in order to:
-
enable the implementation of a tool which allows for the automatic derivation
of 1) and 2) above
-
enable automatic reasoning on equivalence of specifications; the reasoning
will be performed by the coinductive prover
CIRC
[12], which is also the core
of our target tool.
CIRC
is based on algebraic specifications and, therefore, to reach our final goal
we need two things:
-
algebraic specifications
that model both the language and the coalgebraic
structure of expressions associated to polynomial functors to provide to
CIRC
-
a decision procedure, implemented in
CIRC
based on an
equational entailment
relation
, in order to check for the bisimilarity of expressions.
We further give the basic notions the reader needs in order to get an easier
understanding of the algebraic approach. An
algebraic specification
is a triple
E
=(
S, Σ, E
), where
S
is a set of
sorts
,
Σ
is a
many-sorted signature
and
E
is a
set of
conditional equations
of the form (
X
)
t
=
t
if
(
i∈I
u
i
=
v
i
), where
t
,
t
,
∀
u
i
,and
v
i
(
i
I
- a set of indexes for the conditions) are
Σ
-terms with variables
in
X
. We say that the
sort of the equation
is
s
whenever
t, t
∈T
Σ,s
(
X
). Here,
T
Σ,s
(
X
) denotes the set of terms of sort
s
of the
Σ
-algebra freely generated by X.
If
I
=
∈
X
)
t
=
t
.
{}
then the equation is
unconditional
andmaybewrittenas(
∀
Let
be the
equational entailment (deduction) relation
defined as in [5]. We
write
E
e
whenever equation
e
is deducible from
E
.Weextend
E
by adding
the freezing operation
Σ
,where
Frozen
is a
fresh sort. By
t
we represent the
frozen
form of a
Σ
-term
t
,andby
e
a
frozen
equation
of the shape (
−
:
s
→
Frozen
for each sort
s
∈
X
)
t
=
t
is defined over
frozen equations as in [12]. The need for the frozen operator will become clear
in Example 2: without it the congruence rule could be applied freely leading to
the derivation of untrue equations.
Fig. 1 briefly illustrates the parallel between the coalgebraic concepts pre-
sented in [15,2] and their algebraic correspondents. In what follows, we will
∀
if
c
. The entailment relation
Search WWH ::
Custom Search