Proving termination of context-sensitive rewriting by transformation
Proving termination of context-sensitive rewriting by transformation
复制标题
通过转换证明上下文相关重写的终止
DOI：
10.1016/j.ic.2006.07.001
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Salvador Lucas
中科院分区：
文献类型：
--
作者：
Salvador Lucas
上下文相关重写(CSR)是一种重写限制，禁止对函数的选定参数进行删减。有了CSR，我们可以通过修剪(全部)无限重写序列来实现非终止术语重写系统的终止行为。最近，在术语重写和编程语言领域的一些应用中，证明CSR的终止性已经被认为是一个有趣的问题。已经发展了几种方法来证明CSR的终止。具体地说，已经描述了允许将该问题作为标准终止问题来处理的许多转换。本文的主要目的是为了更好地理解和实际使用转换来证明企业社会责任的终止。我们给出了在两个受限(但相关)环境中使用变换的新的完备性结果：(A)规范CSR终止的证明和(B)结合使用变换和简化排序来终止CSR的证明。我们还对这些变换进行了实验评估，从实践的角度对理论分析进行了补充。这导致了变换的新层次，这对于在实现用于证明CSR终止的工具时指导它们的实际使用是有用的。
Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite sequences. Proving termination of CSR has been recently recognized as an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. Specifically, a number of transformations that permit treating this problem as a standard termination problem have been described. The main goal of this paper is to contribute to a better comprehension and practical use of transformations for proving termination of CSR. We provide new completeness results regarding the use of the transformations in two restricted (but relevant) settings: (a) proofs of termination of canonical CSR and (b) proofs of termination of CSR by using transformations together with simplification orderings. We have also made an experimental evaluation of the transformations, which complements the theoretical analysis from a practical point of view. This leads to new hierarchies of the transformations which are useful to guide their practical use when implementing tools for proving termination of CSR.