Unification in commutative semigroups (Q1383954)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Unification in commutative semigroups |
scientific article |
Statements
Unification in commutative semigroups (English)
0 references
26 August 1998
0 references
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.
0 references
unification types
0 references
varieties of commutative semigroups
0 references
automated theorem proving
0 references
finite sets of equations
0 references
0 references