module Linear: sig
.. end
Various operations for the vector space int -> QQ
Various operations for the vector space int -> QQ
exception No_solution
Raised for unsolvable systems of linear equations
exception Nonlinear
module type Vector = sig
.. end
module ZZVector: sig
.. end
module QQVector: sig
.. end
module QQMatrix: sig
.. end
module type AbelianGroup = sig
.. end
module type Ring = sig
.. end
module RingMap: functor (
M
:
sig
type 'a
t
type
key
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val enum : 'a t -> (key * 'a) BatEnum.t
val map : ('a -> 'b) -> 'a t -> 'b t
val find : key -> 'a t -> 'a
val add : key -> 'a -> 'a t -> 'a t
val remove : key -> 'a t -> 'a t
val empty : 'a t
val merge : (key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
end
) ->
functor (
R
:
Ring
) ->
Vector
with type t = R.t M.t
and type dim = M.key
and type scalar = R.t
Lift a map type over a ring to a left-module
val nullspace : QQMatrix.t -> int list -> QQVector.t list
nullspace mat dimensions
computes a basis for the vector space { x :
max*x = 0}
, projected on to the set of dimensions dimensions
. (Note
that the nullspace is not finitely generated in int -> QQ
, hence the
projection).
val solve_exn : QQMatrix.t -> QQVector.t -> QQVector.t
solve_exn mat b
computes a rational vector x
such that mat*x =
b
. Raises No_solution
if there is no solution.
val solve : QQMatrix.t -> QQVector.t -> QQVector.t option
solve mat b
computes a rational vector x
such that mat*x = b
, if
such a vector exists. Otherwise, return None
.
val orient : (int -> bool) -> QQVector.t list -> (int * QQVector.t) list
Given a predicate on dimensions and a list of terms (all implicitly equal
to zero), orient the equations as rewrite rules that eliminate dimensions
that don't satisfy the predicate.
val vector_right_mul : QQMatrix.t -> QQVector.t -> QQVector.t
vector_right_mul m a
computes m*a
val intersect_rowspace : QQMatrix.t ->
QQMatrix.t -> QQMatrix.t * QQMatrix.t
Given two matrices A
and B
, compute matrices C
and D
such that CA
= DB
is a basis for the intersection of the rowspaces of A
and B
.
val divide_right : QQMatrix.t -> QQMatrix.t -> QQMatrix.t option
Given two matrices A and B, compute a matrix C such that CB = A (if one
exists). C exists when the rowspace of B is contained in the rowspace of
A. If A and B are invertible, then C is exactly AB-1.
val max_rowspace_projection : QQMatrix.t -> QQMatrix.t -> QQMatrix.t
Given matrices A
and B
, find a matrix C
whose rows constitute a
basis for the vector space { v : exists u. uA = vB }
val rational_triangulation : QQMatrix.t -> QQMatrix.t * QQMatrix.t
Given a matrix A
, find a pair of matrices (M,T)
such that MA = TM
,
T
is lower-triangular, and the rowspace of MA
is maximal.
val evaluate_affine : (int -> QQ.t) -> QQVector.t -> QQ.t
Affine terms
Various operations for manipulating affine terms over symbols, represented
as rational vectors
val sym_of_dim : int -> Syntax.symbol option
Map a symbol to a dimension. The following equations hold:
sym_of_dim (dim_of_sym sym) = Some sym
sym_of_dim const_dim = None
val dim_of_sym : Syntax.symbol -> int
Map a dimension to symbol. The following equations hold:
sym_of_dim (dim_of_sym sym) = Some sym
sym_of_dim const_dim = None
val const_dim : int
Dimension for representing the coefficient of the constant 1.
val const_linterm : QQ.t -> QQVector.t
Representation of a rational number as an affine term. The equation
const_of_linterm (const_linterm qq) = Some qq
must hold.
val const_of_linterm : QQVector.t -> QQ.t option
Convert an affine term to a rational number, if possible. The equation
const_of_linterm (const_linterm qq) = Some qq
must hold.
val linterm_of : 'a Syntax.context -> 'a Syntax.term -> QQVector.t
Convert a rational vector representing an affine term. Raises Nonlinear
if the input term is non-linear.
val of_linterm : 'a Syntax.context -> QQVector.t -> 'a Syntax.term
Convert a rational vector to an affine term. The equation of_linterm srk
(linterm_of srk t) = t
must hold.
val pp_linterm : 'a Syntax.context -> Format.formatter -> QQVector.t -> unit
Pretty-print an affine term
val evaluate_linterm : (Syntax.symbol -> QQ.t) -> QQVector.t -> QQ.t
evaluate_linterm env t
evaluates the affine term t in the environment
env
val linterm_size : QQVector.t -> int
Count the number of dimensions with non-zero coefficients