| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Termination.SparseMatrix
Description
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 non-zero 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 non-zero 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
| Foldable (Matrix i) Source # | |
Defined in Agda.Termination.SparseMatrix Methods fold :: Monoid m => Matrix i m -> m # foldMap :: Monoid m => (a -> m) -> Matrix i a -> 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 # | |
Defined in Agda.Termination.SparseMatrix | |
| Functor (Matrix i) Source # | |
| (Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) Source # | We assume the matrices have the same dimension. |
| (Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source # | Pointwise comparison. Only matrices with the same dimension are comparable. |
Defined in Agda.Termination.SparseMatrix Methods comparable :: Comparable (Matrix i a) Source # | |
| (Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source # | |
| (Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) 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) => 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).
Arguments
| :: forall a b c i. 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 #
intersectWith f m1 m2m1 and m2.
Uses f to combine non-zero 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 non-zero arguments.
mul :: (Ix i, Eq a) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a Source #
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 non-empty rows in m1 and
c2 is the number of non-empty 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 no-op.
class Diagonal m e | m -> e where Source #
diagonal mm.
For non-square matrices, the length of the diagonal is the minimum of the dimensions of the matrix.
Instances
| HasZero a => Diagonal (CallMatrix' a) a Source # | |
Defined in Agda.Termination.CallMatrix Methods diagonal :: CallMatrix' a -> [a] Source # | |
| Diagonal (CallMatrixAug cinfo) Order Source # | |
Defined in Agda.Termination.CallMatrix Methods diagonal :: CallMatrixAug cinfo -> [Order] 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 non-zero entries of the matrix.
Only non-empty 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.
Arguments
| :: Ord i | |
| => ([(i, a)] -> [(i, c)]) | Only left map remaining. |
| -> ([(i, b)] -> [(i, c)]) | Only right map remaining. |
| -> (a -> Maybe c) | Element only present in left map. |
| -> (b -> Maybe c) | Element only present in right map. |
| -> (a -> b -> Maybe c) | Element present in both maps. |
| -> [(i, a)] | |
| -> [(i, b)] | |
| -> [(i, c)] |