The Exact Unification Type of Commutative Theories

The exact unification type of an equational theory is based on a new preorder on substitutions, called the exactness preorder, which is tailored towards transferring decidability results for unification to disunification. We show that two important results regarding the unification type of commutative theories hold not only for the usual instantiation preorder, but also for the exactness preorder: w.r.t. elementary unification, commutative theories are of type unary or nullary, and the theory ACUIh of Abelian idempotent monoids with a homomorphism is nullary.