Needed Narrowing in Prolog

Sergio Antoy

Portland State University

TR 96-2

May 17, 1996

Abstract

We describe the implementation of needed narrowing deployed in a compiler of a functional-logic language and present a few related concepts and results. Our implementation is obtained by translating rewrite rules into Prolog source code and optionally applying a set of optimizations to this code. We benchmark the effectiveness of each individual optimization. We show that our implementation is more efficient than all other previously proposed similar implementations. We measure both execution times, as is customarily done, and memory allocation that turns out to be a significant factor. We solve equations using a semi-strict equality relation that generalizes classic strict equality with sometimes a smaller search space. We give a new, more declarative and accessible formulation of a definitional tree, a crucial concept of our approach, and we present a simple algorithm to build definitional trees. We briefly explore a notion of simplification that is applicable to and sometimes beneficial for computations in inductively sequential systems, where classic simplification is not applicable.

This work has been supported in part by the National Science Foundation under grant CCR-9406751.

Author’s address: Dept. of Computer Science, P.O. Box 751, Portland, OR 97207, antoy@cs.pdx.edu.

2

1 Introduction

We describe the implementation of an advanced narrowing strategy, needed narrowing [3], in Prolog. Our implementation has been deployed in an extension [4] of the Gödel compiler [12], which translates Gödel source code into Prolog source code. Our implementation is high-level, portable, similar in scope to previously proposed implementations [1, 5, 6, 13, 15, 17] and more efficient.

Narrowing is a widely used procedure for performing functional computations in a logic programming environment [10]. The appeal of narrowing for this task stems from its ability to evaluate functional expressions containing uninstantiated logic variables. Functions are defined by rewriting [7, 14]. A narrowing step rewrites a functional expression after possibly instantiating some of its variables. A narrowing strategy selects in an expression both the instantiation of its variables and its redex, and is aimed at ensuring desirable properties such as the efficiency and completeness of computations.

Narrowing is employed in functional-logic programming mainly to solve equations. Consider the following rewrite system, where upper case identifiers denote the variables.

0 + X → X
s(X) + Y → s(X + Y)
0 ⩽ → true
s( ) ⩽ 0 → false
s(X) ⩽ s(Y) → X ⩽ Y

double(X) → X + X
half (0) → 0
half (s(0)) → 0
half (s(s(X))) → s(half (X))

For example, narrowing computes solutions to the equation X ⩽ Y + Z ≈ true as follows. There are three (most general) substitutions that create a redex in the equation: {X ↦ 0}, {Y ↦ 0}, and {Y ↦ s(Y_{1})}. The first substitution yields 0 ⩽ Y + Z ≈ true which is reduced to true ≈ true by the first rule of ⩽ and eventually to true. Thus, {X ↦ 0} is a solution of the equation. The other substitutions allow us to rewrite the right subterm of ⩽. For example, the third substitution yields X ⩽ s(Y_{1}) + Z ≈ true which is reduced to X ⩽ s(Y_{1} + Z) ≈ true by the second rule of +. Further narrowing steps applied to this equation compute solutions that composed with {Y ↦ s(Y_{1})} compute solutions of the initial equation.

In Section 2 we make precise the scope of our discussion. In Section 3 we recall the needed narrowing strategy. In Section 4 we describe the generation of Prolog code that solves equations by needed narrowing. In Section 5 we describe several transformations of the Prolog code intended to improve the efficiency of computations. In Section 6 we measure the efficiency of our technique. In Section 7 we compare our technique with related work. In Section 8 we discuss future directions of our work.

2 Scope

We consider many-sorted, constructor based, inductively sequential rewrite systems. The first two concepts are standard notions of rewriting defined, e.g., in [7, 14]. The third concept is defined in [2] and recalled in the next section.

We consider a rewrite system with rules R and signature Σ. R may be non-terminating, hence some terms over Σ may not have a normal form. Under these conditions it is appropriate to define the validity of an equation as follows. The equality rules of Σ are defined below, where ∧ is a new right associative, infix symbol and there is one rule for each constructor c in Σ.

true ∧ X → X
c ≈ c → true  ∀c/0 ∈ Σ
c(X_{1}, …, X_{n}) ≈ c(Y_{1}, …, Y_{n}) → (X_{1} ≈ Y_{1}) ∧ ⋯ ∧ (X_{n} ≈ Y_{n})  ∀c/n ∈ Σ

The equality rules define an equivalence on terms referred to as strict equality and commonly used when computations may not terminate [8, 16]. A solution of an equation t ≈ u is a substitution σ such that σ(t ≈ u) rewrites to true using both R and the equality rules of Σ. A literal application of the equality rules may lead to an inefficient enumeration of all the narrowing derivations of a term. We correct this problem, in practice, by extending the above rules with

X ≈ X → true

and imposing that only constructor substitutions are acceptable for X.

We limit our discussion to unconditional rewrite systems. However, extending our discussion to conditional rewrite systems, e.g., as done in [15], does not create significant problems. Indeed, our implementation is applied conditional systems in [4].

3 Needed Narrowing

Needed Narrowing [3] is an optimal strategy in the sense that only unavoidable steps are performed to find the solutions of equations. It is defined for inductively sequential rewrite systems. Each operation in these systems is associated with a structure called definitional tree. Below, we recall this concept, central to our approach, in a more declarative form than in [2]. An algorithm to build definitional trees is presented in Appendix A.

A pattern is a term of the form f(t_{1}, …, t_{n}), where f is a defined operation and, for all i, t_{i} is a constructor term. A definitional tree of an operation f is a non-empty set T of patterns partially ordered by subsumption and having the following properties up to renaming of variables.

• [root property] The minimum element, referred to as the root, of T is f(X_{1}, …, X_{n}), where X_{1}, …, X_{n} are distinct variables.

• [leaves property] The maximal elements, referred to as the leaves, of T are all and only (variants of) the left hand sides of the rules defining f. Non-maximal elements are referred to as branches.

• [parent property] If π is a pattern of T different from the root, there exists in T a unique pattern π′ strictly preceding π such that there exists no other pattern strictly between π and π′. π′ is referred to as the parent of π and π as a child of π′.

• [induction property] All the children of a same parent differ from each other only at the position of a variable, referred to as inductive, of their parent.

There exist operations with no definitional tree, and operations with more than one definitional tree, examples are in [2]. The existence of a definitional tree of a function f is decidable and simple in most practical situations. An operation is called inductively sequential if it has a definitional tree. A rewrite system is called inductively sequential if all its operations are inductively sequential. The inductive sequentiality of a rewrite system R is obtained at no cost by establishing a priority on the rules of R based on either textual ordering or specificity, as done in most functional languages with pattern matching.

The adjective “inductive” is motivated by the fact that, for completely defined operations, the children of a pattern are obtained by “doing a data type induction” on the inductive variable of their parent. This variable is typeset in boldface in the examples. The trees of the operations ⩽ and + are pictorially shown below.

X_{1} ⩽ X_{2} 0 ⩽ X_{2}  s(X_{3}) ⩽ X_{2} s(X_{3}) ⩽ 0  s(X_{3}) ⩽ s(X_{4})  Y_{1} + Y_{2} 0 + Y_{2}  s(Y_{3}) + Y_{2}

Definitional trees make it particularly easy to operationally define needed narrowing. Let t = f(t_{1}, …, t_{k}) be an operation-rooted term to narrow. We most-generally unify t with some nondeterministically chosen maximal pattern π in a definitional tree T of f. Let σ be one such unifier. If π is a leaf of T, σ(t) is a redex and we reduce it. If π is a branch of T, we consider the subterm u of σ(t) matched by the inductive variable of π. u cannot be a variable. If u is operation-rooted, we attempt to narrow u to a head normal form. If u is constructor-rooted, we fail, since it can be shown [3] that σ(t) cannot be narrowed at the top, which is necessary to solve any equation of which t is a side.

For example, consider the term t = X ⩽ Y + Z discussed in our introductory example. Let T be the definitional tree of the operation ⩽ shown earlier. The maximal elements of T that unify with t are 0 ⩽ X_{2} and s(X_{3}) ⩽ X_{2}. The first pattern is a leaf, thus, t{X ↦ 0} can be reduced at the root. The second pattern is a branch and X_{2} is its inductive variable, thus, we attempt to narrow Y + Z, the subterm of s(X_{3}) ⩽ Y + Z matching X_{2}. As seen in this example, needed narrowing does not always chooses most general unifiers.

4 Code Generation

Our implementation maps each defined operation f of an inductively sequential rewrite system R, into a predicate f_{0} of a Prolog program. If the type of f is t_{1} × t_{2} × ⋯ × t_{n} → t, then the type of f_{0} is t_{1} × t_{2} × ⋯ × t_{n} × t. The predicate f_{0} invokes a finite set of auxiliary predicates f_{1}, f_{2}, … depending on f, too. If f_{i}(u_{1}, …, u_{n}, u) succeeds, i ⩾ 0, then u is a head normal form (minimal in a sense not discussed in this paper) of f(u_{1}, …, u_{n}).

We define f_{0}, f_{1}, … as the output of the procedure CodeGen, defined shortly, on input f. CodeGen takes two arguments: p and N. p is a natural number indexing the predicate identifier f and N is a subtree of a definitional tree of f. CodeGen is recursive. The values of p and N in the initial call to CodeGen are 0 and T, a definitional tree of f. The value of p in recursive calls to CodeGen is the next yet unused index in the generation of f_{0}, f_{1}, . . ..

A shallow constructor term is a term c(X_{1}, …, X_{m}), where c is a constructor, m ⩾ 0 is the arity of c and X_{1}, …, X_{m} are fresh variables. If m = 0, the term is simply c. We call shallow constructor term enumeration of sort s an enumeration c_{1}, …, c_{j} of all the shallow constructor terms of a sort s, up to variable renaming.

A head normal form is a term t such that no descendant of t will ever be a redex. In constructor based system “useful” head normal forms are constructor-rooted terms. In the following discussion, we consider uninstantiated variables head normal forms, too, since both our implementation and the Gödel compiler in which it is embedded instantiate variables to constructor-rooted terms only.

The computation of CodeGen depends on whether or not N is a leaf of T. Several optimizations of the code produced by CodeGen will be discussed in the next section.

1. Case N is a branch of T Let π = f(t_{1}, …, t_{n}) be the pattern at the root of N, let t_{i} be the inductive variable of the pattern, and let s be the sort of t_{i}. The clauses generated by CodeGen are called to evaluate to head normal form a functional expression exp = f(u_{1}, …, u_{n}) that is known to unify with π^{1}. The first problem is to find whether π is maximal among the patterns of T that unify with exp. Let u denote the i-th argument of exp. i.e., the subterm of exp matching t_{i}. We consider three subcases:

• u is operation-rooted: then π is maximal.

• u is a variable: then all the children of N contain maximal patterns unifying with exp.

• u is constructor-rooted: then at most one child of N contains maximal patterns unifying with exp (exactly one child if f is completely defined).

Thus, the clauses generated by CodeGen must determine which of the above subcases u satisfies and in each case dispatch an appropriate clause to continue the computation of needed narrowing of exp.

The detection of the subcase satisfied by u is performed via unification by a set of clauses whose heads differ only at the i-th argument. In these clauses, shown below, c_{1}, …, c_{j} is a shallow constructor term enumeration of sort s, and R is a new variable.

f_{p}(t_{1}, …, X, …, t_{n}, R) :− var(X), !, …  0
f_{p}(t_{1}, …, c_{1}, …, t_{n}, R) :− !, …  1
⋯
f_{p}(t_{1}, …, c_{j}, …, t_{n}, R) :− !, …  j
f_{p}(t_{1}, …, X, …, t_{n}, R) :− …  j + 1

The cut makes these clauses mutually exclusive. Now, we describe the code of the yet undefined portions of the bodies.

Clause number 0 is completed as follows

f_{p}(t_{1}, …, X, …, t_{n}, R) :− var(X), !, f_{p_{0}}(t_{1}, …, X, …, t_{n}, R).

where f_{p_{0}} is a new predicate defined by j clauses identical to clauses 1 to j of f_{p}, but without the cut. As shown shortly, this code executes a descent down some non-deterministically chosen path of N where some maximal patterns unifying with exp can be found.

1This fact is obviously true for the root pattern of T and can be shown to be invariant through recursive calls of CodeGen.

The k-th clause, for k in 1, …, j, is either

f_{p}(t_{1}, …, c_{k}, …, t_{n}, R) :− !, f_{p_{k}}(t_{1}, …, c_{k}, …, t_{n}, R).

or

f_{p}(t_{1}, …, c_{k}, …, t_{n}, ) :− !, fail.

The first clause is generated when N has a child, say N_{k}, whose pattern has a variant of c_{k} at the position of the inductive variable of π. In this case, f_{p_{k}} is a new predicate generated by the call CodeGen(p_{k}, N_{k}). This code executes a descent down the unique path of N where some maximal patterns unifying with exp can be found. Otherwise, CodeGen generates the second clause. In this case it can be shown that exp cannot be narrowed to a head normal form because f is not completely defined.

The last clause of f_{p} is executed only when the i-th argument of exp, unified with the variable X, is an operation-rooted term. Clause number j + 1 is defined as follows

f_{p}(t_{1}, …, X, …, t_{n}, R) :− ftp_{s}(X, H), f_{p_{j+1}}(t_{1}, …, H, …, t_{n}, R).

where ftp_{s}, defined later, evaluates the functional expression instantiating X to head normal form and binds this value to Y, and f_{p_{j+1}} is a new predicate defined by j + 1 clauses identical to clauses 0 to j of f_{p}.

In our examples, we use more expressive names than indexing the translated function’s identifier. Below, we show the predicate add generated from the operation + defined in the introduction. The clauses defining add 10 are shown later. The clauses defining add 1s are similarly computed. The clauses defining add 1v and add 1h are easy to compute from the definition of add.

      add(A,B,C) :- var(A), !, add_1v(A,B,C).
      add(0,B,C) :- !, add_10(0,B,C).
      add(s(A),B,C)) :- !, add_1s(s(A),B,C).
      add(A,B,C) :- ftp_nat(A,H), add_1h(H,B,C).

2. Case N is a leaf of T Let π = f(t_{1}, …, t_{n}) be the pattern of N and l → r the rule of R such that l and π are variants. Let σ be a renaming substitution such that f(t_{1}, …, t_{n}) → r′ = σ(l → r). We consider three exhaustive and mutually exclusive subcases, i.e., whether r′ is a variable, or a constructor-rooted term, or an operation-rooted term.

2.1 Case r′ is a variable, say X. There exists a unique occurrence of X in t_{1}, …, t_{n}. Let s be the sort of X and let c_{1}, …, c_{j} be a shallow constructor term enumeration of sort s. CodeGen generates the following j + 2 clauses

f_{p}(t_{1}, …, t_{n}, X) :− var(X),!.  0
f_{p}(t_{11}, …, t_{1n}, c_{1}) :− !.  1
⋯
f_{p}(t_{j1}, …, t_{jn}, c_{j}) :− !.  j
f_{p}(t_{1}, …, t_{n}, R) :− ftp_{s}(X, H), f_{q}(t′_{1}, …, t′_{n}, R).  j + 1

where t_{hk}, 1 ⩽ h ⩽ j, 1 ⩽ k ⩽ n, is identical to t_{k} except for the instantiation of X to c_{h}, t′_{k} is identical to t_{k} except for the replacement of X with H, and f_{q} is a new predicate defined by j + 1 clauses equal to clauses 0 to j of f_{p}.

If one of these clauses succeeds, the last argument of f_{p} is a head normal form. This is obvious for clauses 0 to j. For clause j + 1, this property is a consequence of the definitions of ftp_{s}, presented shortly, and of f_{q}.

For example, the clauses generated by the first rule of + are

      add_10(0,B,B) :- var(B), !.
      add_10(0,0,0) :- !.
      add_10(0,s(B),s(B)) :- !.
      add_10(0,B,C) :- ftp_nat(B,H), add_10_2h(0,H,C).

2.2 Case r′ is a constructor-rooted term. CodeGen generates the following single clause.

f_{p}(t_{1}, …, t_{n}, r′).

If this clause succeeds, the last argument of f_{p} is obviously a head normal form.

2.3 Case r′ is an operation-rooted term. Let r′ = g(u_{1}, …, u_{m}). CodeGen generates the following single clause, where R is a fresh variable and g_{0} is the predicate generated by Codegen on input g.

f_{p}(t_{1}, …, t_{n}, R) :− g_{0}(u_{1}, …, u_{m}, R).

If this clause succeeds, then it can be shown by induction on its proof tree that R is instantiated to a head normal form.

Definition of ftp

We have used in the previous clauses a family of predicates, ftp_{s}, where s is a sort, that we now define. For each each sort s, for each defined operation g whose range is s, we define the following clause of ftp_{s}.

ftp_{s}(g(X_{1}, …, X_{n}), R) :− !, g_{0}(X_{1}, …, X_{n}, R).

This clause is executed during the evaluation of exp when it is necessary to evaluate a subexpression of the form g(t_{1}, …, t_{n}). The execution of this clause invokes the predicate g_{0} generated by CodeGen on input g. If this clause succeeds, R is instantiated to a head normal form of g(t_{1}, …, t_{n}).

For example, the clauses of ftp_{nat} for the operations + and half are shown below, where, as usual, we denote the binary addition with its standard infix operator, and the corresponding predicate generated by CodeGen with add.

      ftp_nat(A+B,H) :- !, add(A,B,H).
      ftp_nat(half(A),H) :- !, half(A,H).

Strict Equality

Equations are solved by narrowing them to true. The equality rules presented in Section 2 define a set of operations, ∧ and ≈_{s}, where s ranges over the sorts of Σ, that are inductively sequential. CodeGen applied to these operations generates Prolog clauses that can be used to compute head normal forms. Indeed, the only head normal form they compute is true, thus, CodeGen gives us the Prolog code for solving equations with no additional machinery.

In practice, we use a “specialized” version of CodeGen, that improves the code in several ways. In particular • The family of Prolog predicates ≈_{s}_{i} is binary. These predicates succeed rather than returning

true in a third argument.

• If both arguments of ≈_{s}_{0} are uninstantiated variables, then ≈_{s}_{0} unifies these variables and succeeds. Since our approach only substitutes variables with constructor terms^{2}, this computation is consistent with our discussion in Section 2.

• ∧_{0}, ∧_{1}, … are not generated. In their places we use the boolean conjunction already available in Prolog.

• We apply to ≈_{s}_{i} the optimizations discussed in the next section and an additional optimization, discussed later, applicable to functions that have more than one definitional tree.

The code implementing the strict equality predicate for natural numbers is shown in Appendix B.

5 Optimizations

In this section we describe some transformations of the code generated by CodeGen that are intended to improve the efficiency of computations. Except where explicitly stated, we describe each optimization independently of the other. In many cases, several optimizations can be applied to the same predicate. Constructor elimination and first argument indexing are borrowed from [11]. Some optimizations are not straightforward and we have only the space to sketch them and show an example.

Rule call elimination

CodeGen on input of a leaf node outputs a predicate defined by only one clause in two of the three cases discussed earlier. A call to this clause is easily unfolded. For example, the second rule of + generates only

      add_1s(s(A),B,s(A+B)).

The predicate add 1s is called from one clause of add, namely

      add(s(A),B,C)) :- !, add_1s(s(A),B,C).

We unfold this call and avoid the definition of add 1s altogether. The result simply becomes

      add(s(A),B,s(A+B)) :- !.

Constructor elimination

Our implementation may generate predicates all of whose invocations and defining clause heads have a same argument rooted by a same constructor, possibly a constant. In this case, the argument may be replaced by the sequence of the argument’s arguments. For example, an auxiliary predicate, that we identify with half 1s, generated by the rules of the defined operation half , is defined by

      half_1s(s(A),B) :- var(A), !, ...
      half_1s(s(0),B) :- !, ...

2This property also holds for Gödel, whose compiler has been extend with our implementation.

half_1s(s(s(A)),B) :- !, ...
half_1s(s(A),B) :- ftp_nat(A,H), ...

The first argument of half 1s is always rooted by the constructor s. half 1s is optimized as follows, assuming that suitable changes are made in the bodies of these clauses and in the call to this predicate.

half_1s(A,B) :- var(A), !, ...
half_1s(0,B) :- !, ...
half_1s(s(A),B) :- !, ...
half_1s(A,B) :- ftp_nat(A,H), ...

Constant arguments can be entirely eliminated. For example, the predicate add 10 discussed in the previous section becomes

add_10(B,B) :- var(B), !.
add_10(0,0) :- !.
add_10(s(B),s(B)) :- !.
add_10(B,C) :- ftp_nat(B,H), add_10_2h(H,C).

First argument indexing

Most Prolog compilers index the clauses of a predicate by hashing on the principal functor of its first argument. If a pattern π has an inductive variable, the predicate’s arguments can be permuted so that the argument corresponding to the inductive variable of π is the first. For example, the clauses of ⩽ when the first argument is rooted by s are invoked by

leq(s(A),B,C) :- !, leq_1s(s(A),B,C).

and are defined by

leq_1s(s(A),B,C) :- var(B), !, ...
leq_1s(s(A),0,C) :- !, ...
leq_1s(s(A),s(B),C) :- !, ...
leq_1s(s(A),B,C) :- ftp_nat(B,H), ...

Swapping the arguments of leq 1s takes better advantage of indexing, i.e.,

leq_1s(B,s(A),C) :- var(B), !, ...
leq_1s(0,s(A),C) :- !, ...
leq_1s(s(B),s(A),C) :- !, ...
leq_1s(B,s(A),C) :- ftp_nat(B,H), ...

This optimization can be performed also for the clauses generated by a rule whose right hand side is a variable, e.g., the first rule of +.

Ftp elimination

The definition of the ftp family of predicates can be eliminated by instantiating the inductive argument in the head of a predicate with all the operation-rooted patterns. For example, the last clause of add can be replaced by the following clauses.

      add(X+Y,B,C) :- !, add(X,Y,H), add_1h(H,B,C).
      add(half(A),B,C) :- !, half(A,H), add_1h(H,B,C).

⋯

Eager discrimination

The case analysis performed by the code output by CodeGen on the inductive variable of an argument may be anticipated to the calling function, when the called function appears on the right hand side of a rule. For example, double is implemented by a single clause

      double(A,B) :- add(A,A,B).

The first argument of add corresponds to the inductive variable of the pattern from which add is generated. We anticipate to double the case analysis that would be performed by add on this argument. In conjunction with the rule call elimination optimization, the predicate add is no longer invoked by double. The resulting clauses are shown below.

      double(X,Y) :- var(X), !, double_1v(X,Y).
        double_1v(0,0).                                  % add(0,0,Y)
        double_1v(s(X),s(X+s(X))).                       % add(s(X),s(X),Y)
      double(0,0) :- !.                                  % add(0,0,Y)
      double(s(X),s(X+s(X))) :- !.                       % add(s(X),s(X),Y)
      double(A,B) :- !, ftp_nat(A,H), double_1h(H,B).
        double_1h(X,Y) :- var(X), !, double_1v(X,Y).
        double_1h(0,0) :- !.                             % add(0,0,Y)
        double_1h(s(X),s(X+s(X))) :- !.                  % add(s(X),s(X),Y)

Variable unflattening

Patterns with constructor-term arguments that are non-shallow yield predicates with clauses that are never invoked when a non-shallow argument is matched by a variable, since variables are instantiated only by shallow constructor terms through our implementation. Clauses that are never invoked can be eliminated and the remaining clause can be generated as if the subtree involved in the generation were flat. For example, the code generated for the operation half is

      half(A,B) :- var(A), !, half_1v(A,B).
        half_1v(0,B) :- half_10(0,B).
        half_1v(s(A),B) :- half_1s(s(A),B).
      ...

The definition of half_1s includes clauses where the first argument’s argument is not instantiated to a variable. These clauses are never executed. The predicate half_1v is defined as follows to avoid the resulting potential inefficiency.

      half_1v(0,B) :- half_10(0,B).
      half_1v(s(0),B) :- half_1s0(s(0),B).
      half_1v(s(s(A)),B) :- half_1ss(s(s(A)),B).

6 Benchmark

We present a benchmark intended both to assess the benefits of the optimizations discussed in Section 5, and to compare our implementation with other similar implementations. Our measures are obtained using the popular SICStus 2.1 Prolog interpreter/compiler. All code is compiled. Since system time measures are subject to some imprecision, the values that we report in the following tables are the averages of 12 executions of the same goals.

We report both the relative execution time and the absolute amount of allocated memory for finding the first solution of the following equations originally proposed in [11, Sect. 7]. As in [11], natural numbers are represented by 0/s-terms. The function one is defined in [11, Example 2].

10000 ⩽ 10000 + 10000 ≈ true  E_{1}
1000 ⩽ X + X ≈ true  E_{2}
400 + X ⩽ (X + 200) + X ≈ true  E_{3}
2000 ⩽ 1000 + (X + X) ≈ true  E_{4}
double(double(one(10000))) ≈ X  E_{5}

The following table summarizes our findings with respect to execution time. Lines 1 to 6 measure the effects of a each optimization. A tabular entry contains the time of the computation as percent of the time taken by the unoptimized code. Line 7 refers to the code with all the optimizations combined. Line 8 shows, in the same scale, the performance of the code proposed in [11]. The comparison with several other implementations of narrowing in Prolog can be inferred using the benchmarks in [11], where it is shown that Hanus’s code is the fastest.

E_{1}  E_{2}  E_{3}  E_{4}  E_{5}  Aver.
1 Rule call elim. 83  77  83  77  61  76
2 Constr. elim.  72  65  76  66  77  72
3 Indexing  72  80  78  79  100  82
4 Ftp elim.  93  94  93  94  84  92
5 Eager discr.  −  −  −  −  25  −
6 Var. Unflat.  −  −  −  −  −  −
7 All opt.  36  35  43  35  11  32
8 Hanus code  56  79  63  79  27  61

Eager discrimination, line 5, is effective only for E_{5}. Variable unflattening, line 6, is not effective for the above equations, but, e.g., reduces by 25% the computation time to solve half (X) ≈ k, where k is an integer literal.

The following table summarizes our findings with respect to memory allocation. Each tabular entry shows, in megabytes, the amount of memory allocated during the computation of the first solution of each equation.

E_{1}  E_{2}  E_{3}  E_{4}  E_{5}
0 Plain  0.680 0.054 0.052 0.130 4.000
1 Rule call elim. 0.440 0.034 0.035 0.086 0.800
2 Constr. elim.  0.280 0.022 0.027 0.058 0.800
3 Indexing  0.680 0.054 0.052 0.130 4.000
4 Ftp elim.  0.680 0.054 0.052 0.130 4.000
5 Eager discr.  0.680 0.054 0.052 0.130 1.600
6 Var. Unflat.  0.680 0.054 0.052 0.130 4.000
7 All opt.  0.280 0.022 0.027 0.058 0.800
8 Hanus code  0.280 0.022 0.027 0.058 0.800

7 Related Work

The last ten years have seen a wealth of results on the foundations and applications of narrowing. The main thrust of this paper is the implementation of narrowing in Prolog, which has received considerable attention within this area [1, 5, 6, 13, 15, 17]. Our benchmark indicates that our implementation is almost twice as fast as Hanus’s implementation [11]. A similar benchmark in [11] indicates that Hanus’s implementation is faster, sometimes substantially, of all other previously published similar implementations. Hanus’s implementation is partly inspired by [15]. Both [11, 15] also propose implementations of narrowing for the larger class of the constructor based, weakly orthogonal rewrite systems and also include sharing, which avoids multiple evaluations of equal terms. Extending our implementation to this larger class of systems and including sharing is possible as well using, e.g., the same approaches as [11, 15].

There are some noticeable differences between our approach and [11]. Our implementation adopts a less strict notion of equality that reduces the size of the search space in some cases. Our implementation allows us to perform more optimizations. Our implementation takes better advantage of mode information. Similar to [11] we consider an uninstantiated variable to be a head normal form. However, we process variables and constructor-rooted terms with different predicates, since there are choice points that must be created for variables, but can be avoided for constructor-rooted terms. This discrimination is not performed in [11]. Our implementation makes better use of the built-in unification, where [11, 15] define a predicate, hnf/2, to evaluate an expression exp to a head normal form. If exp is already a head normal form, hnf/2 returns it unchanged. Hnf/2 detects by unification whether to evaluate exp. Our implementation defines a similar predicate, ftp_{s}/2. However, we perform the unification required to discover whether to evaluate exp before calling ftp_{s}/2. Thus, we save the cost of the call when no evaluation of exp is necessary.

8 Future work

Hanus [9] has shown that adding deterministic rewrite steps to certain non-eager narrowing strategies may reduce infinite search spaces to finite ones. Unfortunately, needed narrowing cannot be improved by this technique. The benefits of this idea seems to originate from postponing the non-deterministic instantiation of variables in favor of more deterministic computations. We have explored some extensions of Hanus’s idea suitable to needed narrowing.

Terms containing a function with distinct definitional trees may have distinct needed narrowing steps. In this case, the choice of the step may affect the efficiency of a computation. Following Hanus’s lead we choose, at run-time, the “more deterministic” step. An opportunity for this strategy is offered by the ubiquitous strict equality. When one and only one side of an equation is a variable, we postpone its instantiation until the other side has been evaluated to head normal form. This strategy makes the instantiation deterministic and yields a marginal efficiency improvement.

Commutative operations, even if they do not have distinct definitional trees, offer a similar opportunity. Consider, for example, the evaluation of t + u to head normal form. If t is a variable, our and most other implementations non-deterministically instantiate it. In this situation, if u is a head normal form, Hanus has shown the benefits of applying simplifying rewrite rules that do not require the (immediate) instantiation of t. We investigate a slightly more general approach. We define a partial ordering relation on terms, referred to as more deterministic than, and, if u is more deterministic than t, we evaluate u + t instead of t + u. For suitable definitions of “more deterministic than” this approach encompasses both delaying the non-deterministic instantiation of a variable in an equation and applying a simplifying rewrite rule to an addition. Note that commuting the arguments of a commutative operation, such as addition, may change the set of the solutions of an equation. We argue, however, that this situation should never occur in well-behaved programs.

Below we show the results of a preliminary benchmark of this idea. We generate Prolog clauses from the rules of + as usual, however, before executing these clauses, we swap the arguments of + if the second argument is more deterministic than the first argument. The “more deterministic than” ordering ranks constructor-rooted terms as the most deterministic ones, variables as the least deterministic ones, and operation-rooted terms in between these to groups. This is more general than using simplifying rules. The next table shows both time and memory allocation results.

E_{1}  E_{2}  E_{3}  E_{4}  E_{5}
Time  220  5  3  8  155
Memory  100  145  115  117  100

The values of each tabular entry show the performance of simplifying code as a percentage of nonsimplifying code. In three equations the speed up is remarkable. Furthermore, the search spaces of both E_{2} and E_{4} become finite. The simplifying code computes all the solutions of these equation in a fraction of the time needed to compute the first solution without simplification.

Acknowledgement

I am very grateful to M. Hanus, R. Loogen, J. J. Moreno Navarro, and M. Rodríguez Artalejo for their interest in my work and for generously exchanging, during the last several years, programs and ideas on the subject of this paper. I am indebted to M. Hanus for showing me, well before [11], that the technique that I proposed in [1] was not as efficient as I had thought—his observation motivated my work—and to B. Barry for implementing the benchmark harness and making many valuable comments on the form and content of this paper.

Appendix A

We describe an algorithm that builds a definitional tree of an operation f from f’s rules’s left hand sides. The merits of this algorithm are its simplicity and the fact that the only information it requires is to distinguish variables from non-variable symbols. This was a crucial consideration for coding the algorithm within an existing compiler with encapsulated information. The algorithm is potentially inefficient, since it relies on non-deterministic choices. The algorithm’s non-determinism can be limited or entirely eliminated at the expense of further computation (and a more complicated description). We assume that the rewrite system is left linear and non-overlapping.

There are two major steps, referred to as “chaining” and “merging”, in the computation of a definitional tree of f. The first step builds, for each left hand side l of a rule of f, a “chain” of l, which is a convenient representation of what could be, if some constraints were ignored, a path from the root of a tree of f down to l. More precisely, a chain is a sequence [l_{0}, p_{1}, l_{1}, p_{2}, …, p_{k}, l_{k}] such that l_{0} = f(X_{1}, …, X_{n}), l_{k} is a variant of l, and for all j = 1, …, k, p_{k} is the position of a shallow constructor term in l_{k} and l_{k−1} is obtained from l_{k} by replacing this term with a variable.

For example, consider the operation ⩽ defined in the introduction. A chain of s(X) ⩽ s(Y), the left hand side of the third rule of ⩽, is [X_{1} ⩽ X_{2}, 1, s(X_{3}) ⩽ X_{2}, 2, s(X_{3}) ⩽ s(X_{4})]. Ignoring the positions, this chain is indeed a path from the root of a tree of ⩽ down to a variant of s(X) ⩽ s(Y). Note, however, that [X_{1} ⩽ X_{2}, 2, X_{1} ⩽ s(X_{4}), 1, s(X_{3}) ⩽ s(X_{4})] is also a chain, but there is no tree of ⩽ in which this chain represents a path.

The second step of the algorithm verifies whether all the chains of f can be “merged” into a definitional tree. If the merging succeeds, a tree of f is generated in the process. Merging chains is a recursive computation that takes a set S of “shortened” chains of f such that the head elements of the chains are variants of each other^{3}. A chain is shortened by removing an even number of elements from its front. If S is a singleton and its chain contains only one term, say l, then the merging succeeds, and the (sub)tree T_{S} generated by S consists of the leaf l. Otherwise, we check whether the first position (second element) is the same in all the chains of S.

If this condition is false, the merging step fails. If this condition is true (remember that all the chains in S begin with variant terms), a variant of the head of a chain in S is the root of the (sub)tree T_{S} generated by S. Then, each chain in S is shortened by removing its first two elements, the leading term and the following position. The shortened chains of S are partitioned into subsets such that the heads of the chains in each subset are variants. Each resulting subset is merged to give a child of T_{S}.

For example, an initial set of chains of ⩽ is {[X_{1} ⩽ X_{2}, 1, 0 ⩽ X_{2}], [Y_{1} ⩽ Y_{2}, 1, s(Y_{3}) ⩽ Y_{2}, 2, s(Y_{3}) ⩽ 0], [Z_{1} ⩽ Z_{2}, 1, s(Z_{3}) ⩽ Z_{2}, 2, s(Z_{3}) ⩽ s(Z_{4})]}. Since the first position of each chain is the same, i.e., 1, X_{1} ⩽ X_{2} is the root of the tree. The chains are stripped of their first two elements and partitioned into the two sets, {[0 ⩽ X_{2}]} and {[s(Y_{3}) ⩽ Y_{2}, 2, s(Y_{3}) ⩽ 0], [s(Z_{3}) ⩽ Z_{2}, 2, s(Z_{3}) ⩽ s(Z_{4})]}. The first set yields the leftmost leaf of the tree of ⩽ shown in Section 3. The second set can be merged too and yields the entire right subtree of the root.

Appendix B

The following code implements the strict equality predicate on natural numbers that we described in the text. If both arguments of strict eq nat are variables, they are unified and the predicate succeeds. This policy, which deviates from the standard definition of strict equality, is consistent with the property that the rest of our implementation instantiates variables only to constructor terms. All the optimizations discussed in Section 5 are included in the following code.

3All the chains in the initial set of chains begin with variant terms, and this property is invariant for any set of this kind subsequently processed during the merging.

strict_eq_nat(X,Y) :- var(X), !, sen_r_2v(Y,X).
sen_r_2v(Y,X) :- var(Y), !, X=Y.           % semi strict, really
sen_r_2v(0,0) :- !.
sen_r_2v(s(Y),s(X)) :- !, sen_r_2v(Y,X).
sen_r_2v(Y,X) :- ftp_nat(Y,H), sen_r_1h_2v(H,X).
  sen_r_1h_2v(Y,X) :- var(Y), !, X=Y.      % semi strict, really
  sen_r_1h_2v(0,0) :- !.
  sen_r_1h_2v(s(Y),s(X)) :- sen_r_2v(Y,X).
strict_eq_nat(0,Y) :- !, sen_10(Y).
sen_10(0) :- !.
sen_10(s(_)) :- !, fail.
sen_10(Y) :- ftp_nat(Y,0).
strict_eq_nat(s(X),Y) :- !, sen_r_2s(Y,X).
sen_r_2s(Y,X) :- var(Y), !, Y=s(Z), strict_eq_nat(X,Z).
sen_r_2s(0,_) :- !, fail.
sen_r_2s(s(Y),X) :- !, strict_eq_nat(X,Y).
sen_r_2s(Y,X) :- ftp_nat(Y,s(Z)), strict_eq_nat(X,Z).
strict_eq_nat(X,Y) :- ftp_nat(X,H), sen_1h(H,Y).
sen_1h(X,Y) :- var(X), !, sen_r_2v(Y,X).
sen_1h(0,Y) :- !, sen_10(Y).
sen_1h(s(X),Y) :- sen_r_2s(Y,X).

References

[1] S. Antoy. Lazy evaluation in logic. In Proc. of the 3th Intl. Symp. on Programming Language Implementation and Logic Programming, pages 371–382. Springer LNCS 528, 1991.

[2] S. Antoy. Definitional trees. In Proc. of the 4th Intl. Conf. on Algebraic and Logic programming, pages 143–157. Springer LNCS 632, 1992.

[3] S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. In Proc. 21st ACM Symposium on Principles of Programming Languages, pages 268–279, Portland, 1994.

[4] B. J. Barry. Needed narrowing as the computational strategy of evaluable functions in an extension of Gödel. Master’s thesis, Portland State University, June 1996.

[5] P.H. Cheong. Compiling lazy narrowing into prolog. Technical Report 25, LIENS, 45, rue d’Ulm, 7505 Paris, France, 1990.

[6] P.H. Cheong and L. Fribourg. Implementation of narrowing: The Prolog-based approach. In K.R. Apt, J.W. de Bakker, and J.J.M.M. Rutten, editors, Logic programming languages: constraints, functions, and objects, pages 1–20. MIT Press, 1993.

[7] N. Dershowitz and J. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243–320. North Holland, Amsterdam, 1990.

[8] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: a logic plus functional language. The Journal of Computer and System Sciences, 42:139–185, 1991.

[9] M. Hanus. Combining lazy narrowing and simplification. In Proc. 6th International Symposium on Programming Language Implementation and Logic Programming, pages 370–384. Springer LNCS 844, 1994.

[10] M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19&20:583–628, 1994.

[11] M. Hanus. Efficient translation of lazy functional logic programs into Prolog. In Proc. Fifth International Workshop on Logic Program Synthesis and Transformation, pages 252– 266. Springer LNCS 1048, 1995.

[12] P. M. Hill and J. W. Lloyd. The Gödel Programming Language. MIT Press, 1993.

[13] J.A. Jiménez-Martín, J. Mariño-Carballo, and J. J. Moreno-Navarro. Efficient compilation of lazy narrowing into prolog. In LOPSTR’92, 1992.

[14] J. W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Vol. II, pages 1–112. Oxford University Press, 1992. Previous version: Term rewriting systems, Technical Report CS-R9073, Stichting Mathematisch Centrum, Amsterdam, 1990.

[15] R. Loogen, F. J. López-Fraguas, and M. Rodríguez-Artalejo. A demand driven computation strategy for lazy narrowing. In PLILP’93, pages 184–200, Tallinn, Estonia, August 1993. Springer LNCS 714.

[16] J. J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic programming with functions and predicates: The language BABEL. Journal of Logic Programming, 12:191–223, 1992.

[17] M. H. van Emden and K. Yukawa. Logic programming with equations. The Journal of Logic Programming, 4:265–288, 1987.