The KA signature

Synopsis

signature KA
structure Path : KA
structure Conway : KA


A signature for Kleenean algebras. The regular languages over an alphabet (see Reg) form the free Kleenean algebra generated by the letters.

Interface

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


Description

type t


zero

returns the neutral element of addition, 0.

sum (a, b)

returns the addition of a and b.

unit

returns the neutral element of multiplication, 1.

prod (a, b)

returns the product of a and b.

star a

returns the Kleenean closure of a, the least element b such that ab+1<=b.

See Also

Reg, kaMatrix

Discussion

Example:

The structure Path:KA is a Kleenean algebra which is used to compute shortest paths in weighted graphs, by coding the graph as a matrix M over Path and considering M*.

structure Path : KA =
    struct
	type t = int
	val SOME zero = Int.maxInt
	val sum = Int.min
	val unit = 0
	fun prod (n,m) = if m=zero orelse n=zero then zero else n+m
	fun star x = 0
    end

Example:

The 4-element structure Conway:KA satisfies all equations between regular expressions that are true in the language interpretation. But it is not a Kleenean algebra, because 2* is not the least b such that 2b+1 <= b. In particular, Conway does not satisfy 1 + y + yy + yyy + ... = y*.

 structure Conway : KA =
    struct
	type t = int  (* {0,1,2,3} *)
	val zero = 0
	val unit = 1
	val sum = Int.max
	fun prod (x,y) = if x=0 orelse y=0 then 0 else Int.max (x,y)
	fun star 0 = 1
	  | star 1 = 1
	  | star 2 = 3
	  | star 3 = 3
	  | star _ = raise Size
    end