Reduction Strategy

点击翻译按钮获取中文摘要

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