The Reg structure


signature pKA
structure Reg : pKA

The structure Reg is an approximation of the free Kleenean algebra over some alphabet. The free Kleenean algebra over an alphabet has equivalence classes of regular expressions (over the alphabet) as objects, while in Reg we use (quasi-) normal forms of regular expressions.

The signature pKA is a signature for polymorphic Kleenean algebras, in the sense that the type of its objects is parametric in some other type. We want to use regular expressions without fixing the alphabet in advance.


type 'a t
val unit : 'a t
val zero : 'a t
val sum : ''a t * ''a t -> ''a t
val prod : ''a t * ''a t -> ''a t
val star : ''a t -> ''a t


type 'a t
the type of objects of the algebra, the regular expressions over alphabet 'a, or 'a RegExp.t.

the neutral element of multiplication, RegExp.Times [].

the neutral element of addition, RegExp.Plus [].

sum (a, b)
returns the sum of a and b, more precisely of RegExp.Plus [a,b].

prod (a, b)
returns the product of a and b, more precisely of RegExp.Times [a,b].

star a
returns the iteration of a, more precisely, returns of RegExp.Star a.

See Also

RegExp, pkaMatrix, KA


The iteration of an element a of a Kleenean algebra is the least element b such that unit <= b and prod(a,b) <= b, where x <= y is defined by sum(x,y) = y.

Is strong enough to define an equality on Reg by x = y iff x <= y and y <= x ?