Narrowing Strategies for Arbitrary Canonical Rewrite Systems

Alexander Bockmayr Stefan Krischer Andreas Werner

MPI–I–94–233 July 1993 Authors’ Addresses

Alexander Bockmayr, Max-Planck-Institut für Informatik, Im Stadtwald, D-66123 Saarbrücken, bockmayr@mpi-sb.mpg.de Stefan Krischer, CRIN & INRIA-Lorraine, B.P.239, F-54506 Vandœuvre-lès-Nancy, krischer@loria.fr Andreas Werner, SFB 314, Univ. Karlsruhe, D-76128 Karlsruhe, werner@ira.uka.de

Publication Notes

The present report has been submitted for publication elsewhere and will be copyrighted if accepted.

Acknowledgements

The first author’s work was supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9103. The second author’s work was supported by the Centre National de Recherche Scientifique (CNRS), departement Science pour l’Ingenieur. The third author’s work was supported by the Deutsche Forschungsgemeinschaft as part of the SFB 314 (project S2).

Abstract

Narrowing is a universal unification procedure for equational theories defined by a canonical term rewriting system. In its original form it is extremely inefficient. Therefore, many optimizations have been proposed during the last years. In this paper, we present the narrowing strategies for arbitrary canonical systems in a uniform framework and introduce the new narrowing strategy LSE narrowing. LSE narrowing is complete and improves all other strategies which are complete for arbitrary canonical systems. It is optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. Moreover, LSE narrowing computes only normalized narrowing substitutions.

Contents

1 Introduction 2 2 Preliminaries 3 3 Narrowing: The Basic Idea 4 4 Left-to-Right Basic Narrowing 8

4.1 Basic Narrowing . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2 Left-to-Right Basic Narrowing . . . . . . . . . . . . . . . . . . . . 9 4.3 SL Left-to-Right Basic Narrowing . . . . . . . . . . . . . . . . . . 10

5 LSE Narrowing 11 6 Normalizing LSE Narrowing 16

6.1 Normalizing Narrowing . . . . . . . . . . . . . . . . . . . . . . . 16 6.2 Normalizing LSE Narrowing . . . . . . . . . . . . . . . . . . . . . 18 6.3 Normalizing LSE and SL Left-to-Right Basic Narrowing . . . . . 21

7 Empirical Results 23

7.1 Comparing all narrowing strategies for a functional term rewrite

system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 7.2 Comparing the best narrowing strategies for a arbitrary canoni-

cal system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 8 Conclusion 28

1 Introduction

Narrowing is known as a complete unification procedure for any equational theory that can be defined by a canonical term rewriting system [Fay79, Hul80]. It is also the operational semantics of various logic and functional programming languages. In its original form, narrowing is extremely inefficient [Boc86]. Therefore, many optimizations have been proposed during the last years [Hul80, RKKL85, Fri85, Her86, Rét87, NRS89, BGM88, Ech88, Rét88, Boc88, You88, Pad88, Höl89, DG89, You91].

In this paper, we present the narrowing strategies for arbitrary canonical term rewrite systems in a uniform framework and introduce the new narrowing strategy LSE narrowing together with its normalizing variant normalizing LSE narrowing. LSE narrowing is complete and improves all previously known strategies which are complete for arbitrary canonical systems, such as left-to-right basic narrowing and the sufficient largeness condition of [Rét87]. It is optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. Moreover, there is a one-to-one correspondence between LSE narrowing derivations and a special form of leftmostinnermost rewriting derivations. Finally, LSE narrowing computes only normalized narrowing substitutions.

We are interested in arbitrary canonical term rewriting systems that do not have to satisfy additional properties such as constructor discipline [Fri85], leftlinearity or non-overlapping left-hand sides [You88, You91, DG89]. For special classes of term rewrite systems, narrowing strategies which are not complete in the general case may be more efficient than LSE narrowing.

For arbitrary canonical systems, the most efficient complete narrowing strategy known before was normalizing SL left-to-right basic narrowing [Rét87]. An analysis of Réty’s approach shows that it can be considerably improved if the term rewriting system has non-regular rules and overlapping left-hand sides. In this case various redundancies in the narrowing process can be avoided. LSE narrowing uses three reducibility tests to detect redundant narrowing derivations. The three tests are more powerful than Réty’s test for sufficient largeness. Moreover, they imply that any LSE narrowing derivation is also a SL left-to-right basic narrowing derivation. The converse, however, is not true.

The organization of the paper is as follows. After some preliminaries in Section 2, we recall in Section 3 the basic idea of narrowing and give a detailed proof of the well-known lifting lemma of Hullot [Hul80] which establishes a fundamental relationship between rewriting and narrowing derivations. In Section 4, we discuss basic narrowing, left-to-right basic narrowing, and SL left-to-right basic narrowing. While a leftmost-innermost rewriting derivation always generates a SL left-to-right basic narrowing derivation, the converse is not true. In Section 5, we introduce the narrowing strategy LSE narrowing and show that there is a one-to-one correspondence between LSE narrowing derivations and left reductions, which are a special form of leftmost-innermost rewriting derivations. Using this correspondence, we can give very simple proofs of the completeness of LSE narrowing and the optimality property that no narrowing substitution can be generated twice. Moreover, we show that LSE narrowing generates only normalized narrowing substitutions. In Section 6, we present the normalizing form of LSE narrowing. The same results hold as in the non-normalizing case. The proofs, however, are more complicated. Finally, in Section 7, we present some empirical results which illustrate the various strategies.

This paper is the full version of [BKW92]. It unifies and simplifies our previous results in [KB91] and [Wer91].

2 Preliminaries

We recall briefly some basic notions that are needed in the sequel. More details can be found in the survey of [HO80].

Σ = (S, F) denotes a signature with a set S of sort symbols and a set F of function symbols together with an arity function.

A Σ-algebra A consists of a family of non-empty sets (A_{s})_{s∈S} and a family of functions (f^{A})_{f∈F} such that if f : s_{1} × … × s_{n} → s then f^{A} : A_{s_{1}} × … × A_{s_{n}} → A_{s}.

X represents a family (X_{s})_{s∈S} of countably infinite sets X_{s} of variables of sort s. T (F, X) is the Σ-algebra of terms with variables over Σ.

For a term t ∈ T (F, X), Var(t), Occ(t), and F uOcc(t) denote the set of variables, occurrences and non-variable occurrences in t respectively. The root of a term is denoted by the empty occurrence ϵ. An occurence ω is a prefix of an occurrence ω′, ω ⪯ ω′, iff there exists υ ∈ N^{∗} such that ω′ = ω.υ. We denote by t/ω the subterm of t at position ω ∈ Occ(t) and by t[ω ← s] the term obtained from t by replacing the subterm t/ω with the term s ∈ T (F, X).

A substitution σ : X → T (F, X) is a family of mappings σ_{s} : X_{s} → T (F, X)_{s}, s ∈ S, which are different from the identity id only for a finite subset Dom(σ) of X. We do not distinguish σ from its canonical extension to T (F, X). Im(σ) =^{def} ⋃_{x∈Dom(σ)} Var(σ(x)) is the set of variables introduced by σ. If σ is a substitution and V is a set of variables then the restriction σ|_{V} of σ to V is

defined by σ|_{V} (x) = \{ \begin{matrix}σ(x) & if x ∈ Dom(σ) ∩ V \\ x & else \end{matrix} .

A syntactic unifier of two terms s, t is a substitution σ such that σ(s) = σ(t). A most general syntactic unifier of s and t is a unifier σ of s and t with Dom(σ) ∩ Im(σ) = ∅ such that for any other unifier τ of s and t there exists a substitution λ with λ ∘ σ = τ.

A binary relation →= (→_{s})_{s∈S} on a Σ-algebra A is Σ-compatible iff t_{1} → υ_{1}, …, t_{n} → υ_{n} implies f^{A}(t_{1}, …, t_{n}) → f^{A}(υ_{1}, …, υ_{n}) for all t_{i}, υ_{i} ∈ A_{s_{i}} and all f : s_{1} × … × s_{n} → s in F. By →^{∗} we denote the reflexive-transitive closure of →. A congruence is a Σ-compatible equivalence relation.

An equation is an expression of the form s ≐ t where s and t are terms of T (F, X) belonging to the same sort. A system of equations G is an expression of the form s_{1} ≐ t_{1} ∧ … ∧ s_{n} ≐ t_{n}, n ≥ 1 with equations s_{i} ≐ t_{i}, i = 1, …, n.

Let E be a set of equations. The equational theory ≡_{E} associated with E is the smallest congruence ≡ on T (F, X) such that σ(l) ≡ σ(r) for all equations l ≐ r in E and all substitutions σ. Given two substitutions σ, τ : X → T (F, X) and a set of variables V we write σ = τ [V] iff σ(x) = τ(x), for all x ∈ V, and σ ≡_{E} τ [V] iff σ(x) ≡_{E} τ(x), for all x ∈ V. E-subsumption of substitutions is defined by σ ≤_{E} τ [V] iff there is a substitution λ with τ(x) ≡_{E} λ(σ(x)) for all x ∈ V.

A rewriting rule π is an expression of the form l → r with terms l, r ∈ T (F, X) of the same sort such that Var(r) ⊆ Var(l) and l ∉ X. The rule is regular iff Var(l) = Var(r). The rule is left-linear iff no variable occurs twice in l. A term rewriting system R is a set of rewriting rules. The equational theory ≡_{R} generated by R is obtained by considering for every rule l → r in R the corresponding equation l ≐ r.

The reduction relation →_{R} associated with R is defined as follows: s →_{R} t, more precisely s →_{[υ,l→r,τ]} t, iff there is an occurrence υ ∈ Occ(s) and a rule l → r in R such that there exists a substitution τ : X → T (F, X) with τ(l) = s/υ and t = s[υ ← τ(r)]. R is confluent iff for any terms s, t_{1}, t_{2} with s →^{∗}_{R} t_{1} and s →^{∗}_{R} t_{2} there exists a term u with t_{1} →^{∗}_{R} u and t_{2} →^{∗}_{R} u. R is noetherian iff there exists no infinite chain t_{1} →_{R} t_{2} →_{R} … →_{R} t_{n} →_{R} . . .. R is canonical iff R is confluent and noetherian.

A term t is irreducible or normalized iff there exists no term u such that t →_{R} u. Otherwise t is called reducible. A substitution σ is normalized iff for any x ∈ X the term σ(x) is irreducible. If R is canonical then there exists for any term t a unique irreducible term t↓ such that t →^{∗}_{R} t↓. t↓ is called the normal form of t. For any two terms s, t, we have s ≡_{R} t iff s↓ = t↓.

3 Narrowing: The Basic Idea

Narrowing provides a complete E-unification procedure for any equational theory E that can be defined by a canonical term rewrite system.

Definition 3.1 Let E be a set of equations. A system of equations G

s_{1} ≐ t_{1} ∧ … ∧ s_{n} ≐ t_{n}, n ≥ 1,

is called E-unifiable iff there exists a substitution σ : X → T (F, X) such that

σ(s_{1}) ≡_{E} σ(t_{1}), …, σ(s_{n}) ≡_{E} σ(t_{n}).

The substitution σ is called an E-unifier of G.

A set cU_{E}(G) of substitutions is called a complete set of E-unifiers of G iff

• every σ ∈ cU_{E}(G) is an E-unifier of G

• for any E-unifier τ of G there is σ ∈ cU_{E}(G) such that σ ≤_{E} τ [Var(G)]

• for all σ ∈ cU_{E}(G) : Dom(σ) ⊆ Var(G).

cU_{E}(G) is called minimal iff it satisfies further the condition

• for all σ, σ′ ∈ cU_{E}(G) : σ ≤_{E} σ′ [Var(G)] implies σ = σ′.

Narrowing allows to find complete sets of E-unifiers for equational theories E that can be defined by a canonical term rewrite system R by associating with every rule l → r in R the equation l ≐ r in E. The basic idea is as follows. Suppose we want to R-unify a system of equations s_{1} ≐ t_{1} ∧ … ∧ s_{n} ≐ t_{n}. This means that we have to find a substitution σ such that

σ(s_{1}) ≡_{R} σ(t_{1}), …, σ(s_{n}) ≡_{R} σ(t_{n}).  (1)

Since R is a canonical term rewriting system this is equivalent to

σ(s_{1})↓ = σ(t_{1})↓, …, σ(s_{n})↓ = σ(t_{n})↓.  (2)

If the problem has a solution σ, then either σ is a syntactic unifier of G, which can be computed by standard unification, or σ does not syntactically unify G. In this case the system of equations σ(G) must be reducible by R since otherwise it would be impossible to have (2). The idea is now to lift the rewriting derivation σ(G) → … → σ(G)↓ on the unknown instance σ(G) of G to a narrowing derivation G −∧∨→_{δ_{1}} … −∧∨→_{δ_{n}} G_{n} on the given system G such that the last system of equations G_{n} is syntactically unifiable with most general unifier τ and τ ∘ δ_{n} ∘ … ∘ δ_{1} ≤_{R} σ [V ar(G)]. This lifting is done by constructing substitutions δ_{1}, …, δ_{n} such that δ_{1}(G), …, δ_{n}(G_{n−1}) become reducible.

Definition 3.2 (Narrowing) Let R be a term rewriting system. A system of equations G is narrowable to a system of equations G′ with narrowing substitution δ,

G −∧∨→_{[υ,l→r,δ]} G′,

iff there exist a non-variable occurrence υ ∈ Occ(G) and a rule l → r in R such that G/υ and l are syntactically unifiable with most general unifier δ and G′ = δ(G)[υ ← δ(r)]. We always assume that V ar(l) ∩ V ar(G) = ∅.

A narrowing derivation G_{0} −∧∨→_{σ}^{∗} G_{n} with narrowing substitution σ is a sequence of narrowing steps G_{0} −∧∨→_{δ_{1}} G_{1} −∧∨→_{δ_{2}} … −∧∨→_{δ_{n}} G_{n}, n ≥ 0, where σ = (δ_{n} ∘ … ∘ δ_{1}) |_{Var(G)}. The narrowing substitution leading from G_{i} to G_{j}, for 0 ≤ i ≤ j ≤ n, will be denoted by

λ_{i,j} =^{def} δ_{j} ∘ … ∘ δ_{i+1}.

In particular, λ_{i,i} = id, for i = 0, …, n.

A narrowing strategy S is a property of narrowing derivations. We say that S-narrowing is complete iff for any canonical term rewriting system R and any system of equations G the set of all substitutions σ such that there exists a S-narrowing derivation G = G_{0}−∧∨→_{δ_{1}} … −∧∨→_{δ_{n}}G_{n}, n ≥ 0, such that G_{n} is syntactically unifiable by a most general unifier τ and σ = τ ∘δ_{n} ∘…∘δ_{1} |_{Var(G)}, is a complete set of R-unifiers of G.

In order to treat syntactical unification as a narrowing step, we introduce a new rule

x ≐ x → true,

where x denotes a variable. Then t ≐ t′ −∧∨→_{δ} true holds if and only if t and t′ are syntactically unifiable with most general unifier δ. This additional rule is called ϵ-rule (since it can be applied only at occurrence ϵ) and affects neither confluence nor termination. Obviously, σ is a solution of G if and only if σ(G) can be reduced by the rules in R and the ϵ−rule to the trivial system true ∧ … ∧ true.

Now we are able to formulate the fundamental relationship between rewriting and narrowing derivations that will provide the basis for most of the proofs in this paper.

Proposition 3.3 (Hullot 80) Let R be a term rewriting system and let G be a system of equations. If μ is a normalized substitution and V a set of variables such that Var(G) ∪ Dom(μ) ⊆ V, then for every rewriting derivation

H_{0} =^{def} μ(G) →_{[υ_{1},l_{1}→r_{1},τ_{1}]} H_{1} … →_{[υ_{n},l_{n}→r_{n},τ_{n}]} H_{n}  (3)

there exist a normalized substitution λ and a narrowing derivation

G_{0} =^{def} G −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} … −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n}  (4)

using the same rewrite rules at the same occurrences such that

μ = λ ∘ δ_{n} ∘ … ∘ δ_{1} [V] and  (5)
H_{i} = (λ ∘ δ_{n} ∘ … ∘ δ_{i+1}) (G_{i}), for all i = 0, …, n.  (6)

Conversely, if μ =^{def} λ∘δ_{n} ∘…∘δ_{1} then there exists for any narrowing derivation (4) and any substitution λ a rewriting derivation (3) such that (6) holds.

Proof: The proof is similar to [Hul80] and uses induction on n. The technical details, however, are different.

First assume that we are given the rewriting derivation (3) of length n. If n = 0, we can choose λ = μ. So suppose n > 0 and μ(G) →_{[υ_{1},l_{1}→r_{1},τ_{1}]} H_{1} → … → H_{n}. Then

μ(G)/υ_{1} = τ_{1}(l_{1}) and H_{1} = μ(G)[υ_{1} ← τ_{1}(r_{1})]. Since μ(x) is irreducible for all x ∈ V we get υ_{1} ∈ F uOcc(G) and μ(G)/υ_{1} = μ(G/υ_{1}). Since we may assume that V and l_{1} have no variables in common and that Dom(τ_{1}) ⊆

V ar(l_{1}), the substitution ϕ =^{def} τ_{1} ⊎ μ =^{def} \{ \begin{matrix}μ(x), & if x ∈ Dom(μ) \\ τ_{1}(x), & if x ∈ Dom(τ_{1}) \end{matrix} is well-

defined and ϕ(G/υ_{1}) = ϕ(l_{1}). This means that ϕ is a syntactic unifier of G/υ_{1} and l_{1}. Let δ_{1} be a most general syntactic unifier of G/υ_{1} and l_{1} with Dom(δ_{1}) ⊆ Var(G/υ_{1}) ∪ Var(l_{1}). Then there exists a substitution ρ with Dom(ρ) ⊆ (((Dom(τ_{1}) ∪ Dom(μ)) \ Dom(δ_{1})) ∪ Im(δ_{1}) such that ϕ = ρ ∘ δ_{1} [V ∪ Var(l_{1})]. It follows

G −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1}

with G_{1} =^{def} δ_{1}(G[υ_{1} ← r_{1}]).

Next we show that the substitution ρ is normalized. Suppose there exists a variable x ∈ Dom(ρ) such that ρ(x) is reducible. Since μ is normalized we get x ∈ (Dom(τ_{1}) \ Dom(δ_{1})) ∪ Im(δ_{1}) . If x ∈ Dom(τ_{1})\Dom(δ_{1}) then x ∈ Var(l_{1}) and since δ_{1}(x) = x, we get x ∈ δ_{1}(l_{1}). If x ∈ Im(δ_{1}), then it follows from Dom(δ_{1}) ⊆ Var(G/υ_{1}) ∪ Var(l_{1}) that x occurs in δ_{1}(l_{1}) or δ_{1}(G/υ_{1}). But since δ_{1}(l_{1}) = δ_{1}(G/υ_{1}), in both cases x must occur in δ_{1}(G/υ_{1}). So there exists a variable y ∈ G such that x occurs in δ_{1}(y). Then ρ(x) is a subterm of (ρ ∘ δ_{1})(y). This implies that (ρ ∘ δ_{1})(y) = μ(y) is reducible in contradiction to the fact that μ is normalized.

Now ρ(G_{1}) = ρ(δ_{1}(G[υ_{1} ← r_{1}])) = (ρ ∘ δ_{1})(G[υ_{1} ← r_{1}]) = ϕ(G[υ_{1} ← r_{1}]) =

ϕ(G)[υ_{1} ← ϕ(r_{1})] = μ(G)[υ_{1} ← τ_{1}(r_{1})] = H_{1} →_{[υ_{2},l_{2}→r_{2},τ_{2}]} H_{2} →^{∗} H_{n}, with ρ

normalized. Let V′ =^{def} V ∪ Im(δ_{1}). Then by induction hypothesis there exists a substitution λ and a narrowing derivation

G_{1} −∧∨→_{[υ_{2},l_{2}→r_{2},δ_{2}]} … −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n}

such that ρ = λ ∘ δ_{n} ∘ … ∘ δ_{2} [V′] and

H_{i} = (λ ∘ δ_{n} ∘ … ∘ δ_{i+1})(G_{i}),

for 1 ≤ i ≤ n. By the variable disjointness of V and l_{1} we get μ = ρ ∘ δ_{1} [V]. From V′ = V ∪ Im(δ_{1}) and ρ = λ ∘ δ_{n} ∘ … ∘ δ_{2} [V′] we conclude ρ ∘ δ_{1} = λ ∘ δ_{n} ∘ … ∘ δ_{1} [V] . Together this implies

μ = λ ∘ δ_{n} ∘ … ∘ δ_{1} [V]

and in particular

H_{0} = μ(G_{0}) = (λ ∘ δ_{n} ∘ … ∘ δ_{1})(G_{0}).

The reverse direction is again proved by induction.

The case n = 0 is trivial. Assume therefore n > 0. Let λ be a substitution and

G −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},l_{2}→r_{2},δ_{2}]} … −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n}

a narrowing derivation. Consider the substitution ν =^{def} λ ∘ δ_{n} ∘ … ∘ δ_{2}. Then it follows from the induction hypothesis that ν(G_{1}) = H_{1} → … → H_{n} with H_{i} = λ ∘ δ_{n} ∘ … ∘ δ_{i+1}(G_{i}), for i = 1, …, n. From G −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} we get δ_{1}(G/υ_{1}) = δ_{1}(l_{1}) and G_{1} = δ_{1}(G[υ_{1} ← r_{1}]) = δ_{1}(G)[υ_{1} ← δ_{1}(r_{1})]. This means δ_{1}(G) →_{[υ_{1},l_{1}→r_{1},δ_{1}|_{Var(l_{1})}]} G_{1} . Since → is stable under substitutions we obtain μ(G) = (ν ∘ δ_{1})(G) → ν(G_{1}) = H_{1} →^{∗} H_{n}. This proves the proposition. □

Proposition 3.4 A narrowing strategy S is complete if for any canonical term rewriting system R, any system of equations G, and any normalized R-unifier μ of G there exists a rewriting derivation μ(G) →^{∗} true ∧ … ∧ true such that the corresponding narrowing derivation (according to Proposition 3.3) is a Sderivation.

Proof: Given R and G let U denote the set of all substitutions σ such that there exists a S-narrowing derivation G = G_{0}−∧∨→_{δ_{1}} … −∧∨→_{δ_{n}}G_{n}, n ≥ 0, such that G_{n} is of the form true ∧ … ∧ true and σ = (δ_{n} ∘ … ∘ δ_{1}) |_{Var(G)}.

We will show that U is a complete set of R-unifiers of G.

By definition, we have Dom(σ) ⊆ Var(G). Suppose that σ ∈ U. Then there exists a narrowing derivation G = G_{0} −∧∨→_{δ_{1}} … −∧∨→_{δ_{n}} G_{n}, n ≥ 0, such that G_{n} is of the form true ∧ … ∧ true and σ = (δ_{n} ∘ … ∘ δ_{1}) |_{Var(G)}. By Proposition 3.3, there exists a rewriting derivation σ(G) = H_{0} →_{[l_{1}→r_{1},υ_{1}]} H_{1} … →_{[υ_{n},l_{n}→r_{n}]} H_{n} such that H_{i} = (δ_{n} ∘ … ∘ δ_{i+1})(G_{i}), for i = 0, …, n. In particular, we get H_{n} = G_{n} = true ∧ … ∧ true which implies that σ is a R-unifier of G.

Now let μ be an arbitrary R-unifier of G and μ^{↓} its normal form, that is μ^{↓}(x) =^{def} μ(x)↓, for all x ∈ X. Then there exists a rewriting derivation μ^{↓}(G) = H_{0} →^{∗} H_{n} = true ∧ … ∧ true such that the corresponding narrowing derivation (according to Proposition 3.3) G = G_{0}−∧∨→_{δ_{1}} … −∧∨→_{δ_{n}}G_{n}, is a S-derivation. Furthermore, there is a substitution λ such that μ^{↓} = λ ∘ δ_{n} ∘ … ∘ δ_{1} [V ar(G)]. By definition, the substitution σ =^{def} (δ_{n} ∘ … ∘ δ_{1}) |_{V ar(G)} belongs to the set of substitutions U and σ ≤ μ^{↓} ≡_{R} μ [V ar(G)]. □

Putting the two preceding propositions together, we get immediately the completeness of naive narrowing.

Theorem 3.5 Narrowing is complete.

We close this section with a technical lemma that we will need in the sequel.

Definition 3.6 Two systems of equations G, G′ are identical up to variable renaming iff there exist substitutions τ, τ′ such that τ(G) = G′ and τ′(G′) = G.

Lemma 3.7 Let G_{0} and G′_{0} be two systems of equations which are identical up to variable renaming. If G_{0}−∧∨→_{[υ,l→r,δ]}G_{1} and G′_{0}−∧∨→_{[υ,l→r,δ′]}G′_{1}, then G_{1} and G′_{1} are also identical up to variable renaming.

Proof: Suppose that τ_{0}(G_{0}) = G′_{0} and τ′_{0}(G′_{0}) = G_{0}, for some substitutions τ_{0}, τ′_{0} with Dom(τ_{0}) ⊆ V ar(G_{0}) and Dom(τ′_{0}) ⊆ V ar(G′_{0}).

By definition, G_{1} = δ(G_{0}[υ ← r]) and G′_{1} = δ′(G′_{0}[υ ← r]) with a most general unifier δ of G_{0}/υ and l and a most general unifier δ′ of G′_{0}/υ and l. Since G_{0}/υ = τ′_{0}(G′_{0})/υ and G′_{0}/υ = τ_{0}(G_{0})/υ we can conclude from Dom(τ_{0})∩ Var(l) = Dom(τ′_{0}) ∩ Var(l) = ∅ that δ(τ′_{0}(l)) = δ(l) = δ(G_{0}/υ) = δ(τ′_{0}(G′_{0}/υ)) and similarly δ′(τ_{0}(l)) = δ′(l) = δ′(G′_{0}/υ) = δ′(τ_{0}(G_{0}/υ)). Hence δ ∘ τ′_{0} unifies G′_{0}/υ and l and δ′∘τ_{0} unifies G_{0}/υ and l. Since δ and δ′ are most general unifiers, there exist substitutions τ_{1} and τ′_{1} with τ_{1} ∘ δ = δ′ ∘ τ_{0} and τ′_{1} ∘ δ′ = δ ∘ τ′_{0}. It follows τ_{1}(G_{1}) = τ_{1}(δ(G_{0}[υ ← r])) = δ′(τ_{0}(G_{0}[υ ← r])) = δ′(τ_{0}(G_{0})[υ ← τ_{0}(r)]) = δ′(G′_{0}[υ ← r]) = G′_{1} and similarly τ′_{1}(G′_{1}) = G_{1}. This shows that G_{1} and G′_{1} are identical up to variable renaming. □

[figure: \begin{aligned}& & q(x) ._{=}s(0) \\ & 0 ._{=}s(0) & & s((q(y)+y)+y) ._{=}s(0) \\ s(q(0)+0) ._{=}s(0) & s(q(0)+0) ._{=}s(0) & s(s(q(z))+s(z)+z) ._{=}s(0) & s(s(q(z))+z+s(z)) ._{=}s(0) & s(0+0+0) ._{=}0 & s(s(q(z)+z+z)+s(z)+s(z)) ._{=}s(0) \end{aligned}; x/0; x/s(y); y/0; y/0; y/s(z); y/s(z); y/0; y/s(z); z/s(u); z/s(u); u/0; z/s(u); z/s(u); z/s(u); u/0; z/s(u); u/0; z/s(u); u/0; z/0; z/s(u); z/s(u); z/s(u); z/s(u)]

Figure 1: Narrowing tree for q(x) ≐ s(0)

4 Left-to-Right Basic Narrowing

Narrowing in its original form is extremely inefficient [Boc86].

Example 4.1 Consider the canonical rewrite system

\begin{aligned}R & = \{ & x + 0 → x, & x + s(y) → s(x + y), \\ & & q(0) → 0, & q(s(x)) → s((q(x) + x) + x)\} \end{aligned}

for adding and squaring natural numbers and suppose we want to solve the query q(x) ≐ s(0). The corresponding narrowing tree is given in Fig. 1.

The example shows that on different pathes in the search tree the same narrowing substitution is generated again and again. The narrowing substitution, however, is the only interesting information obtained in a narrowing derivation. If there are two derivations G−∧∨→_{σ_{1}}^{∗}G_{1} and G−∧∨→_{σ_{2}}^{∗}G_{2} such that σ_{1} = σ_{2} [Var(G)], then G_{1} ≡_{R} G_{2} independently of the narrowing occurrences and the rules that have been selected. In this case, one of the two derivations is redundant.

If μ is a normalized R-unifier of the system of equations G, then any rewriting derivation μ(G) →^{∗} true ∧ … ∧ true can be lifted to a narrowing derivation G −∧∨→_{σ}^{∗} true ∧ … ∧ true such that the narrowing substitution σ subsumes μ. It follows that there are as many narrowing derivations generating (a generalization of) the same solution μ as there are different normalizations of μ(G). This is one of the main reasons for the inefficiency of narrowing.

The natural solution to this problem is

• to introduce a normalization strategy for μ(G) and

• to consider only those narrowing derivations which correspond to rewriting derivations following this strategy.

4.1 Basic Narrowing

A first step in this direction was Hullot’s basic narrowing [Hul80]. A basic narrowing derivation is obtained, when an innermost rewriting derivation on μ(G), where μ denotes a normalized substitution, is lifted to the narrowing level.

Definition 4.2 (Basic Narrowing) The sets B_{i}, i = 0, …, n, of basic occurrences in a narrowing derivation

G_{0} −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},l_{2}→r_{2},δ_{2}]} … −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n}

are inductively defined as follows

• B_{0} =^{def} F uOcc(G_{0})

• B_{i} =^{def} (B_{i−1} \ {υ ∈ B_{i−1} | υ ⪰ υ_{i}}) ∪ {υ_{i}.υ | υ ∈ F uOcc(r_{i})}, i > 0.

For a basic narrowing derivation we require that υ_{i} ∈ B_{i−1}, for all i = 1, …, n.

While original narrowing considers any non-variable occurrence in the goal, basic narrowing discards those occurrences which have been introduced by the narrowing substitution of a previous narrowing step.

Since, in canonical systems, an innermost normalization of μ(G) always exists, Proposition 3.4 implies that basic narrowing is complete. A formal proof will be given in Corollary 5.13. Note that naive innermost narrowing is not complete.

4.2 Left-to-Right Basic Narrowing

In 1986, Herold showed that it is possible to restrict the set of narrowing occurrences further without loosing completeness. After a narrowing step G −∧∨→_{[υ,l→r,σ]} G′, we may discard also those narrowing occurrences which are strictly left of υ [Her86].

Definition 4.3 An occurrence ω is strictly left of an occurrence ω′, ω < ω′ (resp. ω′ > ω) iff there exist occurrences o, υ, υ′ and natural numbers i, i′ such that i < i′, ω = o.i.υ and ω′ = o.i′.υ′.

Definition 4.4 (Left-to-Right Basic Narrowing) The sets LRB_{i}, i = 0, …, n, of left-to-right basic occurrences in a narrowing derivation

G_{0} −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},l_{2}→r_{2},δ_{2}]} … −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n}

are inductively defined as follows

• LRB_{0} =^{def} F uOcc(G_{0})

• LRB_{i} =^{def} (LRB_{i−1} \ {υ ∈ LRB_{i−1} | υ ⪰ υ_{i} or υ < υ_{i}}) ∪ {υ_{i}.υ | υ ∈

F uOcc(r_{i})}, i > 0.

For a left-to-right basic narrowing derivation we require that υ_{i} ∈ LRB_{i−1}, for all i = 1, …, n. Sometimes, we will use the abbreviation LRB(U, υ, l → r) for the set of occurrences (U \ {ω ∈ U | ω ⪰ υ or ω < υ}) ∪ {υ.ω | ω ∈ F uOcc(r)}.

We could also define a right-to-left basic narrowing derivation. If we allow arbitrary selection strategies we obtain the basic selection narrowing of [BGM88], which includes left-to-right and right-to-left basic narrowing as special cases.

Herold showed that narrowing derivations corresponding to leftmostinnermost normalizations of μ(G), for a normalized substitution μ, are leftto-right basic. This implies immediately the completeness of left-to-right basic narrowing (see Corollary 5.14 for a formal proof).

4.3 SL Left-to-Right Basic Narrowing

To further improve left-to-right-basic narrowing, Réty introduced the notion of sufficient largeness [Rét87, Rét88].

Definition 4.5 (Sufficient Largeness) A set U of occurrences of a term t is said to be sufficiently large on t, iff t/ω is in normal form for all ω ∈ Occ(t) \ U.

Réty noticed that sufficient largeness is preserved by leftmost-innermost rewriting derivations.

Lemma 4.6 Let H_{0} →^{∗} H_{n} be a leftmost-innermost rewriting derivation, U_{0} a sufficiently large set of occurrences of H_{0}, and U_{i+1} =^{def} LRB(U_{i}, υ_{i+1}, π_{i+1}). Then U_{i} is sufficiently large on H_{i}, for all i = 0, …, n.

Proof: By induction on the length of the derivation. For n = 0 the lemma is trivial. If U_{n} is sufficiently large on H_{n}, then the step H_{n} →_{[υ,π,τ]} H_{n+1} satisfies υ ∈ U_{n}. Since the strategy is innermost, the matching substitution τ is normalized. This holds because l cannot be a variable and therefore τ(x) is a proper subterm of τ(l). Since the strategy is leftmost, the part of H_{n} strictly left of υ is normalized. This shows that U_{n+1} is sufficiently large on H_{n+1}. □

Lifting this property to the narrowing level yields SL left-to-right basic narrowing.

Definition 4.7 (SL Left-to-Right Basic Narrowing) A SL left-to-right basic narrowing derivation is a left-to-right basic narrowing derivation

G_{0} −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},l_{2}→r_{2},δ_{2}]} … −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n}

such that the set of left-to-right basic occurrences LRB_{i} is sufficiently large on G_{i}, for i = 1, …, n.

By Proposition 3.4, we can conclude that SL left-to-right basic narrowing is complete (see also Corollary 5.15).

While lifting a leftmost-innermost rewriting derivation to the narrowing level always yields a SL left-to-right basic narrowing derivation, the converse is not true.

A SL left-to-right basic narrowing derivation need not generate a leftmost-innermost rewriting derivation.

Example 4.8 Consider the rule

π : z ∗ 0 → 0.

Starting with the term (y ∗ x) ∗ x there are two SL left-to-right basic narrowing derivations

\begin{matrix}(y ∗ x) ∗ x & −∧∨→_{[1,π,\{x←0,z←y\}]} & 0 ∗ 0 & −∧∨→_{[ϵ,π]} & 0 \\ (y ∗ x) ∗ x & −∧∨→_{[ϵ,π,\{x←0,z←y∗0\}]} & & & 0 \end{matrix}

There is an obvious redundancy. In both derivations, the narrowing substitution {x ← 0} and the derived term 0 are the same.

The reduction

(y ∗ 0) ∗ 0 →_{[ϵ,π]} 0

corresponding to the second narrowing derivation is not leftmost-innermost, since y ∗ 0 can be reduced.

5 LSE Narrowing

Our aim is now to introduce a new narrowing strategy which has the property that the corresponding rewriting derivations are always leftmost-innermost.

We start by refining the notion of a leftmost-innermost rewriting derivation. Leftmost-innermost derivations are not unique. If the rewrite system has unifiable left-hand sides, then it may happen that two different rules are applicable at the same occurrence. In order to eliminate this indeterminism we assume that the rules are ordered by a total well-founded ordering <. If several rules can be applied at the same occurrence, we require that the minimal rule is chosen.

Definition 5.1 (Left Reduction) A reduction step t →_{[υ,π,σ]} t′ is called a left reduction step iff

• all subterms t/ω with ω strictly left of υ are in normal form (“leftmost”)

• all proper subterms of t/υ are in normal form (“innermost”)

• t/υ cannot be reduced by a rule π′ smaller than π (“minimal rule”).

A rewriting derivation is a left reduction iff all steps are left reduction steps.

While leftmost-innermost derivations are not unique due to the indeterminism in the selection of the rule, left reductions are unique.

Proposition 5.2 For all terms t there exists a unique left reduction to the normal form of t.

Proof: We prove the proposition by noetherian induction. If t is in normal form, then the theorem holds trivially. If t can be reduced, then there exists a unique first left reduction step t → t′, since the ordering < ∪ ≺ on Occ(t) and the ordering on rules are total and well-founded. By induction hypothesis, there is a unique left derivation t′ →^{∗} t′↓. If we join the two derivations together, we get the unique left reduction t → t′ →^{∗} t′↓ = t↓. □

Now we will show how reducibility tests which are performed after a narrowing step can be used to obtain a one-to-one correspondence between narrowing derivations and left reductions.

Definition 5.3 (LSE Narrowing) In a narrowing derivation

G_{0} −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},π_{2},δ_{2}]} … G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n}

the step G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n} is called LSE iff the following three conditions are satisfied:

(Left-Test) For all i ∈ {0, …, n−1} the subterms of λ_{i,n}(G_{i}) which lie strictly left of υ_{i+1} are in normal form.

(Sub-Test) For all i ∈ {0, …, n − 1} the proper subterms of λ_{i,n}(G_{i}/υ_{i+1}) are in normal form.

(Epsilon-Test) For all i ∈ {0, …, n − 1} the term λ_{i,n}(G_{i}/υ_{i+1}) is not reducible at occurrence ϵ with a rule smaller than π_{i+1}.

A narrowing derivation is LSE iff any single narrowing step is LSE.

In [KB91], LSE narrowing was introduced as a refinement of SL left-to-right basic narrowing [Rét87]. A LSE-SL left-to-right basic narrowing derivation was defined as a left-to-right basic narrowing derivation for which the SL-Test, the Sub-Test, and the Epsilon-Test detect no redundancy. By introducing the Left-Test, this definition and the subsequent proofs could be considerably simplified. The Left-Test replaces the SL-Test and implies together with the Sub-Test that a LSE narrowing derivation is also left-to-right basic. However, while the notion of left-to-right basic occurrences is not needed anymore in the definition of LSE narrowing, it is still very useful in a practical implementation. We do not have to perform the Left- or Sub-Test at a non-left-to-right-basic occurrence because we know in advance that a redundancy will be detected.

Proposition 5.4 Consider a system of equations G and a normalized substitution μ. If

H_{0} =^{def} μ(G_{0}) →_{[υ_{1},π_{1}]} H_{1} →_{[υ_{2},π_{2}]} … →_{[υ_{n},π_{n}]} H_{n}

is a left reduction, then the corresponding narrowing derivation

G_{0} −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},π_{2},δ_{2}]} … G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n}

is a LSE narrowing derivation.

Proof: By Proposition 3.3 there exists a substitution λ such that H_{i} = (λ ∘ λ_{i,n})(G_{i}), for i = 0, …, n. We have to show that none of the reducibility tests detects a redundancy.

Suppose that the step G_{m−1} −∧∨→_{[υ_{m},π_{m},δ_{m}]} G_{m} is not LSE, for some m ∈ {1, …, n}. Then there exists i ∈ {0, …, m − 1} such that either

1. λ_{i,m}(G_{i}) is reducible at an occurrence υ strictly left of υ_{i+1} or

2. λ_{i,m}(G_{i}) is reducible at an occurrence υ strictly below υ_{i+1} or

3. λ_{i,m}(G_{i}) is reducible at occurrence υ_{i+1} with a rule smaller than π_{i+1}.

Since H_{i} = (λ∘λ_{m,n} ∘λ_{i,m})(G_{i}) and → is stable under substitutions this implies that one of the properties (1) to (3) must hold with H_{i} in place of λ_{i,m}(G_{i}). But this means that H_{i} →_{[υ_{i+1},π_{i+1}]} H_{i+1} is not a left reduction step in contradiction to our assumption. □

As an immediate consequence, we get by Proposition 5.2 and Proposition 3.4 the following theorem.

Theorem 5.5 LSE narrowing is complete.

Next we consider the converse of Proposition 5.4.

Proposition 5.6 If

G_{0} −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},π_{2},δ_{2}]} … G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n}

is a LSE narrowing derivation and H_{i} =^{def} λ_{i,n}(G_{i}), for i = 0, …, n, then the rewriting derivation

H_{0} →_{[υ_{1},π_{1}]} H_{1} →_{[υ_{2},π_{2}]} … →_{[υ_{n},π_{n}]} H_{n}

is a left reduction.

Proof: Suppose that the derivation is not a left reduction. Then there exists i ∈ {0, …, n − 1} and a rewriting step λ_{i,n}(G_{i}) →_{[υ,π]} λ_{i+1,n}(G_{i+1}) such that either

1. υ lies strictly left of υ_{i+1} or

2. υ lies strictly below υ_{i+1} or

3. the rule π is smaller than π_{i+1}

But this implies that the narrowing step G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n} is not LSE in contradiction to our assumption. □

This proposition has a number of important consequences. First of all, we can easily prove the following minimality property of LSE narrowing which first appeared in [Wer91].

Theorem 5.7 Consider two LSE narrowing derivations

G = G_{0} −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},π_{2},δ_{2}]} … G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n},

G = G′_{0} −∧∨→_{[υ′_{1},π′_{1},δ′_{1}]} G′_{1} −∧∨→_{[υ′_{2},π′_{2},δ′_{2}]} … G′_{m−1} −∧∨→_{[υ′_{m},π′_{m},δ′_{m}]} G′_{m}.

If the narrowing substitutions σ =^{def} δ_{n} ∘ … ∘ δ_{1} and σ′ =^{def} δ′_{m} ∘ … ∘ δ′_{1}, where n ≤ m, coincide on Var(G) up to variable renaming, that is if there exist substitutions λ and λ′ such that σ = λ′ ∘ σ′ [Var(G)] and σ′ = λ ∘ σ [Var(G)], then

• π_{i} = π′_{i} and υ_{i} = υ′_{i} for 1 ≤ i ≤ n,

• the narrowing derivation

G′_{n} −∧∨→_{[υ′_{n+1},π′_{n+1},δ′_{n+1}]} G′_{n+1} … −∧∨→_{[υ′_{m},π′_{m},δ′_{m}]} G′_{m}

is a left reduction (up to variable renaming).

Proof: By Proposition 5.6 the rewriting derivations

σ(G) = λ_{0,n}(G_{0}) →_{[υ_{1},π_{1}]} λ_{1,n}(G_{1}) →_{[υ_{2},π_{2}]} … →_{[υ_{n},π_{n}]} λ_{n,n}(G_{n})

σ′(G) = λ′_{0,m}(G′_{0}) →_{[υ′_{1},π′_{1}]} λ′_{1,m}(G′_{1}) →_{[υ′_{2},π′_{2}]} … →_{[υ′_{m},π′_{m}]} λ′_{m,m}(G′_{m})

are both left reductions. Since σ and σ′ coincide on Var(G) up to variable renaming, the systems σ(G) and σ′(G) are identical up to variable renaming. By the unicity of left reductions, this implies π_{i} = π′_{i} and υ_{i} = υ′_{i} for 1 ≤ i ≤ n.

Using Lemma 3.7 we can conclude by induction that G_{i} and G′_{i} resp. λ_{i,n}(G_{i}) and λ′_{i,m}(G′_{i}) are identical up to variable renaming, for i = 1, …, n. Since λ_{n,n}(G_{n}) = G_{n}, this implies that G′_{n} and λ′_{n,m}(G′_{n}) are identical up to variable renaming. Therefore, again by Lemma 3.7, the narrowing derivation starting from G′_{n} and the left reduction starting from λ′_{n,m}(G′_{n}) are the same up to variable renaming. □

If we assume that narrowing derivations starting from the same goal and using the same rules at the same occurrences produce the same narrowing substitution (in any practical implementation, this will be the case), we get the following corollary.

Corollary 5.8 If LSE narrowing enumerates two solutions σ and σ′ which coincide up to variable renaming, then σ = σ′ holds and the two derivations coincide.

Proof: We use the same notation as in Theorem 5.7. Then G_{n} = G′_{m} = true ∧ … ∧ true implies n = m. □

Another important property of LSE narrowing is that it generates only normalized substitutions. The other narrowing strategies produce also nonnormalized substitutions, which blow up the narrowing search space. If one wants to eliminate them one has to perform an additional normalization test, which is not necessary for LSE narrowing.

Proposition 5.9 For any LSE narrowing derivation

G = G_{0} −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},π_{2},δ_{2}]} G_{2} … −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n}

the narrowing substitution δ_{n} ∘ … ∘ δ_{1}|_{Var(G)} is normalized.

Proof: Let x be a variable of G such that λ_{0,n}(x) is reducible. Suppose x is instantiated for the first time in the i-th narrowing step. Then there must be an occurrence of x in G_{i−1} which lies below the narrowing occurrence υ_{i}. More formally, there exists an occurrence υ ≠ ϵ such that G_{i−1}/υ_{i}.υ = x. Then λ_{i−1,n}(G_{i−1}/υ_{i}.υ) = λ_{i−1,n}(x) = λ_{0,n}(x) is reducible in contradiction to the Sub-Test. □

Corollary 5.10 LSE narrowing enumerates only normalized substitutions.

Note that the last two corollaries no longer hold if we replace the last narrowing step, which uses the ϵ-rule, by a simple unification of the left and the right hand side of G_{n}. Using the ϵ-rule requires not only that the left and the right hand side are unifiable but also that none of the tests detects a redundancy.

Unfortunately, even if there exists a minimal set of solutions for a given equation, LSE narrowing enumerates not necessarily such kind of set.

Example 5.11 Consider the rules

\begin{aligned}π_{1} : & f(z, c) & → & a, \\ π_{2} : & g(c) & → & c. \end{aligned}

where x, y and z are variables and a, c are constants. Starting with the equation f(g(x), y) ≐ a there are two LSE narrowing derivations:

\begin{matrix}f(g(x), y) ≐ a & −∧∨→_{[1,π_{2},\{x←c\}]} & f(c, y) ≐ a & −∧∨→_{[ϵ,π_{1},\{y←c\}]} & a ≐ a \\ f(g(x), y) ≐ a & −∧∨→_{[ϵ,π_{1},\{y←c\}]} & a ≐ a \end{matrix}

{{y ← c}} is a minimal set of solutions for the given equation, but LSE narrowing computes the non minimal set of solutions {{x ← c, y ← c}, {y ← c}}.

Finally, let us mention how LSE narrowing is related to SL left-to-right basic narrowing.

Proposition 5.12 Any LSE narrowing derivation is SL left-to-right basic.

Proof: Let

G_{0} −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} −∧∨→_{[υ_{2},π_{2},δ_{2}]} … G_{n−1} −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n}

be a LSE narrowing derivation and

H_{0} →_{[υ_{1},π_{1}]} H_{1} →_{[υ_{2},π_{2}]} … →_{[υ_{n},π_{n}]} H_{n}

with H_{i} =^{def} λ_{i,n}(G_{i}), for i = 0, …, n, the corresponding rewriting derivation.

By Proposition 5.9, δ_{n} ∘ … ∘ δ_{1}|_{Var(G_{0})} is normalized. Thus, U_{0} =^{def} F uOcc(G_{0}) is sufficiently large on H_{0} = λ_{0,n}(G_{0}). By Proposition 5.6, the rewriting derivation is a left reduction. By Lemma 4.6, U_{i} =^{def} LRB(U_{i−1}, υ_{i}, π_{i}) is sufficiently large on H_{i} for 1 ≤ i ≤ n. Thus, υ_{i} ∈ U_{i−1}, for i = 1, …, n.

By induction we get LRB_{i} = U_{i} for 0 ≤ i ≤ n. Hence, υ_{i} ∈ LRB_{i} for i = 1, …, n. Furthermore, since H_{i} = λ_{i,n}(G_{i}), LRB_{i} is sufficiently large on G_{i} for i = 1, …, n. □

From Theorem 5.5 we get immediately the following corollaries.

Corollary 5.13 (Hullot 80) Basic narrowing is complete

Corollary 5.14 (Herold 86) Left-to-right basic narrowing is complete.

Corollary 5.15 (Réty 87) SL left-to-right basic narrowing is complete.

6 Normalizing LSE Narrowing

One of the most important optimizations of naive narrowing is normalizing narrowing: after every narrowing step the goal is normalized with respect to the given canonical term rewriting system. This allows us to take advantage of the special properties of rewriting steps compared to narrowing steps. Rewriting steps are special narrowing steps which leave invariant the solution space of the current system of equations and thus do not contribute to the construction of a solution. Naive narrowing does not distinguish rewriting and narrowing steps. Every rewriting step leads to a new path in the search space (“don’t know indeterminism”), whereas in a canonical term rewriting system the rewriting steps may be executed in an arbitrary ordering (“don’t care indeterminism”).

6.1 Normalizing Narrowing

Definition 6.1 (Normalizing Narrowing) Let G be a normalized system of equations. A normalizing narrowing step

G −∧∨→_{[υ,l→r,δ]}^{↓} G′↓

is given by a narrowing step G −∧∨→_{[υ,l→r,δ]} G′ followed by a normalization

G′ →^{∗}_{R} G′↓ with G′↓ normalized.

Since G and G↓ have the same R-unifiers we may assume that G is already in normal from. Note that −∧∨→^{↓} ⊆ −∧∨→^{∗} but in general −∧∨→^{↓} ⊈ −∧∨→.

It is not possible to associate with each rewriting derivation a corresponding normalizing narrowing derivation where the same rules are applied at the same occurrences. However, for any rewriting derivation σ(G) →^{∗} σ(G)↓, where σ is normalized and σ(G)↓ is in normal form, there exists another rewriting derivation σ(G) →^{∗} σ(G)↓ which has a corresponding normalizing narrowing derivation. Moreover, we can assume that the rewriting steps on σ(G) corresponding to narrowing steps on G are left reduction steps. This will be used in the proof of the completeness and minimality of normalizing LSE narrowing.

Theorem 6.2 Consider a normalized system of equations G, a normalized substitution μ and a set of variables V such that V ar(G) ∪ Dom(μ) ⊆ V. Then there exists a normalization of H =^{def} μ(G)

H = H′_{0} →_{[υ_{1},l_{1}→r_{1}]} H_{1} →_{[υ_{11},l_{11}→r_{11}]} … →_{[υ_{1k_{1}},l_{1k_{1}}→r_{1k_{1}}]} H′_{1}

⋮

H′_{n−1}  →_{[υ_{n},l_{n}→r_{n}]} H_{n} →_{[υ_{n1},l_{n1}→r_{n1}]} … →_{[υ_{nkn},l_{nkn}→r_{nkn}]} H′_{n} = H↓,

with left reduction steps H′_{i} →_{[υ_{i+1},l_{i+1}→r_{i+1}]} H_{i+1}, i = 0, …, n − 1, such that there exists a normalizing narrowing derivation

G = G_{0}↓ −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1} →_{[υ_{11},l_{11}→r_{11}]} … →_{[υ_{1k_{1}},l_{1k_{1}}→r_{1k_{1}}]} G_{1}↓

⋮

G_{n−1}↓ −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n} →_{[υ_{n1},l_{n1}→r_{n1}]} … →_{[υ_{nkn},l_{nkn}→r_{nkn}]} G_{n}↓

which uses the same rules at the same occurrences. Moreover, there exists a normalized substitution λ such that

• λ ∘ δ_{n} ∘ … ∘ δ_{1} = μ [V]

• H_{i} = (λ ∘ δ_{n} ∘ … ∘ δ_{i+1}) (G_{i}), i = 1, …, n

• H′_{i} = (λ ∘ δ_{n} ∘ … ∘ δ_{i+1}) (G_{i}↓), i = 0, …, n

• λ(G_{n}↓) = H↓.

Proof: By noetherian induction on the rewriting relation →.

If H = μ(G) is in normal form, then G is also in normal from and the proposition holds trivially with λ = μ.

If H is not in normal form, then there exists a left reduction step H →_{[υ_{1},l_{1}→r_{1}]} H_{1} which by Proposition 3.3 can be lifted to a narrowing step G −∧∨→_{[υ_{1},l_{1}→r_{1},δ_{1}]} G_{1}. Moreover, there exists a normalized substitution ψ with μ = ψ ∘ δ_{1} [V] and H_{1} = ψ(G_{1}). If G_{1} →_{[υ_{11},l_{11}→r_{11}]} … →_{[υ_{1k_{1}},l_{1k_{1}}→r_{1k_{1}}]} G_{1}↓ is a normalization of G_{1}, then by the stability of the rewriting relation under substitutions ψ(G_{1}) = H_{1} →_{[υ_{11},l_{11}→r_{11}]} … →_{[υ_{1k_{1}},l_{1k_{1}}→r_{1k_{1}}]} ψ(G_{1}↓) = H′_{1}.

Let V′ =^{def} V ∪ Im(δ_{1}). By applying the induction hypothesis, we obtain a normalization

H′_{1}  →_{[υ_{2},l_{2}→r_{2}]} H_{2} →_{[υ_{21},l_{21}→r_{21}]} … →_{[υ_{2k_{2}},l_{2k_{2}}→r_{2k_{2}}]} H′_{2}

⋮

H′_{n−1} →_{[υ_{n},l_{n}→r_{n}]} H_{n} →_{[υ_{n1},l_{n1}→r_{n1}]} … →_{[υ_{nkn},l_{nkn}→r_{nkn}]} H′_{n} = H↓,

with left reduction steps H′_{i} →_{[υ_{i+1},l_{i+1}→r_{i+1}]} H_{i+1}, i = 1, …, n − 1, and a corresponding narrowing derivation

G_{1}↓ −∧∨→_{[υ_{2},l_{2}→r_{2},δ_{2}]} G_{2} →_{[υ_{21},l_{21}→r_{21}]} … →_{[υ_{2k_{2}},l_{2k_{2}}→r_{2k_{2}}]} G_{2}↓

⋮

G_{n−1}↓ −∧∨→_{[υ_{n},l_{n}→r_{n},δ_{n}]} G_{n} →_{[υ_{n1},l_{n1}→r_{n1}]} … →_{[υ_{nkn},l_{nkn}→r_{nkn}]} G_{n}↓.

Moreover, there is a substitution λ such that • λ ∘ δ_{n} ∘ … ∘ δ_{2} = ψ [V′]

• H_{i} = (λ ∘ δ_{n} ∘ … ∘ δ_{i+1}) (G_{i}), i = 2, …, n

• H′_{i} = (λ ∘ δ_{n} ∘ … ∘ δ_{i+1}) (G_{i}↓), i = 1, …, n

• λ(G_{n}↓) = H↓.

From μ = ψ ∘ δ_{1} [V] and ψ = λ ∘ δ_{n} ∘ … ∘ δ_{2} [V′], we get λ ∘ δ_{n} ∘ … ∘ δ_{1} = μ [V] and the proposition follows. □

Since −∧∨→^{↓} ⊆ −∧∨→^{∗}, Proposition 3.4 holds also for normalizing narrowing strategies. It follows:

Corollary 6.3 (Réty et al. 85) Normalizing narrowing is complete.

6.2 Normalizing LSE Narrowing

Our aim is now to extend the idea of LSE narrowing to the case of normalizing narrowing. We can use essentially the same definition as before. Again, the tests have to be applied to the goals where a narrowing step has taken place. These are the goals G_{i}↓, i = 0, …, n − 1.

Definition 6.4 (Normalizing LSE Narrowing) In a normalizing narrowing derivation

G_{0}↓ −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} →^{∗} G_{1}↓
⋮
G_{n−1}↓ −∧∨→_{[υ_{n},π_{n},δ_{n}]} G_{n} →^{∗} G_{n}↓

the step G_{n−1}↓ −∧∨→ G_{n} →^{∗} G_{n}↓ is called a LSE step iff the following three conditions are satisfied

(Left-Test) For all i ∈ {0, …, n − 1} the subterms of λ_{i,n}(G_{i}↓) which lie strictly left of υ_{i+1} are in normal form.

(Sub-Test) For all i ∈ {0, …, n − 1} the proper subterms of λ_{i,n}(G_{i}↓/υ_{i+1}) are in normal form.

(Epsilon-Test) For all i ∈ {0, …, n − 1} the term λ_{i,n}(G_{i}↓/υ_{i+1}) is not reducible at occurrence ϵ with a rule smaller than π_{i+1}.

A normalizing narrowing derivation is called a normalizing LSE narrowing derivation iff all steps are LSE steps.

The following proposition extends Proposition 5.4 to the case of normalizing narrowing.

Proposition 6.5 The normalizing narrowing derivation constructed in Theorem 6.2 is a normalizing LSE derivation.

Proof: Analogous to the proof of Proposition 5.4 with G_{i}↓ instead of G_{i}. □

As an immediate consequence we get:

Theorem 6.6 Normalizing LSE narrowing is complete.

Next we extend Proposition 5.6 to the normalizing case.

Proposition 6.7 Let

G = G_{0}↓ −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} →^{∗} G_{1}↓ −∧∨→_{[υ_{2},π_{2},δ_{2}]} … −∧∨→_{[υ_{n},π_{n},δ_{n}]}G_{n} →^{∗} G_{n}↓

be a normalizing LSE narrowing derivation.

Then in the corresponding rewriting derivation

H = H′_{0} →_{[υ_{1},π_{1}]} H_{1} →^{∗} H′_{1} →_{[υ_{2},π_{2}]} … →_{[υ_{n},π_{n}]} H_{n} →^{∗} H′_{n} = H↓,

where H_{i} =^{def} λ_{i,n}(G_{i}), for i = 1, …, n and H′_{i} =^{def} λ_{i,n}(G_{i}↓), for i = 0, …, n, the

steps H′_{i} →_{[π_{i+1},υ_{i+1}]} H_{i+1} are left reduction steps, for all i = 0, …, n − 1.

Proof: Analogous to the proof of Proposition 5.6 with H′_{i} instead of H_{i} and G_{i}↓ instead of G_{i}. □

Using this proposition we are now able to prove the minimality result for normalizing LSE narrowing.

Theorem 6.8 Consider two normalizing LSE narrowing derivations

\begin{matrix}G_{0} & −∧∨→_{[υ_{1},π_{1},δ_{1}]}^{↓} & G_{1}↓ & −∧∨→_{[υ_{2},π_{2},δ_{2}]}^{↓} & … & −∧∨→_{[υ_{n},π_{n},δ_{n}]}^{↓} & G_{n}↓ \\ G′_{0} & −∧∨→_{[υ′_{1},π′_{1},δ′_{1}]}^{↓} & G′_{1}↓ & −∧∨→_{[υ′_{2},π′_{2},δ′_{2}]}^{↓} & … & −∧∨→_{[υ′_{m},π′_{m},δ′_{m}]}^{↓} & G′_{m}↓. \end{matrix}

Let λ_{i,n} =^{def} δ_{n} ∘ … ∘ δ_{i+1}, for i = 0, …, n and λ′_{j,m} =^{def} δ′_{m} ∘ … ∘ δ′_{j+1} for

j = 0, …, m, where λ_{n,n} = λ′_{m,m} = id. Suppose that G_{0} and G′_{0} respectively λ_{0,n} and λ′_{0,m} are identical up to variable renaming, that is there exist substitutions τ_{0}, τ′_{0}, ρ, ρ′ such that

• τ_{0}(G_{0}) = G′_{0}, τ′_{0}(G′_{0}) = G_{0} and

• λ_{0,n} = ρ′ ∘ λ′_{0,m} ∘ τ_{0} [Var(G_{0})], λ′_{0,m} = ρ ∘ λ_{0,n} ∘ τ′_{0} [Var(G′_{0})]

Then the two derivations are identical up to variable renaming, that is

• n = m

• υ_{i} = υ′_{i}, for i = 1, …, n

• π_{i} = π′_{i}, for i = 1, …, n

• there exist substitutions τ_{i}, τ′_{i} such that

– τ_{i}(G_{i}↓) = G′_{i}↓, τ′_{i}(G′_{i}↓) = G_{i}↓,

– λ_{i,n} = ρ′ ∘ λ′_{i,m} ∘ τ_{i} [Var(G_{i})], λ′_{i,m} = ρ ∘ λ_{i,n} ∘ τ′_{i} [Var(G′_{i})],

for i = 1, …, n.

Proof: Without loss of generality we assume n ≤ m. First we show by induction on n that the first n steps of the two derivations are identical up to variable renaming. For n = 0 nothing has to be shown. Assume therefore n ≥ 1 and consider the associated rewriting derivations

λ_{0,n}(G_{0}) →_{[υ_{1},π_{1}]} λ_{1,n}(G_{1}) →^{∗} λ_{1,n}(G_{1}↓) →_{[υ_{2},π_{2}]} … →^{∗} λ_{n,n}(G_{n}↓)

and

λ′_{0,m}(G′_{0}) →_{[υ′_{1},π′_{1}]} λ′_{1,m}(G′_{1}) →^{∗} λ′_{1,m}(G′_{1}↓) →_{[υ′_{2},π′_{2}]} … →^{∗} λ′_{m,m}(G′_{m}↓).

By Proposition 6.7, the rewriting steps λ_{0,n}(G_{0}) →_{[υ_{1},π_{1}]} λ_{1,n}(G_{1}) and λ′_{0,m}(G′_{0}) →_{[υ′_{1},π′_{1}]} λ′_{1,m}(G′_{1}) are both left reduction steps. From λ′_{0,m}(G′_{0}) = (ρ∘ λ_{0,n} ∘τ′_{0})(G′_{0}) = ρ(λ_{0,n}(G_{0})) and λ_{0,n}(G_{0}) = (ρ′ ∘λ′_{0,m} ∘τ_{0})(G_{0})) = ρ′(λ′_{0,m}(G′_{0})) we deduce that λ_{0,n}(G_{0}) and λ′_{0,m}(G′_{0}) are identical up to variable renaming. By the unicity of left reductions, this implies υ_{1} = υ′_{1} and π_{1} = π′_{1}.

From Lemma 3.7 and its proof we get the existence of substitutions τ_{1} and τ′_{1} with τ_{1} ∘ δ_{1} = δ′_{1} ∘ τ_{0} and τ′_{1} ∘ δ′_{1} = δ_{1} ∘ τ′_{0} such that τ_{1}(G_{1}) = G′_{1} and τ′_{1}(G′_{1}) = G_{1}. Since τ_{1} and τ′_{1} are renaming substitutions, we get even τ_{1}(G_{1}↓) = τ_{1}(G_{1})↓ = G′_{1}↓ and τ′_{1}(G′_{1}↓) = τ′_{1}(G′_{1})↓ = G_{1}↓.

From λ_{1,n} ∘ δ_{1} = λ_{0,n} = ρ′ ∘ λ′_{0,m} ∘ τ_{0} = ρ′ ∘ λ′_{1,m} ∘ δ′_{1} ∘ τ_{0} = ρ′ ∘ λ′_{1,m} ∘ τ_{1} ∘ δ_{1} [Var(G_{0})] we deduce λ_{1,n} = ρ′ ∘ λ′_{1,m} ∘ τ_{1} [(Var(G_{0}) \ Dom(δ_{1})) ∪ Im(δ_{1}|_{Var(G_{0})})]. Since (Var(G_{0}) \ Dom(δ_{1})) ∪ Im(δ_{1}|_{Var(G_{0})}) = Var(δ_{1}(G_{0})) = Var(δ_{1}(G_{0}[υ_{1} ← l_{1}])) ⊇ Var(δ_{1}(G_{0}[υ_{1} ← r_{1}])) = Var(G_{1}) ⊇ Var(G_{1}↓), this implies λ_{1,n} = ρ′ ∘ λ′_{1,m} ∘ τ_{1} [Var(G_{1}↓)]. In the same way, we can show that λ′_{1,m} = ρ ∘ λ_{1,n} ∘ τ′_{1} [Var(G′_{1}↓)].

Now we can apply the induction hypothesis and we get

• υ_{i} = υ_{i}, for i = 2, …, n

• π_{i} = π′_{i}, for i = 2, …, n

• there exist substitutions τ_{i}, τ′_{i} such that

– τ_{i}(G_{i}↓) = G′_{i}↓, τ′_{i}(G′_{i}↓) = G_{i}↓,

– λ_{i,n} = ρ′ ∘ λ′_{i,m} ∘ τ_{i} [Var(G_{i})], λ′_{i,m} = ρ ∘ λ_{i,n} ∘ τ′_{i} [Var(G′_{i})],

for i = 2, …, n.

Finally, let us show that n = m. Assume n < m holds and consider

the derivation G′_{n}↓ −∧∨→_{[υ′_{n+1},π′_{n+1},δ′_{n+1}]} G′_{n+1} →^{∗} G′_{n+1}↓ −∧∨→^{↓} … −∧∨→^{↓} G′_{m}↓.

Then λ′_{n,m}(G′_{n}↓) is reducible at occurrence υ′_{n+1} with rule π′_{n+1}. Since G_{n}↓ = λ_{n,n}(G_{n}↓) = (ρ′ ∘ λ′_{n,m} ∘ τ_{n})(G_{n}↓) = ρ′(λ′_{n,m}(G′_{n}↓)) and → is stable under substitutions, this would imply that G_{n}↓ is reducible in contradiction to the fact that G_{n}↓ is the normal form of G_{n}. This shows that n = m and the theorem is proved. □

Assuming again that narrowing derivations starting from the same goal and using the same rules at the same occurrences produce the same narrowing substitution we get:

Corollary 6.9 If normalizing LSE narrowing enumerates two solutions σ and σ′ which coincide up to variable renaming, then σ = σ′ holds and the two derivations coincide.

Theorem 6.10 For any normalizing LSE narrowing derivation

G_{0}↓ −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} →^{∗} G_{1}↓ −∧∨→_{[υ_{2},π_{2},δ_{2}]} … −∧∨→_{[υ_{n}π_{n},δ_{n}]} G_{n} →^{∗} G_{n}↓

the narrowing substitution δ_{n} ∘ … ∘ δ_{1}|_{Var(G_{0}↓)} is normalized.

Proof: Analogous to the proof of Proposition 5.9 with G_{i}↓ instead of G_{i}. □

Corollary 6.11 Normalizing LSE narrowing enumerates only normalized substitutions.

Example 5.11 is still valid if we use normalizing LSE narrowing instead of LSE narrowing.

6.3 Normalizing LSE and SL Left-to-Right Basic Narrowing

Finally, we want to investigate the relationship of normalizing LSE narrowing to normalizing left-to-right basic narrowing as studied in [Rét87, Rét88]. It is well-known that a naive combination of (left-to-right) basic narrowing and normalizing narrowing is not complete.

For rewriting derivations the computation of the sets of basic occurrences is more complicated than for narrowing derivations. We need the notion of weakly basic rewriting derivation [Rét87].

Definition 6.12 (Antecedent) Let t →_{[υ,l→r]} t′ be a rewriting step. We say that the occurrence ω in t is an antecedent of the occurrence ω′ in t′ iff

• ω = ω′ and neither ω ⪯ υ nor υ ⪯ ω or

• there exists an occurrence ρ′ of a variable x in r such that ω′ = υ.ρ′.o and ω = υ.ρ.o where ρ is an occurrence of the same variable x in l.

See Fig. 2 for illustration.

Definition 6.13 (Weakly Basic Rewriting) Given a rewriting derivation

G_{1} →_{[υ_{1},l_{1}→r_{1}]} G_{2} →_{[υ_{2},l_{2}→r_{2}]} … →_{[υ_{n−1},l_{n−1}→r_{n−1}]} G_{n}

and a set WB_{1} ⊆ Occ(G_{1}) of occurrences in G_{1} the corresponding sets of weakly basic occurrences are inductively defined by

WB_{i+1} =^{def} (WB_{i} \ {υ ∈ WB_{i} | υ ⪰ υ_{i}}) ∪ {υ_{i}.o | o ∈ F uOcc(r_{i})} ∪ {υ ∈ Occ(G_{i+1}) |

υ = υ_{i}.o, o ∉ F uOcc(r_{i}) and all antecedents of υ in G_{i} are in WB_{i}},

for i = 1, …, n − 1. The rewriting derivation is weakly based on WB_{1} iff υ_{i} ∈ WB_{i}, for all i = 1, …, n − 1. Instead of WB_{n} we will also write

WB(WB_{1}, G_{1} →^{∗} G_{n}).

[figure: r; l; o; ρ′; υ; t′ = t[υ ← σ(r)]; σ(r); σ(l); o; ρ; υ; t]

Figure 2: Illustration of antecedents: the occurrence υ.ρ.o is an antecedent of υ.ρ′.o.

The main difference compared to the computation of the set B_{i+1} of basic occurrences is that occurrences under υ_{i} which do not correspond to nonvariable occurrences in r_{i} may belong to WB_{i+1}. Note that different reductions G →^{∗} G′ can lead to different sets WB(U, G →^{∗} G′). But this does not affect the completeness of the narrowing strategies introduced below (see [Wer91]).

The notion of weakly basic occurrences is closely related to the notion of sufficient largeness as is illustrated by the following lemma [Rét87].

Lemma 6.14 Let U be sufficiently large on G_{1}. Then any rewriting derivation G_{1} →^{∗} G_{n} is weakly based on U, and WB(U, G_{1} →^{∗} G_{n}) is sufficiently large on G_{n}.

Proof: By induction on the length of the derivation. In the case n = 1 nothing has to be shown. Assume therefore that G_{1} →^{∗} G_{n−1}, n > 1, is weakly based on U = WB_{1} and that WB_{n−1} is sufficiently large on G_{n−1}. Then the occurrence υ_{n−1} in G_{n−1} →_{[υ_{n−1},π_{n−1}]} G_{n} must belong to WB_{n−1}. If ω_{n} ∈ Occ(G_{n}) \ WB_{n}, then at least one antecedent ω_{n−1} of ω_{n} in G_{n−1} does not belong to WB_{n−1}. Since WB_{n−1} is sufficiently large on G_{n−1}, we deduce that G_{n}/ω_{n} = G_{n−1}/ω_{n−1} is irreducible. This shows that WB_{n} is sufficiently large on G_{n}. □

Definition 6.15 (Normalizing SL Left-to-Right Basic Narrowing) Let G_{0}↓ be a normalized system of equations. A derivation

(G_{0}↓, U_{0}↓)  −∧∨→_{[υ_{1},π_{1},δ_{1}]}  (G_{1}, U_{1})  →^{∗}  (G_{1}↓, U_{1}↓)
⋮
(G_{n−1}↓, U_{n−1}↓) −∧∨→_{[υ_{n},π_{n},δ_{n}]} (G_{n}, U_{n}) →^{∗}  (G_{n}↓, U_{n}↓),

with U_{0}↓ =^{def} FuOcc(G_{0}↓), U_{i} =^{def} LRB(U_{i−1}↓, υ_{i}, π_{i}) and U_{i}↓ =^{def}

WB(U_{i}, G_{i} →^{∗} G_{i}↓) is called a normalizing left-to-right basic narrowing derivation if for i = 1, …, n

• υ_{i} ∈ U_{i−1}↓,

• G_{i} →^{∗} G_{i}↓ is weakly based on U_{i}, and

• G_{i}↓ is normalized.

The derivation is called a normalizing SL left-to-right basic narrowing derivation if moreover U_{i}↓ is sufficiently large on G_{i}↓, for all i = 1, …, n.

Theorem 6.16 Any normalizing LSE narrowing derivation is also a normalizing SL left-to-right basic narrowing derivation.

Proof: Consider a normalizing LSE narrowing derivation

G_{0}↓ −∧∨→_{[υ_{1},π_{1},δ_{1}]} G_{1} →^{∗} G_{1}↓ −∧∨→_{[υ_{2},π_{2},δ_{2}]} … −∧∨→_{[υ_{n}π_{n},δ_{n}]} G_{n} →^{∗} G_{n}↓

and the corresponding rewriting derivation

H = H′_{0} →_{[υ_{1},π_{1}]} H_{1} →^{∗} H′_{1} →_{[υ_{2},π_{2}]} … →_{[υ_{n},π_{n}]} H_{n} →^{∗} H′_{n} = H↓,

with H_{i} =^{def} λ_{i,n}(G_{i}), for i = 1, …, n, and H′_{i} =^{def} λ_{i,n}(G_{i}↓), for i = 0, …, n.

Define the sets of occurrences U_{0}↓ =^{def} FuOcc(G_{0}↓), U_{i} =^{def} LRB(U_{i−1}↓, υ_{i}, π_{i})

and U_{i}↓ =^{def} WB(U_{i}, G_{i} →^{∗} G_{i}↓), for i = 1, …, n.

By induction on j = 0, …, n, we prove for all i = 1, …, j that

• υ_{i} ∈ U_{i−1}↓,

• G_{i} →^{∗} G_{i}↓ is weakly based on U_{i}

and for all i = 0, …, j that

• U_{i}↓ is sufficiently large on G_{i}↓ and H′_{i}.

Since λ_{0,n}|_{Var(G_{0}↓)} is normalized by Theorem 6.10, U_{0}↓ = FuOcc(G_{0}↓) is sufficiently large on both G_{0}↓ and H′_{0} = λ_{0,n}(G_{0}↓).

Suppose the statement is true for 0 ≤ j − 1 < n. By the induction hypothesis the statement holds for all i < j. Hence, U_{j−1}↓ is sufficently large on H′_{j−1}. Consider the rewriting step H′_{j−1} →_{[υ_{j},π_{j}]} H_{j}. Since U_{j−1}↓ is sufficiently large on H′_{j−1}, we get υ_{j} ∈ U_{j−1}↓. By Proposition 6.7, H′_{i−1} →_{[υ_{i},π_{i}]} H_{i} is a left reduction step. Using Lemma 4.6, we can conclude that the set U_{j} = LRB(U_{j−1}↓, υ_{j}, π_{j}) is sufficiently large on H_{j}. Since H_{j} = λ_{j,n}(G_{j}), this shows that U_{j} is also sufficiently large on G_{j}. By Lemma 6.14, this implies that the rewriting derivations G_{j} →^{∗} G_{j}↓ and H_{j} →^{∗} H′_{j} are weakly based on U_{j} and

that U_{j}↓ = WB(U_{j}, G_{i} →^{∗} G_{j}↓) = WB(U_{j}, H_{i} →^{∗} H′_{j}) is sufficiently large on G_{j}↓

and H′_{j}. Therefore, the statement is true for j.

□

Corollary 6.17 Normalizing SL left-to-right basic narrowing is complete.

7 Empirical Results

In this last section, we give a number of empirical results to illustrate the various narrowing strategies. In particular we show how the narrowing search space can be reduced using the LSE strategy.

Our computations have been done in the KArlsruhe NArrowing Labor KANAL [Kri90] which is implemented in the Prolog dialect KA-Prolog on a SUN SPARC 10/41.

We will proceed in two steps. First we give for a very simple example the size of the narrowing tree for all strategies which have been discussed in this paper. In this example, LSE narrowing yields the same results as SL left-to-right basic narrowing.

Then we focus on the most efficient strategies for arbitrary canonical systems, namely normalizing left-to-right basic narrowing, normalizing SL leftto-right basic narrowing and normalizing LSE narrowing and show on some larger examples how the narrowing search space can be reduced by the various reducibility tests.

7.1 Comparing all narrowing strategies for a functional term rewrite system

Consider the canonical term rewriting system

\begin{aligned}R & = & \{ & 0 + x → x, & s(x) + y → s(x + y), \\ & & & 0 ∗ x → 0, & s(x) ∗ y → y + x ∗ y & \} \end{aligned}

for the addition and multiplication of natural numbers. This term rewrite system is functional in the sense of [DG89]: the rules are constructor-based, left-linear and non-overlapping.

We would like to answer the query

?− x ∗ x + y ∗ y ≐ s(0)

which has two solutions

σ_{1} = {x ← 0, y ← s(0)} and σ_{2} = {x ← s(0), y ← 0}.

First we consider the narrowing strategies without normalization. The solution σ_{1} is found in depth 6, the solution σ_{2} in depth 7 of the narrowing tree.

The number of nodes in the narrowing tree is given in Fig. 3. The numbers for LSE narrowing are the same as for SL left-to-right basic narrowing.

If we do narrowing with normalization both solutions are found in depth 3 and many fewer narrowing steps are needed. The naive narrowing tree contains 51372 nodes at depth 7 whereas in the normal tree at depth 3 there are only 72. Although normalizing narrowing steps are more costly than naive narrowing steps, this is an enormous gain of efficiency (see Fig. 4). Again there is no difference between normalizing SL left-to-right basic narrowing and normalizing LSE narrowing.

7.2 Comparing the best narrowing strategies for a arbitrary canonical system

For simple term rewrite systems, LSE narrowing does not improve the performance of narrowing compared to other strategies. However, with increasing

3  4  5  6  7

Depth 0 10000 20000 30000 40000 50000 60000

Nodes

61 . . . . . . . . . . 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1472 . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51372

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

Naive Narrowing

55 211 …. 818 …. . . . . . …. . . . . . …. . . . . . 3228 . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12795

.

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

.

Basic Narrowing

15  21  28  37  46

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

SL Left-to-Right Basic Narrowing

Figure 3: Non-normalizing strategies

1  2  3  4  5

Depth 0 500 1000 1500 2000 2500 Nodes

4 . . . . . . . . . . 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2400

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

Normalizing Narrowing

4 16 …. . . . . . 64 . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1024

.

.

.

.

. .

.

.

. .

.

.

.

. .

.

.

. .

.

.

.

. .

.

.

. .

.

.

.

. .

.

.

. .

.

.

.

.

Normalizing Basic Narrowing

4 . . . . . . . . . . . . . . . . . . . . . . 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

Normalizing SL Left-to-Right Basic Narrowing

Figure 4: Normalizing strategies complexity of the rewrite systems and queries, the LSE strategy becomes more and more important. In particular, the following properties of rewriting systems and goals are relevant for LSE narrowing:

• overlapping left-hand sides

• non-regular rules l → r

• left-hand sides with several defined function symbols

• non-linear rule sides and non-linear goals

To illustrate these points, consider a family R_{n} of canonical rewriting systems for arithmetic modulo an integer number n ≥ 1.

R_{n} = {  0 + x → x
s(x) + y → s(x + y)
x + s(y) → s(x + y)
0 ∗ x → 0
s(x) ∗ y → x ∗ y + y
\underbrace{s(s(… s}_{n-times}(x) …)) → x
(… ((x + \underbrace{y) + y) + … y)}_{n-times} → x
(… ((\underbrace{x + x) + x) + … + x)}_{n-times} → 0 \}.

With increasing n, the last three rules generate more and more redundancies in the normalizing SL left-to-right basic narrowing tree which can be eliminated by the LSE-Tests.

We solve the goal

?− x ∗ y + x ≐ s(0).

for the systems R_{3}, R_{5}, R_{7}, R_{9}, R_{11}, R_{13}. For the system R_{n} the narrowing tree has depth 2n+1, then no more derivations are possible. If we compare the running time (in seconds) needed by normalizing SL left-to-right basic narrowing and LSE narrowing in order to compute the narrowing tree of depth 2n + 1 for the system R_{n}, we get the following results.

System Depth Time: SL Time: LSE Time: Factor
R_{3}  7  0  0  1
R_{5}  11  4  3  1,3
R_{7}  15  43  15  2,8
R_{9}  19  383  49  7,8
R_{11}  23  3366  142  23,7
R_{13}  27  23387  307  76,1

Note that in this example the performance of LSE narrowing increases although the derivations get longer and longer.

0  1  2  3  4  5

Depth 10000 20000 30000 40000 50000

12 130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1004 . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44876

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

. Normalizing Left-to-Right Basic Narrowing

12  80  324 …. . . . . . 1044 …. . . . . . …. . . . . . …. 2932

.

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

. .

.

.

.

.

Normalizing SL Left-to-Right Basic Narrowing

6  27  76 . . . . . . . . . . . . . . . . . . . . . . 183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 400

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

Normalizing LSE Narrowing

Figure 5: Best narrowing strategies for arbitrary systems (only normalized substitutions)

We finish this section with a large practical example where the three tests work together in a very nice way. We consider the canonical term rewriting system for the integer arithmetic given in [RKKL85]

Int = { s(p(x))  → x,
p(s(x))  → x,
0 + x  → x,  x + 0  → x,
s(x) + y  → s(x + y),  x + s(y)  → s(x + y),
p(x) + y  → p(x + y),  x + p(y)  → p(x + y),
−0  → 0,
−s(x)  → p(−x),
−p(x)  → s(−x),
0 ∗ x  → 0,  x ∗ 0  → 0,
s(x) ∗ y  → y + (x ∗ y),  x ∗ s(y)  → (x ∗ y) + x,
p(x) ∗ y  → (−y) + (x ∗ y), x ∗ p(y)  → (x ∗ y) + (−x),
−(−x)  → x,
(−x) + x → 0, x + (−x) → 0,
x + ((−x) + z) → z,  (−x) + (x + z) → z,
−(x + y)  → (−y) + (−x),
(x + y) + z  → x + (y + z) }

and take the goal ?− x ∗ x + y ∗ y ≐ s^{5}(0).

The number of nodes in the narrowing tree is given in Fig. 5. To compute the narrowing tree of depth 5, we needed 381 sec. for ordinary

normalizing left-to-right basic narrowing, 74 sec. for SL normalizing left-to-right basic narrowing, and 19 sec. for normalizing LSE narrowing.

0  1  2  3  4  5

Depth 50000 100000 150000 200000 250000

12 162 . . . . . . . 1802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249616

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

Normalizing Left-to-Right Basic Narrowing

12  92  488 2420 …. . . . . . …. . . . . . 10720

….

. . . . .

….

. . . . .

….

. . . . .

….

. . . . .

….

Normalizing SL Left-to-Right Basic Narrowing

6  27  76  183  400

.

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

. .

.

.

.

.

.

.

.

.

.

.

.

.

.

Normalizing LSE Narrowing

Figure 6: Best narrowing strategies for arbitrary systems (all substitutions)

In all the previous examples, we computed for normalizing left-to-right basic narrowing and normalizing SL left-to-right basic narrowing only narrowing derivations that generate normalized narrowing substitutions. For LSE narrowing, this is automatically the case. For the other strategies, however, this makes a big difference: If we admit also non-normalized narrowing substitutions, we get the numbers given in Fig. 6.

These examples illustrate that the reducibility tests done after a narrowing step are just as important for the efficiency of the narrowing procedure as is the choice of the right narrowing strategy.

8 Conclusion

In this paper, we have introduced a new narrowing strategy LSE narrowing and its normalizing variant. The main features of LSE narrowing are the following

• there is a one-to-one correspondence between LSE narrowing derivations and left reductions.

• LSE narrowing is complete for arbitrary canonical systems.

• two different LSE narrowing derivations cannot generate the same narrowing substitution.

• LSE narrowing generates only normalized narrowing substitutions.

In a subsequent paper, we will show how LSE narrowing can be realized very efficiently by a slight modification of a WAM-based implementation of left-to-right basic narrowing [WBK93]. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be considered. However, using left-to-right basic occurrences this number can be reduced in a drastic way.

References

[BGM88] P. G. Bosco, E. Giovannetti, and C. Moiso. Narrowing vs. SLD-Resolution. Theoretical Computer Science, 59:3 –23, 1988.

[BKW92] A. Bockmayr, S. Krischer, and A. Werner. An optimal narrowing strategy for general canonical systems. In Conditional Term Rewriting Systems, CTRS’92, Pont-à-Mousson, France. Springer, LNCS 656, 1992.

[Boc86] A. Bockmayr. Narrowing with inductively defined functions. Technical Report 25/86, Fakultät für Informatik, Univ. Karlsruhe, 1986.

[Boc88] A. Bockmayr. Narrowing with built-in theories. In First Int. Workshop Algebraic and Logic Programming, Gaußig. Springer, LNCS 343, 1988.

[DG89] J. Darlington and Y. Guo. Narrowing and unification in functional programming - an evaluation mechanism for absolute set abstraction. In Proc. Rewriting Techniques and Applications, Chapel Hill. Springer, LNCS 355, 1989.

[Ech88] R. Echahed. On completeness of narrowing strategies. In Proc. CAAP’88, Nancy. Springer, LNCS 299, 1988.

[Fay79] M. Fay. First-order unification in an equational theory. In 4th Workshop on Automated Deduction, Austin, Texas, 1979.

[Fri85] L. Fribourg. Handling function definitions through innermost superposition and rewriting. In Proc. Rewriting Techniques and Applications, Dijon. Springer, LNCS 202, 1985.

[Her86] A. Herold. Narrowing techniques applied to idempotent unification. SEKI-Report SR-86-16, Univ. Kaiserslautern, 1986.

[HO80] G. Huet and D. C. Oppen. Equations and rewrite rules, A survey. In R. V. Book, editor, Formal Language Theory. Academic Press, 1980.

[Höl89] S. Hölldobler. Foundations of Equational Logic Programming. Springer, LNCS 353, 1989.

[Hul80] J. M. Hullot. Canonical forms and unification. In Proc. 5th Conference on Automated Deduction, Les Arcs. Springer, LNCS 87, 1980.

[KB91] S. Krischer and A. Bockmayr. Detecting redundant narrowing derivations by the LSE-SL reducibility test. In Proc. Rewriting Techniques and Applications, Como. Springer, LNCS 488, 1991.

[Kri90] S. Krischer. Vergleich und Bewertung von Narrowing-Strategien. Diplomarbeit, Fakultät für Informatik, Univ. Karlsruhe, 1990.

[NRS89] W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295–317, 1989.

[Pad88] P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs. Springer, 1988.

[Rét87] P. Réty. Improving basic narrowing techniques. In Proc. Rewriting Techniques and Applications, Bordeaux. Springer, LNCS 256, 1987.

[Rét88] P. Réty. Méthodes d’Unification par Surréduction. PhD thesis, Univ. Nancy, 1988.

[RKKL85] P. Réty, C. Kirchner, H. Kirchner, and P. Lescanne. NARROWER: a new algorithm for unification and its application to logic programming. In Proc. Rewriting Techniques and Applications, Dijon. Springer, LNCS 202, 1985.

[WBK93] A. Werner, A. Bockmayr, and S. Krischer. How to realize LSE narrowing. Technical Report 6/93, Fakultät für Informatik, Univ. Karlsruhe, 1993.

[Wer91] A. Werner. Termersetzung und Narrowing mit geordneten Sorten. Diplomarbeit, Fakultät für Informatik, Univ. Karlsruhe, 1991.

[You88] J. You. Solving equations in an equational language. In First Int. Workshop Algebraic and Logic Programming, Gaußig. Springer, LNCS 343, 1988.

[You91] J. You. Unification modulo an equality theory for equational logic programming. J. Comp. Syst. Sc., 42:54–75, 1991.