The pkaMatrix functor

The `pkaMatrix` functor

Synopsis

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

Description


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.

Discussion

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).