A Decision Procedure for Bisimilarity of Generalized Regular Expressions - Formal Methods: Foundations and Applications - page 229

Definition 2. Let ⊆ PF × PF be the least reflexive and transitive relation on

polynomial functors such that

A

G 1 G 1 × G 2 , G 2 G 1 × G 2 , G 1 G 1 + G 2 , G 2 G 1 + G 2 , G G

Here and throughout this document we use F G as a shorthand for F , G ∈ .

. For example, 2, Id , Id A and If F G ,then F is said to be an ingredient of G D

itself are all the ingredients of the deterministic automata functor D .

A language of regular expressions for polynomial coalgebras. We now
associate a language of expressions Exp G with each polynomial functor G .

Definition 3 (Expressions). Let A be a finite set, B a finite join-semilattice
and X a set of fixed-point variables. The set Exp of all expressions is given by
the following grammar, where a

∈ A , b ∈ B and x ∈ X :

ε ::= ∅ | x | ε ⊕ ε | μx.γ | b | l ε | r ε | l [ ε ] | r [ ε ] | a ( ε ) (2)

where γ is a guarded expression given by:

γ ::= ∅ | γ ⊕ γ | μx.γ | b | l ε | r ε | l [ ε ] | r [ ε ] | a ( ε ) (3)

In the expression μx.γ , μ is a binder for all the free occurrences of x in γ .Vari-
ables that are not bound are free. A closed expression is an expression without
free occurrences of fixed-point variables x . We denote the set of closed expres-
sions by Exp c .
The language of expressions for polynomial coalgebras is a generalization of
the classical notion of regular expressions: ε 2 and μx.γ play similar roles

to the regular expressions denoting empty language, the union of languages and
theKleenestar.Theexpressions l

∅ , ε 1 ⊕

, l [ ε ], r [ ε ]and a ( ε ) refer to the left and
right hand-side of products and coproducts, and function application, respec-
tively. Next, we present a type assignment system for associating expressions
to polynomial functors. This will allow us to associate with each functor

ε , r ε

G the

∈ Exp c that are valid specifications of expressions ε G -coalgebras.

Definition 4 (Type system). We now define a typing relation ⊆ Exp × PF ×

PF that will associate an expression ε with two polynomial functors F and G ,

which are related by the ingredient relation ( F is an ingredient of G ). We shall

write ε : F G for ε, F , G ∈ . The rules that define are the following:

ε : G G
μx.ε : G G ∅ : F G b : B G x : G G

ε 1 : F G ε 2 : F G
ε 1 ⊕ ε 2 : F G

ε : G G
ε :

ε : F 2 G
r [ ε ]: F 1

ε : F G
a ( ε ): F A G

+

Id G F 2 G

F 1 G
lε : F 1 × F 2 G

ε : F 2 G

rε : F 1 × F 2 G

ε : F 1 G

l [ ε ]: F 1

ε :

+ F 2 G