nextupprevious
Next:Example Using the Up:The On-demand E-strategyPrevious:The On-demand E-strategy

Restriction Imposed by the E-strategy

Although the E-strategy makes it possible to simulate a variant of lazy evaluation, it imposes a restriction on constructing rewrite rules. If non-variable terms are put on lazy positions in the left sides, some terms cannot be rewritten as intended. Suppose that cons is a list constructor and has (1 0) as its local strategy, and tl and 2nd are usual functions, whose rewrite rules are tl(cons(X, L)) --> L and 2nd(cons(X, cons(Y,L))) --> Y, to return the tail and the second element of a list respectively, the term 2nd(cons(a, tl(cons(b, cons(c, nil))))) is not rewritten to c. The term is rewritten as follows. The argument is first evaluated because of the local strategy of 2nd. But no rewrite occurs owing to the local strategy of cons. Although a pattern matcher tries to match the term with the left sides of rewrite rules succeedingly, there is no rewrite rule whose left side can match with the term because the second one of the term's argument is tl(cons(b, cons(c, nil))). Therefore c is not got as a result.

CafeOBJ adopts the on-demand E-strategy that is an extended version of the E-strategy in order to remove the restriction of the E-strategy. The on-demand E-strategy allows us to declare local strategies with negative integers as well as zero and positive integers. A negative integer -k in a local strategy given to a function symbol f means that each subterm in the kth argument tk of a term f(t1, ..., tn) is marked with an on-demand flag. While a term is tried to be matched with the left sides of rewrite rules, some of the subterms marked with on-demand flags may be rewritten.
 


nextupprevious
Next:Example Using the Up:The On-demand E-strategyPrevious:The On-demand E-strategy


 


Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999