Module Rewriting.UnificationSpec

Library for specifying the unification on first-order terms.

This library implements a general unification algorithm. Because the algorithm is easy to understand, but rather slow, it serves as a specification for more elaborate implementations.

Author: Michael Hanus, Jan-Hendrik Matthes, Jonas Oberschweiber, Bjoern Peemoeller

Version: February 2020

Summary of exported operations:

showUnificationError :: (a -> String) -> UnificationError a -> String  Deterministic 
Transforms a unification error into a string representation.
unify :: (Eq a, Show a) => [(Term a,Term a)] -> Either (UnificationError a) (Map Int (Term a))  Deterministic 
Unifies a list of term equations.
unifiable :: (Eq a, Show a) => [(Term a,Term a)] -> Bool  Deterministic 
Checks whether a list of term equations can be unified.

Exported datatypes:

UnificationError

Representation of a unification error, parameterized over the kind of function symbols, e.g., strings.

Constructors:

  • Clash :: (Term a) -> (Term a) -> UnificationError a : The constructor term t1 is supposed to be equal to the constructor term t2 but has a different constructor.
  • OccurCheck :: VarIdx -> (Term a) -> UnificationError a : The variable v is supposed to be equal to the term t in which it occurs as a subterm.

Exported operations:

showUnificationError :: (a -> String) -> UnificationError a -> String  Deterministic 

Transforms a unification error into a string representation.

unify :: (Eq a, Show a) => [(Term a,Term a)] -> Either (UnificationError a) (Map Int (Term a))  Deterministic 

Unifies a list of term equations. Returns either a unification error or a substitution.

unifiable :: (Eq a, Show a) => [(Term a,Term a)] -> Bool  Deterministic 

Checks whether a list of term equations can be unified.