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.

Constructors

Matrix (Size i) [(MIx i, b)]

Instances

Functor (Matrix i)

Defined in Agda.Termination.SparseMatrix

Methods

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

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

Foldable (Matrix i)

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

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)

Defined in Agda.Termination.SparseMatrix

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)

Defined in Agda.Termination.SparseMatrix

Methods

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

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

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

Defined in Agda.Termination.SparseMatrix

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)

Defined in Agda.Termination.SparseMatrix

Methods

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

show :: Matrix i b -> String

showList :: [Matrix i b] -> ShowS

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

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

Defined in Agda.Termination.SparseMatrix

Methods

comparable :: Comparable (Matrix i a)

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

Defined in Agda.Termination.SparseMatrix

Methods

pretty :: Matrix i b -> Doc

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

prettyList :: [Matrix i b] -> Doc

(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o)

We assume the matrices have the same dimension.

Defined in Agda.Termination.Order

Methods

notWorse :: Matrix i o -> Matrix i o -> 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.

Defined in Agda.Termination.SparseMatrix

Methods

diagonal :: Matrix i b -> [b]

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

Association of indices to values.

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)

Defined in Agda.Termination.SparseMatrix

Methods

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

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

Ord i => Ord (Size i)

Defined in Agda.Termination.SparseMatrix

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)

Defined in Agda.Termination.SparseMatrix

Methods

showsPrec :: Int -> Size i -> ShowS

show :: Size i -> String

showList :: [Size i] -> ShowS

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)

Defined in Agda.Termination.SparseMatrix

Methods

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

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

Ord i => Ord (MIx i)

Defined in Agda.Termination.SparseMatrix

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)

Defined in Agda.Termination.SparseMatrix

Methods

showsPrec :: Int -> MIx i -> ShowS

show :: MIx i -> String

showList :: [MIx i] -> ShowS

Ix i => Ix (MIx i)

Defined in Agda.Termination.SparseMatrix

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

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.

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.

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

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.

Methods

diagonal :: m -> [e]

Instances

Diagonal (CallMatrixAug cinfo) Order

Defined in Agda.Termination.CallMatrix

Methods

diagonal :: CallMatrixAug cinfo -> [Order]

HasZero a => Diagonal (CallMatrix' a) a

Defined in Agda.Termination.CallMatrix

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.

Defined in Agda.Termination.SparseMatrix

Methods

diagonal :: Matrix i b -> [b]

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

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

Compute the matrix size of the union of two matrices.

zipAssocWith

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

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

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.