This library attempts to formalize the matrix-free implementation of linear
algebra, where a matrix is represented as a linear map from one vector space
to another. This is accomplished by representing matrices as a pair of
functions (matrix vector multiply M and matrix transpose vector multiply
Mᵀ) that must have two properties
-
Each function respects linearity and homogeneity.
- Linearity:
(u v : Vec A m) → f (u +ⱽ v) ≡ f u +ⱽ f v - Homogeneity:
(c : A) → (v : Vec A m) → f (c ∘ⱽ v) ≡ c ∘ⱽ (f v)
- Linearity:
-
The pair of functions must form a valid inner product:
(x : Vec A m) → (y : Vec A n) → ⟨ x , M ·ˡᵐ y ⟩ ≡ ⟨ y , Mᵀ ·ˡᵐ x ⟩.
This library is based off the following previous implementations of the idea.
- PyOp, a Python library for composing matrix-free linear algebra.
Has primary been used in Magnetic Particle Imaging (MPI) reconstruction
techniques that involve convex optimization. Represents matrices as a pair
of functions of type
numpy.ndarray -> numpy.ndarray. No proofs or size checking is performed. - convex, a Haskell implementation of PyOp that is an investigation
into how dependent Haskell can be used to add compile time guarantees to
the composition of matrix-free operators. Represents matrices as a pair of
functions on dependent vector (
Vec A n) types. Sizes are checked at compile time, but there are no proofs of linearity, homogeneity, or the inner product property.
A presentation comparing how these representations can be used and what bugs can occur in each was presented for LambdaConf 2020.
All of these instructions assume that the nix package manager is installed.
This repository includes a shell file that will make the agda 2.6.4.1 binary
available. Simply type nix-shell to get started.
It is recommended that you use emacs to write Agda code, although any editor with agda-mode support will work.
This library can be included in other Agda packages using either the
agdaPackages.mkDerivation or agdaPackages.callPackage functions in
nixpkgs. More details on how to package Agda with nix can
be found in the Agda section of the nixpkgs manual.
The following Agda libraries are used:
standard-library(version 2.0 only, does not work with the 1.x series)
You can override which specific version of the standard library is being used
through Nix by changing the use-overlay-standard-library boolean in
agda-stardard-library.nix and updating the git revision to the one you'd like
to use.
If you want to learn more Agda (from a fellow Agda beginner) or have a new idea, please submit a pull request! I would like to get to the following at some point:
- Square root of a matrix. This should be finding a matrix A^(1/2) such that B = A^(1/2)A^(1/2) is held.
- Proving that a matrix is positive semidefinite. This should be possible by using the inner product definition.
- Prove a transformation of an optimization problem preserves the problem solution.