Information Technology Reference
In-Depth Information
coalgebraic
algebraic
ε
:
F
G
E
G
ε
:
F
G
=
true
Exp
F
G
{ε ∈T
Σ,
Exp
|E
G
ε
:
F
G
=
true}
Exp
G
{ε ∈T
Σ,
Exp
|E
G
ε
:
G
G
=
true}
F
(
Exp
G
)
{σ ∈T
Σ,
ExpStruct
|E
G
σ
:
F
(
Exp G
)=
true}
δ
F
G
:
Exp
F
G
→
F
(
Exp
G
)
Ingredient Exp
→
ExpStruct
E
G
σ
:
F
(
Exp G
)=
true
,
E
G
σ
:
F
(
Exp G
)=
true
δ
( ):
σ, σ
∈
F
(
cl
(
R
id
))
E
G
∪ R
PF
σ
=
σ
(
i
)
cl
(
R
id
)isabisimulation
E
G
∪ R
PF
δ
G
G
(
R
)
(
ii
)
Fig. 1.
Polynomial functors - coalgebraic vs. algebraic approach
provide some explanations on the algebraic side, in order to model what we
presented coalgebraically in the previous section, analyzing the components of
Fig. 1.
The algebraic specification of a polynomial functor.
For the provided
functor
E
G
=(
S, Σ, E
) is incrementally built according to
the items common to all regular expressions, extended with the items specific to
G
G
, the specification
(
e.g.
, the semilattices, the exponentiation alphabets). As an initial step in the
construction of
E
G
, we use the general rule for translating definitions based on
Backus-Naur grammars into algebraic specifications. Each syntactical category
and vocabulary is considered as a sort, and each production is considered as
a constructor operation or a subsort relation. For instance, according to the
grammar of generalized regular expressions in Definition 3, we have: a sort
Exp
representing expressions
ε
,
FixpVar
the sort for the vocabulary of the fixed-point
variables,
Alph
the sort for the elements of the alphabets, and
Slt
the sort for
the elements of the semilattices. Moreover, we consider constructor operations
for all the productions. For example, the production
ε
:: =
ε
⊕
ε
is represented
by an operation
⊕
:
Exp Exp
→
Exp
. Using a similar mechanism, we specify:
-
structured expressions
σ
, the counterpart of
F
(
Exp
G
), defined by
,σ
)
we denote the sort of this kind of expressions by
ExpStruct
(the construction
λx.
(
a,
σ
::=
ε
|
σ, σ
|
k
1
(
σ
)
|
k
2
(
σ
)
|⊥||
λx.
(
a,
F
G
∈
F
A
(
Exp
G
))
-
polynomial functors defined by grammar (1); the associated sort is
Functor
-
functor ingredients given in Definition 2; the corresponding sort is
Ingredient
F
G
,σ
) has as coalgebraic correspondent a function
f
The set
Exp
F
G
of expressions of type
F
G
is algebraically represented by the
set of
Σ
-terms
ε
of sort
Exp
, such that
=
true
. The type-checking
relation in Definition 4 is given by an operation : :
Exp Ingredient
→
Bool
and
an equation for each inference rule defining this relation. For example
E
G
ε
:
F
G
Search WWH ::
Custom Search