ModuleAgda-2.7.0.1Haskell2010

Agda.Termination.SparseMatrix

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.

3 types
1 class
18 values

PackageAgda-2.7.0.1
Exports23
LanguageHaskell2010
LicenceMIT
SourceSparseMatrix.hs

Basic data types

4 declarations

datadata Matrix i b

Type of matrices, parameterised on the type of values.

Sparse matrices are implemented as an ordered association list, mapping coordinates to values.

Constructors

Matrix
- size :: Size i
  Dimensions of the matrix.
- unM :: [(MIx i, b)]
  Association of indices to values.

Instances11Functor, Foldable, Traversable, Eq, Ord, Show, …

Functor (Matrix i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Foldable (Matrix i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Traversable (Matrix i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
(Eq i, Eq b) => Eq (Matrix i b)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
(Ord i, Ord b) => Ord (Matrix i b)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
(Integral i, HasZero b, Show i, Show b) => Show (Matrix i b)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
(Ord i, PartialOrd a) => PartialOrd (Matrix i a)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Pointwise comparison. Only matrices with the same dimension are comparable.
(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o)Defined in Agda-2.7.0.1 · Agda.Termination.Order
We assume the matrices have the same dimension.
Ord i => Transpose (Matrix i b)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Matrix transposition.
O(n log n) where n is the number of non-zero elements in the matrix.
(Integral i, HasZero b) => Diagonal (Matrix i b) bDefined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Diagonal of sparse matrix.
O(n) where n is the number of non-zero elements in the matrix.

valueunM :: Matrix i b -> [(MIx i, b)]

Association of indices to values.

datadata Size i

Size of a matrix.

Constructors

Size
- rows :: i
  Number of rows, >= 0.
- cols :: i
  Number of columns, >= 0.

Instances4Eq, Ord, Show, Transpose

Eq i => Eq (Size i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Ord i => Ord (Size i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Show i => Show (Size i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Transpose (Size i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Size of transposed matrix.

datadata MIx i

Type of matrix indices (row, column).

Constructors

MIx
- row :: i
  Row index, 1 <= row <= rows.
- col :: i
  Column index 1 <= col <= cols.

Instances5Eq, Ord, Show, Ix, Transpose

Eq i => Eq (MIx i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Ord i => Ord (MIx i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Show i => Show (MIx i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Ix i => Ix (MIx i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Transpose (MIx i)Defined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Transposing coordinates.

Generating and creating matrices

3 declarations

valuefromLists

:: (Ord i, Num i, Enum i, HasZero b)
=> Size i
-> [[b]]
-> Matrix i b

fromLists sz rs constructs a matrix from a list of lists of values (a list of rows). O(size) where size = rows × cols.

Precondition: length rs == rows sz and all ((cols sz ==) . length) rs.

valuefromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b

Constructs a matrix from a list of (index, value)-pairs. O(n) where n is size of the list.

Precondition: indices are unique.

valuetoLists :: (Integral i, HasZero b) => Matrix i b -> [[b]]

Converts a matrix to a list of row lists. O(size) where size = rows × cols.

Combining and querying matrices

14 declarations

valuesize :: Matrix i b -> Size i

Dimensions of the matrix.

valuesquare :: Ix i => Matrix i b -> Bool

True iff the matrix is square.

valueisEmpty :: (Num i, Ix i) => Matrix i b -> Bool

Returns True iff the matrix is empty.

valueisSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b

Returns 'Just b' iff it is a 1x1 matrix with just one entry b. O(1).

valuezipMatrices

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

valueadd

:: (Ord i, HasZero a)
=> a -> a -> a
-> Matrix i a
-> Matrix i a
-> Matrix i a

add (+) m1 m2 adds m1 and m2, using (+) to add values. O(n1 + n2).

Returns a matrix of size supSize m1 m2.

valueintersectWith

:: Ord i
=> a -> a -> a
-> Matrix i a
-> Matrix i a
-> Matrix i a

intersectWith f m1 m2 build the pointwise conjunction m1 and m2. Uses f to combine non-zero values. O(n1 + n2).

Returns a matrix of size infSize m1 m2.

valueinterAssocWith :: Ord i => (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]

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.

valuemul :: (Ix i, Eq a) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a

mul semiring m1 m2 multiplies matrices m1 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.

methodtranspose :: a -> a

classclass Diagonal m e | m -> e where

diagonal m extracts the diagonal of m.

For non-square matrices, the length of the diagonal is the minimum of the dimensions of the matrix.

Methods

diagonal :: m -> [e]

Instances3Diagonal

HasZero a => Diagonal (CallMatrix' a) aDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
Diagonal (CallMatrixAug cinfo) OrderDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
(Integral i, HasZero b) => Diagonal (Matrix i b) bDefined in Agda-2.7.0.1 · Agda.Termination.SparseMatrix
Diagonal of sparse matrix.
O(n) where n is the number of non-zero elements in the matrix.

valuetoSparseRows :: Eq i => Matrix i b -> [(i, [(i, b)])]

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.

valuesupSize :: Ord i => Matrix i a -> Matrix i b -> Size i

Compute the matrix size of the union of two matrices.

valuezipAssocWith

:: 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)]

General pointwise combination function for association lists. O(n1 + n2) where ni is the number of non-zero element in matrix i.

In zipAssocWith fs gs f g h l l',

fs is possibly more efficient version of mapMaybe ( (i, a) -> (i,) $ f a), and same for gs and g.

Modifying matrices

2 declarations

valueaddRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b

addRow x m adds a new row to m, after the rows already existing in the matrix. All elements in the new row get set to x.

valueaddColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b

addColumn x m adds a new column to m, after the columns already existing in the matrix. All elements in the new column get set to x.