Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

Agda.Termination.SparseMatrix

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

# Basic data types

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

Instances

 Source # Methodsfmap :: (a -> b) -> Matrix i a -> Matrix i b #(<\$) :: a -> Matrix i b -> Matrix i a # Source # Methodsfold :: 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 # Source # Methodstraverse :: 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 b, Eq i) => Eq (Matrix i b) Source # Methods(==) :: Matrix i b -> Matrix i b -> Bool #(/=) :: Matrix i b -> Matrix i b -> Bool # (Ord b, Ord i) => Ord (Matrix i b) Source # Methodscompare :: 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) Source # MethodsshowsPrec :: 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) Source # Generate a matrix of arbitrary size. Methodsarbitrary :: Gen (Matrix i b) #shrink :: Matrix i b -> [Matrix i b] # (Integral i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b) Source # Methodscoarbitrary :: Matrix i b -> Gen b -> Gen b # (Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source # Methodspretty :: Matrix i b -> Doc Source #prettyPrec :: Int -> Matrix i b -> Doc Source # (Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source # Pointwise comparison. Only matrices with the same dimension are comparable. Methods Ord i => NotWorse (Matrix i Order) Source # We assume the matrices have the same dimension. Methods (Integral i, HasZero b) => Diagonal (Matrix i b) b Source # Diagonal of sparse matrix.O(n) where n is the number of non-zero elements in the matrix. Methodsdiagonal :: Matrix i b -> [b] Source #

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

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

data Size i Source #

Size of a matrix.

Constructors

 Size Fieldsrows :: iNumber of rows, >= 0.cols :: iNumber of columns, >= 0.

Instances

 Eq i => Eq (Size i) Source # Methods(==) :: Size i -> Size i -> Bool #(/=) :: Size i -> Size i -> Bool # Ord i => Ord (Size i) Source # Methodscompare :: 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) Source # MethodsshowsPrec :: Int -> Size i -> ShowS #show :: Size i -> String #showList :: [Size i] -> ShowS # Integral i => Arbitrary (Size i) Source # Methodsarbitrary :: Gen (Size i) #shrink :: Size i -> [Size i] # CoArbitrary i => CoArbitrary (Size i) Source # Methodscoarbitrary :: Size i -> Gen b -> Gen b #

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

Size invariant: dimensions are non-negative.

data MIx i Source #

Type of matrix indices (row, column).

Constructors

 MIx Fieldsrow :: iRow index, 1 <= row <= rows.col :: iColumn index 1 <= col <= cols.

Instances

 Eq i => Eq (MIx i) Source # Methods(==) :: MIx i -> MIx i -> Bool #(/=) :: MIx i -> MIx i -> Bool # Ord i => Ord (MIx i) Source # Methodscompare :: 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) Source # MethodsshowsPrec :: Int -> MIx i -> ShowS #show :: MIx i -> String #showList :: [MIx i] -> ShowS # Ix i => Ix (MIx i) Source # Methodsrange :: (MIx i, MIx i) -> [MIx i] #index :: (MIx i, MIx i) -> MIx i -> Int #unsafeIndex :: (MIx i, MIx i) -> MIx i -> IntinRange :: (MIx i, MIx i) -> MIx i -> Bool #rangeSize :: (MIx i, MIx i) -> Int #unsafeRangeSize :: (MIx i, MIx i) -> Int Integral i => Arbitrary (MIx i) Source # Methodsarbitrary :: Gen (MIx i) #shrink :: MIx i -> [MIx i] # CoArbitrary i => CoArbitrary (MIx i) Source # Methodscoarbitrary :: MIx i -> Gen b -> Gen b #

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

Indices must be positive, >= 1.

# Generating and creating matrices

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

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.

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

Generates a matrix of the given size.

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 Source #

Dimensions of the matrix.

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

True iff the matrix is square.

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

Returns True iff the matrix is empty.

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

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

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

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

transpose :: Transpose a => a -> a Source #

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

Minimal complete definition

diagonal

Methods

diagonal :: m -> [e] Source #

Instances

 Diagonal (CallMatrixAug cinfo) Order Source # Methodsdiagonal :: CallMatrixAug cinfo -> [Order] Source # HasZero a => Diagonal (CallMatrix' a) a Source # Methodsdiagonal :: CallMatrix' a -> [a] Source # (Integral i, HasZero b) => Diagonal (Matrix i b) b Source # Diagonal of sparse matrix.O(n) where n is the number of non-zero elements in the matrix. Methodsdiagonal :: Matrix i b -> [b] Source #

# Modifying matrices

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

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