Unification in monoidal theories is solving linear equations over semirings

Although for numerous equational theories unification algorithms have been developed 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 the corresponding semiring. More specifically, problems without free constants are translated into homogeneous equations. For problems with free constants inhomogeneous equations have to be solved in addition. Exploiting the correspondence between unification and linear algebra we give algebraic characterizations of the unification type of a theory. In particular, we show that with respect to unification without constants monoidal theories are either unitary or nullary. Applying Hilbert's Basis Theorem we prove that theories of groups with commuting homomorphisms are unitary with respect to unification with and without constants