AI 中文总结
本文提出一种通过相容性和边交换性条件扩展有限子ARS来证明合流性的新方法，并应用于证明非E-重叠弱浅层TRS的合流性，去掉了非坍缩假设，得到可判定的合流充分条件。
AI 中文摘要
本文提出了一种证明抽象归约系统（ARS）合流性的新方法，通过阐明充分条件（称为相容性和边交换性），以添加重写边的方式将给定的有限子ARS扩展为合流系统。该方法可视为我们早期工作的延伸，早期工作证明了弱非重叠、浅层且非坍缩的项重写系统（TRS）是合流的。此外，我们应用该方法证明了非E-重叠且弱浅层的TRS是合流的。此处，若每个定义函数符号要么出现在根位置，要么出现在基子项中，则该项称为弱浅层的；若一个TRS的所有重写规则的两侧都是弱浅层的，则该TRS是弱浅层的。这去掉了我们先前关于弱浅层TRS工作中所假设的非坍缩条件。此外，由于弱浅层TRS在非ω-重叠时必为非E-重叠，且后者性质是可判定的，我们也得到了合流性的可判定充分条件：非ω-重叠且弱浅层的TRS是合流的。
英文摘要
This paper proposes a new method for proving the confluence of an abstract reduction system (ARS) by clarifying the sufficient conditions, called compatibility and edge commutativity, for expanding a given finite sub-ARS into a confluent one by adding rewrite edges. This method can be regarded as an extension of our earlier work, which showed that a weakly non-overlapping, shallow, and non-collapsing term rewriting system (TRS) is confluent. Furthermore, we apply our method to demonstrate that a non-$E$-overlapping and weakly shallow TRS is confluent. Here, a term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a TRS is weakly shallow if both sides of all its rewrite rules are weakly shallow. This drops the non-collapsing condition assumed in our previous work on weakly shallow TRSs. Moreover, since a weakly shallow TRS is non-$E$-overlapping whenever it is non-$ω$-overlapping, and the latter property is decidable, we also obtain a decidable sufficient condition for confluence: non-$ω$-overlapping and weakly shallow TRSs are confluent.
Comments68 pages, 17 figures
