cmu-1.1: Unification in a Commutative Monoid

Algebra.CommutativeMonoid.Unification

Description

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 `isVar`).

The axioms associated with the algebra are:

Communtativity
x + y = y + x
Associativity
(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.

Synopsis

# Terms

data Term Source

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.

Instances

 Eq Term Read Term Show Term

`ide` represents the identity element (zero).

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.

Return a term that consists of a single variable.

mul :: Int -> Term -> TermSource

Multiply every coefficient in a term by an non-negative integer.

add :: Term -> Term -> TermSource

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

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

# Equations and Substitutions

newtype Equation Source

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

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)] -> SubstitutionSource

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

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

Return all variable-term pairs in ascending variable order.

Return the result of applying a substitution to a term.

# Unification

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