Algebra.CommutativeMonoid.Unification

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.

Terms

data Term

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.

Instances

Eq Term

Read Term

Show Term

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 non-negative 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

Read Equation

Show Equation

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

Read Substitution

Show Substitution

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

unify :: Equation -> Substitution

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