The pkaMatrix functor


signature pkaMATRIX
functor pkaMatrix (pKA) : pkaMATRIX

This functor generates the matrices over a given (polymorphic) Kleenean algebra.

Functor result 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


structure Ring : pKA
the argument structure, a (polymorphic) Kleenean algebra.

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, RegEqnsFm


The matrix algebra over the free Kleenean algebra is useful in solving systems of regular recursion equations. To use this method in RegEqnsFm, we define the matrix algebra over Reg by:

structure RegMat : pkaMATRIX = pkaMatrix(Reg).

Since the dimension of matrices in RegMat varies, we have a family of unit matrices, val Un = unit (n,n), for example. The matrix operations raise an exception Size, if the dimensions of the argument matrices do not fit.