Reduction Strategy

语义标记是证明术语重写系统终止的有力工具。然而，在Zantema的一篇论文中描述的对方程项重写的扩展的有用性是相当有限的。在[1]中，我们引入了一个更强版本的方程语义标记，通过三个选择参数化：(1)基础代数上的顺序（偏序与准序），(2)代数与重写系统之间的关系（模型与准模型），以及(3)出现在方程中的函数符号的标记（禁止与允许）。我们给出了各种实例的健全性和完备性结果，分析了它们之间的关系，并给出了我们的等价语义标记技术的两种应用。我们也继续研究懒惰性狭窄结石的完全性。在之前的一篇论文中，我们证明了惰性条件缩窄演算LCNC是完备的，它是关于在重写规则的条件部分没有所谓额外变量的合流但不一定终止的条件重写系统的类的可规范化解的。不幸的是，这个证明并没有提供任何有用的完整的选择函数，因此在实现中我们需要回溯目标中方程的选择，以保证枚举所有的解。这与无条件情况相反，在无条件情况下，最左边的选择函数的完备性是已知的。在[2]中，我们通过证明LCNC关于上述条件重写系统的最左侧选择策略的完备性来缩小差距。在与Irene Durand的一篇联合论文中，我们介绍了一个强大的框架来研究需求计算调用。利用初等树自动机技术和地面树换能器，得到了重写系统类的简单可决性证明，这些重写系统的类比以前使用复杂顺序概念定义的类大得多。在b[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