The E-strategy

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₁, ..., t_n) that each have the function symbol f at the head of them are evaluated. The order is prescribed with a list of integers ranging from zero through the arity (the number of the arguments) of the function symbol. A term  f(t₁, ..., t_n) is evaluated according to the local strategy of its top function symbol f. If the top of the local strategy is a positive integer k, the kth argument t_k is first evaluated, the result t'_k next replaces the argument, and then the altered term f(..., t'_k, ...) is evaluated according to the remainder of the local strategy. If the top of the local strategy is zero, the term is tried to be matched with the left sides of rewrite rules: if there exists a rewrite rule whose left side matches with the term (i.e. the term is a redex), the term is replaced by the corresponding instance of the right side (i.e. the contractum of the term), and then the new term is evaluated according to the local strategy of its top function symbol; otherwise the term is continuously evaluated according to the remainder of the local strategy. Such rewriting is going on until a local strategy becomes empty. We here show an example that needs lazy evaluation.

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(1, inf(1)) $(D"4(B  -->  nth(1,cons(1, inf(1 + 1)))
                                                        -->  nth(sd(1,1), inf(1 + 1))
                                                        -->  nth(0, inf(1 + 1))
                                                        -->  nth(0, inf(2))
                                                        -->  nth(0, cons(2, inf(2 + 1)))
                                                        -->   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 PIth argument is first evaluated and then the altered term is continuously evaluated according to the remainder LS of the local strategy.