-- 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.7


-- | 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,<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></li>
--   <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 GHC.Classes.Eq Algebra.AbelianGroup.UnificationMatching.Maplet
instance GHC.Classes.Eq Algebra.AbelianGroup.UnificationMatching.Substitution
instance GHC.Classes.Eq Algebra.AbelianGroup.UnificationMatching.Equation
instance GHC.Classes.Eq Algebra.AbelianGroup.UnificationMatching.Term
instance GHC.Show.Show Algebra.AbelianGroup.UnificationMatching.Maplet
instance GHC.Read.Read Algebra.AbelianGroup.UnificationMatching.Maplet
instance GHC.Show.Show Algebra.AbelianGroup.UnificationMatching.Substitution
instance GHC.Read.Read Algebra.AbelianGroup.UnificationMatching.Substitution
instance GHC.Show.Show Algebra.AbelianGroup.UnificationMatching.Equation
instance GHC.Read.Read Algebra.AbelianGroup.UnificationMatching.Equation
instance GHC.Show.Show Algebra.AbelianGroup.UnificationMatching.Term
instance GHC.Read.Read Algebra.AbelianGroup.UnificationMatching.Term