The RegMat structure


Synopsis

structure RegMat : sig ... end

This is the matrix algebra over the Kleenean algebra Reg of regular expressions (with free variables).


Interface

structure Ring : pKA
type 'a t
val dimension : 'a t -> int * int
val tabulate : int * int
                 -> (int * int -> 'a Ring.t) -> 'a t
val sub : 'a t * (int * int) -> 'a Ring.t
val map : ('a Ring.t -> 'a Ring.t) -> 'a t -> 'a t
val zero : int * int -> 'a t
val unit : int * int -> 'a t
val sum : ''a t * ''a t -> ''a t
val prod : ''a t * ''a t -> ''a t
val star : ''a t -> ''a t
val transpose : ''a t -> ''a t

Description

structure Ring : pKA
the structure Reg, an approximation of the free Kleenean algebra of regular expressions under provable equivalence.

type 'a t
the type of matrices with entries of type 'a Ring.t.

dimension A
returns the dimension of the matrix A.

tabulate (i, j) f
returns the matrix of dimension (i,j) with entries f(i',j').

sub (A, (i, j))
returns the element at field (i,j) of matrix A.

map f A
returns the matrix whose fields contain the f-images of the fields of A.

zero (i, j)
returns the matrix of dimension (i, j) whose fields are filled with the zero element of the ring Ring.

unit (i, j)
returns the matrix of dimension (i, j) whose fields (k,k) are filled with the unit element of Ring, and all other fields are filled with the zero element of Ring.

sum (A, B)
returns the sum of the matrices A and B.

prod (A, B)
returns the product of the matrices A and B.

star A
returns the iteration of the matrix A.

transpose A
returns the transposition of the matrix A.


See Also

Reg, RegEqns

Discussion

The matrix algebra over Reg is useful in solving systems of regular recursion equations. (It is used in RegEqnsFm to translate a finite automaton to a regular expression by solving a system of regular right-linear recursion equations that describe the automaton.)