by María Alpuente, Santiago Escobar and Salvador Lucas.
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]):
The OBJ evaluation of the term 2nd(from(0)) is given by the sequence: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:
Now, we do not need to reduce the second argument of the inner occurrence of cons anymore, since reducing at the root position yields the final value: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:
The expression length'(from(0)) is rewritten (in one step) to length(from(0)). No evaluation is demanded on the argument of length' for enabling this step and no further evaluation on length(from(0)) should be performed due to the local strategy (0) of length. However, the annotation (-1 0) of function length' is treated in such a way that the on-demand evaluation of the expression length'(from(0)) yields an infinite sequence whether we use the operational model in [OF00] or whether we use [NO01]; we use the CafeOBJ interpreter: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:
Click here to see our experiments.EX2> red length'(from(0)) . Normal form: length(from(0)) { 0.0000 sec., 1 rewrites, 4 on-demand steps. }
Last version of Feb 23 2004 with minor changes in syntax of OBJ programs and the addition of two program
transformations ([WRLA02] for ensuring correctness and completeness of OBJ programs
with positive annotations and [RULE03A] for transforming an OBJ program with negative annotations
into an OBJ program with only positive annotations).
The prototype interpreter only implements a subset of the OBJ program syntax
(described in the file "grammar.txt" included in the distribution).
No prelude information is included (e.g. conditional function "if", I/O functions)
and only one module can be considered at the same time. The implementation includes options to
evaluate an expression, evaluate all possibilities in a breath-first search, trace an evaluation,
or normalize an expression.
[AEGL02] M. Alpuente, S. Escobar, B. Gramlich, and S. Lucas. Improving on-demand strategy annotations. In Matthias Baaz and Andrei Voronkov, editors, Proc. 9th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'02), Lecture Notes in Computer Science, Tbilisi, Georgia, October 2002. Springer-Verlag.
[WRLA02] M. Alpuente, S. Escobar, S. Lucas. Correct and Complete (Positive) Strategy Annotations for OBJ. 4th Int'l Workshop on Rewriting Logic and its Applications (WRLA 2002), Pisa (Italy). Electronic Notes on Theoretical Computer Science, Vol. 71. To appear 2003.
[RULE03A] M. Alpuente, S. Escobar, S. Lucas. On-Demand evaluation by program transformation. In Proc. of the 4th International Workshop on Rule-Based Programming (RULE'03). Electronic Notes on Theoretical Computer Science. To appear 2003.
[RULE03B] M. Alpuente, S. Escobar, and S. Lucas. OnDemandOBJ: A Laboratory for Strategy Annotations. In Proc. of the 4th International Workshop on Rule-Based Programming (RULE'03). Electronic Notes on Theoretical Computer Science. To appear 2003.
[OF00] K. Ogata and K. Futatsugi. Operational semantics of rewriting with the on-demand evaluation strategy. In Proc. of 2000 International Symposium on Applied Computing, SAC'00, pages 756-763. ACM Press, 2000.
[NO01] M. Nakamura and K. Ogata. The evaluation strategy for head normal form with and without on-demand flags. In Proc. of 3rd International Workshop on Rewriting Logic and its Applications, WRLA'00, volume 36. Electronic Notes in Theoretical Computer Science, Elsevier Sciences, 2001.
ELP | GPLIS | DSIC | UPV |
Last update Feb 23 2004 # sescobar@dsic.upv.es