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 group 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
The axioms associated with the algebra are:
- x + y = y + x
- (x + y) + z = x + (y + z)
- Group Identity
- 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.
- data Term
- ide :: Term
- isVar :: String -> Bool
- var :: String -> Term
- mul :: Int -> Term -> Term
- add :: Term -> Term -> Term
- assocs :: Term -> [(String, Int)]
- newtype Equation = Equation (Term, Term)
- data Substitution
- subst :: [(String, Term)] -> Substitution
- maplets :: Substitution -> [(String, Term)]
- apply :: Substitution -> Term -> Term
- unify :: Equation -> Substitution
A term in a commutative monoid is represented by the group 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 group identity, the plus sign is the group operation.
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
Return all variable-coefficient pairs in the term in ascending variable order.
Equations and Substitutions
An equation is a pair of terms. For the show and read methods, the two terms are separated by an equal sign.
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.
Construct a substitution from a list of variable-term pairs.
Return all variable-term pairs in ascending variable order.