On-Demand Strategy Annotations Revisited
Authors
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 ``evaluate on-demand''. While
strategy annotations containing only natural numbers have been
implemented and investigated to some extent (regarding, e.g.,
termination and completeness), fully general annotations (also called
on-demand strategy 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, such as
undecidability of the reduction relation or inadequacy of the model.
Then, we propose a solution to these problems by keeping an accurate
track of annotations along evaluation sequences. This solution is
defined as a suitable extension of the E-evaluation strategy of
OBJ-like languages (which only considers annotations given as natural
numbers) to on-demand strategy annotations. Our strategy overcomes the
drawbacks of these previous proposals and also exhibits better
computational properties. For instance, 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. Finally, we present an interpreter of the new strategy
together with some encouraging experiments.
Keywords
Declarative programming, demandedness, lazy evaluation,
OBJ, on-demand strategy annotations