Unification in commutative semigroups (Q1383954)

Let \(V\) be a variety of algebras and \(X\) a fixed set of variables. Every function \(\sigma\) assigning \(V\)-terms to variables is called a substitution. If \(p\) is a term and \(\sigma\) is a substitution, the term \(\sigma(p)\) is defined in the usual way. Let \(\Sigma\) be a finite set of equations over \(V\). A substitution \(\sigma\) is said to be a unifier of \(\Sigma\), if for every equation \(p\approx q\in\Sigma\), the equation \(\sigma(p)\approx\sigma(q)\) holds in \(V\). The problem is to describe the structure of the set \(U(\Sigma,V)\) of all unifiers of \(\Sigma\). Speaking non-formally, it means that we want to describe all solutions of finite sets of equations, defining if every solution comes from a most general solution, and if so, defining how many most general solutions are needed to generate all solutions. This problem is solved for all varieties of commutative semigroups. A unifier \(\sigma_1\) is called more general than a unifier \(\sigma_2\) (\(\sigma_1\leq\sigma_2\)) if \(\sigma_2=\tau\sigma_1\) for some substitution \(\tau\). One of the results obtained states that every nontrivial variety \(V\) of commutative semigroups has finitary unification type (it means that all unifiers are generated, relative to \(\leq\), by a finite number of most general unifiers), unless \(V\) is the variety of abelian groups of exponent \(r>1\) or the variety of nullsemigroups, in which cases the unification type is unitary. Another result states that for commutative semigroups the unification problem is solvable. The author assumes that this is the first so general result in the area.