Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems

Abstract

We define E-unification, weak E-unification, E-upper bound, E-lower bound and E-generalization problems and the corresponding notions of unification, weak unification, upper bound, lower bound and generalization type of an equational theory. Most general unifiers, most general weak unifiers, suprema, infima and most specific generalizers correspond to "weak versions" of well-known categorical concepts. The problems are first studied for the empty theory using the restricted instantiation ordering ( i.e., substitutions are compared w.r.t. their behaviour on finite sets of variables ) and the unrestricted instantiation ordering ( i.e., substitutions are compared w.r.t. their behaviour on all variables ). This shows that the unrestricted instantiation ordering should only be used for unification. For the other problems the restricted ordering yields much better results. We shall also show that there exists an equational theory where unification problems always have most general unifiers w.r.t. the restricted instantiation ordering but not w.r.t. the unrestricted instantiation ordering. This accounts for the fact that equational unification is mostly done with restricted instantiation. Most general unifiers ( i.e., weak coequalizers ) modulo commutative theories cannot always be chosen as coequalizers. But we can give algebraic conditions under which this is possible. For the class of commutative theories there always exist least specific generalizers. That means that all commutative theories have generalization type "unitary".