Unification in monoidal theories is solving linear equations over semirings
Werner Nutt · 1992
Although unification algorithms have been developed for numerous equational theories there is still a lack of general methods. In this paper we apply algebraic techniques to the study of a whole class of theories, which we call monoidal. Our approach leads to general results on the structure of unification algorithms and the unification type of such theories. An equational theory is monoidal if it contains a binary operation which is associative and commutative, an identity for the binary operation, and an arbitrary number of unary symbols which are homomorphisms for the binary operation and the identity. Monoidal theories axiomatize varieties of abelian monoids. Examples are the theories of abelian monoids (AC), idempotent abelian monoids (ACI), and abelian groups. To every monoidal theory we associate a semiring. Intuitively, semirings are rings without subtraction. We show that every unification problem in a monoidal theory can be translated into a system of linear equations over t...