In this section a hint about giving local strategies to operators (or
function symbols) is presented. The on-demand E-strategy gives us two ways
of postponing evaluating some terms. If we want to postpone evaluating
the
*k*th argument of a term *f*(*t*_{1}, ..., *t _{n}*),
the operator

It is possible to avoid wasteful evaluation by giving local strategies
excluding some positive integers to operators (i.e. functions). A typical
example of avoiding wasteful evaluation is the conditional operator *if_then_else_fi*.

*Example 7 (Conditional operator if_then_else_fi).*
** op** *if_then_else_fi*
: *Bool S S* -> *S* { **strat:** (1 0) }
** eq** *if true then
X:S else Y:S fi* = *X* .
** eq** *if false then
X:S else Y:S fi* = *Y* .

A term with *if_then_else_fi* as its top operation such as ``*if
cond then comp1 else comp2 fi*'' is replaced by the second argument
*comp1*
or the third argument *comp2* depending on the result (i.e. *true*
or *false*) of evaluating the first argument *cond*. If the result
of evaluating the first argument is *true* (or
*false*), the
second (or third) argument replaces the whole term, and the third (or second)
argument is just discarded and does not cause wasteful evaluation.

It is possible to deal with infinite data structures by giving local
strategies including negative integers to operators (data constructors).
For example, infinite lists can be dealt with by giving the local strategy
(1 -2 0) to the list constructor _ _ as follows: _ _ : *Nat* *ooList***->**
*ooList* { **strat:** (1 -2 0) } (* ooList* stands for infinite
lists and lists of natural numbers are considered for brevity). The result
of evaluating some term denoting an infinite list is in head normal form,
but the evaluation does not lead to infinite rewriting. Suppose that *inf*
is declared as *inf* : *Nat***->** *ooList* and *inf*(*X*:*
Nat*) = *X* *inf*(*X* + 1), the result of evaluating
*inf*(0) is ``0 *inf*(1).'' But the result of evaluating even
some term denoting a finite list might be in head normal form. For example,
the result of evaluating ``*tp*(1 2
*nil*)
*tl*(1 2 3 *nil*)''
is ``1 *tl*(1 2 3 *nil*)'' that is in head normal form, but not
in normal form. The result of evaluating some term denoting a finite list
should be in normal form. Since *CafeOBJ* supports order-sorted rewriting,
infinite lists are allowed to coexist with finite lists well by having
the sort *ooList* have a subsort
*List* for finite lists and
declaring the constructor for finite lists. The constructor for finite
lists is given the eager local strategy (1 2 0).

*Example 8 (Coexistence of infinite lists with finite lists).*

[ *List* < *ooList*
]
** op** *nil* : ->
*List*
** op** _ _ : *Nat List*
-> *List* { **strat:** (1 2 0) }
** op** _ _ : *Nat ooList*
-> *ooList* { **strat:** (1 -2 0) }
** op** *tp* : *ooList*
-> *Nat*
** op** *tl* : *List*
-> *List*
** op** *tl* : *ooList*
-> *ooList*

The result of evaluating ``*tp*(1 2 *nil*) *tl*(*inf*(0))''
is ``1 *tl*(*inf*(0)),'' while the result of evaluating ``*
tp*(1 2 *nil*) *tl*(1 2 3 *nil*)'' is ``1 2 3 *nil*.''
Since the top operator _ _ of the former term is the constructor for infinite
lists because the second term *tl*(*inf*(0)) denotes an infinite
list, the second argument is not evaluated because of the local strategy
(1 -2 0) of the operator. The top operator _ _ of the latter term is the
constructor for finite lists because the second argument *tl*(1 2
3 *nil*) is finite, and the both of the first and second arguments
are evaluated.