On equational theories, unification, and (un)decidability (Q1825184)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | On equational theories, unification, and (un)decidability |
scientific article |
Statements
On equational theories, unification, and (un)decidability (English)
0 references
1989
0 references
We investigate the following classes of equational theories which are important in unification theory: permutative, finite, Noetherian, almost collapse free, collapse free, regular, and \(\Omega\)-free theories. We show some relationships between the particular classes and their connections to the unification hierarchy. Especially, we study conditions under which minimal and complete sets of unifiers always exist. We have some undecidability results for the membership problem of equational theories to these classes (the `class problem'): simplicity, almost collapse freeness, and \(\Omega\)-freeness are undecidable properties. Finiteness is known to be also undecidable, and the other investigated properties, permutativity, regularity, collapse freeness, are known to be trivially decidable. We give an equational theory where every single equation has a minimal set of unifiers, however, for some systems of equations no minimal set of unifiers exists. This example suggests that the definition of a unification problem has to be modified and that the definitions of the unification types have to be adapted accordingly.
0 references
solving equations
0 references
decidability
0 references
equational theories
0 references
unification
0 references
undecidability
0 references