Syntacticness, Cycle-Syntacticness, and Shallow Theories
Syntacticness, Cycle-Syntacticness, and Shallow Theories
复制标题
句法性、循环句法性和浅层理论
DOI：
10.1006/inco.1994.1043
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
J. Jouannaud
中科院分区：
文献类型：
--
作者：
Hubert Comon;Marianne Haberstrau;J. Jouannaud
在自由代数T(F，X)(即统一)中，方程的求解采用两个规则：ƒ(S)=ƒ(T)→S=t(分解)和S[x]=x→⊥(出现-检验)。这两个规则在有限生成的同余=E的商T(F，X)中是不正确的。在C.Kirchner之后，我们首先定义了几类等式理论(分别称为句法和循环句法)，对于这些理论，可以推导出一些规则来取代上面的两种规则。然后，我们证明了这些抽象类是相关的：所有浅层理论，即变量在深度至多出现一个的方程所生成的理论，都是句法和循环句法。此外，新的统一规则正在终结，这证明了在肤浅的理论中，统一是可决定的和有限的。我们还给出了进一步的扩展。如果等价类集是无限的，这个问题在浅表理论中证明是可判定的，那么浅表理论满足Colmerauer的方程独立性原理(n个方程的合取是可解的当且仅当每个方程是可解的)。这使我们能够推导出量词消除规则。结果表明，这些规则对于浅理论确实是终止的；因此，当F是有限的而E是浅的时，商代数T(F)/=E的一阶理论是可判定的。这推广了Mal‘cev关于完全可公理的(置换)局部自由代数类的结果。
Abstract Solving equations in the free algebra T ( F, X ) (i.e., unification ) uses the two rules: ƒ( s ) = ƒ( t ) → s = t (decomposition) and s [ x ] = x → ⊥ (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.