[Back]

M. Alpuente, B. Gramlich, A. Villanueva:
"Timed Concurrent Constraint Programming with Instantaneous Computations";
in: "Proc. 6th Spanish Conference on Programming and Computer Languages (PROLE 2006)", P. Lucio (ed.); The University of the Basque Country, 2006, 221 - 230.

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.