Semi-unification

Abstract

Semi-unification is a generalization of both matching and ordinary unification: for a given pair of terms s and t, two substitutions ρ and σ are sought such that ρ(σ(s))=σ(t). Semi-unifiability can be used as a check for non-termination of a rewrite rule, but constructing a correct semi-unification algorithm has been an elusive goal; for example, an algorithm given by Purdom in his RTA-87 paper was incorrect. This paper presents a decision procedure for semi-unification based on techniques similar to those used in the Knuth-Bendix completion procedure. When its inputs are semi-unifiable, the procedure yields a canonical term-rewriting system from which substitutions ρ and σ are easily extracted. Though exponential in its computing time, the decision procedure can be improved to a polynomial time algorithm, as will be shown.