Agda-2.4.2.4: 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 Source Source (Eq i, Eq b) => Eq (Matrix i b) Source (Ord i, Ord b) => Ord (Matrix i b) Source (Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) Source (Show i, Ord i, Integral i, Enum i, Ix i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b) Source (Arbitrary i, Num i, Integral i, Arbitrary b, HasZero b) => Arbitrary (Matrix i b) Source Generate a matrix of arbitrary size. (Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source Pointwise comparison. Only matrices with the same dimension are comparable. (Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source Ord i => NotWorse (Matrix i Order) Source We assume the matrices have the same dimension. (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.

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 Ord i => Ord (Size i) Source Show i => Show (Size i) Source CoArbitrary i => CoArbitrary (Size i) Source (Arbitrary i, Integral i) => Arbitrary (Size i) Source

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 Ord i => Ord (MIx i) Source Show i => Show (MIx i) Source Ix i => Ix (MIx i) Source CoArbitrary i => CoArbitrary (MIx i) Source (Arbitrary i, Integral i) => Arbitrary (MIx i) Source

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 :: (Arbitrary i, Integral i, Arbitrary b, HasZero b) => Size i -> Gen (Matrix i b) Source

Generates a matrix of the given size.

Arguments

 :: (Arbitrary i, Integral i, Arbitrary b, 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 :: (Enum i, Num i, 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.

Methods

diagonal :: m -> [e] Source

Instances

 Diagonal (CallMatrixAug cinfo) Order Source HasZero a => Diagonal (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.

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