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
sum (a, b)
prod (a, b)
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 RegExp.nf strong enough to define an equality on Reg by x = y iff x <= y and y <= x ?