# A Needed Narrowing Strategy.

Abstract. The narrowing relation over terms constitutes the basis of the most important operational semantics of languages that integrate functional and logic programming paradigms. It also plays an important role in the definition of some algorithms of unification modulo equational theories that are defined by confluent term rewriting systems. Due to the inefficiency of simple narrowing, many refined narrowing strategies have been proposed in the last decade. This paper presents a new narrowing strategy that is optimal in several respects. For this purpose, we propose a notion of a needed narrowing step that, for inductively sequential rewrite systems, extends the Huet and Levy notion of a needed reduction step. We define a strategy, based on this notion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal with respect to the cost measure that counts the number of distinct steps of a derivation, computes only incomparable and disjoint unifiers, and is efficiently implemented by unification.Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.1.6 [Programming Techniques]: Logic Programming; D.3.3 [Programming Languages]: Language Constructs and Features--control structures; D.3.4 [Programming Languages]: Processors--optimization; F.4.2 [Mathematical Logic and Formal Languages]: Grammars and Other Rewriting Systems; G.2.2 [Discrete Mathematics]: Graph Theory--trees; I.1.1 [Algebraic Manipulation]: Expressions and Their Representation--simplification of expressions.

General Terms: Algorithms, Languages, Performance, Theory.

Additional Key Words and Phrases: Call-by-need, functional logic programming languages, narrowing strategies, rewrite systems

1. Introduction

Declarative programs are more abstract than equivalent imperative programs. Declarative languages replace pointers with algebraic data types, split complex computations into small, easily parameterizable units and avoid the manipulation of an explicit state through assignments. These features promise to ease some difficult essential tasks of software development. For example, they simplify reasoning about programs (verification of nonexecutable specifications), promote freedom of implementation (use of parallel architectures), and reduce both development time and maintenance efforts (code is compact and easier to read and understand). All these advantages stem from various factors--the most important being the solid mathematical foundations of declarative computing paradigms.

Currently, the field of declarative programming is split into two main paradigms based on different mathematical formalisms: functional programming (lambda calculus) and logic programming (predicate logic). This situation has a negative impact on teaching, research and applications. Usually there are different courses on functional programming and logic programming, and students do not perceive the similarities between them. In terms of research, each field has its own community, conferences, and journals, and sometimes similar solutions are developed twice. Each field also has its own application areas and some effort has been devoted to show that one paradigm can cover applications of the other paradigm [Wadler 1985] instead of showing the advantages of declarative programming in various application fields.

Each paradigm, of course, has its own advantages. Functional programming offers nested expressions, efficient evaluation by deterministic (often lazy) evaluation, and higher-order functions. Logic programming offers existentially quantified variables, partial data structures, and built-in search. On the other hand, functional and logic languages have a common core and can be seen as different facets of a single idea. Consequently, the interest in integrating functional and logic programming has grown over the last decade and resulted in various proposals of integrated functional logic languages that combine the advantages of both paradigms (see Hanus [1994] for a survey). Functional logic languages extend both functional languages and logic languages. Functional languages are extended with facilities such as function inversion, partial data structures, and logic variables [Reddy 1985]. Logic languages are extended with nested expressions, a more efficient operational behavior [Hanus 1990], and less need for impure control features such as the Prolog "cut."

This paper concerns narrowing. Narrowing is a computation model of considerable importance both for declarative programming in general and for functional logic languages in particular. We explain why using an example.

Example 1. Consider the following rules defining the concatenation of lists (as an infix operator + +) where we use the Prolog syntax for lists, that is, [] denotes the empty list and [E|R] denotes a nonempty list consisting of a first element E and a remaining list R:

[] ++ L [right arrow] L

[E|R] ++ L [right arrow] [E|R ++ L]

In a functional language, this definition is used to concatenate two lists, for example, [a, b] + + [c, d] evaluates to the list [a, b, c, d]. It is understood that (the value of) the arguments of ++ must be known in order to apply a rule. Narrowing extends the use of ++ without altering its definition in a remarkable way. Even if all or part of either argument of ++ is unknown (i.e., is an uninstantiated variable), narrowing keeps computing. In principle, this is not difficult--a value is assigned to the unknown parts of an argument--but the technical details that make this approach practical (sound, complete, and as efficient as the best functional computation when the arguments are fully known) are nontrivial and are the central subject of this paper. For the time being, we only want to show the advantages provided by narrowing in both declarative programming, in general, and functional logic languages, in particular. We begin with the latter.

A major obstacle in the integration of functional and logic programming is the evaluation of functional expressions containing logic uninstantiated variables. Narrowing, for its very nature, is obviously an elegant solution to this problem. An alternative solution is to residuate, that is, to delay the evaluation of expressions containing uninstantiated variables until they are more instantiated, but there is no guarantee that these expressions will later become instantiated enough to be evaluated.

Economy of code, both textual and conceptual, is one of the advantages of narrowing. For example, any abstraction of a type List, which defines the concatenation operation, is likely to define several other functions such as split (a function that given a list L returns two lists X and Y that concatenated together produce L), isPrefix (a function that given two lists X and L tells whether there exists a list Y such that X concatenated with Y produces L), and many others. Narrowing makes (the definitions of) split, isPrefix, and many other functions superfluous. The advantage for the programmer is not only the time and effort saved during software development (because many function definitions can be omitted), but also, and perhaps even more so, during software maintenance.

In any abstraction, there are groups of functions, such as ++, split, and isPrefix, that are intimately related, but neither the groups nor the relationships between the functions in a group are explicit in the code. When a function in a group changes due to maintenance, other functions in the same groups might have to change accordingly. Without a good understanding of the code, the programmer cannot know which functions should change or how. In this situation, the potential of introducing errors that are difficult to find and correct is high. Since narrowing allows us to avoid defining many related functions, these maintenance errors can no longer occur.

We demonstrate how the definition of related functions becomes superfluous by continuing our example. The key is the ability to solve equations. The details of this activity will be a central issue of this paper. For the time being, our discussion is informal and intuitive. The definition of ++ is used to split a list L into two lists X and Y by solving the equation X ++ Y [approximately equals] L. For instance, solving the equation X ++ Y [approximately equals] [a, b] yields the three solutions {X [right arrow] [], Y [right arrow] [a, b]}, {X [right arrow] [a], Y [right arrow] [b]}, and {X [right arrow] [a, b], Y [right arrow] []}. Similarly, we compute a prefix P of a list L (or check whether P is a prefix of L, if P is instantiated) by solving the equation P ++_ [approximately equals] L (_denotes an anonymous variable). Likewise, the last element E of a list L is computed by solving the equation _++ [E] [approximately equals] L.

The ability to solve equations over user-defined types is an essential feature in application programs to describe problems in a declarative and readable manner. For instance, a classic solution to the 8-queens problem checks whether two queens can capture each other. Within a program, this task is translated into selecting two distinct elements in a list L and checking whether they satisfy a given property p. The selection of two distinct elements in a list does not require defining any additional function beside ++. The entire task is simply coded as

_++[E] ++_++ [F] ++_ [approximately equals] L [conjunction] p(E, F)

In order to solve equations between expressions containing defined functions, most proposals for the integration of functional and logic programming languages are based on narrowing.(1) Narrowing, introduced in automated theorem proving [Slagle 1974] is a relation over terms induced by a term rewriting system. For a given term rewriting system R, narrowing is used to solve equations by computing unifiers with respect to the equational theory defined by R [Fay 1979]. Informally, narrowing unifies a term with the left-hand side of a rewrite rule and fires the rule on the 90 term.

Example 2. Consider the following rewrite rules defining the operations "less than or equal to" and addition for natural numbers represented by terms built with 0 and s:

0 [is less than or equal to] X [right arrow] true [R.sub.1]

s(X) [is less than or equal to] 0 [right arrow] false [R.sub.2]

s(X) [is less than or equal to] s(Y) [right arrow] X [is less than or equal to] Y [R.sub.3]

0 + X [right arrow] X [R.sub.4]

s(X) + Y [right arrow] s(X + Y) [R.sub.5]

The rules defining "[is less than or equal to]" will be used in following examples. To narrow the equation Z + s(0) [approximately equals] s(s(0)), rule [R.sub.5] is applied by instantiating Z to s(X). To narrow the resulting equation, s(X + s(0)) [approximately equals] s(s(0)), [R.sub.4] is applied by instantiating X to 0. The resulting equation, s(s(0)) [approximately equals] s(s(0)), is trivially true. Thus, {Z [right arrow] s(0)} is the equation's solution.

To apply the general idea of narrowing to integrated functional logic languages, a functional logic program is considered as a set of rewrite rules (with some additional restrictions explained later). A computation is initiated by solving an equation, t [approximately equals] t', which possibly contains variables. This includes goal solving, as in logic programming, as well as evaluating expressions as in functional programming. An expression e can be evaluated by solving the equation X [approximately equals] e so that X is instantiated to the result of evaluating e.

An important aspect in the design of functional logic languages is the definition of an appropriate strategy to solve equations. Such a strategy should be sound (i.e., only correct solutions are computed) and complete (i.e., all solutions or more general representatives of all solutions are computed). The narrowing relation can be used to define such a strategy, but a brute-force approach to finding all the solutions of an equation would attempt to unify each rule with each nonvariable subterm of the given equation in every narrowing step. The resulting search space would be huge, even for small rewrite programs. Therefore, many narrowing strategies for limiting the size of the search space have been proposed, for example, basic [Hullot 1980], innermost [Fribourg 1985], outermost [Echahed 1990], standard,(2) lazy,(3) or narrowing with redundancy tests [Bockmayr et al. 1995]. Each strategy demands certain conditions of the rewrite relation to ensure the completeness of narrowing (the ability to compute all the solutions of an equation.)

Example 3. Consider the rewrite rules of Example 2. Although the equation (X + X) + X [approximately equals] 0 has only one solution, eager narrowing strategies that evaluate argument terms first have an infinite search space for this equation by always applying rule [R.sub.5] to the innermost term headed by +. This infinite derivation can be avoided by a lazy narrowing strategy which evaluates a term only if it is demanded. The right definition of "demanded" is a subtle point since the "demandedness" of a term may depend on the instantiation of other variables. For instance, consider the term X [is less than or equal to] Y + Y. The evaluation of the second argument Y + Y is not demanded if X is instantiated to 0, but it is demanded if X is instantiated to s(...). A lazy narrowing strategy where the notion of "demanded" is independent of variable instantiations is defined in Moreno-Navarro and Rodriguez-Artalejo [1992]. Thus, this strategy may perform superfluous steps and computes answers that are too specialized. This fact motivated various improvements,(4) but none of them could show that the performed computation steps are really necessary and cannot be avoided.

Our contribution is a strategy that, for inductively sequential systems [Antoy 1992], preserves the completeness of narrowing and performs only steps that are "unavoidable" for solving equations. This characterization leads to the optimality of our strategy with respect to the number of "distinct" steps of a derivation. Advantages of our strategy over existing ones include: the large class of rewrite systems to which it is applicable, both the optimality of the derivations and the incomparability of the unifiers it computes, and the ease of its implementation.

The notion of an unavoidable step is well known for rewriting. Orthogonal systems have the property that in every term t not in normal form, there exists a redex called needed that must "eventually" be reduced to compute the normal form of t [Huet and Levy 1991; Klop and Middeldorp 1991; O'Donnell 1977]. Furthermore, repeated rewriting of needed redexes in a term suffices to compute its normal form, if it exists. Loosely speaking, only needed redexes really matter for rewriting in orthogonal systems. We extend this fact to narrowing in inductively sequential systems--a subclass of the orthogonal systems.

We also present a second optimality result (which cannot be stated for rewriting derivation) concerned with the substitution computed by a narrowing derivation. Every derivation of a same equation computes a set of substitutions. Different derivations compute disjoint sets of substitutions. This property nicely complements the neededness of a step in that the derivations computed by the strategy are needed in their entirety as well. Any solution computed by a derivation is not computed by any other derivation; hence, every derivation leading to a solution is needed as well as any step of the derivation.

Restricting our discussion to inductively sequential systems is not a limitation for the use of narrowing in programming languages. In fact, inductively sequential systems model the first-order functional component of programming languages, such as ML and Haskell, that establish priorities among rules by textual precedence or specificity [Kennaway 1990]. Computing a needed redex in a term is an unsolvable problem. Strongly sequential systems are a large class for which the problem has an efficient solution. Inductively sequential systems are constructor-based and strongly sequential [Antoy 1992]. It has been shown both that inductively sequential systems are the constructor-based subclass of strongly sequential systems [Hanus et al. 1998] and that a meaningful notion of needed redex can be formulated for overlapping inductively sequential systems [Antoy 1997].

After some preliminaries in Section 2, we present our strategy in Section 3. We formulate the soundness and completeness results in Section 4. We address our strategy's optimality in Section 5. Section 6 outlines several recent extensions of our strategy. We compare related work in Section 7. Our conclusion is in Section 8.

2. Preliminaries

We recall some key notions and notations about rewriting. We are consistent with the conventions of Dershowitz and Jouannaud [1990] and Klop [1992]. First of all, we fix the notations for terms.

Definition 1. A many-sorted signature [Sigma] is a pair (S, [Omega]) where S is a set of sorts and [Omega] is a family of operation sets of the form [Omega] = ([[Omega].sub.w,s]|w [element of] S*, s [element of] S). Let H = ([H.sub.s]|s [element of] S) be an S-sorted, countably infinite set of variables. Then the set T[([Sigma], H).sub.s] of terms of sort s built from [Sigma]; and H is the smallest set containing [H.sub.s] such that f([t.sub.1], ..., [t.sub.n]) [element of] T[([Sigma], H).sub.s] whenever [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. If f [element of] [[Omega].sub.[Epsilon], s], we write f instead of f(). T([Sigma], H) denotes the set of all terms. The set of variables occurring in a term t is denoted by Var(t). A term t is called ground term if Var(t) = 0. A term is called linear if it does not contain multiple occurrences of one variable. In the following, [Sigma] stands for a many-sorted signature.

In practice, most equational logic programs are constructor-based; symbols, called constructors, that construct data terms are distinguished from those, called defined functions or operations, that operate on data terms (see, e.g., the Equational Interpreter [O'Donnell 1985] and the functional logic languages ALF [Hanus 1990], BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992], K-LEAF [Giovannetti et al. 1991], LPG [Bert and Echahed 1986], SLOG [Fribourg 1985]). Hence, we define:

Definition 2. The set of operations [Omega] of a signature [Sigma] is partitioned into two disjoint sets C and D. C is the set of constructors and D is the set of defined operations. The terms in T(C, H) are called constructor terms. A term f([t.sub.1], ..., [t.sub.n]) (n [is less than or equal to] 0) is called a pattern if f [element of] D and [t.sub.1], ..., [t.sub.n] are constructor terms. A term f([t.sub.1], ..., [t.sub.n]) (n [is less than or equal to] 0) is called operation-rooted term (respectively constructor-rooted term) if f [element of] D (respectively f [element of] D). A constructor-based term rewriting system R is a set of rewrite rules, l [right arrow] r, such that l and r have the same sort, l is a pattern, and Var(r) [subset or equal to] Var(l).

In the rest of this paper, we assume that R is a constructor-based term rewriting system. Substitutions are an essential concept to define the notions of rewriting and narrowing.

Definition 3. A substitution is a mapping [Sigma]: H [right arrow] T([Sigma], H) with [Sigma](x) [element of] T([Sigma], H)s for all variables x [element of] [X.sub.s] such that its domain Dom([Sigma]) = {x [element of] H|[Sigma](x) [is not equal to] x} is finite. We frequently identify a substitution or with the set {x ?? [Sigma](x)|x [element of] Dom([Sigma])}. The image of a substitution or is the set of variables Im([Sigma]) = {y [element of] Var([Sigma](x))|x [element of] Dom([Sigma])}. Substitutions are extended to morphisms on T([Sigma], H) by [Sigma](f([t.sub.1], ..., [t.sub.n])) = f([Sigma]([t.sub.1]), ..., [Sigma]([t.sub.n])) for every term f([t.sub.1], ..., [t.sub.n]). A substitution or is called (ground) constructor substitution if [Sigma](x) is a (ground) constructor term for all x [element of] Dom([Sigma]). The composition of two substitutions [Sigma] and [Tau] is defined by ([Sigma] ?? [Tau])(x) = [Sigma]([Tau](x)) for all x [element of] H. The restriction [[Sigma].sub.|v] of a substitution [Sigma] to a set V of variables is defined by [[Sigma].sub.|v](X) = [Sigma](x) if x [element of] V and [[Sigma].sub.|v](x) = x if x [is not element of] V. A substitution [Sigma] is more general than [Sigma]', denoted by [Sigma] [is less than or equal to] [Sigma]', if there is a substitution [Tau] with [Sigma]' = [Tau] [Omicron] [Sigma]. If V is a set of variables, we write [Sigma] = [Sigma]' [V] iff [[Sigma].sub.|v] = [[Sigma].sub.|v], and we write [Sigma] [is less than or equal to] [Sigma]' [V] iff there is a substitution [Tau] with [Sigma]' = [Tau] ?? [Sigma][V]. A substitution [Sigma] is idempotent iff [Sigma] ?? [Sigma] = [Sigma].

A term t' is an instance of t if there is a substitution [Sigma] with t' = [Sigma](t). In this case we write t [is less than or equal to] t'. A term t' is a variant of t if t [is less than or equal to] t' and t' [is less than or equal to] t.

A unifier of two terms s and t is a substitution [Sigma] with [Sigma](s) = [Sigma](t). A unifier or is called most general (mgu) if [Sigma] [is less than or equal to] [Sigma]' for every other unifier [Sigma]'. Most general unifiers are unique up to variable renaming. By introducing a total ordering on variables we can uniquely choose the most general unifier of two terms. Hence, we denote by mgu(s, t) the most general unifier of s and t.

All the unifiers considered in this paper will be computed from a term and a linear pattern whose set of variables are disjoint. Under these conditions it is easy to verify that, restricted to the variables of these terms, only idempotent substitutions are computed. Therefore, we implicitly assume in our proofs that a unifier is an idempotent substitution and that any variable in the domain of a unifier is already contained in one of the terms being unified.

We now introduce positions, which are essential to define the notions of rewriting and narrowing.

Definition 4. An occurrence or position is a sequence of positive integers identifying a subterm in a term. For every term t, the empty sequence denoted by [Lambda], identifies t itself. For every term of the form f([t.sub.1], ..., [t.sub.k]), the sequence i [multiplied by] p, where i is a positive integer not greater than k and p is a position, identifies the subterm of [t.sub.i] at p. The subterm of t at p is denoted by [t.sub.|p] and the result of replacing [t.sub.|p] with s in t is denoted by t[[s].sub.p]. If p and q are positions, we write p [is less than or equal to] q if p is above or is aprefix of q, and we write p [parallel] q if the positions are disjoint (see Dershowitz and Jouannaud [1990] for details). The expression p [multiplied by] q denotes the position resulting from the concatenation of the positions p and q, that is, we overload the symbol "[multiplied by]."

We are now ready to define rewriting.

Definition 5. A reduction step is an application of a rewrite rule to a term, that is, t [[right arrow].sub.p,R] s if there exist a position p, a rewrite rule R = l [right arrow] r and a substitution [Sigma] with [t.sub.|p], = [Sigma](l) and s = t[[Sigma][(r)].sub.p].

In this case we say t is rewritten (at position p) to s and [t.sub.|p] is a redex of t. We will omit the subscripts p and R if they are clear from the context. A redex [t.sub.|p] of t is an outermost redex if there is no redex [t.sub.|q] of t with q [is less than] p. ?? denotes the transitive and reflexive closure of [right arrow]. ?? denotes the transitive, reflexive and symmetric closure of [right arrow]. A term t is reducible to a term s if t ?? s. A term t is called irreducible or in normal form if there is no term s with t [right arrow] s. A term s is a normal form of t if t is reducible to the irreducible term s.

Rewriting is computing, that is, the value of a functional expression is its normal form obtained by rewriting. Functional logic programs compute with partial information, that is, a functional expression may contain logic variables. The goal is to compute values for these variables such that the expression is evaluable to a particular normal form, for example, a constructor term [Giovannetti et al. 1991; Moreno-Navarro and Rodriguez-Artalejo 1992]. This is done by narrowing.

Definition 6. A term t is narrowable to a term s if there exist a nonvariable position p in t (i.e., [t.sub.|p], [is not element of] H), a variant l [right arrow] r of a rewrite rule in R with Var(t) [intersection] Var(l [right arrow] r) = 0 and a unifier [Sigma] of [t.sub.|p], and l such that s = [Sigma] (t[[r].sub.p]). In this case, we write t [??.sub.p,l [right arrow] [Sigma]] s. If [Sigma] is a most general unifier of [t.sub.|p] and l, the narrowing step is called most general. We write to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] if there is a narrowing derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with [Sigma] = [[Sigma].sub.n] ?? ... ?? [[Sigma].sub.2] ?? [[Sigma].sub.1].

Since the instantiation of the variables in the rule l [right arrow] r by [Sigma] is not relevant for the computed result of a narrowing derivation, we will omit this part of [Sigma] in the example derivations in this paper.

Example 4. Referring to Example 2,

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

and

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

are narrowing steps of A + B, but only the latter is a most general narrowing step.

Padawitz [1988] also distinguishes between narrowing and most general narrowing but, in most papers, narrowing is intended as most general narrowing (e.g., Hullot [1980]). Most general narrowing has the advantage that most general unifiers are uniquely computable, whereas there exist many distinct unifiers. Dropping the requirement that unifiers be most general is crucial to the definition of a needed narrowing step since these steps may be impossible with most general unifiers.

Narrowing solves equations, that is, computes values for the variables in an equation such that the equation becomes true, where an equation is a pair t [approximately equals] t' of terms of the same sort. In a constructor-based setting, it is reasonable to consider only ground constructor terms as values and to require that an equation holds if both sides have the same value (see also Giovannetti et al. [1991] for a more detailed discussion on this topic). Since we do not require terminating term rewriting systems, normal forms or values do not exist for each functional expression. Hence, we define the validity of an equation as a strict equality on terms in the spirit of functional logic languages with a lazy operational semantics such as K-LEAF [Giovannetti et al. 1991] and BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992]; an equation is satisfied if both sides are equivalent to a same ground constructor term. This is formally expressed by the following definition (since we consider in this paper only confluent rewrite systems).

Definition 7. An equation is a pair t [approximately equals] t' of terms of the same sort. A substitution [Sigma] is a solution for an equation t [approximately equals] t' iff [Sigma](t) and [Sigma](t') are reducible to a same ground constructor term.

Our definition of solution is weaker than convertibility, that is, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. This is due to the fact that we are discussing constructor-based, not necessarily terminating rewrite systems.

Equations can also be interpreted as terms by defining the symbol [approximately equals] as a binary operation symbol, more precisely, one operation symbol for each sort. Therefore, all notions for terms, such as substitution, rewriting, narrowing etc., will also be used for equations. The semantics of [approximately equals] are defined by the following rules, where [conjunction] is assumed to be a right-associative infix symbol and c is a constructor of arity 0 in the first rule and arity n [is less than] 0 in the second rule.

c [approximately equals] c [right arrow] true

c([X.sub.1], ..., [X.sub.n]) [approximately equals] c([Y.sub.1], ..., [Y.sub.n]) [right arrow] ([X.sub.1] [approximately equals] [Y.sub.1]) [conjunction] ... [conjunction] ([X.sub.n] [approximately equals] [Y.sub.n])

true [conjunction] X [right arrow] X

These are the equality rules of a signature (this encoding of strict equality as rewrite rules is analogous to the encoding equality by the rule x [approximately equals] x [right arrow] true in completion-based approaches to equation solving [Dershowitz 1989]). It is easy to see that the orthogonality status of a rewrite system (see below) is not changed by these rules. The same holds true for the inductive sequentiality, which will be defined shortly. With these rules, a solution of an equation is computed by narrowing it to true--an approach also taken in K-LEAF [Giovannetti et al. 1991] and BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992]. The equivalence between the reducibility to a same ground constructor term and the reducibility to true using the equality rules is addressed by Proposition 1.

We also require orthogonality, which ensures the good-behavior of computations.

Definition 8. A term rewriting system R is orthogonal if for each rule l [right arrow] r [element of] R the left-hand side l is linear (left-linearity) and for each nonvariable subterm l[|.sub.p] of l there exists no rule l' [right arrow] r' [element of] R such that l[|.sub.p] and l' unify (nonoverlapping) (where l' [right arrow] r' is not a variant of l [right arrow] r in case of p = [Lambda]).

Our strategy extends to narrowing the rewriting notion of need. The idea, for rewriting, is to reduce in a term only certain redexes which must be reduced to compute the normal form of t. In orthogonal term rewriting systems, every term not in normal form has a redex that must be reduced to compute the term's normal form. The following definition [Huet and Levy 1991] formalizes this idea.

Definition 9. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be a reduction step of some term t into t' at position u with rule l [right arrow] r. The set of descendants (or residuals) of a position v by A, denoted v\A, is

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The set of descendants of a position v by a reduction sequence B is defined by induction as follows

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

A position u of a term t is called needed iff in every reduction sequence of t to a normal form a descendant of t[|.sub.u] is rewritten at its root.

A position uniquely identifies a subterm of a term. The notion of descendant for terms stems directly from the corresponding notion for positions.

A more intuitive definition of descendant of a position or term is proposed in Klop and Middeldorp [1991]. Let t ?? t' be a reduction sequence and s a subterm of t. The descendants of s in t' are computed as follows: underline the root of s and perform the reduction sequence t ?? t'. Then, every subterm of t' with an underlined root is a descendant of s.

Example 5. Consider the operation that doubles its argument by means of an addition. The rules of addition are in Example 2.

double(X) [right arrow] X + X [R.sub.6]

In the following reduction of double(0 + 0), we show, by means of underlining, the descendants of 0 + 0.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The set of descendants of position 1 by the above reduction is {1, 2}.

3. Outermost-Needed Narrowing

An efficient narrowing strategy must limit the search space. No suitable rule can be ignored, but some positions in a term may be neglected without losing completeness. For instance, Hullot [1980] has introduced basic narrowing, where narrowing is not applied at positions introduced by substitutions. Fribourg [1985] has proposed innermost narrowing, where narrowing is applied only to a pattern. Holldobler [1989] has combined innermost and basic narrowing. Narrowing only at outermost positions is complete only if the rewrite system satisfies strong restrictions such as nonunifiability of subterms of the left-hand sides of rewrite rules [Echahed 1990]. Lazy narrowing [Giovannetti et al. 1991; Moreno-Navarro et al. 1990; Reddy 1985] akin to lazy evaluation in functional languages, attempts to avoid unnecessary evaluations of expressions. A lazy narrowing step is applied at outermost positions with the exception that inner arguments of a function are evaluated, by narrowing them to their head normal forms, if their values are required for an outermost narrowing step. Unfortunately, the property "required" depends on the rules tried in following steps, but looking-ahead is not a viable option.

We want to perform only narrowing steps that are necessary for computing solutions. Naively, one could say that a narrowing step t [??.sub.p, l [right arrow] r, [Sigma]] t' is needed iff p is a position of t, [Sigma] is the most general unifier of t[|.sub.p] and l, and [Sigma](t[|.sub.p]) is a needed redex. Unfortunately, a substantial complication arises from this simple approach. If t' is a normal form, the step is trivially needed. However, some instantiation performed later in the derivation could "undo" this need.

Example 6. Referring to Example 2, consider the term t = X [is less than or equal to] Y + Z. According to the naive approach, the following narrowing step of t at position 2

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

would be needed since X [is less than or equal to] Z is a normal form. This step is indeed necessary to solve the inequality if s(x) for some term x is eventually substituted for X, although this claim may not be obvious without the results presented in this paper. However, the same step becomes unnecessary if 0 is substituted for X. The following derivation computes a more general solution of the inequation without ever narrowing any descendant of t at 2.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Thus, in our definition, we impose a condition strong enough to ensure the necessity of a narrowing step, no matter which unifiers might be used later in the derivation.

Definition 10. A narrowing step t [??.sub.p, R, [Sigma]] t' is called needed or outermost-needed iff, for every [Eta] [is greater than or equal to] [Sigma], p is the position of a needed or outermost-needed redex of [Eta](t), respectively. A narrowing derivation is called needed or outermost-needed iff every step of the derivation is needed or outermost-needed; respectively.

Our definition adds, with respect to rewriting, a new dimension to the difficulty of computing needed narrowing steps. We must take into account any instantiation of a term in addition to any derivation to normal form. Luckily, as for rewriting, the problem has an efficient solution in inductively sequential systems. We forgo the requirement that the unifier of a narrowing step be most general. The instantiation that we demand in addition to that for the most general unification ensures the need of the position irrespective of future unifiers. It turns out that this extra instantiation would eventually be performed later in the derivation. Thus, we are only "anticipating" it and the completeness of narrowing is preserved. This approach, however, complicates the notion of narrowing strategy.

According to Echahed [1990] and Padawitz [1988], a narrowing strategy is a function from terms into non-variable positions in these terms so that exactly one position is selected for the next narrowing step. Unfortunately, this notion of narrowing strategy is inadequate for narrowing with arbitrary unifiers which, as Example 6 shows, are essential to capture the need of a narrowing step.

Definition 11. A narrowing strategy is a function from terms into sets of triples. If S is a narrowing strategy, t is a term, and (p, l [right arrow] r, [Sigma]) [element of] S(t), then p is a position of t, l [right arrow] r is a rewrite rule, and [Sigma] a substitution such that t [??.sub.p, l [right arrow] r, [Sigma]] [Sigma](t[[r].sub.p]) is a narrowing step.

We now define a class of rewrite systems for which there exists an efficiently computable needed narrowing strategy. Systems in this class have the property that the rules defining any operation can be organized in a hierarchical structure called definitional tree [Antoy 1992], which is used to implement needed rewriting. This paper generalizes that result to narrowing.

The symbols branch and leaf, used in the next definition, are uninterpreted functions used to classify the nodes of the tree. A definitional tree can be seen as a partially ordered set of patterns with some additional constraints.

Definition 12. T is a partial definitional tree, or pdt, with pattern [Pi] iff one of the following cases holds:

T = branch([Pi], o, [T.sub.1], ..., [T.sub.k]), where [Pi] is a pattern, o is the occurrence of a variable of [Pi], the sort of [Pi][|.sub.o] has constructors [c.sub.1], ..., [c.sub.k], for some k [is greater than] 0, and for all i in {1, ..., k}, [T.sub.i] is a pdt with pattern [Pi][[c.sub.i]([X.sub.1], ..., [X.sub.n])].sub.o], where n is the arity of [c.sub.i] and [X.sub.1], ..., [X.sub.n] are new distinct variables.

T = leaf([Pi]), where [Pi] is a pattern.

We denote by P([Sigma]) the set of pdts over the signature [Sigma]. Let R be a rewrite system. T is a definitional tree of an operation f iff T is a pdt whose pattern argument is f([X.sub.1], ..., [X.sub.n]), where n is the arity of f and [X.sub.1], ..., [X.sub.n] are new distinct variables, and for every rule l [right arrow] r of R with l = f([t.sub.1], ..., [t.sub.n]), there exists a leaf leaf([Pi]) of T such that l is a variant of [Pi], and we say that the node leaf([Pi]) represents the rule l [right arrow] r. We call minimal a definitional tree T of an operation f iff below any branch node of T there is a leaf representing a rule defining f.

We call inductively sequential an operation, f, of a rewrite system, R, iff there exists a definitional tree T of f such that each leaf node of T represents at most one rule of R. We call inductively sequential a rewrite system R iff any operation of R is inductively sequential.

Example 7. We show pictorial representations of definitional trees of the operations defined in Example 2. A branch node of the picture shows the pattern of a corresponding node of the definitional tree. Every leaf node represents a rule. We show the right side of each such rule below the pattern of the leaf which is connected by an arrow. The occurrence argument of a branch node is shown by emboldening the corresponding subterm in the pattern argument.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Distinguishing whether or not a leaf node of a definitional tree of some operation f represents a rule defining f is sometimes important in our treatment. We write exempt([Pi]) instead of leaf([Pi]) to point out that leaf([Pi]) is a pdt that does not represent any rule. Likewise, we abbreviate with rule([Pi], [Sigma](l) [right arrow] [Sigma](r)) the fact that leaf([Pi]) is a pdt representing some rule l [right arrow] r of the considered rewrite system, where [Sigma] is the renaming substitution such that [Sigma](l) = [Pi]. The patterns of a definitional tree are a finite set partially ordered by the subsumption preordering. The set of the patterns occurring within the leaves of a definitional tree is complete with respect to the set of constructors in the sense of Huet and Hullot [1982]. Consequently, the defined functions of an inductively sequential term rewriting system are completely defined over their application domains [Guttag and Horning 1978; Thiel 1984] (i.e., any ground term has a constructor term as a normal form) if the considered term rewriting system is terminating and the possible definitional trees do not contain exempt nodes.

We now give an informal account of our strategy. Let t = f([t.sub.1], ..., [t.sub.k]) be a term to narrow. We unify t with some maximal element of the set of patterns of a definitional tree of f. Let [Pi] denote such a pattern, [Tau] the most general unifier of t and [Pi], and T the pdt in which [Pi] occurs. If T is a rule pdt, then we narrow [Tau](t) at the root with the rule represented by T. If T is an exempt pdt, then [Tau](t) cannot be narrowed to a constructor-rooted term. If [Tau] is a branch pdt, then we recur on [Tau](t[|.sub.o]), where o is the occurrence contained in T and [Tau] is the anticipated substitution. The result of the recursive invocation is suitably composed with [Tau] and o. The details of this composition are in the formal definition presented below.

We derive our outermost-needed strategy from a mapping, [Lambda], that implements the above computation. [Lambda] takes an operation-rooted term, t, and a definitional tree, T, of the root of t, and non-deterministically returns a triple, (p, R, [Sigma]), where p is a position of t, R is either a rule l [right arrow] r of R or the distinguished symbol "?," and [Sigma] is a substitution. If R = l [right arrow] r, then our strategy performs the narrowing step t [??.sub.p, l [right arrow] r, [Sigma]] [Sigma](t[[r].sub.p]). If R = ?, then our strategy gives up, since it is impossible to narrow t to a constructor-rooted term.

In the following, pattern(T) denotes the pattern argument of T, and ?? denotes the Noetherian ordering on T([Sigma], H) x P([Sigma]) defined by: ([t.sub.1], [T.sub.1]) ?? ([t.sub.2], [T.sub.2]) if and only if either: (i) [t.sub.1] has fewer occurrences of defined operation symbols than [t.sub.2] or (ii) [t.sub.1] = [t.sub.2] and [T.sub.1] is a proper subtree of [T.sub.2].

Definition 13. The function [Lambda] takes two arguments: an operation-rooted term, t, and a pdt, T, such that pattern(T) and t unify. The function [Lambda] yields a set of triples of the form (p, R, [Sigma]), where p is a position of t, R is either a rewrite rule or the distinguished symbol "?," and [Sigma] is a unifier of pattern(T) and t. Thus, let t be a term and T a pdt in the domain of [Lambda]. The function [Lambda] is defined by induction on ?? as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

The function [Lambda] is trivially well defined in the third case. By the definition of pdt, there exists a proper subpdt [T.sub.i] of T such that pattern([T.sub.i]) and t unify if t[|.sub.o] is constructor-rooted or a variable. Similarly, [Lambda] is well defined in the fourth case, since this case can only occur if t[|.sub.o] is operation-rooted. In this case, [[Tau].sub.|Var(t)] is a constructor substitution since [Pi] is a linear pattern. Since t is operation-rooted and o [is not equal to] [Lambda], [Tau](t[|.sub.o]) has fewer occurrences of defined operation symbols than t. Since t[|.sub.o] is operation-rooted, so is [Tau](t[|.sub.o]). By the definition of pdt, pattern(T') [is less than or equal to] [Tau](t[|.sub.o]), that is, pattern(T') and [Tau](t[|.sub.o]) unify. This implies that [Lambda] is well defined in this case as well.

As in proof procedures for logic programming, we have to apply variants of the rewrite rules with fresh variables to the current term. Therefore, we assume in the following that the definitional trees contain new variables if they are used in a narrowing step.

The computation of [Lambda](t, T) may entail a nondeterministic choice when T is a branch pdt--the integer i when t[|.sub.o] is a variable. The substitution [Tau], when t[|.sub.o] is operation-rooted, is the anticipated substitution guaranteeing the need of the computed position. It is pushed down in the recursive call to [Lambda] to ensure the consistency of the computation when t is nonlinear. The anticipated substitution is neglected when t[|.sub.o] is not operation-rooted since the pattern in [T.sub.i] is an instance of [Pi]. Hence, [Sigma] extends the anticipated substitution.

Example 8. We trace the computation of [Lambda] for the initial step of a derivation of X [is less than or equal to] Y + Z as discussed in Example 6.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Note that we consider narrowing of operation-rooted terms. This limitation shortens our discussion and suffices for solving equations (see proof of Theorem 4). Extending our results to constructor-rooted terms is straightforward. To compute an outermost-needed narrowing step of a constructor-rooted term, it suffices to compute an outermost-needed narrowing step of any of its maximal operation-rooted subterms.

We prove two simple technical lemmas concerning the mutual relationships between the patterns of the pdts of a definitional tree:

LEMMA 1. Let T be a pdt, p and q two positions of T, and [[Pi].sub.p] and [[Pi].sub.q] the patterns of the pdts at the positions p and q of T, respectively. If p [is less than or equal to] q, then [[Pi].sub.p] [is less than or equal to] [[Pi].sub.q].

PROOF. If p [is less than or equal to] q, then there exists a position, r, such that q = p [multiplied by] r. The proof is by induction on the length of r. Base case: r = [Lambda] implies p = q and consequently [[Pi].sub.p] = [[Pi].sub.q]. Induction step: r = i [multiplied by] r', for some positive integer i and position r'. Let [T.sub.p] be the pdt of T at p. [T.sub.p] = branch([[Pi].sub.p], o, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]), for some position o, and pdts [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for some k [is greater than or equal to] i. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be the pattern in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Since [[Pi].sub.p] is linear and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is obtained by instantiating with a constructor term the variable of [[Pi].sub.p] at o, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By construction, [[Pi].sub.q] is equal to the pattern of the pdt of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] at r'. By the induction hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By the transitivity of "[is less than or equal to]," [[Pi].sub.p] [is less than] [[Pi].sub.q]. []

LEMMA 2. The patterns of the pdts at two disjoint positions of a pdt T do not unify.

PROOF. The proof is by structural induction on the pdt T.

Base case: T = leaf([Pi]), for some pattern [Pi].

There are no disjoint positions in T and the claim vacuously holds.

Induction step: T = branch([Pi], o, [T.sub.1], ..., [T.sub.k]), for some pattern [Pi], position o, and pdts [T.sub.1], ..., [T.sub.k], for some k [is greater than] 0.

Let p and q be two disjoint positions in T. Both p and q differ from [Lambda]; hence, there exist integers i and j in {1, ..., k}, and positions p' and q' such that p = i [multiplied by] p' and q = j [multiplied by] q'. If i = j, then p' and q' are disjoint positions of [T.sub.i]. The patterns of T at p and q are equal to the patterns of [T.sub.i] at p' and q', respectively. The latter do not unify by the induction hypothesis. If i [is not equal to] j, then, by Lemma 1, the patterns of T at p and q are instances of the root patterns of [T.sub.i] and [T.sub.j], respectively. The latter do not unify since they have a different symbol at position o; thus, the former do not unify either. []

LEMMA 3. If R is an inductively sequential rewrite system, then R is orthogonal.

PROOF. Let f be any operation of R. By definition of inductive sequentiality, there exists a definitional tree of f, T, such that every rule defining f is represented by one leaf of T. Thus, the left-hand sides of the rules defining f are linear since all patterns of a definitional tree are linear by definition. They are also nonoverlapping by Lemma 2. Finally, since the left-hand sides are patterns, the rules of different operations do not overlap. Hence, R is orthogonal. []

We are interested only in narrowing derivations that end in a constructor term. Our key result is that if [Lambda], on input of a term t, computes a position p and a substitution [Sigma] and [Eta] extends [Sigma], then [Eta](t) must "eventually" be narrowed at p to obtain a constructor term. "Eventually" is formalized by the notion of descendant which, initially proposed for rewriting [Huet and Levy 1991] is extended to narrowing simply by replacing [[right arrow].sub.u,l [right arrow] r] with [??.sub.u,l [right arrow] r,[Sigma]] in Definition 9.

THEOREM 1. Let R be an inductively sequential rewrite system, t an operation-rooted term, and T a definitional tree of the root of t. Let (p, R, [Sigma]) [element of] [Lambda](t, T) and [Eta] extend [Sigma], that is, [Eta] [is greater than or equal to] [Sigma].

(1) In any narrowing derivation of [Eta](t) to a constructor-rooted term a descendant of [Eta](t|p) is narrowed to a constructor-rooted term.

(2) If R = l [right arrow] r, then t [??.sub.p,R,[Sigma]] [Sigma](t[[r].sub.p]) is an outermost-needed narrowing step.

(3) If R = ?, then [Eta](t) cannot be narrowed to a constructor-rooted term.

PROOF. We prove by Noetherian induction on ?? the claim generalized by considering T a subtree of a definitional tree of the root of t such that pattern(T) and t unify. We consider the cases of the definition of [Lambda].

Base case: Consider (t, T) where t is an operation-rooted term and T = leaf([Pi]), for some pattern [Phi]. We consider the two subcases of the definition of [Lambda] for leaf nodes:

T = rule([Pi], R'), for some pattern [Pi] and rule R'.

In this case (p, R, [Sigma]) = ([Lambda], R', mgu(t, [Pi])). Since [Eta](t) is operation-rooted and is a descendant of itself, claim number 1 trivially holds. Let R' = l [right arrow] r, for some terms l and r. By the definition of a definitional tree, [Pi] = l; hence, [Sigma](l) = [Sigma](t[|.sub.p]). Thus, t [??.sub.p,R,[Sigma]] [Sigma](t[[r].sub.p]) is a narrowing step. Since R is orthogonal (by Lemma 3), its redex schemes do not overlap; consequently, R keeps matching any descendant of [Eta](t) obtained by reductions strictly below [Lambda]. Thus, [Eta](t) is a needed redex of itself and it is obviously outermost. Claim number 3 vacuously holds.

T = exempt([Pi]), for some pattern [Pi].

In this case (p, R, [Sigma]) = ([Lambda], ?, mgu(t, [Pi])). Since [Eta] [is greater than or equal to] [Sigma], [Eta] also unifies [Pi] and t. We could extend R by changing the exempt node into a rule node in which the left-hand side of the rule is obviously [Pi] and the right-hand side is arbitrary. Thus, similar to the previous case, [Pi] would keep unifying with any descendant of [Eta](t) obtained by reductions strictly below the root. Thus, by Lemma 2, there exists no rule in R that would unify with [Eta](t). Thus, [Eta](t) cannot be narrowed to a constructor-rooted term which implies claim number 3 and, trivially, claim number 1. Claim number 2 vacuously holds.

Induction step: Consider (t, T) where t is an operation-rooted term and T = branch([Pi], o, [T.sub.1], ..., [T.sub.k]), for some pattern [Pi] position o, and pdts [T.sub.1], ..., [T.sub.k], for some k [is greater than] 0. We consider the two subcases of the definition of [Lambda] for branch nodes.

t[|.sub.o] is either constructor-rooted or is a variable.

By the definition of pdt, there exists some i in {1, ..., k} such that pattern ([T.sub.i]) and t unify. By the definition of [Lambda], [Lambda](t, T) = [Lambda](t, [T.sub.i]). By the induction hypothesis, all the claims hold already for [Lambda](t, [T.sub.i]) and they are independent of [T.sub.i].

t[|.sub.o] is operation-rooted.

By the hypothesis, [Pi] and t unify. Let [Tau] = mgu(t, [Pi]). Since t[|.sub.o] is operation-rooted, so is [Tau](t[|.sub.o]). Let T' be a definitional tree of the root of [Tau](t[|.sub.o]). Let (p', R', [Sigma]') [element of] [Lambda]([Tau](t[|.sub.o]), T') such that (p, R, [Sigma]) = (o [multiplied by] p', R', [Sigma]' o [Tau]), where p' is a position of t[|.sub.o], R' is either a rule or "?," and [Sigma]' is a substitution. In this case (t[|.sub.o])[|.sub.p]' = t[|.sub.o [multiplied by] p'] = t[|.sub.p]. By Lemma 2, any rule whose left-hand side might unify with t is represented by a leaf of [T.sub.i]. If l [right arrow] r is a rule represented by a leaf of [T.sub.i] then, by Lemma 1, pattern ([T.sub.i]) [is less than or equal to] l. Thus, by the definition of definitional tree, l has a constructor symbol at position o. However, the case being considered assumes that t has an operation symbol at position o. Hence, in any narrowing derivation of [Eta](t) that includes a step at the root, a descendant of [Eta](t[|.sub.o]) must be narrowed to a constructor-rooted term. Since t is operation-rooted, [Eta](t) is also operation-rooted. In any narrowing derivation of [Eta](t) to a constructor-rooted term a descendant of [Eta](t) is narrowed at the root and, consequently, a descendant of [Eta](t[|.sub.o]) is narrowed to a constructor-rooted term. By the definition of [Lambda], [Tau](t[|.sub.o]) has fewer occurrences of operation symbols than t. Thus, by the induction hypothesis, for any [Eta]' [is greater than or equal to] [Sigma]', in any narrowing derivation of [Eta]'([Tau](t[|.sub.o])) to a constructor-rooted term a descendant of [Eta]'([Tau](t[|.sub.p])) is narrowed to a constructor-rooted term. Since [Eta] [is greater than or equal to] [Sigma], [Eta] = [Phi] ?? [Sigma] for some substitution [Phi]. Let [Eta]' = [Phi] ?? [Sigma]' [is greater than or equal to] [Sigma]', which implies [Eta]'([Tau](t)) = [Eta](t) since [Sigma] = [Sigma]' ?? [Tau]. Hence, in any narrowing derivation of [Eta](t[|.sub.o]) to a constructor-rooted term, a descendant of [Eta](t[|.sub.p]) is narrowed to a constructor-rooted term. Thus, claim number 1 holds by transitivity. We consider the two cases for R'.

R' is a rule.

By the induction hypothesis, [Tau](t[|.sub.o]) [??.sub.p',R,[Sigma']], [Sigma]'([Tau](t[|.sub.o])[[r].sub.p]') is an outermost-needed narrowing step; hence, t ?? p,R,[Sigma] [Sigma](t[[r].sub.p]) is a narrowing step. The need of [Eta](t[|.sub.p]) with respect to [Eta](t) is an immediate consequence of claim number 1. By the hypothesis, [Tau] and t unify and, by the definition of definitional tree, [Pi] is a pattern and o is a position of [Pi]. These conditions imply that there is only one operation symbol in [Sigma](t) above o: the root of [Sigma](t). In constructor-based systems, redexes occur only at positions of operation symbols. We have proved above that [Eta](t) is not a redex. Thus, there are no redexes in [Eta](t) above o and, by the induction hypothesis, the redex [Eta](t[|.sub.p]) is outermost in [Eta](t) too. Claim number 3 vacuously holds.

R' = ?.

We have proved above that, in any narrowing derivation of [Eta](t) to a constructor-rooted term, a descendant of [Eta](t[|.sub.o]) is narrowed to a constructor-rooted term. By the induction hypothesis, for any [Eta]' [is greater than or equal to] [Sigma]', [Eta]'([Tau](t[|.sub.o])) cannot be narrowed to a constructor-rooted term. Since [Eta] [is greater than or equal to] [Sigma], [Eta] = [Phi] ?? [Sigma] for some substitution [Phi]. Let [Eta]' = [Phi] [Omicrom] [Sigma]' [is greater than or equal to] [Sigma]' which implies [Eta] = [Eta]' ?? [Tau] since [Sigma] = [Sigma]' ?? [Tau]. Thus, [Eta](t[|.sub.o]) = [Eta]'([Tau](t[|.sub.o])) cannot be narrowed to a constructor-rooted term. Hence, [Eta](t) cannot be narrowed to a constructor-rooted term. Claim number 2 vacuously holds. []

We say that a narrowing derivation is computed by [Lambda] iff for each step t [??.sub.p,R,[Sigma]] t' of the derivation, (p, R, [Sigma]) belongs to [Lambda](t, T). The function [Lambda] implements our narrowing strategy as discussed next. The theorem shows (claim 2) that our strategy [Lambda] computes only outermost-needed narrowing steps. The theorem, however, does not show that the computation succeeds, that is, a narrowing step is computed for any operation-rooted; hence, expectedly narrowable, term. This requirement may seem essential, since to narrow a term "all the way" a strategy should compute a narrowing step, when one exists. Indeed, in incomplete rewrite systems, [Lambda] may fail to compute any narrowing step even when some step could be computed.

Example 9. Consider an incompletely defined operation, f, taking and returning a natural number.

f(0) [right arrow] 0

The term t = f(s(f(0))) can be narrowed (actually rewritten, since it is ground) to its normal form, f(s(0)). The only redex position of t is 1 [multiplied by] 1, but [Lambda] on a minimal definitional tree of f returns the set {(1, ?, { })}.

The inability of [Lambda] to compute certain outermost-needed narrowing steps is a blessing in disguise. The theorem (claim 3) justifies giving up a narrowing attempt as soon as the failure to find a rule occurs--without further attempts to narrow t at other positions with the hope that a different rule might be found after other narrowing steps or that the position might be deleted [Boudol 1985] by another narrowing step. If (p, ?, [Sigma]) [element of] [Lambda](t, T), no equation having [Sigma](t) as one side can be solved. This is an opportunity for optimization. In fact [Sigma](t) may be narrowable at other positions different from p and an equation with [Sigma](t) as a side may even have an infinite search space. However, any amount of work applied toward finding a solution would be wasted.

Example 10. Consider the following term rewriting system for subtraction:

X - 0 [right arrow] X [R.sub.1] s(X) - s(Y) [right arrow] X - Y [R.sub.2]

This term rewriting system is inductively sequential and a definitional tree, T, of the operation "-" has an exempt node for the pattern 0 - s(X), i.e., the system is incomplete and ([Lambda], ?, { }) [element of] [Lambda](0 - s(X), T). Therefore we can immediately stop the needed narrowing derivation of the equation 0 - s(X) [approximately equals] Y - Z although there exist infinitely many narrowing derivations for the right-hand side of this equation.

The definition of our outermost-needed narrowing strategy does not determine the computation space for a given inductively sequential rewrite system in a unique way. The concrete strategy depends on the definitional trees, and there is some freedom to construct these. For a discussion on how to compute definitional trees from rewrite rules and the implications of some nondeterministic choices of this computation, see Antoy [1992]. As we will show in Section 5, this does not affect the optimality of our strategy with respect to computed solutions. But in case of failing derivations, a definitional tree which is "unnecessarily large" could result in unnecessary derivation steps.

For example, a minimal definitional tree of the operation "-" in Example 10 has an exempt node for the pattern 0 - s(X). However, Definition 12 also allows a definitional tree with a branch node for the pattern 0 - s(X) which has exempt nodes for the patterns 0 - s(0) and 0 - s(s([X.sub.1])). Our strategy would perform some unnecessary steps if this definitional tree were used for narrowing the term 0 - s(t), where t is an operation-rooted term. These unnecessary steps are avoided if all branch nodes in a definitional tree are useful, that is, the tree is minimal.

However, the nondeterminism of the trees of certain operations makes it possible that some work may be wasted when a narrowing derivation computed by [Lambda] terminates with a non-constructor term. The problem seems inevitable and is due to the inherent parallelism of certain operations, such as [approximately equals] (this issue is discussed in some depth in Antoy [1992, Display (8)]). The problem occurs only in terms with two or more outermost-needed narrowing positions, one of which cannot be narrowed to a constructor-rooted term.

4. Soundness and Completeness

Outermost-needed narrowing is a sound and complete procedure to solve equations if we add the equality rules to narrow equations to true. The following proposition shows the equivalence between the reducibility to a same ground constructor term and the reducibility to true using the equality rules.

PROPOSITION 1. Let R be a term rewriting system without rules for [approximately equals] and [conjunction]. Let R' be the system obtained by adding the equality rules to R. The following propositions are equivalent for all terms t and t':

(1) t and t' are reducible in R to a same ground constructor term.

(2) t [approximately equals] t' is reducible in R' to `true'.

PROOF. To show that Claim 1 implies Claim 2, consider a ground constructor term u such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] using rules from R. Hence, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] using rules from R'. To show Claim 2, it is sufficient to show [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true using the equality rules. This is done by induction on the structure of u.

Base case: If u is a 0-ary constructor, say c, then u [approximately equals] u can be directly reduced to true using the equality rule c [approximately equals] c [right arrow] true. Induction step: Let u = c([t.sub.1], ..., [t.sub.n]). Then

u [approximately equals] u [right arrow] ([t.sub.1] [approximately equals] [t.sub.1]) [conjunction] ... [conjunction]([t.sub.n] [approximately equals] [t.sub.n])

is a reduction step using the equality rule for the n-ary constructor c. By the induction hypothesis, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true using the equality rules (i = 1, ..., n). Moreover, true [conjunction] ... [conjunction] true can be reduced to true using the equality rule for [conjunction].

To show that Claim 2 implies Claim 1, consider a reduction sequence [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true using rules from R'. We show the existence of a ground constructor term, u, such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] using rules from R by induction on the number, say k, of [approximately equals]-rule applications in this reduction sequence.

Base case (k = 1): There is exactly one application of a [approximately equals]-rule:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

r cannot have the symbol [conjunction] at the root; otherwise, there must be further applications of a [approximately equals]-rule in the derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true. Hence, the applied [approximately equals]-rule is of the form c [approximately equals] c [right arrow] true, which implies Claim 1.

Induction step (k [is greater than] 1): Then there is a first application of a [approximately equals]-rule:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

r [is not equal to] true; otherwise, there are no further applications of a [approximately equals]-rule in [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true. Therefore, s = c([t.sub.1], ..., [t.sub.n]), s' = c([t'.sub.1], ..., [t'.sub.n]), and r = ([t.sub.1] [approximately equals] [t'.sub.1]) [conjunction] ... [conjunction] ([t.sub.n] [approximately equals] [t'.sub.n]). Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true, an [conjunction]-rule must be applied to the root in this sequence, that is, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Thus, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with at most k - 1 [approximately equals]-rule applications. By the induction hypothesis, there is a ground constructor term [u.sub.1] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] using rules from R. By a further induction on the arguments [t.sub.i], [t'.sub.i], we can show the existence of ground constructor terms [u.sub.1], ..., [u.sub.n] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] using rules from R. Altogether, we obtain the derivations

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

using rules from R. This implies Claim 1. []

The soundness of outermost-needed narrowing is easy to prove since outermost-needed narrowing is a special case of general narrowing.

THEOREM 2. (SOUNDNESS OF OUTERMOST-NEEDED NARROWING). Let R be an inductively sequential rewrite system extended by the equality rules. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true is an outermost-needed narrowing derivation, then [Sigma] is a solution for t [approximately equals] t'.

PROOF. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true, there exists a derivation

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

such that [t.sub.n] = true and [Sigma] = [[Sigma].sub.n] ?? ... ?? [[Sigma].sub.1]. By induction on the number n of narrowing steps, it is easy to prove that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true. By Proposition 1, this implies that [Sigma](t) and [Sigma](t') are reducible to a same ground constructor term without using the equality rules. By Definition 7, [Sigma] is a solution for t [approximately equals] t'. []

In order to prove completeness of the outermost-needed narrowing strategy, we lift the completeness result for the corresponding rewrite strategy [Antoy 1992] to narrowing derivations. For this purpose, we recall the definition of the outermost-needed rewrite strategy for inductively sequential systems. Similarly to [Lambda], this rewrite strategy is implemented by a function, [Psi], that takes two arguments: an operation-rooted term, t, and a definitional tree, T, of the root of t (the definition of [Psi] is a slightly modified version of the definition given in Antoy [1992] extended to nonground terms). Throughout an interleaved descent down both t and T, [Psi] computes a position p and, whenever possible, a rule R such that the rewriting of t at p by means of R is outermost-needed.

Definition 14. The function [Psi] takes two arguments, an operation-rooted term t and a pdt T such that pattern(T) [is less than or equal to] t. The function [Psi] yields a pair, (p, R), where p is a position of t and R is either a rewrite rule or the distinguished symbol "?." Thus, let t be a term and T be a pdt in the domain of [Psi]. The function [Psi] is defined by structural induction on t with a nested structural induction on T as follows.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The function [Psi] is well defined in the third case since, by the definition of pdt, a proper subpdt [T.sub.i] of T with pattern([T.sub.i]) [is less than or equal to] t must uniquely exist iff t[|.sub.o] is constructor-rooted. Similarly, [Psi] is well defined in the fourth case since t[|.sub.o] is a proper subterm of t and pattern(T') [is less than or equal to] t[|.sub.o] by the definition of pdt.

The following theorem, which compacts various results of Antoy [1992], shows that the function [Psi] computes outermost-needed redexes. The proof parallels that of Theorem 1.

THEOREM 3. Let R be an inductively sequential rewrite system, t an operation-rooted term, T a definitional tree of the root of t, and [Psi](t, T) = (p, R).

(1) In any reduction sequence of t to a constructor-rooted term, a descendant of t[|.sub.p] is reduced to a constructor-rooted term.

(2) If R is a rule of R, then t[|.sub.p] is an outermost-needed redex of t matched by R.

(3) If R = ?, then t cannot be reduced to a constructor-rooted term.

PROOF. We prove by Noetherian induction on ?? the claim generalized by considering T a subtree of a definitional tree of the root of t such that pattern(T) [is less than or equal to] t. We consider the cases of the definition of [Psi].

Base case: Consider (t, T) where t is an operation-rooted term and T = leaf([Pi]) for some pattern [Pi].

We consider the two subcases of the definition of [Psi] for leaf nodes:

T = rule([Pi], R'), for some pattern [Pi] and rule R'.

In this case, (p, R) = ([Lambda], R'). Since t is operation-rooted and is a descendant of itself, claim number 1 trivially holds. By the hypothesis, [Pi] [is less than or equal to] t. By the definition of definitional tree, R is a rule whose left-hand side is equal to [Pi]. Thus, t is a redex, it is matched by R, and it is obviously outermost. Since R is orthogonal (by Lemma 3), its redex schemes do not overlap; consequently, R keeps matching any descendant of t obtained by reductions strictly below [Lambda]. Thus, t is a needed redex. Claim number 3 vacuously holds.

T = exempt([Pi]), for some pattern [Pi].

In this case, (p, R) = ([Lambda], ?). By the hypothesis, [Pi] [is less than or equal to] t. We could extend R by changing the exempt node into a rule node in which the left-hand side of the rule is obviously [Pi] and the right-hand side is arbitrary. Thus, similar to the previous case, [Pi] keeps matching any descendant of t obtained by reductions strictly below the root. Thus, by Lemma 2, there exists no rule in R for a reduction of t at the root. Thus, t cannot be reduced to a constructor-rooted term which implies claim number 3 and, trivially, claim number 1. Claim number 2 vacuously holds.

Induction step: Consider (t, T) where t is an operation-rooted term and T = branch([Pi], o, [T.sub.1], ..., [T.sub.k]), for some pattern [Pi], position o, and pdts [T.sub.1], ..., [T.sub.k], for some k [is greater than] 0. We consider three exhaustive (and mutually exclusive) cases for t[|.sub.o]:

t[|.sub.o] is constructor-rooted.

By the definition of pdt, there exists some i in {1, ..., k} such that pattern([T.sub.i]) [is less than or equal to] t. By the definition of [Psi], [Psi](t, T) = [Psi](t, [T.sub.i]). By the induction hypothesis, all the claims hold already for [Psi](t, [T.sub.i]) and they are independent of [T.sub.i].

t[|.sub.o] is operation-rooted.

Let T' be a definitional tree of the root of t[|.sub.o]. Let [Psi](t[|.sub.o], T') = (p', R'), where p' is a position of t[|.sub.o] and R' is either a rule or "?." In this case, (p, R) = (o [multiplied by] p', R') and (t[|.sub.o])[|.sub.p'] = t[|.sub.o [multiplied by] p'] = t[|.sub.p]. By the hypothesis, [Pi] [is less than or equal to] t. By Lemma 2, any rule that might reduce t at the root is represented by a leaf of some [T.sub.i] with 1 [is less than or equal to] i [is less than or equal to] k since the left-hand side of any other rule does not unify with [Pi]. If l [right arrow] r is a rule represented by a leaf of [T.sub.i], then, by Lemma 1, pattern ([T.sub.i]) [is less than or equal to] l. Thus, by the definition of definitional tree, l has a constructor symbol at position o. However, the case being considered assumes that t does not have a constructor symbol at position o. Hence, in any reduction sequence of t that includes a reduction at the root a descendant of t[|.sub.o] must be reduced to a constructor-rooted term. Since t is operation-rooted, in any reduction sequence of t to a constructor-rooted term, a descendant of t is reduced at the root. Consequently, a descendant of t[|.sub.0] is reduced to a constructor-rooted term. By the induction hypothesis, in any reduction sequence of t[|.sub.o] to a constructor-rooted term, a descendant of t[|.sub.p] is reduced to a constructor-rooted term. Thus, claim number 1 holds by transitivity.

We consider the two cases for R':

R' is a rule.

By the induction hypothesis, t[|.sub.p] is an outermost-needed redex of t[|sub.o] matched by R'; hence, t[|.sub.p] is a redex of t matched by R'. The need of t[|.sub.p] with respect to t is an immediate consequence of claim number 1. By the hypothesis, [Pi] [is less than or equal to] t, and by the definition of definitional tree, [Pi] is a pattern and o is a position of [Pi]. These conditions imply that there is only one operation symbol in t above o: the root of t. In constructor-based systems, redexes occur only at positions of operation symbols. We have just proved that t is not a redex. Thus, there are no redexes in t above o and, by the induction hypothesis, the redex t[|.sub.p] is outermost in t too.

R' = ?.

By claim number 1, in any reduction sequence of t to a constructor-rooted term, a descendant of t[|.sub.p] is reduced to a constructor-rooted term. By the induction hypothesis, t[|.sub.p] cannot be reduced to a constructor-rooted term. Thus, t cannot be reduced to a constructor-rooted term.

t[|.sub.o] is a variable.

In this case, (p, R) = (o, ?). The proofs of claims number 1 and 3 are similar to those of the previous case, but do not require induction hypotheses. Claim number 2 vacuously holds. []

The following proposition shows that the strategy [Lambda] behaves as [Psi] on ground terms.

PROPOSITION 2. Let R be an inductively sequential rewrite system. Let t be a ground operation-rooted term, T be a definitional tree of the root of t. Then, there exists a substitution [Sigma] such that [Lambda](t, T) = {(p, R, [Sigma])} and [Psi](t, T) = (p, R), where p is some position, R is some rewrite rule or the distinguished symbol "?," and [Sigma] is some substitution.

PROOF. We prove by Noetherian induction on ?? the claim generalized by considering T a subtree of a definitional tree of the root of t satisfying the condition pattern(T) [is less than or equal to] t. We consider the cases of the definitions of [Lambda] and [Psi]:

Base case: Consider (t, T) where t is an operation-rooted term and T = leaf([Pi]), for some pattern [Pi]. We consider the two subcases of the definitions of [Lambda] and [Psi] for leaf nodes.

T = rule([Pi], R'), for some pattern [Pi] and rule R'.

In this case, [Psi](t, T) = ([lambda], R') = (p, R) and [Lambda](t, T) = {([lambda], R', mgu(t, [Pi]))} = {(p, R, [Sigma])}.

T = exempt([Pi]), for some pattern [Pi].

In this case [Psi](t, T) = ([Lambda], ?) = (p, R) and [Lambda](t, T) = {(Lambda], ?, mgu(t, [Pi]))} = {(p, R, [Sigma])}. Thus, the claim holds.

Induction step: Consider (t, T) where t is an operation-rooted term and T = branch([Pi], o, [T.sub.1], ..., [T.sub.k]), for some pattern [Pi], position o, and pdts [T.sub.1], ..., [T.sub.k], for some k [is greater than] 0. We consider three exhaustive (and mutually exclusive) cases for t[|.sub.o]:

t[|.sub.o] is constructor-rooted.

By definition of pdt, there exists some i in {1, ..., k} such that pattern([T.sub.i]) and t unify. Since t is ground, we have pattern([T.sub.i]) [is greater than or equal to] t and for all j in {1, ..., k} such that j [is not equal to] i, pattern([T.sub.j]) and t do not unify. Therefore, by the definition of [Psi], [Psi](t, T) = [Psi](t, [T.sub.i]) and by the definition of [Lambda], [Lambda](t, T) = [Lambda](t, [T.sub.i]). Thus, by the induction hypothesis the claim holds.

t[|.sub.o] is operation-rooted.

By the hypothesis, [Pi] [is less than or equal to] t. Hence, t and [Pi] unify. Let [Tau] = mgu(t, [Pi]). Since t is ground, [Tau](t) = t. By the definition of pdt, t and pattern([T.sub.i]) do not unify for each i in {1, ..., k} since t[|.sub.o] is operation-rooted, whereas pattern([T.sub.i]) has a constructor symbol at position o. Let T' be a definitional tree of the root of t[|.sub.o]. By the definition of [Psi], [Psi](t, T) = (o [multiplied by] p', R') where (p', R') = [Psi](t[|.sub.o], T'). Likewise, by the definition of [Lambda], [Lambda](t, T') = {(o multiplied by] p", R", [Sigma]" ?? [Tau])|(p", R", [Sigma]") [element of] [Lambda]([Tau](t[|.sub.o]), T')}. Since t[|.sub.o] contains fewer operation symbols than t, we deduce by induction hypotheses that there exists a substitution [Sigma]" such that [Lambda]([Tau](t[|.sub.o]), T') = [Lambda](t[|.sub.o], T') = {(p', R', [Sigma]")}. Thus, [Lambda](t, T) = {(o [multiplied by] p', R', [Sigma]" ?? [Tau])} and the claim holds.

t[|.sub.o] is a variable: This case cannot occur since t is ground. []

The following lemma shows the close ties between [Psi] and [Lambda], which are instrumental to lift outermost-needed reduction sequences to corresponding narrowing derivations. This will allow us to prove the completeness of the outermost-needed narrowing strategy.

LEMMA 4. Let R be an inductively sequential rewrite system. Let t be an operation-rooted term, T be a definitional tree of the root of t, and [Sigma] be a constructor substitution. If [Sigma](t) [[right arrow].sub.p,R] t' with (p, R) = [Psi]([Sigma](t), T), then there exists a substitution [Theta] such that

(1) (p, R, [Theta]) [element of] [Lambda](t, T)

(2) [Theta] [is less than or equal to] [Sigma][Var(t)]

PROOF. We prove by Noetherian induction on ?? the claim generalized by considering T a subtree of a definitional tree of the root of t. We consider the cases of the definition of [Psi]:

Base case: Consider (t, T) where t is an operation-rooted term and T = leaf([Pi]), for some pattern [Pi]. We consider the two subcases of the definition of [Psi] for leaf nodes.

T = rule([Pi], R'), for some pattern [Pi] and rule R'

In this case, (p, R) = ([Lambda], R') and [Pi] [is less than or equal to] [Sigma](t). This implies the existence of a substitution [Phi] with [Phi]([Pi]) = [Sigma]([Pi]). Hence, [Pi] and t are unifiable (we assume that [Pi] and t are variable disjoint. Otherwise, take a new variant of the definitional tree) and there exists a most general unifier [Theta] of [Pi] and t with [Theta] [is less than or equal to] [Sigma][Var(t)]. By the definition of [Lambda], (p, R, [Theta]) [element of] [Lambda](t, T).

T = exempt([Pi]): This case cannot occur since R [is not equal to] ?.

Induction step: Consider (t, T) where t is an operation-rooted term and T = branch([Pi], o, [T.sub.1], ..., [T.sub.k]), for some pattern [Pi], position o, and pdts [T.sub.1], ..., [T.sub.k], for some k [is greater than] 0. We consider three exhaustive (and mutually exclusive) cases for t[|.sub.o]:

[Sigma](t)[|.sub.0] is constructor-rooted.

By the definition of pdt, there exists some i in {1, ..., k} such that pattern([T.sub.i]) [is less than or equal to] [Sigma](t). By the definition of [Psi], [Psi]([Sigma](t), T) = [Psi]([Sigma](t), [T.sub.i]). By the induction hypothesis, (p, R, [Theta]) [element of] [Lambda](t, [T.sub.i]) and [Theta] [is less than or equal to] [Sigma][Var(t)]. By the definition of [Lambda] (note that pattern([T.sub.i]) and t unify), (p, R, [Theta]) [element of] [Lambda](t, T).

[Sigma](t)[|.sub.o] is operation-rooted.

By the definition of [Psi], [Pi] [is less than or equal to] [Sigma](t). [Sigma](t) and pattern([T.sub.i]) do not unify for each i in {1, ..., k} since [Sigma](t)[|.sub.o] is operation-rooted, but pattern([T.sub.i]) has a constructor symbol at position o. Let T' be a definitional tree of the root of [Sigma](t)[|.sub.o] and [Psi]([Sigma](t)[|.sub.o], T') = (p', R'). By the definition of [Psi], (p, R) = (o [multiplied by] p', R'). Since [Pi] [is less than or equal to] [Sigma](t), there exists a most general unifier [Tau] of [Pi] and [Sigma](t) with [Tau] [is less than or equal to] [Sigma][Var(t)] (we assume that [Pi] and t are variable disjoint, otherwise take a new variant of the definitional tree), [[Tau].sub.|Var(t)] is a constructor substitution since [Pi] is a linear pattern and t is operation-rooted. Let [Sigma]' be a constructor substitution such that [Sigma]' ?? [Tau] = [Sigma][Var(t)]. Since [Sigma] is a constructor substitution, o is a position of t, and t[|.sub.o] is operation-rooted. Moreover, [Sigma](t) [[right arrow].sub.p.R] t' implies [Sigma]'([Tau](t[|.sub.o])) [[right arrow].sub.p',R'] t'[|.sub.o]. Since o is different from the root position, t is operation-rooted, and [[Tau].sub.|Var(t)] is a constructor substitution, [Tau](t[|.sub.o]) has fewer occurrences of defined operation symbols than t. Hence, by induction hypothesis applied to ([Tau](t[|.sub.o]), T') and [Sigma]', there exists a substitution [Theta]' such that (p', R', [Theta]') [element of] [Lambda]([Tau](t[|.sub.o]), T') and [Theta]' [is less than or equal to] [Sigma]'[Var([Tau](t[|.sub.o]))]. By the definition of [Lambda], (o [multiplied by] p', R', [Theta]' ?? [Tau]) [element of] [Lambda](t, T), that is, (p, R, [Theta]' ?? [Tau]) [element of] [Lambda](t, T). [Theta]' [is less than or equal to] [Sigma]'[Var([Tau](t[|.sub.o]))] implies [Theta]' [is less than or equal to] [Sigma]'[Var([Tau](t))] since [Theta]' instantiates only variables from [Tau](t[|.sub.o]) and new variables of the definitional tree. Hence, [Theta]' ?? [Tau] [is less than or equal to] [Sigma] ?? [Tau][Var(t)] which is equivalent to [Theta]' ?? [Tau] [is less than or equal] [Sigma][Var(t)].

[Sigma](t)[|.sub.o] is a variable: This case cannot occur since R [is not equal to] ?. []

The following lemma shows how to lift an outermost-needed reduction step to an outermost-needed narrowing step.

LEMMA 5. Let R be an inductively sequential rewrite system. Let [Sigma] be a constructor substitution, V be a finite set of variables, t be an operation-rooted term with Var(t) [subset or equal to] V, and T be a definitional tree of the root of t. If [Sigma](t) [[right arrow].sub.p,R] s with (p, R) = [Psi]([Sigma](t), T), then there exist an outermost-needed narrowing step t [??.sub.p.R,[Theta]] t' and a substitution [Sigma]' such that (p, R, [Theta]) [element of] [Lambda](t, T), [Sigma]'(t') = s and [Sigma]' ?? [Theta] = [Sigma][V].

PROOF. Let R be l [right arrow] r. By Lemma 4, there is a triple (p, R, [Theta]) [element of] [Lambda](t, T) with [Theta] [is less than or equal to] [Sigma][Var(t)]. Then there exists [Sigma]' such that [Sigma]' ?? [Theta] = [Sigma][V] (since [Theta] instantiates only variables occurring in t and in the definitional trees, we assume that [Theta](x) = x for all x [element of] V - Var(t) by taking appropriate variants of the definitional trees). By Claim 2 of Theorem 1, t [??.sub.p,R,[Theta]] t' is an outermost-needed narrowing step and [Theta](t)[|.sub.p] = [Theta](l). Hence [Sigma](t)[|.sub.p] = [Sigma]([Theta](t))[|.sub.p] = [Sigma]([Theta](l)) which implies [Sigma](t)[[[Sigma]'([Theta](r))].sub.p] = s. Finally, [Sigma]'(t') = [Sigma]'([Theta](t[[r].sub.p])) = [Sigma]'([Theta](t))[[[Sigma]'([Theta](r))].sub.p] = [Sigma](t)[[[Sigma]'([Theta](r))].sub.p] = s. []

Outermost-needed narrowing instantiates variables to constructor terms. Thus, we only show that outermost-needed narrowing is complete for constructor substitutions as solutions of equations. This is not a limitation in practice, since more general solutions would contain unevaluated or undefined expressions. This is not a limitation with respect to related work, since most general narrowing is known to be complete only for normalizable solutions [Middeldorp and Hamoen 1994] (which can be seen as semantically equivalent to irreducible solutions), and lazy narrowing is complete only for constructor substitutions [Giovannetti et al. 1991; Moreno-Navarro and Rodriguez-Artalejo 1992]. Incidentally, we also believe that needed narrowing is complete for the entire class of the orthogonal rewrite systems with respect to irreducible substitutions, although neither needed rewriting nor needed narrowing steps are computable for this class of rewrite systems. The following theorem shows the completeness of our strategy, [Lambda], and consequently of outermost-needed narrowing, for inductively sequential rewrite systems:

THEOREM 4. (COMPLETENESS OF OUTERMOST-NEEDED NARROWING). Let R be an inductively sequential rewrite system extended by the equality rules. Let [Sigma] be a constructor substitution that is a solution of an equation t [approximately equal to] t' and V be a finite set of variables containing Var(t) [union] Var(t'). Then there exists a derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true computed by [Lambda] such that [Sigma]' [is less than or equal to] [Sigma][V].

PROOF. By Definition 7, there exists a ground constructor term, say u, such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Since R is extended by the equality rules, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] by Proposition 1. Consider the following reduction sequence

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where [s.sub.0] = [Sigma](t [approximately equals] t'), ([p.sub.i+1], [R.sub.i+1]) = [Psi]([s.sub.i], [T.sub.i]) and [T.sub.i] is a definitional tree of the root of [s.sub.i] for i = 0, 1, 2,.... The following claims are easy to show by induction on the derivation steps in this sequence:

(1) [s.sub.i] has a constructor-rooted normal form (true).

(2) If [s.sub.i] [is not equal to] true, then the root of [s.sub.i] is the operation symbol [conjunction] or [approximately equals] (by the definition of equality rules).

(3) If [s.sub.i] [is not equal to] true, then [R.sub.i+1] [is not equal to] ? (claim 3 of Theorem 3) and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is an outermost-needed redex (claim 2 of Theorem 3).

Hence, the reduction sequence is well defined and outermost needed (as long as [s.sub.i] [approximately equals] true). Since repeated rewriting of needed redexes in a term computes the term's normal form, if it exists [Huet and Levy 1991], the sequence is finite and [s.sub.n] = true is the final term for some n [is greater than] 0. We will show by induction on n that there exists a corresponding outermost-needed narrowing derivation

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

such that [t.sub.n] = true and [[Sigma].sub.n] ?? ... ?? [[Sigma].sub.1] [is less than or equal to] [Sigma][V].

n = 1: If we apply Lemma 5 to the reduction step [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], we obtain an outermost-needed narrowing step [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and a substitution [Sigma]' such that [Sigma]' ?? [[Sigma].sub.1] = [Sigma][V] and [Sigma]'([t.sub.1]) = [s.sub.1] = true. Hence, [[Sigma].sub.1] [is less than or equal to] [Sigma][V] and [t.sub.1] = true by the definition of equality rules.

n [is greater than] 1: By Lemma 5 applied to the first reduction step, there exist an outermost-needed narrowing step [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and a substitution [Sigma]' such that [Sigma]' ?? [[Sigma].sub.1] = [Sigma][V] and [Sigma]'([t.sub.1]) = [s.sub.1]. Let [V.sub.1] = {y [element of] Var([[Sigma].sub.1](x))|x [element of] V} (note that Var([t.sub.1]) [subset or equal to] [V.sub.1]). Applying the induction hypothesis to [V.sub.1], [Sigma]' (note that [Sigma]'|[V.sub.1] is a constructor substitution since [Sigma]. is a constructor substitution) and the derivation

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

yields an outermost-needed narrowing derivation

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

with [t.sub.n] = true and [[Sigma].sub.n] ?? ... ?? [[Sigma].sub.2] [is less than or equal to] [Sigma]'[V1]. Combining that with the first narrowing step, we obtain the required outermost-needed narrowing derivation with ([[Sigma].sub.n] ?? ... ?? [is less than or equal to] [Sigma][V] since [Sigma]' ?? [[Sigma].sub.1] = [Sigma][V]. []

The theorem justifies our earlier remark on the relationship between completeness and anticipated substitutions. Any anticipated substitution of a needed narrowing step is irrelevant or would eventually be done later in the derivation; thus, it does not affect the completeness. Anticipating substitutions is appealing even without the benefits related to the need of a step, since less general substitutions are likely to yield a smaller search space to compute the same set of solutions.

5. Optimality

In Section 3, we showed that our strategy computes only necessary steps. We now strengthen this characterization by showing that our strategy computes only necessary derivations of minimum cost. First of all, we show that no redundant derivation is computed by [Lambda]. For this purpose, we need some technical definitions and results that we give below.

Definition 15. Let R be a term-rewriting system. Let t and s be two terms. We write [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Let [[Sigma].sub.1] and [[Sigma].sub.2] be two substitutions and V a set of variables. We write [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for all x [element of] V, and likewise we write [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for some x [element of] V. We write [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] iff there exists a substitution [Theta] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We say that [[Sigma].sub.1]. and [[Sigma].sub.2] are incomparable on V iff neither [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. [[Sigma].sub.1] and [[Sigma].sub.2] are called disjoint on [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for all substitutions [[Theta].sub.1] and [[Theta].sub.2].

The incomparability of substitutions has been used in unification theory [Plotkin 1972] in order to characterize minimal sets of solutions. When they exist, such minimal sets are unique (up to [=.sub.R]). Nevertheless, incomparable substitutions might have a common instance and, therefore, they do not describe disjoint regions of the solution space. For instance, the substitutions {x ?? 0} and {y ?? 0} are incomparable on {x, y} but the substitution {x ?? 0, y ?? 0} is described by both substitutions. However, this is not the case for disjoint substitutions since, by definition, they describe independent regions of the solution space. Thus, disjointness is a stronger notion than incomparability and we will show that the solutions computed by our strategy, [Lambda], are disjoint. First we show that the property of disjointness is indeed stronger than incomparability.

PROPOSITION 3. Let [[Sigma].sub.1] and [[Sigma].sub.2] be two substitutions and V a set of variables. If [[Sigma].sub.1] and [[Sigma].sub.2] are disjoint on V, then [[Sigma].sub.1] and [[Sigma].sub.2] are incomparable on V.

PROOF. Assume that [[Sigma].sub.1] and [[Sigma].sub.2] are not incomparable on V. That is to say, either [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Suppose without loss of generality that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By definition of the preordering [[is less than or equal to].sub.R], there exists a substitution [[Theta].sub.1] such that [[Theta].sub.1] ?? [[Sigma].sub.1] [=.sub.R] [[Sigma].sub.2][V]. Thus, by Definition 15, [[Sigma].sub.1] and [[Sigma].sub.2] are not disjoint on V. []

The two following technical propositions are used in subsequent proofs.

PROPOSITION 4. Let R be an inductively sequential rewrite system. Let [c.sub.1] and [c.sub.2] be two constructor symbols. If [c.sub.1]([t.sub.1], ..., [t.sub.n]) [=.sub.R] [c.sub.2]([u.sub.1], ..., [u.sub.m]), where n, m [is greater than or equal to] 0 and [t.sub.i] and [u.sub.j] are terms for i = 1, ...., n and j = 1, ..., m, then [c.sub.1] = [c.sub.2] (and thus, n = m) and [t.sub.i] [=.sub.R] [u.sub.i], for i = 1, ..., n.

PROOF. Since inductively sequential rewrite systems are orthogonal (cf. Lemma 3), they are confluent and Church-Russer (a TRS R is Church-Russer iff for all terms [t.sub.1] and [t.sub.2], [t.sub.1] [=.sub.R] [t.sub.2] implies the existence of a term [t.sub.3] with [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. From the Church-Russer property of R and the statement [c.sub.1]([t.sub.1], ..., [t.sub.n]) [=.sub.R] [c.sub.2]([u.sub.1], ..., [u.sub.m]), we infer the existence of a term T such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Since inductively sequential rewrite systems are constructor-based, no descendants of the terms [c.sub.1]([t.sub.1], ..., [t.sub.n]) and [c.sub.2]([u.sub.1], ..., [u.sub.m]) can be rewritten at the root. Therefore, [c.sub.1] = [c.sub.2] (and thus n = m) and the term T is of the form T = [c.sub.1]([w.sub.1], ..., [w.sub.n]) such that for all i = 1, ..., n, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. The last statement shows that for all i = 1, ..., n, [t.sub.i] [=.sub.R] [u.sub.i]. []

PROPOSITION 5. Let R be an inductively sequential rewrite system. Let t be a constructor term and [[Sigma].sub.1] and [[Sigma].sub.2] arbitrary substitutions. Then

(1) [[Sigma].sub.1](t) [=.sub.R] [[Sigma].sub.2](t)

implies for all variables y [element of] Var(t),

(2) [[Sigma.sub.1](y) [=.sub.R] [[Sigma].sub.2](y).

PROOF. The proof is by structural induction on t.

Base case: t is either a constant or a variable. In the first subcase, (2) is vacuously true, in the second subcase, (2) is a direct consequence of (1).

Induction step: Let t = c([t.sub.1], ..., [t.sub.n]), for some constructor symbol c and constructor terms [t.sub.1], ..., [t.sub.n]. By definition of substitution, c([[Sigma].sub.1]([t.sub.1]), ..., [[Sigma].sub.1]([t.sub.n])) = [[Sigma].sub.1](t) and c([[Sigma].sub.2]([t.sub.1]), ..., [[Sigma].sub.2]([t.sub.n])) = [[Sigma].sub.2](t). From Proposition 4 and c([[Sigma].sub.1]([t.sub.1]), ..., [[Sigma].sub.1]([t.sub.n])) [=.sub.R] c([[Sigma.sub.2]([t.sub.1]), ..., [[Sigma].sub.2]([t.sub.n])), we deduce that [[Sigma].sub.1]([t.sub.i]) [=.s [[Sigma].sub.2]([t.sub.i]) for i = 1, ..., n. Thus, the claim is immediate from the induction hypothesis. []

PROPOSITION 6. Let R be an inductively sequential rewrite system extended by the equality rules, e an equation to solve and V = Var(e). Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be a derivation computed by [Lambda]. Then, [[Sigma].sub.|v] is a constructor substitution.

PROOF. The proof is by induction on the length n of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Base case: n = 1. In this case [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] with (p, l [right arrow] r, [Sigma]) [element of] [Lambda](e, T), where T is a definitional tree of the root of e. Since the patterns of definitional trees are linear patterns with fresh variables, [[Sigma].sub.|v] is a constructor substitution.

Induction step: Consider now the derivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. By the induction hypothesis, [[Sigma].sub.|var]([e.sub.1]) and [[Sigma].sub.|v] are constructor substitutions. Thus [([Sigma] ?? [[Sigma].sub.1]).sub.|v] is a constructor substitution. []

PROPOSITION 7. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be a narrowing derivation. Then, [inverted] Ax [element of] Var([t.sub.n]), [exists] y [element of] Var([t.sub.0]) such that x [element of] Var([[Sigma].sub.n] ?? ... ?? [[Sigma].sub.1](y)).

PROOF. Note that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (compare proof of Theorem 2). Since reduction steps do not introduce new variables, x [element of] Var(([[Sigma].sub.n] ?? ... ?? [[Sigma].sub.1]([t.sub.0])) for all x [element of] Var([t.sub.n]) which implies the claim. []

PROPOSITION 8. Let R be an inductively sequential rewrite system. Let t be an operation-rooted term, V = Var(t) and ([p.sub.1], [R.sub.1], [[Sigma].sub.1]) and ([p.sub.2], [R.sub.2], [[Sigma].sub.2]) two distinct triples in [Lambda](t, T). Then, [[Sigma].sub.1] and [[Sigma].sub.2] are disjoint on V.

PROOF. The proof is by Noetherian induction on ??. We consider the cases of the definition of [Lambda].

Base case: Consider (t, T) where t is an operation-rooted term and T = leaf([Pi]), for some pattern [Pi]. There are no distinct triples in [Lambda](t, T) and the claim vacuously holds.

Induction step: Consider (t, T) where t is an operation-rooted term and T = branch ([Pi], o, [T.sub.1], .... [T.sub.k]), for some pattern [Pi], position o, and pdts [T.sub.1], ..., [T.sub.k], for some k [is less than] 0. We consider three exhaustive (and mutually exclusive) cases for t[|.sub.o]:

t[|.sub.o] is a variable, say x.

In this case t and pattern ([T.sub.i]) unify for all i = 1, ..., k. By the induction hypothesis, for every i, the substitutions of distinct triples in [Lambda](t, [T.sub.i]) are disjoint on V. Moreover, if ([p.sub.i], [R.sub.i], [[Sigma].sub.i]) [element of] [Lambda](t, [T.sub.i]) and ([p.sub.j], [R.sub.j], [[Sigma].sub.j]) [element of] [Lambda](t, [T.sub.j]) with i [is not equal to] j, then by definition of [Lambda] the roots of [[Sigma].sub.i](x) and [[Sigma].sub.j](x) are different constructors. So, for all substitutions [[Theta].sub.1] and [[Theta].sub.2], the roots of [[Theta].sub.1] ([[Sigma].sub.i](x)) and [[Theta].sub.2]([[Sigma].sub.j](x)) are different constructors too. Hence, by Proposition 4, we have [[Theta].sub.1]([[Sigma].sub.i](x)) [[is not equal to].sub.R] [[Theta].sub.2](([[Sigma].sub.j](x)) which shows that the substitutions [[Sigma].sub.i] and [[Sigma].sub.j] are disjoint on V. Thus, the claim holds.

t[|.sub.o] is constructor-rooted.

By the definition of pdt, there exists one i in {1, ..., k} such that pattern([T.sub.i]) and t unify. By the definition of [Lambda], [Lambda](t, T) = [Lambda](t, [T.sub.i]). By the induction hypothesis, the claim holds for [Lambda](t, [T.sub.i]) and thus for [Lambda](t, T) too.

t[|.sub.o] is operation-rooted.

By the definition of [Lambda], [Pi] and t unify. Let [Tau] = mgu(t, [Pi]). Since t[|.sub.o] is operation-rooted, so is [Tau](t[|.sub.o]). Let T' be a definitional tree of the root of [Tau](t[|.sub.o]). [[Tau].sub.|v] is a constructor substitution since the patterns of definitional trees are linear patterns. Thus, [Tau](t[|.sub.o]) contains fewer defined operation symbols than t. Therefore, if t[|.sub.o] is a ground subterm, by Proposition 2, there are no distinct triples in [Lambda](t, T) and the claim vacuously holds. Otherwise, t[|.sub.o] is not ground and by the induction hypothesis if ([p.sub.1], [R.sub.1], [[Sigma].sub.1]) and ([p.sub.2], [R.sub.2], [[Sigma].sub.2]) are distinct triples in [Lambda]([Tau](t[|.sub.o]), T'), then [[Sigma].sub.1] and [[Sigma].sub.2] are disjoint on Var([Tau](t[|.sub.o])). Let us show by contradiction that [[Sigma].sub.1] ?? [Tau] and [[Sigma].sub.2] ?? r are disjoint on V. Assume the opposite, that is, there exist substitutions [[Theta].sub.1] and [[Theta].sub.2] such that [[Theta].sub.1] ?? [[Sigma].sub.1] ?? [Tau] [=.sub.R] [[Theta].sub.2] ?? [[Sigma].sub.2] ?? [Tau][V]. Let v be any variable in Var([Tau](t[|.sub.o])). Then, there exists a variable z [element of] Var(t[|.sub.o]) such that v [element of] Var([Tau](z)) and [[Theta].sub.1] ?? [[Sigma].sub.1] ?? [Tau](z) [=.sub.R] [[Theta].sub.2] ?? [[Sigma].sub.2] ?? [Tau](z). Since [[Tau].sub.|v] is a constructor substitution, [Tau](z) is a constructor term. Thus, Proposition 5 implies that [[Theta].sub.1] ?? [[Sigma].sub.1](v) [=.sub.R] [[Theta].sub.2] ?? [[Sigma].sub.2](v). Consequently, [[Sigma].sub.1] and [[Sigma].sub.2] are not disjoint on Var(Tau(t[|.sub.o])) contrary to the induction hypothesis. Thus, [[Sigma].sub.1] ?? [Tau] and [[Sigma].sub.2] ?? [Tau] are disjoint on V. Hence, the claim holds. []

The next theorem claims that no redundant derivation is computed by [Lambda].

THEOREM 5 (DISJOINTNESS OF SOLUTIONS). Let R be an inductively sequential rewrite+system extended by the equality rules, e an equation to solve and V = Var(e). Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], true be two distinct derivations computed by [Lambda]. Then, [Sigma] and [Sigma]' are disjoint on V.

PROOF. First, we prove the claim when the initial steps of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] true and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], true differ. By our assumption, the derivations that we are considering are of the forms [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. This implies that [[Sigma.sub.1] and [[Sigma].sub.3] belong to distinct triples in [Lambda](e, T), where T is a definitional tree of [approximately equals]. Notice that, by Proposition 2, equation e is not ground. By Proposition 8, the substitutions [[Sigma].sub.1] and [[Sigma].sub.3] are disjoint on V. By definition of disjoint substitutions, for all substitutions [[Theta].sub.1] and [[Theta].sub.3], [[Theta].sub.1] ?? [Sigma].sub.1] [[is not equal to].sub.R] [[Theta].sub.3] ?? [[Sigma].sub.3][V]. Since [Sigma] = [[Sigma].sub.2] ?? [[Sigma].sub.1] and [Sigma]' = [[Sigma].sub.4] ?? [[Sigma].sub.3], we deduce that [Sigma] and [Sigma]' are disjoint on V.

Now, we consider the general case. By our assumption, the derivations that we are considering are of the forms [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for some i [is less than] 1. The subderivations computed by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], start from the same equation [e.sub.i] and their initial steps differ. Thus, by Proposition 2, equation [e.sub.i] is not ground. We have proved that in this case [[Sigma].sub.2] and [[Sigma].sub.3] are disjoint on Var([e.sub.i]). Hence, by definition of disjoint substitutions, we have

(3) [[Theta].sub.2] ?? [[Sigma].sub.2] [[is not equal].sub.R] [[Theta].sub.3] ?? [[Sigma].sub.3][Var([e.sub.i])] for all substitutions [[Theta].sub.2] and [[Theta].sub.3].

We prove by contradiction that the substitutions [[Sigma].sub.2] ?? [[Sigma].sub.1] and [[Sigma].sub.3] ?? [[Sigma].sub.1] are disjoint on V. So, we assume the opposite, that is, there exist two substitutions [[Beta].sub.2] and [[Beta].sub.3] with

(4) [[Beta].sub.2] ?? [[Sigma].sub.2] ?? [[Sigma].sub.1] [=.sub.R] [[Beta].sub.3] ?? [[Sigma].sub.3] ?? [[Sigma].sub.1][V]

Let y be a variable in Var([e.sub.i]). By Proposition 7, we know that [exists]z [element of] V such that y [element of] Var([[Sigma].sub.1](z)). Since [[Sigma].sub.1](z) is a constructor term (by Proposition 6) and y [element of] Var([[Sigma].sub.1](z)), from Proposition 5, we deduce that

(5) [[Beta].sub.2] ?? [[Sigma].sub.2](y) [=.sub.R] [[Beta].sub.3] ?? [[Sigma].sub.3](y)

and consequently that [[Sigma].sub.2] and [[Sigma].sub.3] are not disjoint on Var([e.sub.i]), which contradicts (3). Thus, the assumption (4) is false. Hence, the claim holds. []

We now discuss the cost and length of a derivation computed by our strategy. Our results are for the most part an extension of similar results for rewriting. We begin by extending to narrowing the notions of narrowing multistep, family of redexes, and complete step.

If p is a needed position of some term t, then in any narrowing derivation of t to a constructor term there is at least one step associated with p. If this step is delayed and p is not outermost, then several descendants of p may be created and several steps may become necessary to narrow this set of descendants (see Example 5). However, from a practical standpoint, if terms are appropriately represented, the cost of narrowing t at (some descendant of) p is largely independent of where the step occurs in the derivation of t. We formalize this viewpoint, which leads to another optimality result for our strategy.

It is well known [Huet and Levy 1991] that, under appropriate conditions, a set of redexes can be reduced simultaneously. This notion can be extended to narrowing steps.

Definition 16. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for i in some set of indices I = {1, ..., n}, be a narrowing step such that for any distinct i and j in I, [p.sup.i] and [p.sup.j] are disjoint and [[Sigma].sup.i] ?? [[Sigma].sup.j] = [[Sigma].sup.j] ?? [[Sigma].sup.i] We say that t is narrowable to t' in a multistep, denoted [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], iff [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [??.sub.i[element of]I] [[Sigma].sup.i] denotes the composition [[Sigma].sup.n] ?? ... ?? [[Sigma].sup.2] ?? [[Sigma].sup.1] (the order is irrelevant).

When we want to emphasize the difference between a step as defined in Definition 6 and a multistep, we refer to the former as elementary. Otherwise, we identify an elementary step with a multistep in which the set of narrowed positions has just one element. A narrowing multistep can be thought of as a set of elementary steps performed in parallel. In fact, the conditions that we impose on the positions and substitutions of each elementary step from which a multistep is defined imply that, in a multistep, the order in which substitutions are composed and positions are narrowed is irrelevant.

The notion of multistep is essential for defining the cost of a derivation. As expected, the cost of a derivation is the total cost of its steps and an elementary step has unit cost. However, it does not seem appropriate, for practical reasons, to set the cost of a multistep equal to the number of positions narrowed in the step. A justification of this choice will be given after the definition of cost. The notions of family of redexes, cost of a derivation, and complete narrowing step defined next extend those for rewriting [Berry and Levy 1979; Huet and Levy 1991; Maranget 1991].

For any set I and equivalence relation ~ on I, |I| denotes the cardinality of I, and I/~ denotes the quotient of I modulo ~.

Definition 17. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] ... be a narrowing (multi)derivation. Let [[Sigma].sub.n] be a shorthand for [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. The symbol [~.sub.n] denotes the equivalence relation on [I.sub.n] defined as follows: for any i and j in [I.sub.n], i [~.sub.n] j iff the subterms identified by these indices have a common ancestor, more precisely, there exists some m, less than n, such that for some position q in [t.sub.m], both [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are descendants of an [[Sigma].sub.n] ?? [[Sigma].sub.n-1] ... ([[Sigma].sub.m+1] ([t.sub.m|q]).

We call a family of [I.sub.n] any set of [~.sub.n]-equivalent indices, and a family of [t.sub.n] any set of redexes whose corresponding indices are [~.sub.n]-equivalent.

The cost of the nth step of [Alpha] is the number of families in [I.sub.n], |[I.sub.n]/[~.sub.n]|. The cost of [Alpha] denoted cost([Alpha]), is the total cost of the steps of [Alpha].

We say that a family is complete iff it cannot be enlarged, and we say that a step is complete iff it contracts only complete families, more precisely, [I.sub.n] is complete iff if i is in [I.sub.n], then for any position q of [t.sub.n-1] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and q have a common ancestor in some term of [Alpha], there exists some j in [I.sub.n] such that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We say that a derivation is complete iff all its steps are complete.

We say that a narrowing multistep [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] u is needed (respectively, outermost-needed) iff each family of I contains a needed (respectively, outermost-needed) narrowing position. A derivation is needed (respectively, outermost-needed) iff all its steps are needed (respectively, outermost-needed).

Example 11. Consider the rule for double in Example 5. Then

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is a narrowing multiderivation where all steps are complete and have cost 1.

If I is the set of indices of a narrowing step and i and j belong to I, then i ~ j iff [p.sub.i] and [p.sub.j] are, using an anthropomorphic metaphor, blood related. A complete derivation is characterized by narrowing complete "families," that is, sets containing all the pairwise blood related subterms of a term. Note that the blood related subterms of a term are all equal and that their positions are pairwise disjoint; thus, all of them can be included in a multistep. Our choice of cost measure is suggested by the observation that if t [??.sub.p,R,[Sigma]] t' and p and q are blood related positions, then narrowing t at q "when t is being narrowed at p" involves no additional computation of a substitution and/or a rule and, consequently, no additional computation of a substituting term (the instantiation of the right-hand side of a rule) since the reducts of blood related subterms are all equal, too.

We show that complete, outermost-needed narrowing derivations have minimum cost and minimum length. The proof relies on the analogous result for orthogonal systems formulated for reduction sequences only [Huet and Levy 1991; Maranget 1991]. Formally, we must give a meaning to the notion of need when a nonelementary step is computed. To achieve optimality, we require multisteps only as far as blood related terms are concerned. Thus, it suffices to consider multisteps in which only one complete family is narrowed. These steps are quite similar to elementary steps when, in the representation of a term, blood related subterms are fully "shared."

The framework of term graph rewriting [Sleep et al. 1993] offers a formal model that leads to a simple and efficient implementation of our strategy. We consider only finite term and acyclic graphs. The computation of a complete needed narrowing step in a term graph, g, proceeds as follows: we unravel g, thus obtaining a "regular" term t; we compute an outermost-needed narrowing step of t using [Lambda] as described earlier; we map back the computed step to g; and finally we perform the narrowing step on g. The adequacy of this approach for the rewrite systems and the terms that we are considering is discussed in Barendregt et al. [1987] and Kennaway et al. [1993]. In practice, the computation of a step is simple and efficient. Since [Lambda] computes a narrowing step by unification, the unraveling of a term graph g is achieved simply by traversing the representation of g as if it were a tree during the unification phase, and no map-back operation is actually required. In the following, we use the notion of reduction multisteps--narrowing multisteps where the step's unification is limited to a matching (cf. Definition 17).

Definition 18. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] be a narrowing multiderivation. Let [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. We say that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the reduction sequence canonically associated to [Alpha] iff for every n [is greater than] 0, if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the nth step of [Alpha], then [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the nth step of A.

Loosely speaking, [Alpha] and A compute the same steps.

LEMMA 6. Let R be an inductively sequential rewrite system, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] a narrowing multiderivation and A the reduction sequence canonically associated to [Alpha]. If [Alpha] is needed, then A is needed, too.

PROOF. Suppose that [Alpha] is not null and that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is the nth step of [Alpha], for some n [is greater than] 0. The nth step of A is [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. For each family in [I.sub.n], there exists an index l such that the narrowing position [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is needed. Since [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], by Definition 10, the position [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is also needed in A. []

LEMMA 7. Let R be an inductively sequential rewrite system, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and A the reduction sequence canonically associated to [Alpha]. If [Alpha] is complete, then A is also complete.

PROOF. We prove that if A is incomplete, then so is [Alpha]. Suppose that [Alpha] is not null and that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], for some n [is greater than] 0, is the first step of [Alpha] such that the corresponding step of A, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], is incomplete. There exists a position q of [t.sub.n-1] such that for no i [element of] [I.sub.n], [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], and for some j [element of] [I.sub.n], q and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are blood related. In other words, the family of [I.sub.n] to which [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] belongs is not complete. Since q and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are blood related, they have a common ancestor. Since the first incomplete step occurs at [t.sub.n-1], the common ancestor occurs in some preceding term [t.sub.l] with l [is less than or equal to] n - 2. Hence, there exists a position r in [[Theta].sub.l+1]([t.sub.l]) such that both q and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are (rewriting) descendants of r. Since the [[Theta].sub.i]'s are constructor substitutions and the root of [t.sub.l|r] is a defined operation, r is a position of [t.sub.l] as well. Thus, both q and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are (narrowing) descendants of r in [t.sub.n-1] and the nth step of [Alpha] is also incomplete. []

COROLLARY 1. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is a complete and needed narrowing multiderivation of a term t into a constructor term u, then [Alpha] has minimum cost. That is, for any multiderivation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], u with [Sigma] = [Sigma]'[Var(t)], cost([Alpha]) [is less than or equal to] cost([Beta]).

PROOF. Let A and B be the reduction sequences canonically associated with the narrowing derivations [Alpha] and [Beta], respectively. By Definition 18, [Sigma] = [Sigma]'[Var(t)] implies that the initial and final terms of A and B are pairwise identical. By Lemmas 6 and 7, A is a complete and needed reduction sequence. Thus, cost(A) [is less than or equal to] cost(B) [Huet and Levy 1991; Maranget 1991]. By Definition 17, cost(A) = cost([Alpha]) and cost(B) = cost([Beta]). Thus, [Alpha] has minimum cost among all the narrowing derivations computing [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. []

Completeness is essential to achieve minimum cost. In fact, if we stick to elementary derivations, the outermost-needed strategy yields the longest derivation among those that narrow terms only at needed positions. Nontrivial families of blood related subterms are created only by non-right-linear rules. The following example highlights these issues:

Example 12. We follow up on Example 5. It is immediate to verify that an outermost-needed narrowing elementary derivation (actually, a reduction sequence since the term is ground) of double(0 + 0) has 4 steps. The following elementary derivation is shorter.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

This derivation is shorter than the outermost-needed one, because its first step narrows the subterm at position 1. By contrast, the first step of the outermost-needed derivation narrows the initial term at the root. This step yields two descendants of position 1, which are both needed. Sharing these blood related subterms would save one step.

6. Extensions of Needed Narrowing

Since the preliminary publication of needed narrowing in Antoy et al. [1994] both needed narrowing and a combination of other strategies originating from this idea have become the preferred choice for the evaluation of modern narrowing-based functional logic languages. We will come back later to the reasons of this acceptance. In this section, we discuss variations and extensions of needed narrowing to classes of functional logic programs which are more general than the inductively sequential ones.

The key idea behind needed narrowing is the discovery that certain steps of a computation (referred to as "needed") must be performed to obtain the computation's result. Definitional trees allow us to efficiently compute needed steps. For instance, Hanus [1995] describes an efficient implementation of needed narrowing by a straightforward transformation of definitional trees into Prolog programs, and Ullan-Hernandez [1995] presents an abstract machine suitable for the direct compilation of needed narrowing into machine code. However, definitional trees also limit the domain of needed narrowing to inductively sequential systems. Inductive sequentiality excludes systems with overlapping left-hand sides, such as the following one, that are interesting in functional logic programming.

Example 13. The following definition of Boolean disjunction is known as the parallel-or:

X [disjunction] true [right arrow] true [R.sub.1] true [disjunction] X [right arrow] true [R.sub.2] false [disjunction] false [right arrow] false [R.sub.3].

This system is not inductively sequential since there is no definitional tree of "[disjunction]." This can be inferred by the fact that neither argument of "[disjunction]" is demanded by all the rules. The first two rules of "[disjunction]" are overlapping. Both rules are applicable, for example, to the term true [disjunction] true. As a consequence, a term of the form [t.sub.1] [disjunction] [t.sub.2] may be narrowed to normal form by narrowing either [t.sub.1] or [t.sub.2], although it is not known how to make this choice without looking ahead. A further consequence is the existence of terms of the form [t.sub.1] [disjunction] [t.sub.2] in which neither [t.sub.1] nor [t.sub.2] need to be evaluated--a condition contrary to the key idea of needed narrowing.

The rules of parallel-or belong to the class of the weakly orthogonal, constructor-based rewrite systems which allow overlapping among the rules' left-hand sides as long as any critical pair is trivial [Dershowitz and Jouannaud 1990; Klop 1992]. A variation of needed narrowing, applicable to this class of rewrite systems, is obtained by extending definitional trees with a new kind of nodes providing a mechanism for the nondeterministic selection of arguments to be evaluated [Antoy 1992; Antoy et al. 1997]. These definitional trees, called parallel, have the additional form or ([T.sub.1], ..., [T.sub.k]), where k [is greater than] 1 and all subtrees [T.sub.j] have the same pattern, but different arguments in the immediately subsequent branch nodes. The parallel definitional tree of the operation of Example 13 is

or(branch([X.sub.1] [disjunction] [X.sub.2], 1, leaf(true [disjunction] [X.sub.2] [right arrow] true), ...), (branch([X.sub.1] [disjunction] [X.sub.2], 2, leaf([X.sub.1] [disjunction] true [right arrow] true), ...)

Weakly needed narrowing [Antoy et al. 1997] is an extension of needed narrowing to weakly orthogonal, constructor-based rewrite systems. This strategy is computed by a function similar to it that nondeterministically selects a subtree of each or node that is encountered during the computation of a narrowing step. This strategy is almost identical to the demand driven narrowing strategy proposed in Loogen et al. [1993] (which is presented without proofs of soundness and completeness) and is a conservative extension of needed narrowing. Since weakly orthogonal term rewriting systems lack a notion of needed redex, the strong optimality results of needed narrowing cannot be preserved by weakly needed narrowing.

By contrast to needed narrowing, weakly needed narrowing, as well as any other previously proposed narrowing strategy for weakly orthogonal systems, does not evaluate every ground term in a deterministic way. Parallel narrowing [Antoy et al. 1997] is a variation of weakly needed narrowing that deterministically evaluates every ground term. It achieves this property by narrowing in a single step several distinct subterms similarly to the rewriting strategy of Sekar and Ramakrishnan [1993]. Parallel narrowing is better than weakly needed at pruning the search space. For instance, consider Example 13 together with the additional rule

f(a) [right arrow] true [R.sub.4]

and the term f(X) [disjunction] f(X). Weakly needed narrowing computes four distinct derivations all with the same substitution, {X ?? a}.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Parallel narrowing computes the same substitution and simultaneously reduces both arguments of "[disjunction]," yielding the unique parallel narrowing derivation

f(X) [disjunction] f(X) [??.sub.{X ?? a}] true [disjunction] true [??.sub.id] true.

Parallel narrowing is a conservative extension of two optimal evaluation strategies. It behaves as needed narrowing on inductively sequential rewrite systems, and is identical to Sekar and Ramakrishnan's [1996] rewrite strategy on ground terms. Parallel narrowing is the only complete strategy for functional logic programs that evaluates ground terms in a fully deterministic way--even in the presence of overlapping and nonterminating rules.

A second extension of needed narrowing deals with so-called nondeterminate functions. The choice operator is a perfect example of this idea. Nondeterminate computations are modeled by overlapping rewrite systems, for example,

choice (X, Y) [right arrow] X choice (X, Y) [right arrow] Y.

Nondeterminate functions support a terse and elegant programming style. For example, the following program nondeterministically computes a permutation of a list.

insert(X, Xs) [right arrow] choice([X|Xs], [insert.sub.1](X, Xs)) [insert.sub.1](X, [Y|Ys] [right arrow] [Y|insert(X, Ys)] permute([ ]) [right arrow] [ ] permute([X|Xs]) [right arrow] insert(X, permute(Xs)).

The use of nondeterminate functions in functional logic programming has been investigated by Antoy [1991] and Gonzales-Moreno et al. [1996]. In particular, Gonzales-Moreno et al. [1996] present a sound and complete narrowing calculus for a very large class of overlapping constructor-based systems that allow nondeterminate computations. A more sophisticated narrowing strategy for a more limited class of overlapping systems is given in Antoy [1997] along the lines of needed narrowing. Overlapping rules in these systems have the same left-hand side except for a renaming of variables. Rules with overlapping left-hand sides are merged by introducing a "choice" in the right-hand side (as shown by the rule of insert in the previous program). Definitional trees in these systems are exactly the definitional trees discussed in this paper--except for leaf nodes which may contain several choices. Systems in which every function has one such tree are called overlapping inductively sequential. Inductively sequential narrowing [Antoy 1997] is a strategy for possibly overlapping inductively sequential systems. This strategy is simply obtained from needed narrowing by adding, where appropriate, a choice of a right-hand side. This strategy preserves, with a few exceptions, the most important properties of needed narrowing including a weaker form of optimality modulo nondeterminate choices.

A third extension of needed narrowing deals with higher-order programming; a feature that greatly contributes to the power of functional languages and has been investigated in the context of functional logic languages by Hanus and Prehofer [1996] and Nakahara [1995]. As shown by Warren [1982] for the case of logic programming, one can extend a first-order language to cover the higher-order features of existing functional languages (including partial applications and lambda abstractions) by providing an application function apply(F, X) [right arrow] F(X). This function can be explicitly defined by first-order rules through an encoding of function names as constructors. By this method, we extend needed narrowing to higher-order functional programming since the rules defining the apply function are inductively sequential. More expressive languages should allow lambda abstractions in patterns (i.e., as arguments in the left-hand sides of rules)--a use that goes beyond current higher-order functional languages. For instance, the following higher-order rules for symbolic differentiation cannot be handled by existing functional languages, but are plausible in a higher-order functional logic language:

diff([Lambda]y.y, X [right arrow] 1 diff([Lambda]y.sin(F(y)), X [right arrow] cos(F(X)) * diff ([Lambda]y.F(y),X diff([Lambda]y.ln(F(y)), X [right arrow] diff([Lambda]y.F (y), X)/F(X).

A higher-order functional logic language is able to synthesize new functions satisfying a given goal. For instance, the equation

[Lambda]x.diff([Lamda]y.sin(F(x, y))), x) [approximately equals] [Lambda]x.cos(x)

is solved by instantiating the functional variable F by the projection function [Lambda]x.[Lambda]y.y. Function synthesis is a complex task that requires higher-order unification. A strategy for higher-order narrowing, based on definitional trees, has been proposed in Hanus and Prehofer [1996]. This strategy computes a minimal set of (higher-order) solutions by extending needed narrowing to deal with lambda abstractions.

A fourth extension of needed narrowing deals with graph rewriting systems [Echahed and Janodet 1998]. Future functional and logic programming languages will handle graph structures explicitly, as is yet the case in the declarative language Clean [Plasmeijer and van Eekelen 1993]. There are many reasons which motivate the use of graphs. They actually allow sharing of subexpressions, which leads to efficient implementations. They also permit to go beyond the processing of first-order terms by efficiently handling real-world data structures (e.g., databases). In Echahed and Janodet [1998], a class of confluent constructor-based graph rewriting systems has been proposed for which needed narrowing has been generalized successfully with the same nice optimality results.

Finally, the ideas of (weakly) needed narrowing and definitional trees have also been extended by concurrency features. This approach provides a unified computation model that encompasses the most important existing declarative programming paradigms [Hanus 1997]. This extension is the foundation of Curry [Hanus 1997; 1999], a new multi-paradigm programming language aiming to integrate functional, logic, and concurrent programming paradigms. The operational model of Curry uses a slightly extended form of definitional trees to specify the evaluation strategy of each function.

As the field of functional logic programming evolves, more demands are placed on narrowing strategies. In addition to soundness, completeness, and efficiency, a strategy must cope with results, features and techniques adopted in this field. One such feature is conditional rules that contribute to the expressiveness of programs. For instance, the following rules define a predicate for list membership on the basis of the function append to concatenate lists:

append([ ], L) [right arrow] L append([E|R], L) [right arrow] [E|append(R, L)] member(E, L) [right arrow] true ?? append(L1, [E|L2]) [approximately equals] L

Variables L1 and L2 do not occur in the left-hand side of their rule; hence, they don't get a value when the rule is fired. However, narrowing is an ideal computation to instantiate them. For example, in order to reduce a term like member(b, [a, b, c]), we can compute (e.g., by narrowing) values for the extra variables L1 and L2 so that the condition "append(L1, [b|L2]) [approximately equals] [a, b, c]" is reducible to true. If the left-hand sides of rewrite rules are non-overlapping, one can easily translate conditional rules into unconditional ones [Bergstra and Klop 1986]. This method has also been used in the functional logic language BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992] to define the semantics of conditional rules. In our example, we transform the rule for member into an unconditional one by interpreting the condition and the right-hand side as a "conditional expression":

member(E, L) [right arrow] cond(append(L1, [E|L2]) [approximately equals] L, true) cond(true, X) [right arrow] X.

On an inductively sequential source system, this transformation yields an inductively sequential target system. Hence, we can apply needed narrowing to the target system, although not all the properties of needed narrowing may be preserved by the transformation.

7. Comparison with Other Narrowing Strategies

The trade-off between power and efficiency is central to the use of narrowing, especially in programming. To this aim, several narrowing strategies(5) have been proposed. The notion of completeness has evolved accordingly. Plotkin's [1972] classic formulation has been relaxed to completeness with respect to ground solutions (e.g., Fribourg [1985]) or completeness with respect to strict equality and domain-based interpretations, as in Giovannetti et al. [1991] and Moreno-Navarro and Rodriguez-Artalejo [1992]. The latter appear more appropriate for narrowing as the computational paradigm of functional logic programming languages in the presence of infinite data structures and computations. For this purpose, we have introduced the equality rules in Section 2 and defined the computation of solutions of an equation as narrowing the equation to true. Although this approach is also taken in other functional logic languages, for example, K-LEAF Giovannetti et al. [1991] or BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992], it has the disadvantage that, in some cases, it simply enumerates all constructor terms.

Example 14. Consider the signature of Example 2 and the equation s(A) [approximately equals] s(s(B)). All possible solutions of this equation can be described by [Sigma] ?? {A ?? s(B)} where [Sigma] is an arbitrary ground constructor substitution with B [element of] Dom([Sigma]). However, applying needed narrowing to this equation with respect to the equality rules produces an infinite set of derivations with outcomes {A ?? s(0), B ?? 0}, {A ?? s(s(0)), B ?? s(0)}, {A ?? s(s(s(0))), B ?? s(s(0))}, etc.

In order to avoid such trivial but infinite search spaces, we can replace narrowing of constructor terms by a computation of the most general unifier. If [t.sub.1] [approximately equals] [t.sub.2] is an equation with [t.sub.1], [t.sub.2] [element of] T(C, H), we compute the most general unifier of [t.sub.1] and [t.sub.2] instead of applying narrowing steps. If both terms are not unifiable, there is no solution of [t.sub.1] [approximately equals] [t.sub.2]. Otherwise, mgu([t.sub.1], [t.sub.2]) represents all solutions of [t.sub.1] [approximately equals] [t.sub.2] in the sense that for each solution [Sigma] there exists a ground constructor substitution [Tau] with [Sigma] = [Tau] ?? mgu([t.sub.1], [t.sub.2]). Note that the restriction to constructor substitutions is essential since {A ?? s(f(0)), B ?? f(0)} is not a solution of the equation s(A) [approximately equals] s(s(B)) if the operation f is defined by

f(0) [right arrow] f(0).

The computation of the most general unifier in the final step of a narrowing derivation is also done in other narrowing strategies for terminating rewrite systems (e.g., Darlington and Guo [1989], Echahed [1990], and Fribourg [1985]).

We briefly recall the underlying ideas of a few major strategies and compare them with ours using the following example. We choose a terminating rewrite system with completely defined operations, otherwise all the eager strategies would be immediately excluded.

Example 15. The symbols a, b, and c are constructors, whereas f and g are defined operations.

f(a) [right arrow] a [R.sub.1] f(b(X)) [right arrow] b(f(X)) [R.sub.2] f(c(x)) [right arrow] a [R.sub.3] g(a, X) [right arrow] b(a) [R.sub.4] g(b(X), a) [right arrow] a [R.sub.5] g(b(X), b(Y)) [right arrow] c(a) [R.sub.6] g(b(X), c(Y)) [right arrow] b(a) [R.sub.7] g(c(X), Y) [right arrow] b(a) [R.sub.8]

The equation to solve is g(X, f(X)) [approximately equals] c(a). Our strategy computes only three derivations--only one of which yields a solution.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Basic narrowing [Hullot 1980] avoids positions introduced by the instantiations of previous steps. Its completeness, and that of its variations,(6) is known for confluent and terminating rewrite systems (see Middeldorp and Hamoen [1994] for a systematic study). This strategy may perform useless steps and computes an infinite search space for our benchmark example. LSE narrowing [Bockmayr et al. 1995] a refinement of basic narrowing with additional redundancy tests, ensures that the same solution (up to variable renaming) is not computed by two different derivations. However, it may be the case that one solution is an instance of another. Hence, different solutions computed by LSE narrowing are not incomparable in general.

Innermost narrowing [Fribourg 1985] narrows only patterns. It is ground complete only for terminating constructor-based systems with completely defined operations. It may perform useless steps and it computes an infinite number of derivations for our benchmark example.

Outermost narrowing [Echahed 1990; 1992] and Fassbender and Vogler [1994] narrows outermost operation-rooted terms. This strategy is ground complete only for a restrictive class of rewrite systems. It computes no solution for our benchmark example unless we transform the considered rewrite system [Echahed 1990].

Lazy narrowing [Giovannetti et al. 1991; Hans et al. 1992; Moreno-Navarro et al. 1990; Moreno-Navarro and Rodriguez-Artalejo 1992; Reddy 1985] narrows an inner term only when the step is demanded to narrow an outer term. For these strategies, the qualifier "lazy" is used as a synonym of "outermost" or "demand driven," rather than in the technical sense we propose. The completeness of these strategies is generally expensive to achieve: Hans et al. [1992] requires an ad-hoc implementation of backtracking, with the potential of evaluating some term several times; Giovannetti et al. [1991] requires flattening of functional nesting and a specialized WAM-like machine in which terms are dynamically reordered; and Moreno-Navarro et al. [1990] requires a transformation of the rewrite system which, for our benchmark example, increases the number of operations and lengthen the derivations. The following example shows a further important difference between lazy narrowing and needed narrowing:

Example 16. Consider the following term rewriting system: one(0) [right arrow] s(0) [R.sub.1] one(s(X)) [right arrow] one(X) [R.sub.2] f(0, 0) [right arrow] 0 [R.sub.3] f(s(X), 0) [right arrow] s(0) [R.sub.4] f(X, s(Y)) [right arrow] s(s(0)) [R.sub.5]

A lazy narrowing strategy reduces a term to a head normal form before a narrowing rule is applied, when this reduction is required for the rule's application [Moreno-Navarro et al. 1990; Reddy 1985]. For instance, if we wish to apply rule R3 to the term f(one(X), X), then f's argument one(X) must be narrowed to head normal form in an attempt to unify the result with f's argument 0 in [R.sub.3]. Unfortunately, there are infinitely many narrowing derivations of one(X) to a head normal form term--for every n [is greater than or equal to] 0, one(X) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] s(0). In a sequential implementation of a lazy strategy, this would delay forever the application of rules [R.sub.4] and [R.sub.5], which would result in an incomplete implementation [Hans et al. 1992]. Apart from this behavior in sequential implementations, lazy narrowing may have an infinite search space which may be avoided by our strategy. For instance, there are infinitely many lazy narrowing derivations of the equation f(one(X), X) [approximately equals] 0 due to the infinite number of derivations of one(X) to head normal form. But our strategy computes only the following two derivations:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The good behavior of our strategy is due to the fact that we have changed the order of redex selection and variable instantiation: our strategy instantiates f's second argument X to one of the constructors 0 or s before the redex is selected. This avoids narrowing the uninstantiated argument one(X).

Standard Narrowing [Darlington and Guo 1993; Ida and Nakahara 1997; Middeldorp and Okui 1998; You 1991] also called leftmost outside-in narrowing [Ida and Nakahara 1997], extends to narrowing the notion of standard rewrite derivations introduced by Huet and Levy [1991]. Thus, standard narrowing characterizes narrowing derivations rather than narrowing steps. In these narrowing derivations, as in lazy narrowing, outer positions are considered before inner positions. This strategy is complete for orthogonal systems with respect to strict equality. Standard narrowing derivations are the same as needed narrowing derivations on the benchmark example. However, You gives no constructive procedure for enumerating standard narrowing derivations. Darlington and Guo [1989] sketch a narrowing strategy called lazy pattern driven narrowing which is intended to compute standard narrowing derivations for orthogonal constructor-based rewrite systems. This strategy is not optimal in the sense that it may generate several times a same standard derivation. On the benchmark example, this strategy generates fourteen standard derivations and three times the unique derivation that computes a solution for the equation g(X, f(X)) [approximately equals] c(a). Ida and Nakahara [1997] give a procedure for enumerating standard narrowing derivations. They do not use the classic definition of a narrowing step (as in Definition 6), but break a narrowing step into more elementary inference steps (selection of a rule, pattern matching, etc). Due to the separation of rule application and pattern matching, their calculus has more nondeterministic choices than needed narrowing. For our benchmark example, their narrowing calculus nondeterministically applies five different inference steps to the initial equation. The same holds for other similar narrowing calculi, for example, Hamada and Middeldorp [1997] and Middeldorp et al. [1993]. Since this strategy is defined for orthogonal, but not necessarily constructor-based rewrite systems, it has also been extended [Nakahara et al. 1995] to provide a complete narrowing calculus for applicative term rewriting systems (which model the higher-order features of current functional languages). Recently, Middeldorp and Okui [1998] improved the strategies in Ida and Nakahara [1997] and Middeldorp et al. [1996] by providing a deterministic lazy narrowing calculus for orthogonal constructor-based rewrite systems (actually, they also provide completeness results for left-linear confluent constructor-based rewrite systems). This improved calculus is complete with respect to strict equality and behaves on the benchmark example as the narrowing calculus given in Ida and Nakahara [1997]. If we reconsider Example 16, all the quoted strategies including the last one, fail to stop on the equation f(one(X), X) [approximately equals] 0 contrary to needed narrowing. Nevertheless, standard narrowing has one optimality result due to the standardization of narrowing derivations. It has been shown in Middeldorp and Okui [1998] and You [1991] that the solutions computed by standard narrowing are always incomparable.

Implementations of narrowing in Prolog(7) are proposed as a prototypical and portable integration of functional and logic languages. For example, Cheong and Fribourg [1993] and Jimenez-Martin et al. [1992] have been proposed as an alternative to the specialized machines required for K-LEAF [Giovannetti et al. 1991] and BABEL [Moreno-Navarro and Rodriguez-Artalejo 1992], respectively. The most recent proposals [Antoy 1996; Loogen et al. 1993] are based on definitional trees and appear to compute needed steps for inductively sequential systems, although both methods neither formalize nor claim this property. The scheme in Antoy [1996] computes [Gamma] directly by unification. The patterns involved in the computation of [Gamma] are a superset of those represented by the leaves of a definitional tree. This is suggested by Claim 1 of Theorem 1 that shows a "strong" need for the positions computed using [Gamma]--not only the terms at these positions must be eventually narrowed, but they must be eventually narrowed to head normal forms. The resulting implementation takes advantage of this characteristic and its performance appears to be superior to the other proposals. This property of needed narrowing is also emphasized by the benchmarks presented in Hanus [1997], which show the superiority of needed narrowing in comparison to other narrowing strategies for Prolog-based implementations of functional logic programs. We summarize the characteristics of the major narrowing strategies in the table of Figure 1. In the requirement columns, C, T and CB denote "confluence," "termination," and "constructor discipline," respectively. In the optimality section, columns IS and DS denote incomparable and disjoint solutions, respectively. The entries "yes" and "no" mean that the corresponding property holds or does not hold, respectively. An empty entry indicates that the corresponding property has not been investigated in the literature. The entry "(yes)" means that the corresponding property has been shown under some additional conditions [Echahed 1990, Theorem 3].

Fig. 1. Summary of the characteristics of some major narrowing strategies.

Requirements Strategy C T CB others basic(1) X X innermost(2) X X X completely defined operations outermost(3) X X X uniformity lazy(4) X nonambiguity(6) standard(5) X (X) orthogonality needed X X inductive sequentiality Optimality length of Strategy Completeness IS DS derivations basic(1) complete no no no innermost(2) ground (yes) no complete outermost(3) ground (yes) no complete lazy(4) complete w.r.t. no no no strict equality standard(5) complete w.r.t. yes strict equality needed complete w.r.t. yes yes yes strict equality

(1) [Hullot 1980]

(2) [Fribourg 1985]

(3) [Echahed 1990; 1992]

(4) [Giovannetti et al. Hans et al. 1992; Moreno-Navarro et al. 1990; Moreno-Navarro and Rodriguez-Artalejo 1992; Reddy 1985]

(5) [Darlington and Guo 1989; Ida and Nakahara 1997; Middeldorp and Okui 1998; You 1991]

(6) [Moreno-Navarro and Rodriguez-Artalejo 1992. p. 197]

It is interesting to note that lazy narrowing, as formally defined in Moreno-Navarro and Rodriguez-Artalejo [1992], does not satisfy any of the optimality properties shown in the table. For instance, consider Example 2 and the goal X [is less than or equal to] X + X. Since both arguments of [is less than or equal to] are demanded in the sense of Moreno-Navarro and Rodriguez-Artalejo [1992], there are the following lazy narrowing derivations (among others):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Thus, the solution {X [right arrow] 0} is computed twice and the second derivation is not of minimal length.

To summarize, the distinguishing features of our strategy are the following: with respect to eager strategies, completeness for nonterminating rewrite systems; with respect to the so-called lazy strategies, a sharp characterization of laziness; with respect to any strategy, optimality and ease of computation.

8. Concluding Remarks

We have proposed a new narrowing strategy obtained by extending to narrowing the well-known notion of need for rewriting. Need for narrowing appears harder to handle than need for rewriting--to compute a needed narrowing step one must also look ahead at a potentially infinite number of substitutions. Remarkably, there is an efficiently algorithm for this computation in inductively sequential systems.

The only nontrivial operation required for the implementation of our strategy is unification. Prolog interpreters and compilers offer efficient built-in implementations of unification. This is one reason for the good performance, as we have reported in the previous section, of implementations of needed narrowing in Prolog (see Hanus [1995] for some benchmarks). In addition to being well-suited to efficient implementations of functional logic languages in Prolog, as described in Antoy [1996], Hanus [1995], and Loogen et al. [1993], our strategy can be easily implemented in other languages. Unification has well-understood algorithms that are efficiently implemented in various programming styles and abstract machines. For instance, Hanus and Sadre [1999] describes the compilation of the functional logic language Curry (which is based on an extension of needed narrowing) into Java.

We have also shown that our strategy computes only disjoint and optimal derivations. Although all the previously proposed lazy strategies have the latter as their primary goal, our strategy is the only one for which this result is formalized and proved.

We want to conclude with a general assessment of the "overall quality" of the narrowing strategy used by a programming language. The key factor is the trade-off between the size of the class of rewrite systems for which the strategy is complete, and the efficiency of its computations.

We have proved both completeness and optimality for inductively sequential systems. We have also discussed how the idea of needed narrowing has been extended into different directions (weakly orthogonal systems, non-determinate functions, conditional rules, higher-order functions, graph rewrite systems). These extensions preserve some of the remarkable characteristics of needed narrowing, such as an inherent conceptual simplicity and efficiency of computations; compatibility with the larger domain in which they are employed; and the full preservation of the key feature of needed narrowing--the computation of needed steps--on the inductively sequential portions of a program.

ACKNOWLEDGMENTS. The authors are grateful to the anonymous referees for their helpful remarks to improve the final version of this paper.

(1) See, for example, Bert and Echahed [1986], Fribourg [1985], Goguen and Meseguer [1986], Hanus [1990], Moreno-Navarro and Rodriguez-Artalejo [1992], and Reddy [1985].

(2) See, for example, Darlington and Guo [1989], Ida and Nakahara [1997], Middeldorp and Okui [1998], and You [1991].

(3) See, for example, Giovannetti et al. [1991], Hans et al. [1992], Moreno-Navarro et al. [1990], Moreno-Navarro and Rodriguez-Artalejo [1992], and Reddy [1985].

(4) See, for example, Hans et al. [1992], Loogen et al. [1993], and Moreno-Navarro et al. [1990; 1996].

(5) See, for example, Bockmayr et al. [1995], Darlington and Guo [1989], Echahed [1990; 1992], Echahed and Janodet [1998], Fay [1979], Fribourg [1985], Giovannetti et al. [1991], Fassbender and Vogler [1994], Hans et al. [1992], Herold [1986], Holldobler [1989], Ida and Nakahara [1997], Middeldorp and Hamoen [1994], Middeldorp and Okui [1998], Middeldorp et al. [1996], Moreno-Navarro et al. [1990], Moreno-Navarro and Rodriguez-Artalejo [1992], Nutt et al. [1989], Reddy [1985], and You [1991].

(6) See, for example, Bockmayr et al. [1995], Herold [1986], Holldobler [1989], Middeldorp and Hamoen [1994], Nutt et al. [1989], and Nieuwenhuis [1995].

(7) See, for example, Antoy [1996], Cheong and Fribourg [1993], Jimenez-Martin et al. [1992], and Loogen et al. [1993].

REFERENCES

ANTOY, S. 1991. Non-determinism and lazy evaluation in logic programming. In Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR'91) (Manchester, UK, July). T. P. Clement and K.-K. Lau, eds. Springer Workshops in Computing Series, Springer-Verlag, New York, pp. 318-331.

ANTOY, S. 1992. Definitional trees. In Proceedings of the International Conference on Algebraic and Logic Programming (ALP'92). Lecture Notes in Computer Science, vol. 632. Springer-Verlag, New York, pp. 143-157.

ANTOY, S. 1996. Needed narrowing in Prolog. In Proceedings of the International Symposium on Programming Languages, Implementations, Logics, and Programs (PLILP'96). Lecture Notes in Computer Science, vol. 632. Springer-Verlag, New York, pp. 473-474. Full version accessible at http: //www.cs.pdx.edu/~antoy.

ANTOY, S. 1997. Optimal non-deterministic functional logic computations. In Proceedings of the International Conference on Algebraic and Logic Programming (ALP'97). Lecture Notes in Computer Science, vol. 1298. Springer-Verlag, New York, pp. 16-30.

ANTOY, S., ECHAHED, R., AND HANUS, M. 1994. A needed narrowing strategy. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, Ore., Jan. 17-21). ACM, New York, pp. 268-279.

ANTOY, S., ECHAHED, R., AND HANUS, M. 1997. Parallel evaluation strategies for functional logic languages. In Proceedings of the 14th International Conference on Logic Programming (ICLP'97). MIT Press, Cambridge, Mass., pp. 138-152.

BARENDREGT, H., VAN EEKELEN, M., GLAUERT, J., KENNAWAY, R., PLASMEIJER, M. J., AND SLEEP, M. 1987. Term graph rewriting. In Proceedings of Parallel Architectures and Languages Europe (PARLE'87). Lecture Notes in Computer Science, vol. 259. Springer-Verlag, New York, pp. 141-158.

BERGSTRA, J. A., AND KLOP, J. W. 1986. Conditional rewrite rules: Confluence and termination. J. Comput. Syst. Sci. 32, 3.

BERRY, G., AND LEVY, J.-J. 1979. Minimal and optimal computations of recursive programs. J. ACM 26, 1 (Jan.), 148-175.

BERT, D., AND ECHAHED, R. 1986. Design and implementation of a generic, logic and functional programming language. In Proceedings of the European Symposium on Programming (ESOP'86). Lecture Notes in Computer Science, vol. 213. Springer-Verlag, New York, pp. 119-132.

BOCKMAYR, A., KRISCHER, S., AND WERNER, A. 1995. Narrowing strategies for arbitrary canonical systems. Fund. Inf. 24, 1, 2, 125-155.

BOUDOL, G. 1985. Computational semantics of term rewriting systems. In Algebraic methods in semantics, M. Nivat and J. C. Reynolds, eds. Cambridge University Press, Cambridge, UK, Chap. 5, pp. 169-236.

CHEONG, P. H., AND FRIBOURG, L. 1993. Implementation of narrowing: The Prolog-based approach. In Logic programming languages: Constraints, functions, and objects, K. R. Apt, J. W. de Bakker, and J. J. M. M. Rutten, eds. MIT Press, Cambridge, Mass., pp. 1-20.

DARLINGTON, J., AND GUO, Y. 1989. Narrowing and unification in functional programming--An evaluation mechanism for absolute set abstraction. In Proceedings of the Conference on Rewriting Techniques and Applications (RTA'89). Lecture Notes in Computer Science, vol. 355. Springer-Verlag, New York, pp. 92-108.

DERSHOWITZ, N. 1989. Completion and its applications. In Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques. H. Ait-Kaci and M. Nivat, eds. Academic Press, New York, Chap. 2, pp. 31-85.

DERSHOWITZ, N., AND JOUANNAUD, J. 1990. Rewrite systems. In Handbook of Theoretical Computer Science B: Formal Methods and Semantics, J. van Leeuwen, ed. North-Holland, Amsterdam, Chap. 6, pp. 243-320.

ECHAHED, R. 1990. On completeness of narrowing strategies. Theoret. Comput. Sci. 72, 133-146.

ECHAHED, R. 1992. Uniform narrowing strategies. In Proceedings of the 3rd International Conference on Algebraic and Logic Programming (ALP'92) (Volterra, Italy). Lecture Notes in Computer Science, vol. 632. Springer-Verlag, New York, pp. 259-275.

ECHAHED, R., AND JANODET, J. C. 1998. Admissible graph rewriting and narrowing. In Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (JICSLP'98). MIT Press, Cambridge, Mass., pp. 325-340.

FASSBENDER, H., AND VOGLER, H. 1994. A universal unification algorithm based on unification-driven leftmost outermost narrowing. Acta Cybern. 11, 3, 139-167.

FAY, M. J. 1979. First-order unification in an equational theory. In Proceedings of the 4th Workshop on Automated Deduction (Austin, Tex.). Academic Press, New York, pp. 161-167.

FRIBOURG, L. 1985. SLOG: A logic programming language interpreter based on clausal superposition and rewriting. In Proceedings of the IEEE International Symposium on Logic Programming (Boston, Mass.). IEEE, New York, pp. 172-184.

GIOVANNETTI, E., LEVI, G., MOISO, C., AND PALAMIDESSI, C. 1991. Kernel LEAF: A logic plus functional language. J. Comput. Syst. Sci. 42, 139-185.

GOGUEN, J. A., AND MESEGUER, J. 1986. Eqlog: Equality, types, and generic modules for logic programming. In Logic Programming, Functions, Relations, and Equations, D. DeGroot and G. Lindstrom, eds. Prentice-Hall, Englewood Cliffs, N.J., pp. 295-363.

GONZALES-MORENO, J. C., HORTALA-GONZALES, M. T., LOPEZ-FRAGUAS, F. J., AND RODRIGUEZ-ARTALEJO, M. 1996. A rewriting logic for declarative programming. In Proceedings of the European Symposium on Programming (ESOP'96). Lecture Notes in Computer Science, vol. 1058. Springer-Verlag, New York, pp. 156-172.

GUTTAG, J. V., AND HORNING, J. J. 1978. The algebraic specification of abstract data types. Acta Inf.

HAMADA, M., AND MIDDELDORP, A. 1997. Strong completeness of a lazy conditional narrowing calculus. In Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming. World Scientific, pp. 14-32.

HANS, W., LOOGEN, R., AND WINKLER, S. 1992. On the interaction of lazy evaluation and backtracking. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (PLILP'92). Lecture Notes in Computer Science, vol. 631. Springer-Verlag, New York, pp. 355-369.

HANUS, M. 1990. Compiling logic programs with equality. In Proceedings of the 2nd International Workshop on Programming Language Implementation and Logic Programming (PLILP'90). Lecture Notes in Computer Science, vol. 456. Springer-Verlag, New York, pp. 387-401.

HANUS, M. 1992. Improving control of logic programs by using functional logic languages. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (PLILP'92). Lecture Notes in Computer Science, vol. 631. Springer-Verlag, New York, pp. 1-23.

HANUS, M. 1994. The integration of functions into logic programming: From theory to practice. J. Logic Prog. 19&20, 583-628.

HANUS, M. 1995. Efficient translation of lazy functional logic programs into Prolog. In Proceedings of the 5th International Workshop on Logic Program Synthesis and Transformation (LOPSTR'95). Lecture Notes in Computer Science, vol. 1048. Springer-Verlag, New York, pp. 252-266.

HANUS, M. 1997. A unified computation model for functional and logic programming. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Paris, France). ACM, New York, pp. 80-93.

HANUS, M. ED. 1999. Curry: An integrated functional logic language. Available at http: //www.i2. informatik.rwth-aachen.de/~hanus/curry.

HANUS, M., LUCAS, S., AND MIDDELDORP, A. 1998. Strongly sequential and inductively sequential term rewriting systems. Inf. Proc. Lett. 67, 1, 1-8.

HANUS, M., AND PREHOFER, C. 1996. Higher-order narrowing with definitional trees. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA '96). Lecture Notes in Computer Science, vol. 1103. Springer-Verlag, New York, pp. 138-152.

HANUS, M., AND SADRE, R. 1999. An abstract machine for Curry and its concurrent implementation in Java. J. Funct. Logic Prog. 6.

HEROLD, A. 1986. Narrowing techniques applied to idempotent unification. Tech. Rep. SR-86-16. SEKI.

HOLLDOBLER, S. 1989. Foundations of Equational Logic Programming. Lecture Notes in Computer Science, vol. 353. Springer-Verlag, New York.

HUET, G., AND HULLOT, J.-M. 1982. Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci. 25, 239-266.

HUET, G., AND LEVY, J.-J. 1991. Computations in orthogonal term rewriting systems. In Computational logic: Essays in honour of Alan Robinson, J.-L. Lassez and G. Plotkin, eds. MIT Press, Cambridge, Mass., pp. 395-443.

HULLOT, J.-M. 1980. Canonical forms and unification. In Proceedings of the 5th Conference on Automated Deduction.

IDA, T., AND NAKAHARA, K. 1997. Leftmost outside-in narrowing calculi. J. Funct. Prog. 7, 2, 129-161.

JIMENEZ-MARTIN, J. A., MARINIO-CARBALLO, J., AND MORENO-NAVARRO, J. J. 1992. Efficient compilation of lazy narrowing into prolog. In Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR'92). Springer Workshops in Computing Series. Springer-Verlag, New York, pp. 253-270.

KENNAWAY, J. R. 1990. The specificity rule for lazy pattern-matching in ambiguous term rewrite systems. In Proceedings of the 3rd European Symposium on Programming (ESOP'90). Lecture Notes in Computer Science, vol. 432. Springer-Verlag, New York, pp. 256-270.

KENNAWAY, J. R., KLOP, J. K., SLEEP, M. R., AND DE VRIES, F. J. 1993. The adequacy of term graph rewriting for simulating term rewriting. In Term Graph Rewriting Theory and Practice. M. R. Sleep, M. J. Plasmeijer, and M. C. J. D. van Eekelen, eds. Wiley, Chichester, UK.

KLOP, J. W. 1992. Term rewriting systems. In Handbook of Logic in Computer Science, Vol. II. S. Abramsky, D. Gabbay, and T. Maibaum, eds. Oxford University Press, Oxford, England.

KLOP, J. W., AND MIDDELDORP, A. 1991. Sequentiality in orthogonal term rewriting systems. J. Symb. Comput., 161-195.

LOOGEN, R., LOPEZ FRAGUAS, F., AND RODRIGUEZ ARTALEJO, M. 1993. A demand driven computation strategy for lazy narrowing. In Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming (PLILP'93). Lecture Notes in Computer Science, vol. 714. Springer-Verlag, New York, pp. 184-200.

MARANGET, L. 1991. Optimal derivation in weak lambda-calculi and in orthogonal term rewriting systems. In Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages (Orlando, Fla., Jan. 21-23). ACM, New York, pp. 255-269.

MIDDELDORP, A., AND HAMOEN, E. 1994. Completeness results for basic narrowing. Applic. Algebra Eng. Commun. Comput. 5, 213-253.

MIDDELDORP, A., AND OKUI, S. 1998. A deterministic lazy narrowing calculus. J. Symb. Comput. 25, 6, 733-757.

MIDDELDORP, A., OKUI, S., AND IDA, T. 1996. Lazy narrowing: Strong completeness and eager variable elimination. Theoret. Comput. Sci. 167, 1,2, 95-130.

MORENO-NAVARRO, J. J., KUCHEN, H., LOOGEN, R., AND RODRIGUEZ-ARTALEJO, M. 1990. Lazy narrowing in a graph machine. In Proceedings of the 2nd International Conference on Algebraic and Logic Programming (ALP'90). Lecture Notes in Computer Science, vol. 463. Springer-Verlag, New York, pp. 298-317.

MORENO-NAVARRO, J. J., AND RODRIGUEZ-ARTALEJO, M. 1992. Logic programming with functions and predicates: The language BABEL. J. Logic Prog. 12, 191-223.

MORENO-NAVARRO, J. J., KUCHEN, H., MARINO-CARBALLO, J., WINKLER, S., AND HANS, W. 1993. Efficient lazy narrowing using demandedness analysis. In Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming (PLILP'93). Lecture Notes in Computer Science, vol. 714. Springer-Verlag, New York, pp. 167-183.

NAKAHARA, K., MIDDELDORP, A., AND IDA, T. 1995. A complete narrowing calculus for higher-order functional logic programming. In Proceedings of the 7th International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP'95). Lecture Notes in Computer Science, vol. 982. Springer-Verlag, New York, pp. 97-114.

NIEUWENHUIS, R. 1995. On narrowing, refutation proofs and constraints. In Rewriting Techniques and Applications, 6th International Conference, RTA-95. Jieh Hsiang, ed. (Kaiserslautern, Germany, April 5-7). Lecture Notes in Computer Science, vol. 914. Springer-Verlag, New York, pp. 56-70.

NUTT, W., RETY, P., AND SMOLKA, G. 1989. Basic narrowing revisited. J. Symb. Comput. 7, 295-317.

O'DONNELL, M. J. 1977. Computing in Systems Described by Equations. Lecture Notes in Computer Science, vol. 58. Springer-Verlag, New York.

O'DONNELL, M. J. 1985. Equational Logic as a Programming Language. MIT Press, Cambridge, Mass.

PADAWITZ, P. 1988. Computing in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, New York.

PLASMEIJER, R., AND VAN EEKELEN, M. 1993. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Reading, Mass.

PLOTKIN, G. D. 1972. Building-in equational theories. Mach. Int. 7, 73-90.

REDDY, U.S. 1985. Narrowing as the operational semantics of functional languages. In Proceedings of the IEEE International Symposium on Logic Programming (Boston, Mass.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 138-151.

SEKAR, R. C., AND RAMAKRISHNAN, I. V. 1993. Programming in equational logic: Beyond strong sequentiality. Inf. Comput. 104, 1, 78-109.

SLAGLE, J. R. 1974. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. J. ACM 21, 4 (Oct.), 622-642.

SLEEP, M. R., PLASMEIJER, M. J., AND VAN EEKELEN, M. C. J. D. EDS. 1993. Term Graph Rewriting Theory and Practice. Wiley, Chichester, UK.

THIEL, J. J. 1984. Stop losing sleep over incomplete data type specifications. In Proceedings of the 11th ACM Symposium on Principles of Programming Languages (Salt Lake City, Ut., Jan. 15-18). ACM, New York, pp. 76-82.

ULLAN HERNANDEZ, E. 1995. A lazy narrowing abstract machine. Tech. rep. DIA/95/3. Univ. Complutense, Madrid, Spain.

WADLER, P. 1985. How to replace failure by a list of successes. In Functional Programming and Computer Architecture. Lecture Notes in Computer Science, vol. 201. Springer-Verlag, New York, pp. 113-128.

WARREN, D. H. D. 1982. Higher-order extensions to prolog: are they needed? Mach. Intell. 10, 441-454.

You, J.-H. 1991. Unification modulo an equality theory for equational logic programming. J. Comput. Syst. Sci. 42, 1, 54-75.

RECEIVED SEPTEMBER 1994; REVISED DECEMBER 1999; ACCEPTED JANUARY 2000

SERGIO ANTOY Portland State University, Portland Oregon

RACHID ECHAHED Laboratoire LEIBNIZ, Institut IMAG, Grenoble, France

AND

MICHAEL HANUS Christian-Albrechts-Universitat zu Kiel, Germany

A preliminary version of this paper appeared in the Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (Portland, Ore., Jan. 17-21). ACM, New York, pp. 268-279.

The Oregon Center for Advanced Technology Education (OCATE) supported in part the collaborative efforts that lead to the writing of this paper.

Sergio Antoy was supported in part by the National Science Foundation grants CCR-9406751. Michael Hanus was supported in part by the German Ministry for Research and Technology (BMFT) under grant ITS 9103, by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics), and by the German Research Council (DFG) under grant Ha 2457/1-1.

Authors' addresses: S. Antoy, Department of Computer Science, Portland State University, P.O. Box 751, Portland, OR 97207, e-mail: antoy@cs.pdx.edu; Rachid Echahed, IMAG-Leibniz, CNRS, 46, avenue Felix Viallet, F-38031 Grenoble, France, e-mail: echahed@imag.fr; and Michael Hanus, Institut fur Informatik und Praktische Mathematik, Christian-Albrechts-Universitat zu Kiel, D-24098 Kiel, Germany, e-mail: mh@informatik.uni-kiel.de.

Permission to make digital/hard copy of part or all of this work for personal or classroom use is granted without fee provided that the copies are not made or distributed for profit or commercial advantage, the copyright notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery (ACM), Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee.

[C] 2000 ACM 0004-5411/00/0700-0776 $05.00

Printer friendly Cite/link Email Feedback | |

Author: | ANTOY, SERGIO; ECHAHED, RACHID; HANUS, MICHAEL |
---|---|

Publication: | Journal of the Association for Computing Machinery |

Geographic Code: | 4EUFR |

Date: | Jul 1, 2000 |

Words: | 26833 |

Previous Article: | Balanced Sequences and Optimal Routing. |

Next Article: | A Bill of Rights and Responsibilities. |

Topics: |