Unification Properties of Idempotent Semigroups

Abstract

Unification in free idempotent semigroups is of unification type zero, i.e. there are unifiable terms s,t but there is no minimal, complete set of unifiers for these two terms. Unification in free idempotent semigroups is strongly complete, i.e. the unification problem <x =AI t> is always solvable with unifier [x <— t], even if x occurs in t. We give a generalization of the usual unification hierarchy and demonstrate that the number of independent unifiers in A+1-unifier sets is not bounded. It is known that there is a conditional, canonical term rewriting system for idempotent semigroups. To strengthen this result, we show that there can be no unconditioned and finite rewriting system.