Reduction Strategy

语义标注是证明术语重写系统终止性的有力工具。然而，Zantema的一篇论文中描述的对方程项重写的扩展的有用性是相当有限的。在[1]中，我们引入了一个更强版本的方程语义标号，它由三个选项来参数化：(1)基础代数上的顺序(偏序与拟序)，(2)代数与重写系统(模型与准模型)之间的关系，以及(3)出现在方程中的函数符号的标号(禁止与允许)。我们给出了各种实例的可靠性和完备性结果，分析了它们之间的关系，给出了等式语义标注技术的两个应用，并继续研究了懒惰缩小演算的完备性。在前面一篇文章中，我们证明了关于…类的可归一化解，懒惰条件收缩演算LCnc是完备的更多的S合流但不一定终止条件重写系统，在没有所谓额外变量的条件部分重写规则。遗憾的是，证明没有提供任何有用的完整选择函数，因此在实现中，我们需要回溯目标中方程的选择，以确保列举所有解。这与无条件情况相反，在无条件情况下，关于最左边的选择函数的完备性是已知的。在文[2]中，我们证明了LCNC关于上述条件重写系统的最左侧选择策略的完备性，从而弥补了这一差距。在与艾琳·杜兰德的一篇联合论文中，我们引入了一个强大的框架来研究按需要计算的呼叫。利用初等树自动机技术和基树换能器，获得了重写系统类的层次结构的简单可判断性证明，这些重写系统的类比使用复杂顺序性概念定义的早期类大得多。在文[3]中，我们研究了新层次中的成员模性。令人惊讶的是，在签名扩展下，层次结构中没有一个类被保留。通过施加各种条件，我们恢复了签名延期下的保全。通过施加一些更多的条件，我们能够将签名扩展结果加强为不相交和构造函数共享组合的模块化。较少

Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in a paper of Zantema is however rather limited. In [1] we introduced a stronger version of equational semantical labelling, parameterized by three choices : (1) the order on the underlying algebra (partial order vs. quasi-order), (2) the relation between the algebra and the rewrite system (model vs. quasi-model), and (3) the labelling of the function symbols appearing in the equations (forbidden vs. allowed). We presented soundness and completeness results for the various instantiations, analyzed the relationships between them, and presented two applications of our equational semantic labelling technique.We also continued our investigations into the completeness of lazy narrowing calculi. In an earlier paper we proved that the lazy conditional narrowing calculus LCNC is complete with respect to normalizable solutions for the clas … More s of confluent but not necessarily terminating conditional rewrite systems without so-called extra variables in the conditional parts of the rewrite rules. Unfortunately, the proof does not provide any useful complete selection function, hence in implementations we need to backtrack over the choice of equations in goals in order to guarantee that all solutions are enumerated. This is in contrast to the unconditional case where completeness with respect to the leftmost selection function is known. In [2] we closed the gap by proving the completeness of LCNC with respect to the leftmost selection strategy for the above-mentioned class of conditional rewrite systems.In a joint paper with Irene Durand we introduced a powerful framework for the study of call by need computations. Using elementary tree automata techniques and ground tree transducers simple decidability proofs were obtained for a hierarchy of classes of rewrite systems that are much larger than earlier classes defined using the complicated sequentiality concept. In [3] we studied the modularity of membership in the new hierarchy. Surprisingly, it turned out that none of the classes in the hierarchy is preserved under signature extension. By imposing various conditions we recovered the preservation under signature extension. By imposing some more conditions we were able to strengthen the signature extension results to modularity for disjoint and constructor-sharing combinations. Less