A challenging problem in modern programming languages is the discovery of sound and complete evaluation strategies which are ``optimal'' w.r.t. some efficiency criterion (typically the number of evaluation steps and the avoidance of infinite, failing or redundant derivations) and which are easily implementable.

For orthogonal term rewriting systems (TRSs), Huet and Lévy's needed rewriting is optimal [HL91]. However, automatic detection of needed redexes is difficult (or even impossible) and Huet and Lévy defined the notion of ``strong sequentiality'', which provides a formal basis for the mechanization of sequential, normalizing rewriting computations [HL91]. In [HL91], Huet and Lévy defined the (computable) notion of strongly needed redexes and showed that, for the (decidable) class of strongly sequential orthogonal TRSs, the steady reduction of strongly needed redexes is normalizing. When strongly sequential TRSs are restricted to constructor systems (CSs), we obtain the class of inductively sequential CSs (see [HLM98]). Intuitively, a CS is inductively sequential if there exists some branching selection structure in the rules. Sekar and Ramakrishnan provided parallel needed reduction [SR93] as the extension of Huet and Lévy needed rewriting for non-inductively sequential CSs (namely, almost orthogonal CSs).

A sound and complete rewrite strategy for the class of inductively sequential CSs is outermost-needed rewriting [Antoy92]. The extension to narrowing is called outermost-needed narrowing [AEH00]. Its optimality properties and the fact that inductively sequential CSs are a subclass of strongly sequential programs explains why outermost-needed narrowing has become useful in functional logic programming as the functional logic counterpart of Huet and Lévy's strongly needed reduction. Weakly outermost-needed rewriting [AEH97] is defined for non-inductively sequential CSs. The extension to narrowing is called weakly outermost-needed narrowing [AEH97] and is considered as the functional logic counterpart of Sekar and Ramakrishnan's parallel needed reduction.

Unfortunately, weakly outermost-needed rewriting and narrowing do not work appropriately on non-inductively sequential CSs.

Consider Berry's program [SR93] where T and F are constructor symbols and X is a variable:

B(T,F,X) = T
B(F,X,T) = T
B(X,T,F) = T

B(B(T,F,T),B(F,T,T),F) -> B(B(T,F,T),T,F) -> T

B(B(T,F,T),B(F,T,T),F) -> B(T,B(F,T,T),F) -> B(T,T,F) -> T

Note that the problem also occurs in weakly outermost-needed narrowing. For instance, term B(X,B(F,T,T),F) has the optimal narrowing sequence

B(X,B(F,T,T),F) ->id B(X,T,F) ->id T

B(X,B(F,T,T),F) ->{X:T} B(T,T,F) ->id T

As Sekar and Ramakrishnan argued in [SR93], strongly sequential systems have been widely used in programming languages and violations are not frequent. However, it is a cumbersome restriction and its relaxation is quite useful in some contexts. It would be convenient for programmers that such a restriction could be relaxed while optimal evaluation is preserved for strongly sequential parts of a program. The availability of optimal and effective evaluation strategies without such a restriction could encourage programmers to formulate non-inductively sequential programs, which could still be executed in an optimal way.

Consider the problem of coding the rather simple inequality

x + y + z + w <= h

solve(X,Y,Z,W,H) = (((X + Y) + Z) + W) <= H
0 <= N = True
s(M) <= 0 = False
s(M) <= s(N) = M <= N
0 + N = N
s(M) + N = s(M + N)

When a more effective program is desired for some input terms, an ordinary solution is to include some assertions by hand into the program while preserving determinism of computations.

For instance, if terms t₁, t₂, and t₃ are part of such input terms of interest, we could obtain the following program

solve(X,s(Y),s(Z),W,s(H)) = solve(X,Y,s(Z),W,H)
solve(X,0,s(Z),W,s(H)) = solve(X,0,Z,W,H)
solve(s(X),Y,0,W,s(H)) = solve(X,Y,0,W,H)
solve(0,s(Y),0,W,s(H)) = solve(0,Y,0,W,H)
solve(0,0,0,0,H) = True
solve(s(X),Y,0,W,0) = False
solve(X,0,s(Z),W,0) = False
solve(0,s(Y),Z,0,0) = False
solve(X,s(Y),s(Z),s(W),0) = False

solve(10!,0+s(0),0+s(0),W,s(0)) 
  -> solve(10!,0+s(0),s(0),W,s(0))
  -> solve(10!,s(0),s(0),W,s(0))
  -> solve(10!,0,s(0),W,0)
  -> False

solve(X,Y,0+s(s(0)),W,s(0))
  ->id solve(X,Y,s(s(0)),W,s(0))
  ->{Y:0} solve(X,0,s(0),W,0) | ->{Y:s(Y')} solve(X,Y',s(s(0)),W,0)
  ->id False | ->{Y':0} False | ->{Y':s(Y''),W:0,X:0} False | ->{Y':s(Y''),W:s(W')} False

Modern (multiparadigm) programming languages apply computational strategies which are based on some notion of demandness of a position in a term by a rule (see [AL02] for a survey discussing this topic). Programs in these languages are commonly modeled by left-linear CSs and computational strategies take advantage of this constructor condition (see [AFJV97,MR92]). Furthermore, the semantics of these programs normally promotes the computation of values (or constructor head-normal forms) rather than head-normal forms. For instance, (weakly) outermost-needed rewriting and narrowing consider the constructor condition though some refinement is still possible, as shown by the following example.

Consider the following TRS from [AG01] defining the symbol %, which encodes the division function between natural numbers.

0 % s(N) = 0
s(M) % s(N) = s( (M - N) % s(N))
M - 0 = M
s(M) - s(N) = M - N