Improving On-Demand Strategy Annotations
Improving On-Demand Strategy Annotations
复制标题
改进按需策略注释
DOI：
10.1007/3-540-36078-6_1
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Salvador Lucas
中科院分区：
文献类型：
--
作者：
M. Alpuente;Santiago Escobar;B. Gramlich;Salvador Lucas
在函数式语言(如OBJ*、CafeOBJ和Maude)中，符号被赋予策略注释，指定计算哪些子项(顺序)。在语法上，它们要么以自然数列表的形式给出，要么以与函数符号相关联的整数列表的形式给出，函数符号的(绝对值)指的是相应符号的自变量。正指数允许对论点进行评估，而负指数意味着“按需评估”。虽然只包含自然数的策略注释已经实现并收到了一些最近的研究努力(例如，关于终止性和完备性)，但令人失望的是，到目前为止，为了支持类OBJ语言中的懒惰而提出的完全通用的注释(也称为按需策略注释)还没有得到充分的探索。在本文中，我们首先指出了当前处理按需策略注释的建议存在的一些问题。然后，将类OBJ语言的电子求值策略(只考虑以自然数形式给出的注解)适当地扩展到按需策略注解，提出了一个解决这些问题的方法。我们的策略结合了对需求的更好的处理，并且还表现出良好的计算特性；特别是，我们展示了如何使用它来计算(头)范式。我们还介绍了一种利用标准技术证明新评估策略的终止性的转换。
In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations which specify (the order in) which subterms are evaluated. Syntactically, they are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index enables the evaluation of an argument whereas a negative index means “evaluate on-demand”. While strategy annotations containing only natural numbers have been implemented and received some recent investigation endeavor (regarding, e.g., termination and completeness), fully general annotations (also calledon-demandstrategy annotations), which have been proposed to support laziness in OBJ-like languages, are disappointingly under-explored to date. In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations. Then, we propose a solution to these problems which is based on a suitable extension of theE-evaluation strategy of OBJ-like languages (that only considers annotations given as natural numbers) to on-demand strategy annotations. Our strategy incorporates a better treatment of demandness and also exhibits good computational properties; in particular, we show how to use it for computing (head-)normal forms. We also introduce a transformation for proving termination of the new evaluation strategy by using standard techniques.