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

We can now formally define the set of G -expressions: well-typed expressions

associated with a polynomial functor G .

Definition 5 ( G -expressions). Let G be a polynomial functor and F an ingre-

dient of G . We define Exp FG by:

∈ Exp c Exp FG = { ε | ε : F G } .

We define the set Exp G of well-typed G -expressions by Exp GG .

In [2], it was proved that the set of G -expressions for a given polynomial functor

G has a coalgebraic structure:

δ G : Exp G → G ( Exp G )

More precisely, in [2,15], which we refer to for the complete definition of δ G ,the
authors defined a function δ FG : Exp FG → F

( Exp G )andthenset δ G = δ GG .
The coalgebraic structure on the set of expressions enabled the proof of a
Kleene like theorem.

Theorem 1 (Kleene's theorem for polynomial coalgebras). Let G be a

polynomial functor.

1. For any ε ∈ Exp G , there exists a finite G -coalgebra ( S, g ) and s ∈ S such that

s .
2. For every

ε ∼

G -coalgebra ( S, g ) and s ∈ S there exists an expression ε s ∈ Exp G

such that ε s ∼

s .

In order to provide the reader we intuition over the notions presented above, we
illustrate them with an example.

Example 1. Let us instantiate the definition of G -expressions to the functors of

streams itself).

Let X be a set of (recursion or) fixed-point variables. The set Exp R of stream
expressions is given by the set of closed and guarded expressions generated by
the following BNF grammar. For x

R = B × Id (the ingredients of this functor are B , Id and R

∈ X :

Exp R ε ::= ∅ | ε ⊕ ε | μx.ε | x | l ε 1 | r ε

(4)

ε 1 ::= ∅ | b | ε 1 ⊕ ε 1

Intuitively, the expression l b is used to specify that the head of the stream

is b , while r specifies a stream whose tail behaves as specified by ε .Forthe

two element join-semilattice B =

ε

{ 0 , 1 } (with ⊥ B = 0), examples of well-typed

expressions include ∅ , l 1 ⊕ r l ∅ and μx.r x ⊕ l 1 . The expressions l [1],

l 1 ⊕ 1and μx. 1 are examples of non well-typed expressions for R , because the

+ , the subexpressions in the sum have different type,
and recursion is not at the outermost level (1 has type B R

functor R does not involve

), respectively.