Let E be an equational theory and let ? be the signature of the term algebra. An E-unification problem is a finite set of equations

An E-unifier of Г is a substitution о, such that

The set of all E-unifiers of Г is denoted U ?E (Г). A complete set of E-unifiers cU ?e (Г) for Г is a set of E-unifiers, such that for every E-unifier т there exists о e cU ?e (Г) with о <E т .Theset pU ?E (Г) is called a minimal complete set of E-unifiers for Г, if it is complete and for all distinct elements о and о' in pU ?E (Г) о <E о' implies о =E о'.

When a minimal complete set of E-unifiers of a unification problem Г exists, it is unique up to subsumption equivalence ~E. Minimal complete sets of E-unifiers need not always exist, and if they do, they might be singular, finite, or infinite. Since minimal complete sets of E-unifiers are isomorphic whenever they exist, they can be used to classify theories with respect to their corresponding unification problem as well. This leads naturally to the concept of a unification hierarchy which was first introduced in Siekmann’s doctoral thesis in 1976 [73] and further refined and extended by himself and his later students as well as by many subsequent workers in the field of unification theory, see [7, 8, 31, 50, 76] for the standard surveys on this aspect.

A unification problem Г is:

  • nullary, if Г is unifiable, but the minimal complete set of E-unifiers does not exist.
  • unitary, if it is not nullary and the minimal complete set of E-unifiers for Г is of cardinality less or equal to 1.
  • finitary, if it is not nullary and the minimal complete set of E-unifiers is always finite.
  • infinitary, if it is not nullary and the minimal complete set of E-unifiers is infinite. An equational theory E is:
  • unitary, if all unification problems for E are unitary
  • finitary, if all unification problems are finitary.
  • infinitary, if there is at least one infinitary unification problem and all unification problems have minimal complete sets of E-unifiers.
  • • If there exists a solvable unification problem Г not having a minimal complete set of E-unifiers, then the equational theory E is nullary or of type zero.

The subsumption order and the encompassment order for E-unifiers are inherited from the above order on substitutions, that is an E-unifier о is more general than an E-unifier т, denoted as о <E т, if there exists a substitution X such that т =VE оХ.

< Prev   CONTENTS   Source   Next >