Algebra.AbelianGroup.UnificationMatching

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:

• the binary symbol +, the group operator,
• a constant 0, the identity element, and
• the unary symbol -, the inverse operator.

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

Cancellation

x + -x = 0

A substitution maps variables to terms. A substitution s is applied to a term as follows.

• s(0) = 0
• s(-t) = -s(t)
• 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. 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.

Terms

data Term

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.

Instances

Eq Term

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Read Term

Methods

readsPrec :: Int -> ReadS Term

readList :: ReadS [Term]

readPrec :: ReadPrec Term

readListPrec :: ReadPrec [Term]

Show Term

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

ide :: Term

ide represents the identity element (zero).

isVar :: String -> Bool

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.

var :: String -> Term

Return a term that consists of a single variable.

mul :: Int -> Term -> Term

Multiply every coefficient in a term by an integer.

add :: Term -> Term -> Term

Add two terms.

assocs :: Term -> [(String, Int)]

Return all variable-coefficient pairs in the term in ascending variable order.

Equations and Substitutions

newtype Equation

An equation is a pair of terms. For the show and read methods, the two terms are separated by an equal sign.

Constructors

Equation (Term, Term)

Instances

Eq Equation

Methods

(==) :: Equation -> Equation -> Bool

(/=) :: Equation -> Equation -> Bool

Read Equation

Methods

readsPrec :: Int -> ReadS Equation

readList :: ReadS [Equation]

readPrec :: ReadPrec Equation

readListPrec :: ReadPrec [Equation]

Show Equation

Methods

showsPrec :: Int -> Equation -> ShowS

show :: Equation -> String

showList :: [Equation] -> ShowS

data Substitution

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.

Instances

Eq Substitution

Methods

(==) :: Substitution -> Substitution -> Bool

(/=) :: Substitution -> Substitution -> Bool

Read Substitution

Methods

readsPrec :: Int -> ReadS Substitution

readList :: ReadS [Substitution]

readPrec :: ReadPrec Substitution

readListPrec :: ReadPrec [Substitution]

Show Substitution

Methods

showsPrec :: Int -> Substitution -> ShowS

show :: Substitution -> String

showList :: [Substitution] -> ShowS

subst :: [(String, Term)] -> Substitution

Construct a substitution from a list of variable-term pairs.

maplets :: Substitution -> [(String, Term)]

Return all variable-term pairs in ascending variable order.

apply :: Substitution -> Term -> Term

Return the result of applying a substitution to a term.

Unification and Matching

unify :: Equation -> Substitution

Given Equation (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.

match :: Monad m => Equation -> m Substitution

Given Equation (t0, t1), return a most general substitution s such that s(t0) = t1 modulo the equational axioms of an Abelian group.