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.
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