Improving On-Demand Strategy Annotations
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 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 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. Then, we propose a solution
to these problems which is based on a suitable extension of the
E-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.