ModuleAgda-2.8.0.2Haskell2010

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.

Contents

Basic data types
Generating and creating matrices
Combining and querying matrices
Modifying matrices

Synopsis

data Matrix
value unM
data Size
data MIx
value fromLists
value fromIndexList
value toLists
value size
value square
value isEmpty
value isSingleton
value zipMatrices
value add
value intersectWith
value interAssocWith
value mul
method transpose
class Diagonal
value toSparseRows
value supSize
value zipAssocWith
value addRow
value addColumn

PackageAgda-2.8.0.2
Exports23
LanguageHaskell2010
LicenceMIT
SourceSparseMatrix.hs

Basic data types

datadata Matrix i b

Source#

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.8.0.2 · Agda.Termination.SparseMatrix
Foldable (Matrix i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Traversable (Matrix i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
(Eq i, Eq b) => Eq (Matrix i b)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
(Ord i, Ord b) => Ord (Matrix i b)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
(Integral i, HasZero b, Show i, Show b) => Show (Matrix i b)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
(Ord i, PartialOrd a) => PartialOrd (Matrix i a)Defined in Agda-2.8.0.2 · 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.8.0.2 · Agda.Termination.Order
We assume the matrices have the same dimension.
Ord i => Transpose (Matrix i b)Defined in Agda-2.8.0.2 · 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.8.0.2 · 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)]

Source#

Association of indices to values.

datadata Size i

Source#

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.8.0.2 · Agda.Termination.SparseMatrix
Ord i => Ord (Size i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Show i => Show (Size i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Transpose (Size i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Size of transposed matrix.

datadata MIx i

Source#

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.8.0.2 · Agda.Termination.SparseMatrix
Ord i => Ord (MIx i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Show i => Show (MIx i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Ix i => Ix (MIx i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Transpose (MIx i)Defined in Agda-2.8.0.2 · Agda.Termination.SparseMatrix
Transposing coordinates.

Generating and creating matrices

valuefromLists

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

Source#

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

Source#

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

Source#

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

Combining and querying matrices

valuesize :: Matrix i b -> Size i

Source#

Dimensions of the matrix.

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

Source#

True iff the matrix is square.

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

Source#

Returns True iff the matrix is empty.

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

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

Source#

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

Source#

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

Source#

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

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.

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

Source#

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

Source#

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.8.0.2 · Agda.Termination.CallMatrix
Diagonal (CallMatrixAug cinfo) OrderDefined in Agda-2.8.0.2 · Agda.Termination.CallMatrix
(Integral i, HasZero b) => Diagonal (Matrix i b) bDefined in Agda-2.8.0.2 · 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)])]

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.

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

Source#

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

Source#

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

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

Source#

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

Source#

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.