The Reg structure

Synopsis

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.

Interface

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


Description

type 'a t


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

unit

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

zero

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

sum (a, b)

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

prod (a, b)

returns the product of a and b, more precisely RegExp.nf of RegExp.Times [a,b].

star a

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

See Also

RegExp, pkaMatrix, KA

Discussion

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 RegExp.nf strong enough to define an equality on Reg by x = y iff x <= y and y <= x ?