**Next:**Example
Using the **Up:**The
On-demand E-strategy**Previous:**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 *k*th argument *t*_{k} of a term
*f*(*t*_{1}, ..., *t*_{n}) 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.

**Next:**Example
Using the **Up:**The
On-demand E-strategy**Previous:**The
On-demand E-strategy

*Kazuhiro Ogata*

*Mon Nov 29 13:47:22 JST 1999*