On-demand Evaluation for Maude

Strategy annotations provide a simple mechanism for introducing some laziness in the evaluation of expressions. As an eager programming language, Maude can take advantage of them and, in fact, they are part of the language. Maude strategy annotations are lists of non-negative integers associated to function symbols which specify the ordering in which the arguments are (eventually) evaluated in function calls. A positive index enables the evaluation of an argument whereas 'zero' means that the function call has to be attempted. The use of negative indices has been proposed to express evaluation on-demand, where the demand is an attempt to match an argument term with the left-hand side of a rewrite rule. In this paper we show how to furnish Maude with the ability of dealing with on-demand strategy annotations.