权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Reduction Strategy

减排策略

基本信息

批准号：
11680338
负责人：
MIDDELDORP Aart
金额：
$ 2.18万
依托单位：
University of Tsukuba
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1999
资助国家：
日本
起止时间：
1999 至 2000
项目状态：
已结题

项目摘要

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

语义标注是证明词项重写系统可终止性的有力工具。然而，Zantema的一份文件中所描述的方程项重写的扩展的有用性是相当有限的。在[1]中，我们引入了一个更强版本的方程语义标记，由三个选择参数化：（1）底层代数的顺序（偏序与准序），（2）代数与重写系统之间的关系（模型与准模型），以及（3）出现在方程中的函数符号的标记（禁止与允许）。我们给出了各种实例的可靠性和完备性结果，分析了它们之间的关系，并给出了我们的等式语义标记技术的两个应用。我们还继续研究了惰性窄化演算的完备性。在之前的一篇论文中，我们证明了懒惰条件收缩演算LCNC对于类的可规范化解是完备的。 ...更多信息在重写规则的条件部分中没有所谓的额外变量的汇合但不一定终止的条件重写系统。不幸的是，证明没有提供任何有用的完整选择函数，因此在实现中，我们需要回溯目标中的方程的选择，以确保所有解都被枚举。这是在对比的无条件的情况下，完整性相对于最左边的选择函数是已知的。在[2]中，我们通过证明LCNC关于上述一类条件重写系统的最左选择策略的完备性来弥补差距。在与Irene Durand的联合论文中，我们介绍了一个强大的框架来研究按需调用计算。使用基本树自动机技术和地面树传感器简单的可判定性证明的重写系统，比以前的类定义的复杂的顺序性概念大得多的层次结构。在[3]中我们研究了新层次中成员的模块性。令人惊讶的是，结果发现层次结构中没有一个类在签名扩展下被保留。通过施加各种条件，我们恢复了签名扩展下的保存。通过施加更多的条件，我们能够将签名扩展结果加强到不相交和构造器共享组合的模块化。少