Termination of on-demand rewriting and termination of OBJ programs

Termination of on-demand rewriting and termination of OBJ programs
复制标题

终止按需重写和终止OBJ程序

DOI：
10.1145/773184.773194
复制
发表时间：
2001
期刊：
ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming
影响因子：
--
通讯作者：
Salvador Lucas
Salvador Lucas
中科院分区：
--
文献类型：
--
作者：
Salvador Lucas

文献摘要

被引文献

相似文献

OBJ，Cafeobj和Maude等声明语言使用句法注释引入旨在提高终止或计算效率的替代限制。不幸的是，缺乏证明这种好处的正式技术。我们表明，上下文敏感的重写和按需重写提供了一个合适的框架来解决此问题。我们提供分析按需重写的终止的方法，并将其应用于分析OBJ，Cafeobj和Maude计划的终止。
Declarative languages such as OBJ, CafeOBJ, and Maude use syntactic annotations to introduce replacement restrictions aimed at improving termination or efficiency of computations. Unfortunately, there is a lack of formal techniques for proving such benefits. We show that context-sensitive rewriting and on-demand rewriting provide a suitable framework to address this problem. We provide methods to analyze termination of on-demand rewriting and apply them to analyze termination of OBJ, CafeOBJ, and Maude programs.