Maude Manual -- 2.1.3 Operator Evaluation Strategies

Go backward to 2.1.2 A Set Hierarchy Example
Go up to 2.1 Functional Modules

2.1.3 Operator Evaluation Strategies

If a collection of equations is Church-Rosser and terminating, given an expression, no matter how the equations are used from left to right as simplification rules we will always reach the same final result. However, even though the final result may be the same, some orders of evaluation can be considerably more efficient than others. It may therefore be useful to have some way of controling the way in which equations are applied by means of strategies.

In general, given an expression f(t₁,...,t_n) we can try to evaluate it to its reduced form in different ways, such as:

first obtaining the reduced form of all the t_is and then applying equations for f at the top of the term, what is called a bottom-up, or eager strategy;
evaluating only some of the arguments, and then trying to evaluate at the top with equations for f; for example, an if_then_else_fi operator will typically be evaluated by evaluating first the first argument, and then the if_then_else_fi operator at the top;
trying to evaluate the top of the term first, and then, if this fails, either not evaluating the subterms at all, or trying to evaluate only some of them, that is, some kind of lazy evaluation strategy.

Typically, a functional language is either eager, or lazy with some strictness analysis added for efficiency, and the user has to live with whatever the language provides. Maude adopts OBJ3's [27] flexible method of user-specified evaluation strategies on an operator-by-operator basis, adding some improvements to the OBJ3 approach to ensure a correct implementation [21]. For an n-ary operator f such strategies can be specified as a list of numbers from 0 to n ending with 0. For example, the default eager strategy given in Maude to all operators, unless another strategy is explicitly declared by the user, is (1 ... n 0), and the one given to the if_then_else_fi is (1 0 2 3 0), whereas a lazy "cons" list constructor may have strategy (0).

The syntax to declare an operator f with strategy (i₁ ... i_k 0) is

   op f : S1 ... Sn -> S [strat (i1 ... ik 0)] .

Of course, if some of the argument positions are never mentioned in some of the operator strategies, the notion of reduced expression becomes now relative to the given strategies and may not coincide with the standard notion. This may be just what we want, since we may be able to achieve termination to a reduced expression relative to some strategies in cases when the equations may be nonterminating in the standard sense. For example, the factorial equation

    fact(N) = if N == 0 then 1 else N * fact(N - 1) fi .

is nonterminating in the standard sense, but it is terminating up to the above strategy for if_then_else_fi. More generally, strategies may allow us to compute with infinite data structures which are evaluated on demand, such as the following slight reformulation of the Sieve of Eratosthenes example--which finds all prime numbers using lazy lists--in Appendix C.5 of [27].

  fmod SIEVE is
    protecting MACHINE-INT .
    sort IntList .
    subsort MachineInt < IntList .
    op nil : -> IntList .
    op _._ : IntList IntList -> IntList 
        [assoc id: nil strat (0)] .
    op force : IntList IntList -> IntList [strat (1 2 0)] .
    op show_upto_ : IntList MachineInt -> IntList .
    op filter_with_ : IntList MachineInt -> IntList .
    op ints-from_ : MachineInt -> IntList .
    op sieve_ : IntList -> IntList .
    op primes : -> IntList .

    var P I E : MachineInt .
    var S L : IntList .

    eq force(L, S) = L . S .
    eq show nil upto I = nil .
    eq show E . S upto I 
      = if I == 0 then nil
        else force(E, show S upto (I - 1)) 
        fi . 
    eq filter nil with P = nil .
    eq filter I . S with P 
      = if (I % P) == 0 then filter S with P
        else I . filter S with P 
        fi .
    eq ints-from I = I . ints-from (I + 1) .
    eq sieve nil = nil .
    eq sieve (I . S) = I . sieve (filter S with I) .
    eq primes = sieve ints-from 2 .
  endfm

  Maude> reduce show primes upto 10 .
  result IntList: 2 . 3 . 5 . 7 . 11 . 13 . 17 . 19 . 23 . 29

The paper [21] documents in much more detail the operational semantics and the implementation techniques for Maude's operator evaluation strategies. In particular, it analyzes carefully a number of subtle anomalies in the OBJ3 implementation that are avoided in Maude, and uses a Maude specification of a rewrite theory (a system module, see Section 2.2) to formally specify the term graph rewriting done by the implementation to execute such strategies.

Of course, operator evaluation strategies, while quite useful, are by design restricted in their scope of applicability to functional modules⁹. As we shall see in Section 2.2, system modules, specifying rewrite theories--that are not functional, and need not be Church-Rosser or terminating--require much more general notions of strategy. Such general strategies are provided by Maude using reflection by means of internal strategy languages, in which strategies are defined by rewrite rules at the metalevel (see Section 2.6).