SYNTACTICNESS, CYCLE-SYNTACTICNESS, AND SHALLOW THEORIES

Solving equations in the free algebra T(F, X) (i.e., unification) uses the two rules: f(s)=f(t)-->s=t (decomposition) and s[x]=x-->perpendicular-to (occur-check). These two rules are not correct in quotients of T(F, X) by a finitely generated congruence = E. Following C. Kirchner, we first define classes of equational theories (called syntactic and cycle-syntactic, respectively) for which it is possible to derive some rules replacing the two above. Then, we show that these abstract classes are relevant: all shallow theories, i.e., theories which can be generated by equations in which variables occur at depth at most one, are both syntactic and cycle syntactic. Moreover, the new set of unification rules is terminating, which proves that unification is decidable and finitary in shallow theories. We give still further extensions. If the set of equivalence classes is infinite, a problem which turns out to be decidable in shallow theories, then shallow theories fulfill Colmerauer's independence of disequations principle (a conjunction of n disequations is solvable iff each disequation alone is solvable). This allows us to derive quantifier-elimination rules. It turns out that these rules do terminate for shallow theories; hence the first-order theory of the quotient algebra T(F)/=E is decidable when F is finite and E is shallow. This extends Mal'cev results on the classes of (permutative) locally-free algebras that are completely axiomatizable. (C) 1994 Academic Press, Inc.