Safe Haskell  None 

Language  Haskell2010 
Sparse matrices.
We assume the matrices to be very sparse, so we just implement them as sorted association lists.
Most operations are linear in the number of nonzero elements.
An exception is transposition, which needs to sort the association
list again; it has the complexity of sorting: n log n
where n
is
the number of nonzero elements.
Another exception is matrix multiplication, of course.
Synopsis
 data Matrix i b = Matrix (Size i) [(MIx i, b)]
 unM :: Matrix i b > [(MIx i, b)]
 data Size i = Size {}
 data MIx i = MIx {}
 fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i > [[b]] > Matrix i b
 fromIndexList :: (Ord i, HasZero b) => Size i > [(MIx i, b)] > Matrix i b
 toLists :: (Integral i, HasZero b) => Matrix i b > [[b]]
 size :: Matrix i b > Size i
 square :: Ix i => Matrix i b > Bool
 isEmpty :: (Num i, Ix i) => Matrix i b > Bool
 isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b > Maybe b
 zipMatrices :: forall a b c i. Ord i => (a > c) > (b > c) > (a > b > c) > (c > Bool) > Matrix i a > Matrix i b > Matrix i c
 add :: (Ord i, HasZero a) => (a > a > a) > Matrix i a > Matrix i a > Matrix i a
 intersectWith :: Ord i => (a > a > a) > Matrix i a > Matrix i a > Matrix i a
 interAssocWith :: Ord i => (a > a > a) > [(i, a)] > [(i, a)] > [(i, a)]
 mul :: (Ix i, Eq a) => Semiring a > Matrix i a > Matrix i a > Matrix i a
 transpose :: Transpose a => a > a
 class Diagonal m e  m > e where
 diagonal :: m > [e]
 toSparseRows :: Eq i => Matrix i b > [(i, [(i, b)])]
 supSize :: Ord i => Matrix i a > Matrix i b > Size i
 zipAssocWith :: Ord i => ([(i, a)] > [(i, c)]) > ([(i, b)] > [(i, c)]) > (a > Maybe c) > (b > Maybe c) > (a > b > Maybe c) > [(i, a)] > [(i, b)] > [(i, c)]
 addRow :: (Num i, HasZero b) => b > Matrix i b > Matrix i b
 addColumn :: (Num i, HasZero b) => b > Matrix i b > Matrix i b
Basic data types
Type of matrices, parameterised on the type of values.
Sparse matrices are implemented as an ordered association list, mapping coordinates to values.
Instances
Functor (Matrix i) Source #  
Foldable (Matrix i) Source #  
Defined in Agda.Termination.SparseMatrix fold :: Monoid m => Matrix i m > m # foldMap :: Monoid m => (a > m) > Matrix i a > m # foldr :: (a > b > b) > b > Matrix i a > b # foldr' :: (a > b > b) > b > Matrix i a > b # foldl :: (b > a > b) > b > Matrix i a > b # foldl' :: (b > a > b) > b > Matrix i a > b # foldr1 :: (a > a > a) > Matrix i a > a # foldl1 :: (a > a > a) > Matrix i a > a # elem :: Eq a => a > Matrix i a > Bool # maximum :: Ord a => Matrix i a > a # minimum :: Ord a => Matrix i a > a #  
Traversable (Matrix i) Source #  
(Eq i, Eq b) => Eq (Matrix i b) Source #  
(Ord i, Ord b) => Ord (Matrix i b) Source #  
Defined in Agda.Termination.SparseMatrix  
(Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) Source #  
(Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source #  Pointwise comparison. Only matrices with the same dimension are comparable. 
Defined in Agda.Termination.SparseMatrix comparable :: Comparable (Matrix i a) Source #  
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source #  
(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) Source #  We assume the matrices have the same dimension. 
(Integral i, HasZero b) => Diagonal (Matrix i b) b Source #  Diagonal of sparse matrix.

Defined in Agda.Termination.SparseMatrix 
Size of a matrix.
Type of matrix indices (row, column).
Generating and creating matrices
fromIndexList :: (Ord i, HasZero b) => Size i > [(MIx i, b)] > Matrix i b Source #
Constructs a matrix from a list of (index, value)
pairs.
O(n)
where n
is size of the list.
Precondition: indices are unique.
toLists :: (Integral i, HasZero b) => Matrix i b > [[b]] Source #
Converts a matrix to a list of row lists.
O(size)
where size = rows × cols
.
Combining and querying matrices
isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b > Maybe b Source #
Returns 'Just b' iff it is a 1x1 matrix with just one entry b
.
O(1)
.
:: Ord i  
=> (a > c)  Element only present in left matrix. 
> (b > c)  Element only present in right matrix. 
> (a > b > c)  Element present in both matrices. 
> (c > Bool)  Result counts as zero? 
> Matrix i a  
> Matrix i b  
> Matrix i c 
General pointwise combination function for sparse matrices.
O(n1 + n2)
.
intersectWith :: Ord i => (a > a > a) > Matrix i a > Matrix i a > Matrix i a Source #
build the pointwise conjunction intersectWith
f m1 m2m1
and m2
.
Uses f
to combine nonzero values.
O(n1 + n2)
.
Returns a matrix of size infSize m1 m2
.
interAssocWith :: Ord i => (a > a > a) > [(i, a)] > [(i, a)] > [(i, a)] Source #
Association list intersection.
O(n1 + n2)
.
interAssocWith f l l' = { (i, f a b)  (i,a) ∈ l and (i,b) ∈ l' }
Used to combine sparse matrices, it might introduce zero elements
if f
can return zero for nonzero arguments.
mul :: (Ix i, Eq a) => Semiring a > Matrix i a > Matrix i a > Matrix i a Source #
multiplies matrices mul
semiring m1 m2m1
and m2
.
Uses the operations of the semiring semiring
to perform the
multiplication.
O(n1 + n2 log n2 + Σ(i <= r1) Σ(j <= c2) d(i,j))
where
r1
is the number of nonempty rows in m1
and
c2
is the number of nonempty columns in m2
and
d(i,j)
is the bigger one of the following two quantifies:
the length of sparse row i
in m1
and
the length of sparse column j
in m2
.
Given dimensions m1 : r1 × c1
and m2 : r2 × c2
,
a matrix of size r1 × c2
is returned.
It is not necessary that c1 == r2
, the matrices are implicitly
patched with zeros to match up for multiplication.
For sparse matrices, this patching is a noop.
class Diagonal m e  m > e where Source #
extracts the diagonal of diagonal
mm
.
For nonsquare matrices, the length of the diagonal is the minimum of the dimensions of the matrix.
Instances
Diagonal (CallMatrixAug cinfo) Order Source #  
Defined in Agda.Termination.CallMatrix diagonal :: CallMatrixAug cinfo > [Order] Source #  
HasZero a => Diagonal (CallMatrix' a) a Source #  
Defined in Agda.Termination.CallMatrix diagonal :: CallMatrix' a > [a] Source #  
(Integral i, HasZero b) => Diagonal (Matrix i b) b Source #  Diagonal of sparse matrix.

Defined in Agda.Termination.SparseMatrix 
toSparseRows :: Eq i => Matrix i b > [(i, [(i, b)])] Source #
Converts a sparse matrix to a sparse list of rows.
O(n)
where n
is the number of nonzero entries of the matrix.
Only nonempty rows are generated.
supSize :: Ord i => Matrix i a > Matrix i b > Size i Source #
Compute the matrix size of the union of two matrices.