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.
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 Methods 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 # | |
Defined in Agda.Termination.SparseMatrix | |
(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 Methods 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)
.
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.
Instances
Diagonal (CallMatrixAug cinfo) Order Source # | |
Defined in Agda.Termination.CallMatrix Methods diagonal :: CallMatrixAug cinfo -> [Order] Source # | |
HasZero a => Diagonal (CallMatrix' a) a Source # | |
Defined in Agda.Termination.CallMatrix Methods 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 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)] |