-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Unification in a Commutative Monoid
--
-- The unification problem is given the problem statement t =? t', find a
-- most general substitution s such that s(t) = s(t') modulo the axioms
-- of a commutative monoid. Substitition s is more general than s' if
-- there is a substitition s" such that s' = s" o s.
@package cmu
@version 1.7
-- | Linear Diophantine Equation solver.
--
-- The solver uses the algorithm of Contejean and Devie as specified in
-- "An Efficient Incremental Algorithm for Solving Systems of Linear
-- Diophantine Equations", Information and Computation Vol. 113, pp.
-- 143-174, 1994 after a modification explained below.
--
-- The algorithm for systems of homogeneous linear Diophantine equations
-- follows. Let e[k] be the kth basis vector for 1 <= k <= n. To
-- find the minimal, non-negative solutions M to the system of equations
-- sum(i=1,n,a[i]*v[i]) = 0, the modified algorithm of Contejean and
-- Devie is:
--
--
-- - [init] A := {e[k] | 1 <= k <= n}; M := {}
-- - [new minimal results] M := M + {a in A | a is a solution}
-- - [breadth-first search] A := {a + e[k] | a in A, 1 <= k <= n,
-- <sum(i=1,n,a[i]*v[i]),v[k]> < 0}
-- - [unnecessary branches] A := {a in A | all m in M : some 1 <= k
-- <= n : m[k] < a[k]}
-- - [test] If A = {}, stop, else go to 2.
--
--
-- The original algorithm reversed steps 3 and 4.
--
-- This module provides a solver for a single linear Diophantine equation
-- a*v = b, where a and v are vectors, not matrices. Conceptually, it
-- uses the homogeneous solver after appending -b as the last element of
-- v and by appending 1 to a at each step in the computation. The extra 1
-- is omitted when an answer is produced.
--
-- Steps 3 and 4 were switched because the use of the original algorithm
-- for the problem 2x + y - z = 2 produces a non-minimal solution.
-- linDiophEq [2,1,-1] 2 = [[1,0,0],[0,2,0]], but the original algorithm
-- produces [[1,0,0],[0,2,0],[1,1,1]].
--
-- The algorithm is likely to be Fortenbacher's algorithm, the one
-- generalized to systems of equations by Contejean and Devie, but I have
-- not been able to verified this fact. I learned how to extend Contejean
-- and Devie's results to an inhomogeneous equation by reading "Effective
-- Solutions of Linear Diophantine Equation Systems with an Application
-- to Chemistry" by David Papp and Bela Vizari, Rutcor Research Report
-- RRR 28-2004, September, 2004,
-- http://rutcor.rutgers.edu/pub/rrr/reports2004/28_2004.ps.
--
-- The example that shows a problem with the original algorithm follows.
-- For the problem linDiophEq [2,1,-1] 2, the value of a and m at the
-- beginning of the loop is:
--
--
-- a m
-- [[0, 0, 1], [0, 1, 0], [1, 0, 0]] []
-- [[0, 1, 1], [0, 2, 0]] [[1, 0, 0]]
-- [] [[1, 0, 0], [0, 2, 0]]
--
--
-- Consider [0, 1, 1] in a. If you remove unnecessary branches first, the
-- element will stay in a. After performing breadth-first search, a will
-- contain [1, 1, 1], which is the unwanted, non-minimal solution.
module Algebra.CommutativeMonoid.LinDiophEq
-- | The linDiophEq function takes a list of integers that specifies
-- the coefficients of linear Diophantine equation and a constant, and
-- returns the equation's minimal, non-negative solutions. When solving
-- an inhomogeneous equation, solve the related homogeneous equation and
-- add in those solutions.
linDiophEq :: [Int] -> Int -> [[Int]]
-- | This module provides unification in a commutative monoid.
--
-- In this module, a commutative monoid is a free algebra over a
-- signature with two function symbols:
--
--
-- - the binary symbol +, the monoid operator,
-- - a constant 0, the identity element, and
--
--
-- The algebra is generated by a set of variables. Syntactically, a
-- variable is an identifer such as x and y (see isVar).
--
-- The axioms associated with the algebra are:
--
--
-- - Communtativity x + y = y + x
-- - Associativity (x + y) + z = x + (y + z)
-- - Identity Element x + 0 = x
--
--
-- A substitution maps variables to terms. A substitution s is applied to
-- a term as follows.
--
--
-- - s(0) = 0
-- - s(t + t') = s(t) + s(t')
--
--
-- The unification problem is given the problem statement t =? t', find a
-- most general substitution s such that s(t) = s(t') modulo the axioms
-- of the algebra. Substitition s is more general than s' if there is a
-- substitition s" such that s' = s" o s.
module Algebra.CommutativeMonoid.Unification
-- | A term in a commutative monoid is represented by the identity element,
-- or as the sum of factors. A factor is the product of a positive
-- integer coefficient and a variable. No variable occurs twice in a
-- term. For the show and read methods, zero is the identity element, the
-- plus sign is the monoid operation.
data Term
-- | ide represents the identity element (zero).
ide :: Term
-- | A variable is an alphabetic Unicode character followed by a sequence
-- of alphabetic or numeric digit Unicode characters. The show method for
-- a term works correctly when variables satisfy the isVar
-- predicate.
isVar :: String -> Bool
-- | Return a term that consists of a single variable.
var :: String -> Term
-- | Multiply every coefficient in a term by an non-negative integer.
mul :: Int -> Term -> Term
-- | Add two terms.
add :: Term -> Term -> Term
-- | Return all variable-coefficient pairs in the term in ascending
-- variable order.
assocs :: Term -> [(String, Int)]
-- | An equation is a pair of terms. For the show and read methods, the two
-- terms are separated by an equal sign.
newtype Equation
Equation :: (Term, Term) -> Equation
-- | A substitution maps variables into terms. For the show and read
-- methods, the substitution is a list of maplets, and the variable and
-- the term in each element of the list are separated by a colon.
data Substitution
-- | Construct a substitution from a list of variable-term pairs.
subst :: [(String, Term)] -> Substitution
-- | Return all variable-term pairs in ascending variable order.
maplets :: Substitution -> [(String, Term)]
-- | Return the result of applying a substitution to a term.
apply :: Substitution -> Term -> Term
-- | Given Equation (t0, t1), return a most general substitution s
-- such that s(t0) = s(t1) modulo the equational axioms of a commutative
-- monoid.
unify :: Equation -> Substitution
instance Eq Term
instance Eq Equation
instance Eq Substitution
instance Eq Maplet
instance Read Substitution
instance Show Substitution
instance Read Maplet
instance Show Maplet
instance Read Equation
instance Show Equation
instance Read Term
instance Show Term