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. More generally, we may be able to achieve the termination property provided we follow a certain order of evaluation, but may lose termination when any evaluation order is allowed. 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_{1},\ldots,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_{i}$ and then applying equations for $f$ at the top of the term; this 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 [44] 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 [37].

For an $n$-ary operator $f$ an evaluation strategy is specified as a list of numbers from 0 to $n$ ending with 0. The nonzero numbers denote argument positions, and a 0 indicates evaluation at the top of the given function symbol. The strategy then specifies what argument positions must be simplified (in the order indicated by the list) before attempting simplification at the top with the equations for the top function symbol. In functional programming terminology, the argument positions to be evaluated are usually called strict argument positions, so we can view an evaluation strategy as a flexible, user-definable way of specifying strictness requirements on argument positions. In the simplest case, a strategy consists of a list of nonzero numbers followed by a 0, so that some arguments are treated strictly and then the function symbol's equations are applied. For example, in Maude, if no strategy is specified, all argument positions are assumed strict, so that for $f$ with $n$ argument positions its default strategy is $(1 2 ... n 0)$; this is the ``eager evaluation'' case. The opposite extreme is a form of lazy evaluation such as the lazy append operator in the SIEVE example below. This operator has strategy $(0)$, thus only equations at the top are tried during evaluation.

The syntax to declare an $n$-ary operator with strategy $(i_{1} \; \ldots \; i_{k} \; 0)$, where $i_j \in \{0,\ldots,n\}$ for $j=1,\ldots,k$, is

  op $\langle$OpName$\rangle$ : $\langle$Sort-1$\rangle$ ... $\langle$Sort-n$\rangle$ -> $\langle$Sort$\rangle$ [strat (i1 ... ik 0)] .

As a simple example consider the operators _and-then_ and _or-else_ in the module EXT-BOOL, that can be found in the file prelude.maude (see Section 7.1).

  fmod EXT-BOOL is
    protecting BOOL .
    op _and-then_ : Bool Bool -> Bool
       [strat (1 0) gather (e E) prec 55] .
    op _or-else_ : Bool Bool -> Bool
       [strat (1 0) gather (e E) prec 59] .
    var B : [Bool] .
    eq true and-then B = B .
    eq false and-then B = false .
    eq true or-else B = true .
    eq false or-else B = B .
  endfm

These operators are computationally more efficient versions of Boolean conjunction and disjunction that avoid evaluating the second of the two Boolean subterms in their arguments when the result of evaluating the first subterm provides enough information to compute the conjunction or the disjunction. For example, letting B:[Bool] stand for an arbitrary Boolean expression

  Maude> red false and-then B:[Bool] .
  result Bool: false

while if B:[Bool] does not evaluate to true or false, then false and B:[Bool] does not evaluate to false, and if evaluation of B:[Bool] does not terminate then neither will evaluation of false and B:[Bool].

If some of the argument positions are never mentioned in some of the operator strategies, the notion of canonical form becomes now relative to the given strategies and may not coincide with the standard notion. Let us consider as a simple example the following two functional modules, which we have displayed side-by-side to emphasize their only difference, namely, the evaluation strategy associated to the operator g.

  fmod STRAT-EX1 is             fmod STRAT-EX2 is
    sort S .                      sort S .
    ops a b : -> S .              ops a b : -> S .
    op g : S -> S .               op g : S -> S [strat(0)] .
    eq a = b .                    eq a = b .
  endfm                         endfm

The canonical form of the term g(a) in STRAT-EX1 is g(b), but in STRAT-EX2 it is g(a) itself, because the equation cannot be applied inside the term due to the lazy strategy strat(0) of the operator g.

This may be just what we want, since we may be able to achieve termination to a canonical form relative to some strategies in cases when the equations may be nonterminating in the standard sense. More generally, operator strategies may allow us to compute with infinite data structures which are evaluated on demand, such as the following formulation of the sieve of Eratosthenes, which finds all prime numbers using lazy lists.

The infinite list of primes is obtained from the infinite list of all natural numbers greater than 1 by filtering out all the multiples of numbers previously taken. Thus, first we take 2 and delete all even numbers greater than 2; then we take 3 and delete all the multiples of 3 greater than 3; and so on. The operation nats-from_ generates the infinite list of natural numbers starting in the given argument; the operation filter_with_ is used to delete all the multiples of the number given as second argument in the list provided as first argument; and the operation sieve_ is used to iterate this process with successive numbers.

Of course, since we are working with infinite lists, we cannot obtain as a result an infinite list. Such an infinite structure is only shown partially by means of the operation show_upto_, which shows only a finite prefix of the whole infinite list. Moreover, the generation and filtering processes have to be done in a lazy way. This is accomplished by giving to the list constructor _._ a lazy strategy strat(0) that avoids evaluating inside the term, and using an operation force with an eager strategy strat(1 2 0) to ``force'' the evaluation of elements inside the list. Specifically, in order to apply the first equation, we must evaluate the arguments L and S before reconstructing the list L . S in the righthand side.

NAT denotes the predefined module of natural numbers and arithmetic operations on them (see Section 7.2), which is imported by means of a protecting declaration, explained in Section 6.1.1. Note the use of the symmetric difference operator sd (see Section 7.2) to decrement I in the third equation, and the successor operator s_ to increment I in the sixth equation.

  fmod SIEVE is
    protecting NAT .
    sort NatList .
    subsort Nat < NatList .
    op nil : -> NatList .
    op _._ : NatList NatList -> NatList [assoc id: nil strat (0)] .
    op force : NatList NatList -> NatList [strat (1 2 0)] .
    op show_upto_ : NatList Nat -> NatList .
    op filter_with_ : NatList Nat -> NatList .
    op nats-from_ : Nat -> NatList .
    op sieve_ : NatList -> NatList .
    op primes : -> NatList .

    vars P I E : Nat .
    vars S L : NatList .

    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 sd(I, 1))
        fi .
    eq filter nil with P = nil .
    eq filter I . S with P
      = if (I rem P) == 0
        then filter S with P
        else I . filter S with P
        fi .
    eq nats-from I = I . nats-from (s I) .
    eq sieve nil = nil .
    eq sieve (I . S) = I . sieve (filter S with I) .
    eq primes = sieve nats-from 2 .
  endfm

We can then evaluate expressions in this module with the reduce command (see Sections 4.9 and 16.2). For example, to compute the list of the first ten prime numbers we evaluate the expression:

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

In the case of associative or commutative binary operators, evaluation strategies might reduce some arguments that the user does not expect to be reduced. The reason is that in such cases terms represent equivalence classes and it might be quite hard to say what is the first or the second argument. The adopted solution is that mentioning either argument implies both.

The paper [37] documents the operational semantics and the implementation techniques for Maude's operator evaluation strategies in much more detail. The mathematical semantics of a Maude functional module having operator evaluation strategies is documented in [45] and is further discussed in Section 4.7.

Of course, operator evaluation strategies, while quite useful, are by design restricted in their scope of applicability to functional modules.^4.9 As we shall see in Chapter 5, system modules, specifying rewrite theories that are not functional, need not be Church-Rosser or terminating, and 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 11.5). However, as discussed in Section 4.4.9, specifying frozen arguments in operators restricts the rewrites allowed with rules in a system module (as opposed to equations) in a way quite similar to how operator evaluation strategies restrict the application of equations in a functional module.