Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Termination.SparseMatrix
Contents
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.
- data Matrix i b = Matrix {}
- 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]]
- 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
- 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.
Constructors
Matrix | |
Instances
Functor (Matrix i) Source # | |
Foldable (Matrix i) Source # | |
Traversable (Matrix i) Source # | |
(Eq b, Eq i) => Eq (Matrix i b) Source # | |
(Ord b, Ord i) => Ord (Matrix i b) Source # | |
(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. |
(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.
|
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
:: 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 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 #
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 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 #
extracts the diagonal of diagonal
mm
.
For non-square matrices, the length of the diagonal is the minimum of the dimensions of the matrix.
Minimal complete definition
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)] |