Unification, weak unification, upper bound, lower bound, and generalization problems

Abstract

We introduce 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. When defining instantiation preorders on solutions of these problems, one can compared substitutions w.r.t. their behaviour on all variables or on finite sets of variables. We shall study the effect which these different instantiation preorders have on the existence of most general or most specific solutions of E-unification, weak E-unification, and E-generalization problems. In addition, we shall elucidate the subtle difference between most general unifiers and coequalizers, and we shall consider generalization in the class of commutative theories.