String Unification is Essentially Infinitary.

A unifier of two terms s and t is a substitution sigma such that s sigma = t sigma and for first-order terms there exists a most general unifier sigma in the sense that any other unifier delta can be composed from sigma with some substitution lambda, i.e. delta = sigma omicron lambda.For many practical applications it turned out to be useful to generalize this notion to E-unification, where E is an equational theory, = (E) is equality under E and sigma is an E-unifier if s sigma = (E) t sigma. Depending on the equational theory E, the set of most general unifiers is always a singleton (as above) or it may have more than one unifier, either finitely or infinitely many unifiers and for some theories it may not even exist, in which case we call the theory of type nullary.String unification (or Lob's problem, Markov's problem, unification of word equations or Makanin's problem as it is often called in the literature) is the E-unification problem, where E = {f(x, f(y, z)) = f(f(x, y), z)}, i.e. unification under associativity or string unification once we drop the fs and the brackets. It is well known that this problem is infinitary and decidable.Essential unifiers, as introduced by Hoche and Szabo, generalize the notion of a most general unifier and have a dramatically pleasant effect in the sense that the set of essential unifiers is often much smaller than the set of most general unifiers. Essential unification may even reduce an infinitary theory to an essentially finitary theory. The most dramatic reduction known so far is obtained for idempotent semigroups or bands as they are called in computer science: bands are of type nullary, i.e. there exist two unifiable terms s and t, for which the complete and minimal set of most general unifiers does not exist. This is in stark contrast to essential unification: the set of essential unifiers for bands always exists and is finite.We show in this paper that string unification in one variable, known to be infinitary, has a finite number of essential unifiers (i.e. is e-finitary), however the early hope for a similar reduction of unification under associativity is not justified: string unification is essentially infinitary. We give an enumeration algorithm for essential unifiers.