On-Demand Strategy Annotations Revisited:
An Improved On-Demand Evaluation Strategy
Author
María Alpuente, Santiago Escobar, Bernhard Gramlich and Salvador Lucas
Abstract
In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given
strategy annotations that specify (the order in) which subterms are evaluated.
Syntactically, strategy annotations 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 prescribes the evaluation of an argument whereas
a negative index means "evaluation on-demand". These on-demand indices have
been proposed to support laziness in OBJ-like languages. While strategy
annotations containing only natural numbers have been implemented and
investigated to some extent (regarding, e.g., termination, confluence, and
completeness), fully general annotations (including positive and negative indices)
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 by keeping an accurate track of annotations
along the evaluation sequences. We formalize this solution
as a suitable extension of the evaluation strategy of OBJ-like languages
(which only consider annotations given as natural numbers) to on-demand strategy
annotations. Our on-demand evaluation strategy (ODE)
overcomes the drawbacks of previous proposals and also has better computational
properties. For instance, we show how to use this strategy for computing
(head-)normal forms. We also introduce a transformation which allows us to
prove termination of the new evaluation strategy by using standard rewriting
techniques. Finally, we present two interpreters of the new strategy together
with some encouraging experiments which demonstrate the usefulness of our
approach.
Keywords
Declarative programming, demandedness, lazy evaluation,
OBJ, on-demand strategy annotations.