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.

Basic data types

data 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.

Instances

Functor (Matrix i)

Methods

fmap :: (a -> b) -> Matrix i a -> Matrix i b

(<$) :: a -> Matrix i b -> Matrix i a

Foldable (Matrix i)

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

toList :: Matrix i a -> [a]

null :: Matrix i a -> Bool

length :: Matrix i a -> Int

elem :: Eq a => a -> Matrix i a -> Bool

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

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

sum :: Num a => Matrix i a -> a

product :: Num a => Matrix i a -> a

Traversable (Matrix i)

Methods

traverse :: Applicative f => (a -> f b) -> Matrix i a -> f (Matrix i b)

sequenceA :: Applicative f => Matrix i (f a) -> f (Matrix i a)

mapM :: Monad m => (a -> m b) -> Matrix i a -> m (Matrix i b)

sequence :: Monad m => Matrix i (m a) -> m (Matrix i a)

(Eq i, Eq b) => Eq (Matrix i b)

Methods

(==) :: Matrix i b -> Matrix i b -> Bool

(/=) :: Matrix i b -> Matrix i b -> Bool

(Ord i, Ord b) => Ord (Matrix i b)

Methods

compare :: Matrix i b -> Matrix i b -> Ordering

(<) :: Matrix i b -> Matrix i b -> Bool

(<=) :: Matrix i b -> Matrix i b -> Bool

(>) :: Matrix i b -> Matrix i b -> Bool

(>=) :: Matrix i b -> Matrix i b -> Bool

max :: Matrix i b -> Matrix i b -> Matrix i b

min :: Matrix i b -> Matrix i b -> Matrix i b

(Integral i, HasZero b, Show i, Show b) => Show (Matrix i b)

Methods

showsPrec :: Int -> Matrix i b -> ShowS

show :: Matrix i b -> String

showList :: [Matrix i b] -> ShowS

(Integral i, Arbitrary b, HasZero b) => Arbitrary (Matrix i b)

Generate a matrix of arbitrary size.

Methods

arbitrary :: Gen (Matrix i b)

shrink :: Matrix i b -> [Matrix i b]

(Integral i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b)

Methods

coarbitrary :: Matrix i b -> Gen b -> Gen b

(Ord i, PartialOrd a) => PartialOrd (Matrix i a)

Pointwise comparison. Only matrices with the same dimension are comparable.

Methods

comparable :: Comparable (Matrix i a)

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)

Methods

pretty :: Matrix i b -> Doc

prettyPrec :: Int -> Matrix i b -> Doc

Ord i => NotWorse (Matrix i Order)

We assume the matrices have the same dimension.

Methods

notWorse :: Matrix i Order -> Matrix i Order -> Bool

(Integral i, HasZero b) => Diagonal (Matrix i b) b

Diagonal of sparse matrix.

O(n) where n is the number of non-zero elements in the matrix.

Methods

diagonal :: Matrix i b -> [b]

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

Matrix indices are lexicographically sorted with no duplicates. All indices must be within bounds.

data Size i

Size of a matrix.

Constructors

Size

Fields

• rows :: i

  Number of rows, >= 0.

• cols :: i

  Number of columns, >= 0.

Instances

Eq i => Eq (Size i)

Methods

(==) :: Size i -> Size i -> Bool

(/=) :: Size i -> Size i -> Bool

Ord i => Ord (Size i)

Methods

compare :: Size i -> Size i -> Ordering

(<) :: Size i -> Size i -> Bool

(<=) :: Size i -> Size i -> Bool

(>) :: Size i -> Size i -> Bool

(>=) :: Size i -> Size i -> Bool

max :: Size i -> Size i -> Size i

min :: Size i -> Size i -> Size i

Show i => Show (Size i)

Methods

showsPrec :: Int -> Size i -> ShowS

show :: Size i -> String

showList :: [Size i] -> ShowS

Integral i => Arbitrary (Size i)

Methods

arbitrary :: Gen (Size i)

shrink :: Size i -> [Size i]

CoArbitrary i => CoArbitrary (Size i)

Methods

coarbitrary :: Size i -> Gen b -> Gen b

sizeInvariant :: (Ord i, Num i) => Size i -> Bool

Size invariant: dimensions are non-negative.

data MIx i

Type of matrix indices (row, column).

Constructors

MIx

Fields

• row :: i

  Row index, 1 <= row <= rows.

• col :: i

  Column index 1 <= col <= cols.

Instances

Eq i => Eq (MIx i)

Methods

(==) :: MIx i -> MIx i -> Bool

(/=) :: MIx i -> MIx i -> Bool

Ord i => Ord (MIx i)

Methods

compare :: MIx i -> MIx i -> Ordering

(<) :: MIx i -> MIx i -> Bool

(<=) :: MIx i -> MIx i -> Bool

(>) :: MIx i -> MIx i -> Bool

(>=) :: MIx i -> MIx i -> Bool

max :: MIx i -> MIx i -> MIx i

min :: MIx i -> MIx i -> MIx i

Show i => Show (MIx i)

Methods

showsPrec :: Int -> MIx i -> ShowS

show :: MIx i -> String

showList :: [MIx i] -> ShowS

Ix i => Ix (MIx i)

Methods

range :: (MIx i, MIx i) -> [MIx i]

index :: (MIx i, MIx i) -> MIx i -> Int

unsafeIndex :: (MIx i, MIx i) -> MIx i -> Int

inRange :: (MIx i, MIx i) -> MIx i -> Bool

rangeSize :: (MIx i, MIx i) -> Int

unsafeRangeSize :: (MIx i, MIx i) -> Int

Integral i => Arbitrary (MIx i)

Methods

arbitrary :: Gen (MIx i)

shrink :: MIx i -> [MIx i]

CoArbitrary i => CoArbitrary (MIx i)

Methods

coarbitrary :: MIx i -> Gen b -> Gen b

mIxInvariant :: (Ord i, Num i) => MIx i -> Bool

Indices must be positive, >= 1.

Generating and creating matrices

fromLists :: (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.

fromIndexList :: (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.

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

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

matrix :: (Integral i, Arbitrary b, HasZero b) => Size i -> Gen (Matrix i b)

Generates a matrix of the given size.

matrixUsingRowGen

Arguments

:: (Integral i, HasZero b)

=> Size i

-> (i -> Gen [b])

The generator is parameterised on the size of the row.

-> Gen (Matrix i b)

Generates a matrix of the given size, using the given generator to generate the rows.

Combining and querying matrices

size :: Matrix i b -> Size i

Dimensions of the matrix.

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

True iff the matrix is square.

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

Returns True iff the matrix is empty.

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

zipMatrices

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

add :: (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.

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

mul :: (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.

transpose :: Transpose a => a -> a

class 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.

Minimal complete definition

diagonal

Methods

diagonal :: m -> [e]

Instances

Diagonal (CallMatrixAug cinfo) Order

Methods

diagonal :: CallMatrixAug cinfo -> [Order]

HasZero a => Diagonal (CallMatrix' a) a

Methods

diagonal :: CallMatrix' a -> [a]

(Integral i, HasZero b) => Diagonal (Matrix i b) b

Diagonal of sparse matrix.

O(n) where n is the number of non-zero elements in the matrix.

Methods

diagonal :: Matrix i b -> [b]

Modifying matrices

addRow :: (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.

addColumn :: (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.

Tests

tests :: IO Bool