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

Safe Haskell | None
Language | Haskell2010

Agda.Termination.SparseMatrix

Contents

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

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

- data Matrix i b = Matrix (Size i) [(MIx i, b)]
- unM :: Matrix i b -> [(MIx i, b)]
- data Size i = Size {
  - rows :: i
  - cols :: i
  }
- data MIx i = MIx {
  - row :: i
  - col :: i
  }
- fromLists :: (Ord i, Num i, Enum i, HasZero b) => Size i -> [[b]] -> Matrix i b
- fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b
- toLists :: (Integral i, HasZero b) => Matrix i b -> [[b]]
- size :: Matrix i b -> Size i
- square :: Ix i => Matrix i b -> Bool
- isEmpty :: (Num i, Ix i) => Matrix i b -> Bool
- isSingleton :: (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b
- zipMatrices :: forall a b c i. Ord i => (a -> c) -> (b -> c) -> (a -> b -> c) -> (c -> Bool) -> Matrix i a -> Matrix i b -> Matrix i c
- add :: (Ord i, HasZero a) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
- intersectWith :: Ord i => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
- interAssocWith :: Ord i => (a -> a -> a) -> [(i, a)] -> [(i, a)] -> [(i, a)]
- mul :: (Ix i, Eq a) => Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
- transpose :: Transpose a => a -> a
- class Diagonal m e | m -> e where
  - diagonal :: m -> [e]
- toSparseRows :: Eq i => Matrix i b -> [(i, [(i, b)])]
- supSize :: Ord i => Matrix i a -> Matrix i b -> Size i
- zipAssocWith :: Ord i => ([(i, a)] -> [(i, c)]) -> ([(i, b)] -> [(i, c)]) -> (a -> Maybe c) -> (b -> Maybe c) -> (a -> b -> Maybe c) -> [(i, a)] -> [(i, b)] -> [(i, c)]
- addRow :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b
- addColumn :: (Num i, HasZero b) => b -> Matrix i b -> Matrix i b

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

Constructors

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

Instances

Functor (Matrix i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods fmap :: (a -> b) -> Matrix i a -> Matrix i b Source # (<$) :: a -> Matrix i b -> Matrix i a Source #
Foldable (Matrix i) Source # |

Instance details

Defined in Agda.Termination.SparseMatrix

Methods

fold :: Monoid m => Matrix i m -> m Source #

foldMap :: Monoid m => (a -> m) -> Matrix i a -> m Source #

foldr :: (a -> b -> b) -> b -> Matrix i a -> b Source #

foldr' :: (a -> b -> b) -> b -> Matrix i a -> b Source #

foldl :: (b -> a -> b) -> b -> Matrix i a -> b Source #

foldl' :: (b -> a -> b) -> b -> Matrix i a -> b Source #

foldr1 :: (a -> a -> a) -> Matrix i a -> a Source #

foldl1 :: (a -> a -> a) -> Matrix i a -> a Source #

toList :: Matrix i a -> [a] Source #

null :: Matrix i a -> Bool Source #

length :: Matrix i a -> Int Source #

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

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

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

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

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

Traversable (Matrix i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods traverse :: Applicative f => (a -> f b) -> Matrix i a -> f (Matrix i b) Source # sequenceA :: Applicative f => Matrix i (f a) -> f (Matrix i a) Source # mapM :: Monad m => (a -> m b) -> Matrix i a -> m (Matrix i b) Source # sequence :: Monad m => Matrix i (m a) -> m (Matrix i a) Source #
(Eq i, Eq b) => Eq (Matrix i b) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods (==) :: Matrix i b -> Matrix i b -> Bool Source # (/=) :: Matrix i b -> Matrix i b -> Bool Source #
(Ord i, Ord b) => Ord (Matrix i b) Source # |

Instance details

Defined in Agda.Termination.SparseMatrix

Methods

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

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

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

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

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

max :: Matrix i b -> Matrix i b -> Matrix i b Source #

min :: Matrix i b -> Matrix i b -> Matrix i b Source #

(Integral i, HasZero b, Show i, Show b) => Show (Matrix i b) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods showsPrec :: Int -> Matrix i b -> ShowS Source # show :: Matrix i b -> String Source # showList :: [Matrix i b] -> ShowS Source #
(Ord i, PartialOrd a) => PartialOrd (Matrix i a) Source # | Pointwise comparison. Only matrices with the same dimension are comparable.
Instance details Defined in Agda.Termination.SparseMatrix Methods comparable :: Comparable (Matrix i a) Source #
(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods pretty :: Matrix i b -> Doc Source # prettyPrec :: Int -> Matrix i b -> Doc Source # prettyList :: [Matrix i b] -> Doc Source #
(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) Source # | We assume the matrices have the same dimension.
Instance details Defined in Agda.Termination.Order Methods notWorse :: Matrix i o -> Matrix i o -> Bool 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.
Instance details Defined in Agda.Termination.SparseMatrix Methods diagonal :: Matrix i b -> [b] Source #

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

Association of indices to values.

data Size i Source #

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) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods (==) :: Size i -> Size i -> Bool Source # (/=) :: Size i -> Size i -> Bool Source #
Ord i => Ord (Size i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods compare :: Size i -> Size i -> Ordering Source # (<) :: Size i -> Size i -> Bool Source # (<=) :: Size i -> Size i -> Bool Source # (>) :: Size i -> Size i -> Bool Source # (>=) :: Size i -> Size i -> Bool Source # max :: Size i -> Size i -> Size i Source # min :: Size i -> Size i -> Size i Source #
Show i => Show (Size i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods showsPrec :: Int -> Size i -> ShowS Source # show :: Size i -> String Source # showList :: [Size i] -> ShowS Source #

data MIx i Source #

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) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods (==) :: MIx i -> MIx i -> Bool Source # (/=) :: MIx i -> MIx i -> Bool Source #
Ord i => Ord (MIx i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods compare :: MIx i -> MIx i -> Ordering Source # (<) :: MIx i -> MIx i -> Bool Source # (<=) :: MIx i -> MIx i -> Bool Source # (>) :: MIx i -> MIx i -> Bool Source # (>=) :: MIx i -> MIx i -> Bool Source # max :: MIx i -> MIx i -> MIx i Source # min :: MIx i -> MIx i -> MIx i Source #
Show i => Show (MIx i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods showsPrec :: Int -> MIx i -> ShowS Source # show :: MIx i -> String Source # showList :: [MIx i] -> ShowS Source #
Ix i => Ix (MIx i) Source # |
Instance details Defined in Agda.Termination.SparseMatrix Methods range :: (MIx i, MIx i) -> [MIx i] Source # index :: (MIx i, MIx i) -> MIx i -> Int Source # unsafeIndex :: (MIx i, MIx i) -> MIx i -> Int inRange :: (MIx i, MIx i) -> MIx i -> Bool Source # rangeSize :: (MIx i, MIx i) -> Int Source # 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 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`.

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

zipMatrices Source #

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

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

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.

Methods

diagonal :: m -> [e] Source #

Instances

Diagonal (CallMatrixAug cinfo) Order Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods diagonal :: CallMatrixAug cinfo -> [Order] Source #
HasZero a => Diagonal (CallMatrix' a) a Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods 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.
Instance details Defined in Agda.Termination.SparseMatrix Methods diagonal :: Matrix i b -> [b] Source #

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

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

Compute the matrix size of the union of two matrices.

zipAssocWith Source #

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