Termination of Context-Sensitive Rewriting
Termination of Context-Sensitive Rewriting
复制标题
上下文相关重写的终止
DOI：
10.1007/3-540-62950-5_69
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
H. Zantema
中科院分区：
文献类型：
--
作者：
H. Zantema
上下文敏感的项重写是指在某些函数符号的固定参数内不允许进行约简的一种项重写。我们介绍了两种证明上下文敏感重写终止的新技术。第一个是在一个有充分根据的顺序中对解释技术的修改，第二个是通过转换隐含的，在这种转换中，原始系统的上下文敏感终止可以从转换后的系统的终止中得出结论。与证明普通终止的纯自动技术相结合，后一种技术也是纯自动的。
Context-sensitive term rewriting is a kind of term rewriting in which reduction is not allowed inside some fixed arguments of some function symbols. We introduce two new techniques for proving termination of context-sensitive rewriting. The first one is a modification of the technique of interpretation in a well-founded order, the second one is implied by a transformation in which context-sensitive termination of the original system can be concluded from termination of the transformed one. In combination with purely automatic techniques for proving ordinary termination, the latter technique is purely automatic too.