Lazy Narrowing and Needed Narrowing: A Comparison

María Alpuente^{1}, Moreno Falaschi^{2}, Pascual Julián^{3}, and Germán Vidal^{1}

       1 DSIC, UPV, {alpuente,gvidal}@dsic.upv.es; ^{2} DIMI, U. Udine,
        falaschi@dimi.uniud.it; ^{3} DI, UCLM, Pascual.Julian@uclm.es

1 Introduction

Functional logic programming [8] allows us to integrate some of the best features of the classical declarative paradigms, namely functional and logic programming. The operational semantics of functional logic languages is usually based on narrowing, an evaluation mechanism which combines the reduction principle of functional languages and the resolution principle of logic languages. Lazy evaluation is a valuable feature of functional (logic) programming languages since it avoids unnecessary computations and allows us to deal with infinite data structures. Recently, Antoy et al. [4] introduced a lazy evaluation strategy for functional logic programs, called needed narrowing, which generalizes Huet and Lévy’s [11] call by need reduction to deal with logical variables and unification in inductively sequential rewrite systems, where functions are defined in a way which is similar to case expressions.

This paper investigates and clarifies the formal relation between needed narrowing and the (not so lazy) demand-driven narrowing strategy of [18]. We demonstrate the following results:

1. Needed narrowing and (demand-driven) lazy narrowing are computationally equivalent on a subclass of inductively sequential programs: the uniform programs of [12, 13], i.e., both strategies compute the same answers and values over this class of programs.

2. This is the broadest class of programs where such an equivalence has been proven. However, (demand-driven) lazy narrowing may still perform some redundant computations which produce several copies of the same value and answer.

3. Therefore, we introduce a complete refinement of (demand-driven) lazy narrowing: uniform lazy narrowing, which is equivalent to needed narrowing on uniform programs and does not perform redundant computations. This implies that uniform lazy narrowing enjoys the optimal properties of needed narrowing.

This paper is organized as follows: After recalling in Section 2 some basic notions, in Section 3 we characterize the class of uniform programs. Section 4 investigates the precise relation between the needed narrowing and demanddriven lazy narrowing strategies. In Section 5, we present an optimization of the demand–driven narrowing strategy and we prove the correctness of the proposed refinement. Section 6 concludes.

2 Preliminaries

We assume familiarity with basic notions of term rewriting [6] and functional logic programming [8]. Throughout this paper, X denotes a countably infinite set of variables and F denotes a set of function symbols (also called the signature), each of which has a fixed associated arity. We often write f/n ∈ F to denote that f is a function symbol of arity n. T (F, X) denotes the set of terms built from F and X. T (F) denotes the set of ground terms. If t ∉ X, then Root(t) is the function symbol heading the term t, also called the root symbol of t. We write \overline{o_{n}} for the sequence of objects o_{1}, …, o_{n}. A linear term does not contain multiple occurrences of the same variable. Var(o) is the set of variables occurring in the syntactic object o.

A substitution σ is a mapping from X to T (F, X) such that its domain Dom(σ) = {x ∈ X | σ(x) ≠ x} is finite. We denote the identity substitution by id. We use the overloaded symbol “≤” to denote the usual preorder on substitutions, i.e., σ ≤ θ iff ∃γ. γ ∘ σ = θ. The restriction σ_{|V̀} of a substitution σ to a set V of variables is defined by σ_{|V̀} (x) = σ(x) if x ∈ V and σ_{|V̀} (x) = x if x ∉ V. A unifier of two terms s and t is a substitution σ such that σ(s) = σ(t). A unifier σ is called the most general unifier (mgu) if σ ≤ θ for all other unifier θ. We say that term s is more general than term t (in symbols, s ≤ t) iff ∃σ such that σ(s) = t.

Positions of a term t are represented by sequences of positive numbers. We let Λ denote the empty sequence, and p.w denote the concatenation of sequences p and w. They are ordered by the prefix ordering “≤”: p ≤ q iff ∃w. p.w = q. Pos(t) and FPos(t) denote, respectively, the set of positions and the set of nonvariable positions of the term t. The subterm of t at position p is denoted by t|_{p} and the result of replacing t|_{p} with a term s is denoted by t[s]_{p}.

2.1 Programs

In this section, we introduce a functional logic language which can be thought of as a “common core” for some popular lazy functional logic languages such as Babel [18], Curry [10], and Toy [15].

A rewrite rule is an ordered pair l → r such that l, r ∈ T (F, X), l ∉ X, and Var(r) ⊆ Var(l). Terms l and r are called the left-hand side (lhs) and the right-hand side (rhs) of the rule, respectively. A term rewriting system (TRS), is a pair ⟨F, R⟩ where F is a signature and R is a set of rewrite rules. Given a TRS ⟨F, R⟩, we assume that the signature F is partitioned into two disjoint sets F = C ⊎ D where D = {Root(l) | (l → r) ∈ R} and C = F \ D. Symbols in C are called constructors and symbols in D are called defined functions or operations. T (C, X) denotes the set of constructor terms. A pattern is a term of the form f(\overline{d_{n}}) where f/n ∈ D and \overline{d_{n}} are constructor terms. For simplicity, we often identify a TRS with the set of rewrite rules R. We say that a TRS is constructor–based (CB) if the lhs’s of R are patterns. We say that a TRS is orthogonal if it is left–linear and non–ambiguous [6]. In this work, TRSs are called programs.

A rewrite step is an application of a rewrite rule to a term, i.e., t →_{p,R} s (or just t → s) if there exists a position p ∈ FPos(t), a rewrite rule R = (l → r) and a substitution σ with t|_{p} = σ(l) and s = t[σ(r)]_{p}. We denote by →^{+} the transitive closure of →, and by →^{∗} the transitive and reflexive closure of →. We say that a term t is a head normal form (hnf) if t is a variable or Root(t) ∈ C.

The equality predicate ≈ is defined, as in functional languages, as the strict equality on terms (note that we do not require terminating rewrite systems and thus reflexivity is not desired), i.e., the equation t_{1} ≈ t_{2} is satisfied if t_{1} and t_{2} are reducible to the same ground constructor term (i.e., ∃d ∈ T (C) such that t_{1} →^{∗} d ^{∗}←t_{2}). Equations can also be interpreted as terms by defining the symbol ≈ as a binary operation symbol.

2.2 Lazy Narrowing Strategies

The operational principle of functional logic languages with a complete semantics is called narrowing [8]. Narrowing was originally proposed as a method to solve equations. A solution of an equation s ≈ t is a substitution σ such that σ(s ≈ t) can be reduced to true.

The narrowing relation is nondeterministic and it can produce a huge search space. Hence, several narrowing strategies which are able to remove some useless derivations have been proposed.

Definition 1 (Narrowing Strategy).

A narrowing strategy is a mapping φ which, given a term t, computes a set of triples ⟨p, R, σ⟩, where p ∈ FPos(t), R = (l → r) is a (standardized apart) program rule and σ is a unifier of t|_{p} and l.^{1}

We say that t ⇝_{φ}^{[p,R,σ]} t′ is a narrowing step using the strategy φ if ⟨p, R, σ⟩ ∈ φ(t)

and σ(t) →_{p,R} t′. Analogously, we say that a derivation t_{0} ⇝_{φ}^{[p_{1},R_{1},σ_{1}]} t_{1} ⇝_{φ}^{[p_{2},R_{2},σ_{2}]}

… ⇝_{φ}^{[p_{n},R_{n},σ_{n}]} t_{n} is a φ-derivation (denoted by t_{0} ⇝_{φ}^{σ}^{∗} t_{n}, where σ = σ_{n}∘σ_{n−1} …∘

σ_{1}), if each narrowing step in the derivation uses φ. We are mainly interested in those derivations leading to a value (a constructor term). A narrowing derivation t ⇝_{φ}^{σ}^{∗} s is successful iff s ∈ T (C ∪X), where s is the computed value and σ is the computed answer. The pair “value/answer” computed in a narrowing derivation is often called output.

An important property of a narrowing strategy φ is completeness: for each solution to a given (equational) goal, a more general answer is still found by narrowing using φ.

Lazy Narrowing. In the following, we specify our (demand driven) lazy narrowing (LN) strategy in the style of [18]. Lazy narrowing reduces expressions at

1 In most narrowing strategies, σ is required to be a most general unifier of the two terms l and t|_{p}. This is not the case of needed narrowing, which may compute substitutions which are not most general.

outermost narrowable positions. Narrowing at inner positions is performed only if it is demanded by the lhs of some rule. Our formalization of LN first appeared in [1], where it was defined for conditional (CB and weakly orthogonal) TRSs. The formalization of LN uses a particular kind of unification algorithm [18] which takes advantage of the pattern discipline and the left-linearity of program rules. In particular, we use the function LU (Linear Unification) to compute the unification between a linear pattern and an arbitrary term. In contrast to standard unification algorithms, LU considers the case when there is a mismatch between a defined function symbol f and a constructor symbol c as a demand of further evaluation of f. Therefore, LU can either succeed (with outcome Success), fail (Fail) or suspend (Demand); when it suspends, it returns the set P of positions which “demand” further evaluation of their arguments. A formal definition of LU can be found in [1].

Now we define the LN strategy. We assume that the rules of R are numbered as R_{1}, …, R_{m}.

Definition 2 (Lazy Narrowing Strategy).

We define the lazy narrowing strategy as a set-valued function λ_{lazy} which, given a term t, computes the set of triples ⟨p, R_{k}, σ⟩, where p ∈ FPos(t) is a position of term t (called “lazy” position), R_{k} = (l_{k} → r_{k}) is a (renamed apart) rule of R, and σ is a substitution, as follows:

λ_{lazy}(t) = ⋃_{k=1}^{m} λ′(t, Λ, R_{k})

where λ′(t, p, R_{k}) = if Root(l_{k}) = Root(t|_{p}) then case LU(l_{k}, t_{|p}) of \{ \begin{matrix}(Success, σ) : & \{⟨p, R_{k}, σ⟩\} \\ (Fail, ∅) : & ∅ \\ (Demand, P) : & ⋃_{q∈P} ⋃_{k=1}^{m} λ′(t, p.q, R_{k}) \end{matrix} else ∅

For CB orthogonal programs, LN is (strongly) complete w.r.t. strict equations and constructor substitutions as solutions [16, 18]. Here, strong completeness means that, given a conjunction t_{1} ∧ t_{2} ∧ … ∧ t_{n}, we can nondeterministically select for evaluation just one of the conjuncts, t_{i}, without losing completeness.^{2} It is well-known that LN does not define a pure lazy evaluation strategy in the sense that it might demand the evaluation of expressions which are not really needed to compute the outcome [4].

Needed Narrowing. Here, we recall the main notions concerning the needed narrowing strategy of [4]. Needed Narrowing (NN) reduces the outermost needed positions of the input term which are unavoidable to compute the final result. NN is defined on inductively sequential programs, a (strict) subset of CB orthogonal programs. The definition of this class of programs, as well as the NN strategy, make use of the notion of a definitional tree, first introduced in [2]. From a

2 Note that, in our context, each t_{i} is a Boolean expression, in particular an equation.

declarative point of view, a partial definitional tree P can be seen as a set of linear patterns partially ordered by the strict subsumption order “<” [3]. pattern(P) denotes the minimum element of P. Given a defined function f/n, we call P a definitional tree of f if P is a partial definitional tree, pattern(P) = f(\overline{x_{n}}), where \overline{x_{n}} are distinct variables and the leaves of P are all and only variants of the left-hand sides of the rules defining f. Note that there can be more than one definitional tree for a defined function.

Definition 3 (Inductively Sequential Program).

A defined function f is called inductively sequential if it has a definitional tree. A rewrite system R is called inductively sequential if all its defined functions are inductively sequential.

Needed narrowing can be formulated as follows^{3}.

Definition 4 (Needed Narrowing Strategy).

Let R be an inductively sequential program. Let t be an operation-rooted term, and P a partial definitional tree with pattern(P) = π such that π ≤ t. We define an application λ from terms and partial definitional trees to sets of triples (position, rule, substitution) as the least set satisfying the following properties. We consider two cases for P:

1. If π is a leaf, i.e., P = {π}, and (π → r) ∈ R, λ(t, P) = {⟨Λ, π → r, id⟩}.

2. If π is a branch, consider the inductive position o of π and a child π_{i} = π[c_{i}(\overline{x_{n}})]_{o} ∈ P. Let P_{i} = \{π′ ∈ P | π_{i} ≤ π′\} be the partial definitional tree where all patterns are instances of π_{i}. We consider the following cases for the subterm t|_{o}:

λ(t, P) ∋ \begin{cases}⟨p, R, σ ∘ τ⟩ & {if t|_{o} = x ∈ X, τ = \{x/c_{i}(\overline{x_{n}})\}, and (p, R, σ) ∈ \atop λ(τ(t), P_{i});} \\ ⟨p, R, σ ∘ id⟩ & if t|_{o} = c_{i}(\overline{t_{n}}) and (p, R, σ) ∈ λ(t, P_{i}); \\ ⟨o.p, R, σ ∘ id⟩ & if t|_{o} = f(\overline{t_{n}}), f ∈ F and (p, R, σ) ∈ λ(t|_{o}, P′) where P′ is a definitional tree for f. \end{cases}

Note that each NN step can be represented as ⟨p, R, ϑ_{k} ∘ ⋯ ∘ ϑ_{1}⟩, which is called the canonical representation of a NN step. We assume that the definitional trees always contain fresh variables when they are used in a narrowing step. By abuse, we call “needed narrowing position” to the position p of a needed redex.

This mechanism differs from the needed reduction of lazy functional languages only in the instantiation of free variables by means of unifiers. The unifiers computed in NN steps may contain extra bindings which would eventually be performed later in (demand-driven) LN narrowing derivations. We refer to them as anticipated substitutions. Roughly speaking, an anticipated substitution is the part of a substitution computed in a NN step which is not computed in a “corresponding” LN step (using the same rule at the same position).

3 This definition slightly differs from the one appeared in [4], although it computes the same needed narrowing steps if we consider substitutions modulo variable renaming and restricted to Var(t). In the sequel we always assume this restriction when we compare needed narrowing and lazy narrowing.

Definition 5 (Anticipated Substitution).

Let R be an inductively sequential program and R a rule of R. Let t be a term rooted by f ∈ F, and P be a definitional tree of f. Let ⟨p, R, θ⟩ ∈ λ(t, P) and ⟨p, R, σ⟩ ∈ λ_{lazy}(t) (if they exist). We say that τ is the anticipated substitution part of θ computed by λ if θ = σ ∘ τ.

It is noteworthy that the concept of “anticipated substitution”, as informally defined in [4], does not correspond with the more declarative notion above introduced. Technically, the “anticipated substitutions” of [4] are made of those bindings computed by traversing definitional trees which do not correspond to the function which is actually reduced. This notion of “anticipation” has an operational flavor and as we are going to show in Section 4.1, for some cases, it may compute additional bindings that can not be considered as “anticipated” when we use Definition 5. Therefore, in order to distinguish between both concepts, we prefer to name the “anticipated substitutions” of [4] as anticipated bindings. A formal definition of this concept is given in Definition 7, which revels to be a valuable tool to prove several results presented in this paper.

Antoy et al. [4] proved that, for inductively sequential programs, NN is complete w.r.t. strict equations and constructor substitutions as solutions. Moreover, NN is optimal w.r.t. the independence of computed solutions and the length of successful derivations (in graph–based implementations).

3 Uniform Programs

Uniform programs were introduced in [12, 13] to improve the implementation of lazy narrowing within the functional logic language Babel [18].

Definition 6 (Uniform Program).

A uniform program is a set of rewrite rules such that the following conditions hold:

1. Flat constructor patterns: the arguments of the lhs’s of the rules are either variables or linear constructor terms of the form c(\overline{x_{n}}).

2. Orthogonality.

3. Uniformity: Let f(\overline{t_{n}}) and f(\overline{s_{n}}) be the lhs’s of two rules defining f; then, t_{i} is a variable iff s_{i} is a variable, for all i ∈ {1, …, n}.

In uniform programs, functions f/n are defined by:

(i) one or more rules whose lhs has the shape:

f(…, c_{k_{1}}(\overline{x_{m_{k_{1}}}} ), …, c_{k_{p}}(\overline{y_{m_{kp}}}), …)

where {k_{1}, …, k_{p}} ⊆ {1, …, n} are fixed positions (called inductive positions of f) addressing flat constructor terms and the remaining positions contain only variable arguments, or

(ii) one single rule whose shape is f(\overline{x_{n}}) → r.

In the former case, for every pair of (distinct) program rules, there exist at least an inductive position of the lhs’s of these rules where the corresponding arguments are rooted by two different constructors.

Example 1. The following program^{4} is uniform

f(X, 1, 2, 3) → 1, f(X, 2, 2, 3) → 2, f(X, 2, 2, 2) → 3.

In [19], simple uniform programs (i.e., uniform programs whose rules have—at most—one inductive position) were introduced and, as an easy consequence of Lemma 2 in [19], the equivalence between NN and LN over this class of programs holds for derivations leading to a hnf.

Implementation Problems and Properties Moreno et al. showed in [17] that, inside a sequential implementation of narrowing, using a deep-first search with backtracking, it is difficult to combine the lazy evaluation strategy with the use of logical variables. Uniform programs were introduced to avoid this drawback. Unfortunately, even if uniform programs have many advantages [12], they do not always suffice to get rid of useless computations (see Example 4).

Proposition 1. Uniform TRSs are inductively sequential.

The structure of the proof is very simple: Given a uniform program R, it suffices to consider that, for each defined function f of R, we can construct an associated definitional tree by using as inductive positions to build the tree the inductive positions of the function symbol (i.e., the nonvariable positions of the lhs’s of the rules defining the function f).

We have that simple uniform programs ⊆ uniform programs ⊆ inductively sequential programs ⊆ CB orthogonal programs.

It is worthwhile to note that, for uniform programs, it is possible to build the associated definitional tree by considering the set of inductive positions of the function in any possible order. This does not generally hold for (non-uniform) inductively sequential programs. In the following, we call standard definitional tree of a function f the tree in which the inductive positions of f are considered from left to right.

4 Equivalence of Lazy Evaluation Strategies

In this section, we establish the precise relation between the needed narrowing strategy of [4] and the (demand-driven) lazy narrowing strategy of [1], first for single steps and then for successful derivations.

4.1 Stepwise Equivalence

To motivate our discussion, let us begin with an example which shows that, even for uniform programs, there is not a direct, one–to–one correspondence between LN and NN steps.

4 We use capital letters to denote variables in examples.

Example 2. Consider the uniform program:

R_{1} : f(a, b) → c, R_{2} : g(c) → b.

where a, b and c are constructor symbols. Using standard definitional trees for f and g, there exists the following NN derivation:

f(X, g(Y)) ⇝_{NN}^{[2,R_{2},{X/a,Y/c}]} f(a, b) ⇝_{NN}^{[Λ,R_{1},id]} c

whereas the corresponding derivation using LN is:

f(X, g(Y)) ⇝_{LN}^{[2,R_{2},{Y/c}]} f(x, b) ⇝_{LN}^{[Λ,R_{1},{X/a}]} c

Note that, in the NN derivation, the binding X/a is computed in the first step, whereas it is computed in the second step in the corresponding LN derivation.

We formalize the precise correspondence between LN and NN steps in Proposition 2. First, we need to prove some preparatory results.

The following lemma establishes that NN does not compute anticipated substitutions when the NN step is performed at the root position of the term.

Lemma 1. Let R be a uniform program and R ∈ R a program rule. Let t be an operation-term and P be a definitional tree for the root of t. Then, ⟨Λ, R, σ⟩ ∈ λ(t, P) iff ⟨Λ, R, σ⟩ ∈ λ_{lazy}(t).

As we mentioned before, the ability to anticipate some bindings in the NN strategy is the key to avoid some unnecessary computations: if the evaluation of a subterm t|_{p} is demanded by some program rule, after the evaluation of this subterm (to a hnf), only the rules which actually demanded the evaluation of t|_{p} can be applied. Indeed, thanks to the anticipated substitutions, only strongly sequential redexes are reduced in needed narrowing derivations [4]. The computation of anticipated substitutions makes the difference between the LN and NN strategies. However, in order to state and prove the precise relation between LN and NN computation steps for arbitrary input terms, we need a more operational and technical notion of “anticipation”, which we formulate by mimicking the definition of a NN step, called anticipated bindings. Both notions do coincide for linear terms but they may differ for non-linear terms.

Definition 7 (Anticipated Bindings).

Let R be a program, t be an operation-rooted term, and P be a partial definitional tree such that pattern(P) = π and π ≤ t. We define the set of anticipated bindings α(t, P) in λ(t, P) as a mapping from terms and partial definitional trees to sets of substitutions as follows:

1. If π is a leaf, α(t, P) = {id}.

2. If π is a branch,

α(t, P) ∋ \begin{cases}τ′ ∘ τ & if t|_{o} = x ∈ X, τ = \{x/c_{i}(\overline{x_{n}})\}, ⟨Λ, R, σ⟩ ∉ λ(τ(t), P_{i}), for some rule R and substitution σ, and τ′ ∈ α(τ(t), P_{i}); \\ τ′ ∘ id & if t|_{o} = c_{i}(\overline{t_{n}}), ⟨Λ, R, σ⟩ ∉ λ(t, P_{i}), for some rule R and substitution σ, and τ′ ∈ α(t, P_{i}); \\ τ′ ∘ id & if ⟨Λ, R, σ⟩ ∉ λ(t, P), t|_{o} = g(\overline{t_{n}}), g ∈ F, ⟨Λ, R, σ⟩ ∉ λ(t|_{o}, P′), for some rule R and substitution σ, and τ′ ∈ α(t|_{o}, P′) with P′ a definitional tree of g. \\ id & otherwise \end{cases}

where o is the inductive position of π, π_{i} = π[c_{i}(x_{1}, …, x_{n})]_{o} ∈ P is a child of π, and P_{i} = {π′ ∈ P | π_{i} ≤ π′} is a proper subtree of P.

The following examples illustrate the difference between this definition and the notion of anticipated substitution.

Example 3. Consider the uniform program:

R_{1} : f(a, b) → c R_{2} : f(a, c) → b R_{3} : g(a) → c R_{4} : g(c) → b

and the standard definitional trees P and P′ for f and g, respectively.

– Consider the term g(Z). Then, pattern(P′) is a branch and the fourth case of Definition 7(2) holds, since

λ(g(a), P′_{1}) = {⟨Λ, R_{3}, id⟩} and λ(g(c), P′_{2}) = {⟨Λ, R_{4}, id⟩}.

Therefore, α(g(Z), P′) = {id}, which does coincide with the anticipated substitution.

– Given the term f(X, f(Y, g(Z))), we have that

⟨2.2, R_{4}, id ∘ {Z/c} ∘ id ∘ {Y/a} ∘ id ∘ {X/a}⟩ ∈ λ(f(X, f(Y, g(Z))), P)

and ⟨Λ, R_{4}, id∘{Z/c}⟩ ∈ λ(f(a, f(a, g(Z)))|_{2.2}, P′). Hence, Definition 7 computes the anticipated bindings: id ∘ {Y/a} ∘ id ∘ {X/a} = {Y/a, X/a} ∈ α(f(X, f(Y, g(Z))), P), which also agree with the anticipated substitution. Roughly speaking, for the above term, the substitution computed by α consists of the bindings computed by λ before the demanded position 2.2 is considered and, hence, before the “non–anticipated” bindings id ∘ {Z/c} are computed by the call to λ(f(a, f(a, g(Z)))|_{2.2}, P′). Note that, the computation of the mapping α stops returning the binding id and disregarding the “non–anticipated” part, when the subterm g(Z) of f(a, f(a, g(Z))) at position 2.2 is reached.

– Finally, consider the non-linear term f(Z, f(Y, g(Z))). Then,

id ∘ id ∘ {Y/a} ∘ id ∘ {Z/a} = {Y/a, Z/a} ∈ α(f(Z, f(Y, g(Z))), P)

Moreover, it holds that

⟨2.2, R_{3}, id ∘ id ∘ id ∘ {Y/a} ∘ id ∘ {Z/a}⟩ ∈ λ(f(Z, f(Y, g(Z))), P)

but ⟨2.2, R_{3}, {Z/a}⟩ ∈ λ_{lazy}(f(Z, f(Y, g(Z)))). This means that the mapping α computes an anticipated binding Z/a which does not belong to the corresponding “anticipated substitution” associated to this step.

The following proposition establishes the precise relation between LN and NN steps: given a NN step from t which computes the substitution σ ∘τ, where τ are the bindings anticipated in this step, there exists a corresponding LN step from τ(t) which computes the substitution σ by reducing the same position using the same program rule (and vice versa).

Proposition 2. Let R be a uniform program and R ∈ R a program rule. Let t be an operation-rooted term. Then, ⟨p, R, σ⟩ ∈ λ_{lazy}(τ(t)) iff there exists some definitional tree P for Root(t) such that ⟨p, R, σ ∘τ⟩ ∈ λ(t, P), where τ ∈ α(t, P) are the anticipated bindings in λ(t, P).

As a corollary, we obtain the following result, which holds for each single narrow-

ing step. A NN step t ⇝_{NN}^{[p,R,σ∘τ]} s can be proved iff there exists a corresponding

LN step τ(t) ⇝_{LN}^{[p,R,σ]} s, where τ ∈ α(t, P) are the bindings anticipated in the computation λ(t, P).

Note that Proposition 2 holds for an arbitrarily fixed definitional tree; this amounts to say that, for each LN step, there is an appropriate definitional tree such that the corresponding NN step can be proven.

To finish this subsection, let us mention a stronger equivalence, step by step, between NN and LN steps over simple uniform programs. This is an easy consequence of Proposition 2, and establishes that, for simple uniform programs, NN does not produce anticipated bindings.

Corollary 1. Let R be a simple uniform program. Let t be an operation-rooted term and P be the definitional tree for Root(t). Then, λ_{lazy}(t) = λ(t, P).

It is interesting to note that Corollary 1 is stronger than Lemma 2 in [19], which only entails the equivalence for derivations leading to a hnf while our results demonstrate the equivalence, step by step, between the NN and LN strategies over simple uniform programs (and thus the equivalence of derivations leading to arbitrary terms). Moreover, our result guarantees that these derivations use the same rules over the same positions at each computation step.

5 Uniform Lazy Narrowing

Proposition 2 shows that every lazy position of a term (w.r.t. a uniform program) is computed by λ, hence it is needed. Since all needed positions must be exploited in order to compute the final outcome and, according to the completeness results for needed narrowing, the order in which needed positions are considered is not relevant, it turns out that, for uniform programs, an optimization of LN is possible by a don’t care selection among the demanded positions of the input term. This is similar to the uniform narrowing strategies introduced in [7] for canonical TRSs, which narrow only one position of the considered term while still preserving completeness. This kind of strategies has inspired us to use the name Uniform Lazy Narrowing (ULN) for the optimization of the LN strategy which we formalize as follows. Again, we assume that the rules of R are numbered as R_{1}, …, R_{m}.

Definition 8 (Uniform LN Strategy).

Let R be a uniform program. We define the uniform lazy narrowing strategy as a set-valued function:

λ_{ulazy}(t) = ⋃_{k=1}^{m} λ′_{u}(t, Λ, R_{k})

where λ′_{u}(t, p, R_{k}) = if Root(l_{k}) = Root(t|_{p}) then case LU(⟨l_{k}, t|_{p}⟩)of \{ \begin{matrix}(Success, σ) : & \{⟨p, R_{k}, σ⟩\} \\ (Fail, ∅) : & ∅ \\ (Demand, P) : & ⋃_{k=1}^{m} λ′_{u}(t, p.q, R_{k}) \\ & with q = select don′t care(P) \end{matrix} else ∅

where the function select don′t care(S) arbitrarily chooses one element of the set S.

Note that the ULN strategy only selects one redex position p in a term (although several triples (p, R, σ) can be associated to that position p). Informally, the above strategy allows us to overcome the loss of efficiency of (unoptimized) LN strategies (w.r.t. NN) which is due to the “don’t-know” nondeterministic choice of all demanded positions in a LN reduction, in contrast to the more effective “don’t-care” choice of the particular definitional tree for f in NN steps. In ULN computations, note that one can fix any selection strategy, e.g., a left-to-right (Prolog like) selection of demanded positions, just in the same way needed narrowing fixes one of the possible definitional trees for computing. The following example illustrates how our ULN strategy takes advantage of this property to disregard some useless “redundant” LN derivations.

Example 4. Given the program

R_{1} : f(a, a) → 0, R_{2} : g(a) → a. and the term t = f(g(X), g(Y)), if we use the standard definitional tree for f, the NN strategy computes only one (successful) derivation:

f(g(X), g(Y)) ⇝_{NN}^{[1,R_{2},{X/a}]} f(a, g(Y))
⇝_{NN}^{[2,R_{2},{Y/a}]} f(a, a)
⇝_{NN}^{[Λ,R_{1},id]} 0.

However, the LN strategy produces a search tree with two branches where the leftmost branch “matches” the former NN derivation and the rightmost branch can be considered a “redundant” LN derivation. On the other hand, if we fix a different definitional tree for f, which first considers the inductive position 2, then the NN strategy only computes the rightmost LN derivation:

f(g(X), g(Y)) ⇝_{NN}^{[2,R_{2},{Y/a}]} f(g(X), a)
⇝_{NN}^{[1,R_{2},{X/a}]} f(a, a)
⇝_{NN}^{[Λ,R_{1},id]} 0.

Now the leftmost branch represents the “redundant” LN derivation.

5.1 Equivalence of Derivations

Now, we are ready to state and prove the relation between general LN and NN derivations over uniform programs. Although we restrict the discussion to the ULN strategy, most of our results can be easily extended to rough LN.

The following example reveals that, even for uniform programs, NN and ULN do not compute the same values and answers for arbitrarily fixed definitional trees, unless we require the evaluation to reach a head normal form.

Example 5. Given the uniform program

R_{1} : f(a, b) → b, R_{2} : g(c(Y)) → Y, R_{3} : h(b) → b.

and the term f(g(X), h(Z)), there exists only one ULN derivation for this term (selecting the subset of triples associated to the leftmost lazy position), which outcomes the result ⟨f(Y, b), {Z/b, X/c(Y)}⟩:

f(g(X), h(Z)) ⇝_{ULN}^{[1,R_{2},{X/c(Y)}]} f(Y, h(Z)) ⇝_{ULN}^{[2,R_{3},{Z/b}]} f(Y, b)

However, by considering standard definitional trees for f, g and h, we have the NN derivation:

f(g(X), h(Z)) ⇝_{NN}^{[1,R_{2},{X/c(Y_{2})}]} f(Y_{2}, h(Z)) ⇝_{NN}^{[2,R_{3},{Z/b}∘{Y_{2}/a}]} f(a, b)

which computes the term f(a, b) and substitution {Z/b, X/c(a)}. Now, if a subsequent narrowing step (reaching a hnf) is performed, both derivations end with the same values and answers (up to renaming). It is important to note that there exists an additional, redundant LN derivation, whose first step uses rule R_{3} and whose second step uses rule R_{2}. This derivation is cut when we choose the select don′t care function to be a left-to-right selection function.

The following theorem establishes that each NN derivation to a head normal form can be mimicked by ULN and vice versa.

Theorem 1. Let R be a uniform program and t an operation-rooted term. Then,

1. there exists a NN derivation D = (t ⇝_{NN}^{σ}^{∗} s), where s is a hnf, iff there exists a corresponding ULN derivation D′ = (t ⇝_{ULN}^{σ}^{∗} s);

2. D and D′ have the same length, and they use the same rules over the same positions on the corresponding steps.

The following result is a direct consequence of Theorem 1.

Corollary 2. Let R be a uniform program and e be an equation. There exists a NN derivation e ⇝_{NN}^{σ}^{∗} true iff there exists the ULN derivation e ⇝_{ULN}^{σ}^{∗} true.

5.2 Correctness of Uniform Lazy Narrowing

Corollary 2 together with the soundness and completeness of NN entail the correctness of ULN w.r.t. the strict equality and constructor substitutions as solutions in uniform programs.

Theorem 2. Let R be a uniform program and e be an equation.

1. (Soundness) if e ⇝_{ULN}^{σ}^{∗} true is a ULN derivation, then σ is a solution for e.

2. (Completeness) For each constructor substitution σ which is a solution of e,

there exists a ULN derivation e ⇝_{ULN}^{σ′}^{∗} true with σ′ ≤ σ [Var(e)].

It is important to note that Theorem 2 demonstrates that ULN is strongly complete (i.e., all lazy positions which may occur inside a term but one can be disregarded without jeopardizing completeness).

6 Conclusions

This paper investigates the precise relation between the needed narrowing strategy of [4] and the (demand-driven) lazy narrowing strategy of [1]. The original contributions are:

– Uniform programs are a subclass of the inductively sequential programs (Proposition 1).

– For uniform programs, a precise relation between needed narrowing and lazy narrowing derivations (and steps) has been established in terms of “anticipated bindings” (Proposition 2).

– For uniform programs, an optimized lazy evaluation strategy, called uniform lazy narrowing, has been formulated, which is still complete and strongly equivalent to needed narrowing on the class of uniform programs (Theorem 1).

These results offer the first proof that (uniform) lazy narrowing enjoys the optimality properties of needed narrowing over the class of uniform programs.

Recent implementations of functional logic languages [5, 15] which are based on definitional trees first transform inductively sequential programs into (a Prolog representation of simple) uniform programs, and then apply a demand-driven strategy codified in Prolog. This is the technique most commonly proposed to compute NN steps in inductively sequential systems even if the correspondence w.r.t. the original NN computation model was never formalized nor claimed [4]. Our results in this paper demonstrate that, by first using a semantics preserving transformation from inductively sequential programs into uniform programs [12, 19], and then using the uniform lazy narrowing strategy to execute the resulting uniform program, we get the same successful derivations as by running the original inductively sequential program by needed narrowing. Since there exist several implementations of functional logic languages which are based on a similar transformation model [9, 12, 14, 15, 18], the results in this paper can be seen as a formal demonstration that current NN implementations fit the intended (needed narrowing) semantics of the languages.

References

1. M. Alpuente, M. Falaschi, P. Julián, and G. Vidal. Specialization of Lazy Functional Logic Programs. In Proc. of PEPM’97, volume 32, 12 of Sigplan Notices, pages 151–162, New York, 1997. ACM Press.

2. S. Antoy. Definitional trees. In Proc. of ALP’92, volume 632 of Lecture Notes in Computer Science, pages 143–157. Springer-Verlag, Berlin, 1992.

3. S. Antoy. Optimal non-deterministic functional logic computations. In Proc. of ALP’97, volume 1298 of Lecture Notes in Computer Science, pages 16–30. Springer-Verlag, Berlin, 1997.

4. S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. Journal of the ACM, 47(4):776–822, July 2000.

5. S. Antoy and M. Hanus. Compiling multi-paradigm declarative programs into prolog. In Proc. of FroCoS 2000, pages 171–185. Springer LNCS 1794, 2000.

6. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

7. R. Echahed. Uniform narrowing strategies. In Proc. of ICALP’92, pages 259–275. Springer LNCS 632, 1992.

8. M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming, 19&20:583–628, 1994.

9. M. Hanus. Efficient translation of lazy functional logic programs into Prolog. In Proc.of LOPSTR’95, pages 252–266. Springer LNCS 1048, 1995.

10. M. Hanus, H. Kuchen, and J.J. Moreno-Navarro. Curry: A Truly Functional Logic Language. In Proc. of ILPS’95, pages 95–107, 1995.

11. G. Huet and J.J. Lévy. Computations in orthogonal rewriting systems, Part I + II. In J.L. Lassez and G.D. Plotkin, editors, Computational Logic – Essays in Honor of Alan Robinson, pages 395–443, 1992.

12. H. Kuchen, R. Loogen, J.J. Moreno-Navarro, and M. Rodríguez-Artalejo. Lazy Narrowing in a Graph Machine. In Proc. of ALP’90, volume 463 of Lecture Notes in Computer Science, pages 298–317, 1990.

13. H. Kuchen, F.J. López-Fraguas, J.J. Moreno-Navarro, and M. Rodríguez-Artalejo. Implementing a Functional Logic Language with Disequality Constrains. In K. Apt, editor, Proc. of JICSLP’93, pages 207–221. The MIT Press, Cambridge, MA, 1993.

14. R. Loogen, F. López-Fraguas, and M. Rodríguez-Artalejo. A Demand Driven Computation Strategy for Lazy Narrowing. In J. Penjam and M. Bruynooghe, editors, Proc. of PLILP’93, pages 184–200. Springer LNCS 714, 1993.

15. F.J. López-Fraguas and J. Sánchez-Hernández. TOY: A Multiparadigm Declarative System. In Proc. of RTA’99, pages 244–247. Springer LNCS 1631, 1999.

16. A. Middeldorp, S. Okui, and T. Ida. Lazy Narrowing: Strong Completeness and Eager Variable Elimination. Theoretical Computer Science, 167(1,2):95–130, 1996.

17. J.J. Moreno-Navarro, H. Kuchen, J. Mariño-Carballo, S. Winkler, and W. Hans. Efficient Lazy Narrowing using Demandedness Analysis. In J. Penjam and M. Bruynooghe, editors, Proc. of PLILP’93, pages 167–183. Springer LNCS 714, 1993.

18. J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: The language Babel. Journal of Logic Programming, 12(3):191–224, 1992.

19. F. Zartmann. Denotational Abstract Interpretation of Functional Logic Programs. In P. Van Hentenryck, editor, Proc. of SAS’97, pages 141–159. Springer LNCS 1302, 1997.