agum-1.0: Unification and Matching in an Abelian Group

Algebra.AbelianGroup.UnificationMatching

Contents

Description

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)
Group Identity
x + 0 = x
Cancellation
x + -x = 0

A substitution maps variables to terms. A substitution s is extended 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.

Synopsis

# Terms

data Term Source

A term in an Abelian group is represented by the group 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 group identity, the plus sign is the group operation, and the minus sign is the group inverse.

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

add :: Term -> Term -> TermSource

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

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

# Unification and Matching

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

newtype Maplet Source

A maplet maps one variable into a term. For the show and read methods, the variable and the term are separated by a colon. A list of maplets represents a substitution.

Constructors

 Maplet (String, Term)

Instances

 Eq Maplet Read Maplet Show Maplet

unify :: Monad m => Equation -> m [Maplet]Source

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

match :: Monad m => Equation -> m [Maplet]Source

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