Agda-2.6.1: 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.

Constructors

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

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.