-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Unification and Matching in an Abelian Group
--   
--   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 an Abelian group. The matching problem is to find a most general
--   substitution s such that s(t) = t' modulo the axioms. Substitition s
--   is more general than s' if there is a substitition s" such that s' =
--   s" o s.
@package agum
@version 2.3


-- | Integer Solutions of Linear Inhomogeneous Equations
--   
--   A linear equation with integer coefficients is represented as a pair
--   of lists of non-zero integers, the coefficients and the constants. If
--   there are no constants, the linear equation represented by (c, []) is
--   the homogeneous equation:
--   
--   <pre>
--   c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = 0
--   </pre>
--   
--   where n is the length of c. Otherwise, (c, d) represents the
--   inhomogeneous equation:
--   
--   <pre>
--   c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1] = g
--   </pre>
--   
--   where g = gcd(d[0], d[1], ..., d[m-1]), and m is the length of d. Thus
--   g is the greatest common denominator of the elements of d.
--   
--   A solution is a partial map from variables to terms, and a term is a
--   pair of lists of integers, the variable part of the term followed by
--   the constant part. The variable part may specify variables not in the
--   input. In other words, the length of the coefficents in the answer may
--   exceed the length of the coefficients in the input. For example, the
--   solution of
--   
--   <pre>
--   64x - 41y = 1
--   </pre>
--   
--   is x = -41z - 16 and y = -64z - 25. The computed solution is read off
--   the list returned as an answer.
--   
--   <pre>
--   intLinEq [64,-41] [1] =
--       [(0,([0,0,0,0,0,0,-41],[-16])),
--       (1,([0,0,0,0,0,0,-64],[-25]))]
--   </pre>
--   
--   The algorithm used to find solutions is described in Vol. 2 of The Art
--   of Computer Programming / Seminumerical Alorithms, 2nd Ed., 1981, by
--   Donald E. Knuth, pg. 327. To show sums, we write
--   
--   <pre>
--   sum[i] c[i]*x[i] for c[0]*x[0] + c[1]*x[1] + ... + c[n-1]*x[n-1].
--   </pre>
--   
--   The algorithm's initial values are the linear equation (c,d) and an
--   empty substitution s.
--   
--   <ol>
--   <li>Let c[i] be the smallest non-zero coefficient in absolute
--   value.</li>
--   <li>If c[i] &lt; 0, multiply c and d by -1 and goto step 1.</li>
--   <li>If c[i] = 1, a general solution of the following form has been
--   found:</li>
--   </ol>
--   
--   <pre>
--   x[i] = sum[j] -c'[j]*x[j] + d[k] for all k
--   </pre>
--   
--   where c' is c with c'[i] = 0. Use the equation to eliminate x[i] from
--   the range of the current substitution s. If variable x[i] is in the
--   original equation, add the mapping to substitution s.
--   
--   <ol>
--   <li>If c[i] divides every coefficient in c,</li>
--   </ol>
--   
--   <ul>
--   <li>if c[i] divides every constant in d, divide c and d by c[i] and
--   goto step 3,</li>
--   <li>otherwise fail because there is no solution.</li>
--   </ul>
--   
--   <ol>
--   <li>Otherwise, eliminate x[i] as above in favor of freshly created
--   variable x[n], where n is the length of c.</li>
--   </ol>
--   
--   <pre>
--   x[n] = sum[j] (c[j] div c[i] * x[j])
--   </pre>
--   
--   Goto step 1 and solve the equation:
--   
--   <pre>
--   c[i]*x[n] + sum[j] (c[j] mod c[i])*x[j] = d[k] for all k
--   </pre>
module Algebra.AbelianGroup.IntLinEq

-- | A linear equation with integer coefficients is represented as a pair
--   of lists of non-zero integers, the coefficients and the constants.
type LinEq = ([Int], [Int])

-- | A solution to a linear equation is a partial map from variables to
--   terms, and a term is a pair of lists of integers, the variable part of
--   the term followed by the constant part. The variable part may specify
--   variables not in the input. In other words, the length of the
--   coefficents in the answer may exceed the length of the coefficients in
--   the input.
type Subst = [(Int, LinEq)]

-- | Find integer solutions to a linear equation or fail when there are no
--   solutions.
intLinEq :: Monad m => LinEq -> m Subst


-- | This module provides unification and matching in an Abelian group.
--   
--   In this module, an Abelian group is a free algebra over a signature
--   with three function symbols:
--   
--   <ul>
--   <li>the binary symbol +, the group operator,</li>
--   <li>a constant 0, the identity element, and</li>
--   <li>the unary symbol -, the inverse operator.</li>
--   </ul>
--   
--   The algebra is generated by a set of variables. Syntactically, a
--   variable is an identifer such as x and y (see <a>isVar</a>).
--   
--   The axioms associated with the algebra are:
--   
--   <ul>
--   <li><i>Communtativity</i> x + y = y + x</li>
--   <li><i>Associativity</i> (x + y) + z = x + (y + z)</li>
--   <li><i>Identity Element</i> x + 0 = x</li>
--   <li><i>Cancellation</i> x + -x = 0</li>
--   </ul>
--   
--   A substitution maps variables to terms. A substitution s is applied to
--   a term as follows.
--   
--   <ul>
--   <li>s(0) = 0</li>
--   <li>s(-t) = -s(t)</li>
--   <li>s(t + t') = s(t) + s(t')</li>
--   </ul>
--   
--   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. The matching problem is to find a most general
--   substitution s such that s(t) = t' modulo the axioms. Substitition s
--   is more general than s' if there is a substitition s" such that s' =
--   s" o s.
module Algebra.AbelianGroup.UnificationMatching

-- | A term in an Abelian group is represented by the identity element, or
--   as the sum of factors. A factor is the product of a non-zero 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 group operation, and the minus sign is the group inverse.
data Term

-- | <a>ide</a> 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 <a>isVar</a>
--   predicate.
isVar :: String -> Bool

-- | Return a term that consists of a single variable.
var :: String -> Term

-- | Multiply every coefficient in a term by an 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 <a>Equation</a> (t0, t1), return a most general substitution s
--   such that s(t0) = s(t1) modulo the equational axioms of an Abelian
--   group. Unification always succeeds.
unify :: Equation -> Substitution

-- | Given <a>Equation</a> (t0, t1), return a most general substitution s
--   such that s(t0) = t1 modulo the equational axioms of an Abelian group.
match :: Monad m => Equation -> m Substitution
instance Eq Maplet
instance Eq Substitution
instance Eq Equation
instance Eq Term
instance Read Substitution
instance Show Substitution
instance Read Maplet
instance Show Maplet
instance Read Equation
instance Show Equation
instance Read Term
instance Show Term