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