Matching — A special case of unification?

AbstractUnification is the problem to solve equations of first order terms by finding (all) substitutions into their variables that make these two terms equal. Matching is the problem to solve equations, where only one of the terms has to be instantiated by the substitution. Usually research in unification theory does not take care of the problems arising with matching, as it is considered as a special form of unification. We recall the various definitions of matching from the literature and we compare matching and unification in a more general framework called restricted unification. We show that matching and unification in collapse free cquational theories behave similar with respect to the existence and the cardinality of minimal complete sets of solutions. We present some counterexamples where matching and unification behave differently, especially we give an equational theory, in which the existence of solutions for unification problems is decidable, for matching problems, however, this is undecidable. Matching and restricted unification as defined here are equivalent to extending the given signature by free constants. Our counterexamples show that unification may become undecidable, if we add new free constants to the signature