The E-strategy is a reduction strategy initiated by *OBJ2*[4].
It not only simulates a variant of lazy evaluation such as the functional
strategy[10], but also is flexible because
it can control the order in which terms are rewritten by giving a local
strategy to each operator (or function symbol). A local strategy given
to a function symbol *f* indicates the order in which terms such as
*f*(*t*_{1},
..., *t _{n}*) that each have the function symbol

*Example 2 (A function nth to take the nth element from an infinite
list)*
** mod!** *TEST1* {
** pr**(*NAT*)

[*S*]
** op** *cons* :
*NatS*
-> *S* { **strat:** (1 0) }
** op** *inf* : *Nat*
-> *S*
** op** *nth* : *NatS*
-> *Nat*
** eq** *inf*(*X*:*Nat*)
= *cons*(*X*, *inf*(*X*+1)) .
** eq** *nth*(0,
*cons*(*X*:*Nat*,
*L*:*S*))
= *X* .
** eq** *nth*(*X*:*NzNat*,
*cons*(*Y*:*Nat*,
*L*:*S*))
= *nth*(*sd*(*X*, 1), *L*) .

}

The operator *cons* has the local strategy (1 0), which means that
a term with *cons* as its top function symbol would be replaced by
another term, which is then evaluated, after evaluating the first argument.
The second argument is not evaluated unless some rewrite frees it from
domination of the operator *cons*. Although the other operators are
given no explicit local strategies, a default strategy such as (1 2 ...
0) is implicitly given to each of them.

Let us evaluate the term *nth*(1,* inf*(1)) w.r.t. *TEST1*.
It is rewritten as follows:
` ` *
nth(*

-->

--> 2.

Subterms to be rewritten are underlined.

We present an excerpt from the operational semantics of rewriting with
the E-strategy in *CafeOBJ*.

**Semantics 1 (Excerpt from the operational semantics of rewriting
with the E-strategy)**
** ceq** *eval*(*T*,
*TRS*)
= *T* **if** *eval?*(*T*) .
** ceq** *eval*(*T*,
*TRS*)
= *reduce*(*T*, *strat*(*T*, *sig*(*TRS*)),
*TRS*)
**if** *not* *eval?*(*T*) .
** eq** *reduce*(*T*,
*nil*,
*TRS*) = *setEFlag*(*T*) .
** eq** *reduce*(*T*,
(0 *LS*), *TRS*) = *reduce2*(*match*(*rules*(*TRS*),
*T*,
*TRS*), *LS*, *TRS*) .
** eq** *reduce*(*T*,
(*PI* *LS*), *TRS*) = *reduce*(*evalArg*(*T*,
*PI*,
*TRS*), *LS*, *TRS*) .
** eq** *reduce2*(`<`*true*
*T* `>`, *LS*, *TRS*) = *eval*(*T*,
*TRS*)
.
** eq** *reduce2*(`<`*false*
*T* `>`, *LS*, *TRS*) = *reduce*(*T*,
*LS*,
*TRS*) .

The operator *eval* is a reducer that takes a term **T** to
be reduced and a TRS *TRS* (i.e. a pair of a signature and a set of
rewrite rules), and returns the result
of evaluating the term. *eval* returns **T** immediately if **T**
has been already evaluated, or otherwise it evaluates **T** according
to the local strategy of the top function symbol of **T** by calling
*reduce*.
The operators *sig* and *strat* return the signature (i.e. a
pair of sets of function symbols and variables) of *TRS* and the local
strategy of the top function symbol of **T**. The operator
*reduce*
takes a term **T**, the strategy list of the top function symbol of
**T**
and a TRS *TRS*, and evaluates **T** according to the local strategy
w.r.t. *TRS*. If the local strategy is or becomes empty (i.e. *nil*),
*reduce*
returns **T** after marking
**T** with a flag (called an evaluated
flag) meaning that **T** has been evaluated. If the top of the local
strategy is zero, the pattern matcher
*match* tries to match **T**
with the left sides of the rewrite rules of
*TRS*: if there exists
a rewrite rule whose left side matches with
**T**, *match* returns
the pair of *true* and the corresponding instance of the right side
(i.e. the contractum of **T**) and *eval* evaluates the new term
(i.e. the instance); otherwise *match* returns the pair of *false*
and the term passed to *match* as the second argument, and *reduce*
continues to evaluate the term according to the remainder *LS* of
the local strategy. If the top of the local strategy is a positive integer
*PI*,
the *PI*th argument is first evaluated and then the altered term is
continuously evaluated according to the remainder *LS* of the local
strategy.