Strategy annotations are used in eager programming languages (e.g., OBJ2, OBJ3, CafeOBJ, and Maude) for improving efficiency and/or reducing the risk of nontermination. 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".

Consider the following OBJ program (borrowed from [NO01]):

obj Ex1 is
  sorts Nat LNat .
  op 0    : -> Nat .
  op s    : Nat -> Nat [strat (1)] .
  op nil  : -> LNat .
  op cons : Nat LNat -> LNat [strat (1)] .
  op from : Nat -> LNat  [strat (1 0)] .
  op 2nd  : LNat -> Nat [strat (1 0)] .
  vars X Y : Nat . var Ys : LNat .
  eq 2nd(cons(X,cons(Y,Ys))) = Y .
  eq from(X) = cons(X,from(s(X))) .
endo

2nd(from(0)) -> 2nd(cons(0,from(s(0))))

The evaluation stops at this point since reductions on the second argument of cons are disallowed due to the syntactic annotation. This is consistent with the evaluation performed by a typical OBJ interpreter (we use the version 2.0 of the SRI's OBJ3 interpreter:

==========================================
obj Ex1
==========================================
reduce in Ex1 : 2nd(from(0))
rewrites: 1
result Nat: 2nd(cons(0,from(s(0))))

Note that we cannot apply the rule defining 2nd because the subterm from(s(0)) should be further reduced. Thus, a further step is demanded (by the rule of 2nd) in order to obtain the desired outcome:

2nd(cons(0,\ul{from(s(0))})) -> 2nd(cons(0,cons(s(0),from(s(s(0))))))

2nd(cons(0,cons(s(0),from(s(s(0))))) -> s(0)

In [OF00,NO01] negative indices are proposed to indicate those arguments that should be evaluated only on-demand, where the demand is an attempt to match an argument term with the left-hand side of a rewrite rule. CafeOBJ is able to deal with negative annotations; for instance, the CafeOBJ interpreter is able to compute value s(0) of expression 2nd(from(0)) before. In [AEGL02], we discussed a number of problems of this approach and proposed a solution to these problems which is based on a suitable extension of the evaluation strategy of OBJ-like languages (that only considers annotations given as natural numbers) to cope with on-demand strategy annotations.

Consider the following OBJ program:

obj Ex2 is
  sorts Nat LNat .
  op 0    : -> Nat .
  op s    : Nat -> Nat        [strat (1)] .
  op nil  : -> LNat .
  op cons : Nat LNat -> LNat  [strat (1)] .
  op from : Nat -> LNat       [strat (1 0)] .
  op length : LNat -> Nat     [strat (0)] .
  op length' : LNat -> Nat    [strat (-1 0)] .
  var X : Nat . var Z : LNat .
  eq from(X) = cons(X,from(s(X))) .
  eq length(nil) = 0 .
  eq length(cons(X,Z)) = s(length'(Z)) .
  eq length'(Z) = length(Z) .
endo

EX2> red length'(from(0)) .
-- reduce in EX2 : length'(from(0))
Error: Stack overflow (signal 1000)

This is because the negative annotations are implemented as marks on terms which can (unproperly) initiate reductions later on; see [AEGL02]. Our interpreter is able to produce the expected result:

EX2> red length'(from(0)) .
Normal form: length(from(0))
{ 0.0000 sec., 1 rewrites, 4 on-demand steps. }