In Proc. of the Twelfth International Conference on Logic Programming, Tokyo, June 1995, MIT Press, pp. 665–679

On Extra Variables in (Equational) Logic Programming

Michael Hanus Informatik II, RWTH Aachen D-52056 Aachen, Germany

hanus@informatik.rwth-aachen.de

Abstract

Extra variables in a clause are variables which occur in the body but not in the head. It has been argued that extra variables are necessary and contribute to the expressive power of logic languages. In the first part of this paper, we show that this is not true in general. For this purpose, we provide a simple syntactic transformation of each logic program into a logic program without extra variables, and we show a strong correspondence between the original and the transformed program. In the second and main part of this paper, we use a similar technique to provide new completeness results for equational logic programs with extra variables. In equational logic programming it is well known that extra variables cause problems since narrowing, the standard operational semantics for equational logic programming, may become incomplete in the presence of extra variables. Using a simple syntactic transformation, we derive a number of new completeness results for narrowing. In particular, we show the completeness of narrowing strategies in the presence of nonterminating functions and extra variables in right-hand sides of rewrite rules. Using these results, current functional logic languages can be extended in a practically useful way.

1 Introduction

Extra variables in a Horn clause L ⇐ B are variables in the body B which do not occur in L (other notions are existential variables [20], local variables [2], or fresh variables [19]). It has been argued that extra variables are necessary and contribute to the expressive power of logic languages. For instance, Dershowitz and Okada [7] claim that the restriction of logic programming to clauses without extra variables “is unacceptable since even very simple relations, such as transitivity, require extra variables in conditions.” In the first part of this paper, we show that this is not true in general since each clause containing extra variables can be transformed into a clause without extra variables by adding the extra variables as a new argument to the predicate in the head. We state a strong correspondence between the original and the transformed program w.r.t. the declarative and the operational semantics, in order to show that there is no loss due to this transformation.

In the second and main part of this paper, we consider equational logic programs. This class of programs is important since it is a basis for integrating functional and logic programming (see [14] for a recent survey on this subject). In equational logic programming it is well known that extra variables cause problems since narrowing, the standard operational semantics for equational logic programming, may become incomplete in the presence of extra variables. This can be seen by the following example [11]:

Example 1.1 Consider the following equational logic program:^{1}

   a → b           b → c ⇐ f(X,b)=f(c,X)
   a → c

This system has all the properties usually required for completeness of narrowing, i.e., it is confluent and terminating. However, narrowing cannot infer the validity of the equation b=c since there is only the following infinite derivation (the subterm where a rule is applied is underlined in each step):

      \underline{b}=c ⇝ f(X,\underline{b})=f(c,X), c=c
           ⇝ f(X1,\underline{b})=f(c,X1), f(X,c)=f(c,X), c=c ⇝ · · ·

In order to prove the condition of the last rule, the extra variable X must be instantiated to a and the instantiated occurrences must be derived to c and b, respectively. However, this is not provided by the narrowing calculus. Although narrowing is complete for confluent and terminating equational logic programs without extra variables, this example shows that narrowing becomes incomplete in the presence of extra variables. □

Extra variables are useful from a programming point of view. For instance, the let construct used in functional programming to share common subexpressions can be expressed in equational logic programming using extra variables [5]. Therefore, much research has been carried out in order to characterize classes of equational logic programs with extra variables for which narrowing is complete (see Section 3 for a detailed discussion). The aim of the second part of this paper is to provide such completeness results. For this purpose, we transform general equational logic programs into programs without extra variables and discuss conditions for the adequacy of this transformation. The main condition is the property that different occurrences of an extra variable need not be derived to different terms in an instantiated rule (note that this is necessary in Example 1.1). An interesting class satisfying this condition are almost orthogonal programs, which is a reasonable class from a programming point of view. Based on these observations, we characterize new classes of equational logic programs for which narrowing and particular narrowing strategies are complete. For instance, we show the completeness of narrowing and lazy narrowing for a class of programs which allows extra variables in right-hand sides of clause heads. Such programs are very useful in practice but seldom discussed in the narrowing literature.

2 Extra Variables in Logic Programming

In this section we propose a method to avoid extra variables in pure logic programming. We use standard notions from logic programming as to be found in [16]. Terms are constructed from variables and function symbols, and (program) clauses have the form L_{0} ⇐ L_{1}, …, L_{k}, where each literal L_{i} is a predicate p applied to a sequence of terms t_{1}, …, t_{n} (in the following we abbreviate sequences of terms by \overline{t}). L_{0} is called head and L_{1}, …, L_{k} is called body of the clause. The set of variables occurring in a term t is denoted by Var(t) (similarly for other syntactic constructions). A term t is called ground if Var(t) = ∅. A logic program is a set of clauses. Consider the clause

1Since the equation in the clause head is always used to derive an instance of the lefthand side to an instance of the right-hand side, we use the arrow ‘→’ instead of the equality symbol in the head.

C: p(\overline{t}) ⇐ q_{1}(\overline{t_{1}}), …, q_{k}(\overline{t_{k}})

A variable x ∈ Var(C) is called extra variable if x ∉ Var(\overline{t}). In order to eliminate all extra variables, we apply the transformation eev (eliminate extra variables) to this clause, which is defined by

eev(C): p(\overline{t}, v_{n+k}(x_{1}, …, x_{n}, y_{1}, …, y_{k})) ⇐ q_{1}(\overline{t_{1}}, y_{1}), …, q_{k}(\overline{t_{k}}, y_{k}) where x_{1}, …, x_{n} are the extra variables of C and y_{1}, …, y_{k} are new variables not occurring in C.^{2} Moreover, v_{0}, v_{1}, v_{2}, … is a family of new function symbols not occurring in the original program. We extend the transformation eev to programs by applying eev to each clause of the program.

Example 2.1 Let P be the program consisting of the following clauses:

   append([],L,L)
   append([E|R],L,[E|RL]) ⇐ append(R,L,RL)
   last(L,E) ⇐ append(R,[E],L)

Then the transformed program eev(P) contains the following clauses:

   append([],L,L,v_{0})
   append([E|R],L,[E|RL],v_{1}(Y)) ⇐ append(R,L,RL,Y)
   last(L,E,v_{2}(R,Y)) ⇐ append(R,[E],L,Y)

□

In the following, we state a strong correspondence between P and eev(P) w.r.t. the declarative and operational semantics. In particular, we show that the initial model of P is identical to the initial model of eev(P) provided that the last argument of all predicates is deleted. For this purpose, we define a mapping on Herbrand interpretations which deletes the additional arguments introduced by eev. Let H be a Herbrand interpretation. Then dla(H) (delete last argument) is the Herbrand interpretation defined by dla(H) := {p(t_{1}, …, t_{n}) | p(t_{1}, …, t_{n}, t_{n+1}) ∈ H}.

Theorem 2.2 Let H be the least Herbrand model of the logic program P, and H′ be the least Herbrand model of P′ := eev(P). Then H = dla(H′).

This theorem shows that there is no basic difference in the declarative semantics between P and eev(P). Everything which is valid w.r.t. P is also valid w.r.t. eev(P), and vice versa, if we disregard the additional arguments in eev(P). The following theorem shows a similar property for the operational semantics (SLD-resolution).

Theorem 2.3 Let P be a logic program, G = p_{1}(\overline{t_{1}}), …, p_{k}(\overline{t_{k}}) be a goal, and x_{1}, …, x_{k} be new variables.

1. If σ is a computed answer for G w.r.t. P, then there are terms e_{1}, …, e_{k} such that {x_{1} ↦ e_{1}, …, x_{k} ↦ e_{k}} ∘ σ is a computed answer for G′ = p_{1}(\overline{t_{1}}, x_{1}), …, p_{k}(\overline{t_{k}}, x_{k}) w.r.t. eev(P).

2. If σ′ is a computed answer for G′ = p_{1}(\overline{t_{1}}, x_{1}), …, p_{k}(\overline{t_{k}}, x_{k}) w.r.t. eev(P), then σ′ restricted to Var(G) is a computed answer for G w.r.t. P.

2The order of the variables in the term v_{n+k}(x_{1}, …, x_{n}, y_{1}, …, y_{k}) is irrelevant. Therefore, we can fix an arbitrary order for each clause.

The proof of this theorem is based on the fact that each resolution derivation w.r.t. P can be transformed into a resolution derivation w.r.t. eev(P), and vice versa. Thus there is also a strong correspondence between P and eev(P) w.r.t. the derivation trees, i.e., P and eev(P) have the same operational behavior. This shows that the restriction to logic programs without extra variables is not a real restriction, i.e., extra variables are not an important feature of logic programming.

3 Extra Variables in Equational Logic Programs

Equational logic programming (see [14] for a survey) amalgamates functional and logic programming styles. It permits the definition of predicates by Horn clauses and the definition of functions by (conditional) equations. Since predicates can be represented as Boolean functions, we assume that all clauses in an equational logic program have the form

l → r ⇐ s_{1} = t_{1}, …, s_{k} = t_{k}

(k ≥ 0), where l, r, s_{1}, t_{1}, …, s_{k}, t_{k} are terms and l is not a variable. Such a clause is also called conditional rewrite rule, and unconditional rewrite rule in case of k = 0. A conditional term rewriting system (CTRS) is a set of conditional rewrite rules. For instance, Example 1.1 is a CTRS. We consider an equational logic program as a CTRS.

3.1 Basic Definitions

In order to give a precise definition of the computation with CTRS, we recall basic notions of (conditional) term rewriting [4, 6].

Substitutions and most general unifiers are defined as in logic programming [16]. A position p in a term t is represented by a sequence of natural numbers (where Λ denotes the root position), t|_{p} denotes the subterm of t at position p, and t[s]_{p} denotes the result of replacing the subterm t|_{p} by the term s (see [6] for details).

Let → be a binary relation on a set S. Then →^{∗} denotes the transitive and reflexive closure of the relation →. We write e_{1} ↓ e_{2} if there exists an element e_{3} ∈ S with e_{1} →^{∗} e_{3} and e_{2} →^{∗} e_{3}. → is called confluent if e_{1} ↓ e_{2} for all e, e_{1}, e_{2} ∈ S with e →^{∗} e_{1} and e →^{∗} e_{2}.

Let R be an unconditional term rewriting system, i.e., an equational logic program where all rules have the form l → r with Var(r) ⊆ Var(l). A rewrite step (w.r.t. R) is an application of a rewrite rule to a term (rewriting with conditional rules is discussed below), i.e., t →_{R} s if there are a position p in t, a rewrite rule l → r ∈ R and a substitution σ with t|_{p} = σ(l) and s = t[σ(r)]_{p}. In this case we say t is reducible. A term t is called irreducible or in normal form if there is no term s with t →_{R} s.

The confluence of the rewrite relation →_{R} is a basic requirement to apply rules only in one direction during equational reasoning. In order to ensure confluence even for nonterminating rewrite systems,^{3} we need some syntactic restrictions on the rewrite rules. A rewrite rule l → r is called left-linear if there are no multiple occurrences of the same variable in l. An unconditional term rewriting system R is called orthogonal if each rule l → r ∈ R is leftlinear and for each non-variable subterm l|_{p} of l there exists no rule l′ → r′ ∈ R such that l|_{p} and l′ unify (where l′ → r′ is not a variant of l → r in case of p = Λ). R is almost orthogonal if all rules are left-linear and for each pairs of rules l → r, l′ → r′ ∈ R, nonvariable subterm l|_{p} of l, and mgu σ for l|_{p} and l′, p is the root position Λ and the terms σ(r) and σ(r′) are identical.

3We do not require the termination of the rewrite system since this cannot be checked automatically. Moreover, such a requirement excludes important functional programming techniques like programming with infinite data structures.

An important property of almost orthogonal systems is the confluence of the rewrite relation (see [15] for a comprehensive survey on results for orthogonal systems).

If R is a CTRS, we denote by R_{u} := {l → r | l → r ⇐ C ∈ R} the unconditional part of R. A CTRS R is called (almost) orthogonal if R_{u} is (almost) orthogonal.

3.2 Equational Logic Programs

The computation mechanism of unconditional term rewrite systems was defined by the rewrite relation →_{R} in the previous section. If we want to define the computation with a CTRS, we have to explain the evaluation of the condition in a rewrite step. Due to [4, 7], there are different possibilities. Here we consider normal CTRS where t_{1}, …, t_{k} are ground normal forms w.r.t. R_{u} for each condition s_{1} = t_{1}, …, s_{k} = t_{k}, and such a condition is provable if every s_{i} is reducible to t_{i}. Note that this definition of conditional rewriting is recursive, but we can also provide an iterative definition. Let R be a normal CTRS. We inductively define the following unconditional term rewriting systems R_{n} (n ≥ 0) by:

\begin{matrix}R_{0} := & \{l → r | l → r ∈ R\} \\ R_{n+1} := & \{σ(l) → σ(r) | l → r ⇐ s_{1} = t_{1}, …, s_{k} = t_{k} ∈ R and σ(s_{i}) →_{R_{n}} t_{i}\} \end{matrix}

We have s →_{R} t iff s →_{R_{n}} t for some n ≥ 0. The restriction to normal CTRS is essential, otherwise the rewrite relation may not be confluent even for orthogonal CTRS (see [4]). On the other hand, normal CTRS have the following confluence property [15]:

Theorem 3.1 The rewrite relation of an almost orthogonal normal CTRS is confluent.

Therefore, we consider in the following only normal CTRS as equational logic programs (this restriction is also made in the functional logic languages BABEL [18] and K-LEAF [10]). This is not a restriction from a logic programming point of view, since each logic program can be transformed into a almost orthogonal normal CTRS by representing predicates as Boolean functions and eliminating multiple occurrences of variables in left-hand sides by introducing new variables and new equations for them in the condition part (see [18] for details).

In practice, most equational logic programs are constructor-based, i.e., the set of function symbols is divided into a set of constructors C and a set of defined functions or operations D (see, for instance, the functional logic languages ALF [12], BABEL [18], K-LEAF [10], or SLOG [9]). A constructor term is a term containing only variables and symbols from C. In a constructorbased term rewrite system, the left-hand side of each clause must be of the form f(t_{1}, …, t_{n}), where f ∈ D and t_{1}, …, t_{n} are constructor terms. Additionally, in a constructor-based normal CTRS, each conditional rule l → r ⇐ s_{1} = t_{1}, …, s_{k} = t_{k} has the property that t_{1}, …, t_{k} are ground constructor terms.

In constructor-based normal CTRS we cannot write arbitrary equations in conditions. However, we can provide an explicit definition of an equality function ≡ between constructor terms by the following rules (this strict equality is the only sensible notion of equality for possible nonterminating systems, since normal forms may not exist [10, 18]):

c ≡ c → true  for all 0-ary c ∈ C
c(x_{1}, …, x_{n}) ≡ c(y_{1}, …, y_{n}) → ∧_{i=1}^{n}(x_{i} ≡ y_{i}) for all n-ary c ∈ C
true ∧ x → x

The reduction of s ≡ t to true is equivalent to the reduction of s and t to a same ground constructor term ([1], Proposition 1). In the rest of this paper, we assume that an equation s ≡ t in a condition of a constructor-based normal CTRS denotes the equation (s ≡ t) = true.

We are interested in the influence of extra variables to the completeness of narrowing strategies for equational logic programs. In contrast to pure logic programming, equational logic programming allows a refined classification of rules according to the occurrence of extra variables. Each conditional rule l → r ⇐ C is classified according to the following table [17]:

Type Requirement
1 Var(r) ∪ Var(C) ⊆ Var(l)
2 Var(r) ⊆ Var(l)
3 Var(r) ⊆ Var(l) ∪ Var(C)
4 no restrictions

All variables in a conditional rule which do not occur in the left-hand side l are called extra variables. An n-CTRS contains only rules of type n, i.e., a 1-CTRS does not contain extra variables, a 2-CTRS may contain extra variables only in the condition, and a 3-CTRS may contain extra variables in the right-hand side, but these extra variables must also occur in the condition.

Example 3.2 The program in Example 1.1 is a 2-CTRS, and the following equational version of Example 2.1 is a constructor-based normal 3-CTRS:

   append([],   L) → L
   append([E|R],L) → [E|append(R,L)]
   last(L) → E ⇐ append(R,[E]) ≡ L

□

3.3 Conditional Narrowing

In equational logic programming we are interested in solving equational goals, i.e., we want to compute a substitution such that terms rewrite to some normal forms under this substitution. Due to the restriction on conditions in rules introduced in the previous section, we define a (normal equational) goal (w.r.t. a normal CTRS R) as a sequence of equations s_{1} = t_{1}, …, s_{k} = t_{k}, where t_{1}, …, t_{k} are ground normal forms w.r.t. R_{u}. Since it is straightforward to extend the definitions of Section 3.1 to goals, we will use them in the following. For instance, we use notions like “subterms of goals” and apply rewrite steps to goals.

A narrowing step transforms a goal G into another goal by applying a rule to some subterm of G. More precisely, G narrows to G′, denoted G ⇝_{σ} G′, if there exist a nonvariable position p in the goal G (i.e., G|_{p} is not a variable), a variant l → r ⇐ C of a rewrite rule in R and a substitution σ such that σ is a mgu of G|_{p} and l, and G′ = σ(C, G[r]_{p}). Since R is a normal CTRS, it is clear that G′ is again a well-defined goal. If there is a narrowing sequence G_{1} ⇝_{σ_{1}} G_{2} ⇝_{σ_{2}} ⋯ ⇝_{σ_{n−1}} G_{n}, we write G_{1} ⇝_{σ}^{∗} G_{n} with σ = σ_{n−1}∘⋯∘σ_{2}∘σ_{1}. A narrowing sequence is successful if the final goal G_{n} is trivial, i.e., it has the form t_{1} = t_{1}, …, t_{k} = t_{k}.

The important property of evaluation strategies for (equational) logic programs is their completeness, i.e., their ability to compute all answers which are valid w.r.t. the declarative semantics. In our context we say narrowing is complete w.r.t. the equational logic program R if, for all goals G and substitutions σ so that σ(G) can be rewritten to a trivial goal, there exists a narrowing derivation G ⇝_{σ′}^{∗} G′, where G′ is a trivial goal and σ = ϕ ∘ σ′ for some substitution ϕ. That is, each valid answer σ is subsumed by a more general answer σ′ computed by narrowing.

There are many results for the completeness of narrowing w.r.t. different classes of programs (see [17] for a comprehensive survey). However, simple narrowing defined so far is more or less of theoretical interest due to its huge search space. In order to reduce the search space and to avoid superfluous work, lazy narrowing strategies have been proposed for languages like BABEL [18] and K-LEAF [10], where lazy narrowing selects an outermost position but also allows narrowing steps at an inner position if the value at this position is demanded by some rule (see [18] for details). It is well-known that lazy narrowing is complete for almost orthogonal normal 2-CTRS. However, there are many cases where 2-CTRS are too restricted and 3-CTRS are appropriate, but no completeness results are known for this class. Moreover, there are operationally better strategies than lazy narrowing. For instance, needed narrowing [1] is an optimal strategy for inductively sequential programs, which is a subclass of unconditional orthogonal programs, and for almost orthogonal programs it has been shown that the combination of lazy narrowing with intermediate simplification steps yields a better behavior [13]. Again, there are no results for these refined strategies w.r.t. extra variables.

In order to avoid separate completeness proofs w.r.t. extra variables for all these (and possible future) extensions, we present a systematic method to eliminate extra variables in equational logic programs. The method is based on the ideas presented in Section 2, but the incompleteness of narrowing in the presence of extra variables shows that this method cannot work in general. Therefore, we will discuss conditions for the adequacy of our method.

3.4 Eliminating Extra Variables in Conditional Rules

In this section we present a transformation on equational logic programs to eliminate all extra variables. The purpose of this transformation is to provide a general method to derive completeness results in the presence of extra variables. This method consists of the following steps:

1. Transform an equational logic program into a new program without extra variables.

2. Apply a complete narrowing strategy to the transformed program (note that more such strategies are known if extra variables do not occur).

3. Check the correspondence of narrowing derivations between the original and the transformed program.

In this section we discuss conditions for the correctness of steps 1 and 3. Applications of the entire method are discussed in Section 3.5.

In order to eliminate extra variables in equational logic programs, we transform each rewrite rule by adding new arguments to each function occurring in the rule. Since functions can be nested, we have to add new arguments in each subterm. For this purpose, we denote by t̂ the term obtained from t by adding a new variable argument to each function occurring in t, i.e., t̂ can be defined as follows:

x̂ = x  for all variables x
t̂ = f(t̂_{1}, …, t̂_{n}, y) if t = f(t_{1}, …, t_{n}) and y is a new variable

The new arguments added to each function call are called extension arguments and the new variables introduced in these arguments are called extension variables. Terms that contain extension arguments for each subterm (which may be instantiated) are called extended terms. Although the names of the extension variables are not fixed, we consider in the following the transformation as a mapping from terms into terms (this can be formalized by taking a list of new variables as an additional argument to , but for the sake of readability we avoid this formalism). The transformation will also be applied to lists of terms and equations. We omit the straightforward definition.

Each conditional rewrite rule R: f(\overline{t}) → r ⇐ C is transformed into a rule eev(R) by applying the transformation to \overline{t}, r and C, and adding the extra variables to the left-hand side, i.e.,

eev(R): f(ˆ\overline{t}, v_{n}(x_{1}, …, x_{n})) → r̂ ⇐ Ĉ

where \{x_{1}, …, x_{n}\} = (Var(r̂) ∪ Var(Ĉ))\Var(ˆ\overline{t}).^{4} The transformed clause may not be a normal one, but this causes no problems since the requirement for normal CTRS is only necessary for the original programs in order to ensure the confluence of the original rewrite relation.

We extend eev to sets of rewrite rules by applying it to each rule. For the sake of readability, we use the following obvious optimization in concrete examples: Introduce extension arguments only in function calls of the form f(\overline{s}) where there is some rewrite rule f(\overline{t}) → r ⇐ C for f. In particular, extension arguments are not introduced in constructor terms if R is a constructor-based program.

Example 3.3 Let R be the program of Example 1.1. Then eev(R) is the following program:

   a(v_{1}(Y)) → b(Y)       b(v_{2}(X,Z)) → c ⇐ f(X,b(Z))=f(c,X)

   a(v_{0})  → c

It is not necessary to add extension arguments to the functions c and f since there are no rewrite rules for them. □

The elimination of extra variables in equational logic programs seems to be very similar to pure logic programs. However, there is an essential difference. The transformation does not change the meaning in the case of pure logic programs (cf. Theorem 2.2), but this is no longer true in the equational case. The meaning of an equational logic program is the set of valid equalities. For instance, b=c is valid w.r.t. Example 1.1 (since the instantiated condition f(a,b)=f(c,a) can be rewritten to the trivial equation f(c,b)=f(c,b), i.e., b →_{R_{1}} c). However, no instance of the equation b(V)=c is valid w.r.t. the transformed program in Example 3.3. In the original program the term a can be rewritten to b as well as c, which is necessary to prove the condition of the last rule. However, in the transformed program, there is no term which is simultaneously reducible to b(Y) and c.

4 In contrast to pure logic programming, the order of the variables in the term v_{n}(x_{1}, …, x_{n}) is relevant to ensure that the transformed programs are almost orthogonal if the original programs are almost orthogonal (see Proposition 3.8). Therefore, we fix the same ordering principle for all rules. A possible choice is a left-to-right innermost ordering for all variables in r̂, Ĉ.

The meanings of the original and the transformed program differ whenever it is necessary to rewrite an instance of a variable to different terms in the original program. The inversion of this observation yields a criterion for the adequacy of the transformation. We can ensure that the original and the transformed program have the same meaning if all occurrences of the same variable are reduced to an identical term, i.e., if the same rewrite steps are applied to all occurrences of a variable (in the instantiated rule). This can be expressed by the notion of sharing, which means that all occurrences of a rule variable are represented only once. Sharing is also a well-known implementation technique in functional and logic languages. Sharing in rewriting can be formally treated in the framework of term graph rewriting [3]. In order to avoid repeating all details of term graph rewriting, we assume familiarity with graphs to represent shared subterms (see [3] for details). We only cite the following result, which is important in our framework.

Theorem 3.4 ([3]) If R is an unconditional almost orthogonal term rewriting system, then graph rewriting (where all variables in rules are shared) is a sound and complete implementation of term rewriting; in particular, the normal forms (w.r.t. traditional term rewriting) of terms are also computable if all rule variables are shared.

The restriction to almost orthogonal systems is essential. Otherwise, rewriting with sharing is incomplete (see [3]). To apply the result of Theorem 3.4 in our framework, we have to extend it to conditional rewrite systems. Although this is not possible in general, sharing is a complete implementation for the class of programs which we consider as equational logic programs. This also shows that the restriction to normal CTRS is sensible from an implementation point of view.

Theorem 3.5 Let R be an almost orthogonal normal CTRS (with extra variables). Then all variables in rewrite rules can be shared during the computation of a normal form.

Now we want to relate rewrite proofs in R with rewrite proofs in the transformed system eev(R). In order to compare extended terms with original terms, we define a mapping dv to delete extension arguments by dv(x) = x for all variables x and dv(f(t_{1}, …, t_{n}, t_{n+1})) = f(dv(t_{1}), …, dv(t_{n})). Clearly, dv(t̂) = t for all terms t. The following theorem shows that every normal form computation w.r.t. R can also be performed for the extended terms w.r.t. eev(R), provided that R is an almost orthogonal normal CTRS.

Theorem 3.6 Let R be an almost orthogonal normal CTRS (with extra variables), t be a term and R′ = eev(R). If t →_{R}^{∗} s (where s is a normal form), then there is an extended term t′ with dv(t′) = t and t′ →_{R′}^{∗} ŝ.

This theorem implies that all strict equalities w.r.t. R are also valid w.r.t. eev(R). The next theorem shows that each narrowing derivation w.r.t. eev(R) corresponds to a narrowing derivation w.r.t. R, i.e., if there is a narrowing derivation on the extended level, then there is also a narrowing derivation on the original level. This property will be used to state new completeness results for narrowing strategies in the presence of extra variables. Remember that all trivial goals have the form t_{1} = t_{1}, …, t_{n} = t_{n}, where t_{1}, …, t_{n} are in normal form (not necessarily ground if they contain extension arguments).

Theorem 3.7 Let R be a normal CTRS such that eev(R) is almost orthogonal and G be a goal. If there is a narrowing derivation Ĝ ⇝_{σ}^{∗} G_{1}, where G_{1} is a trivial goal, then there is a narrowing derivation G ⇝_{ϕ}^{∗} G_{0} with dv(G_{1}) = G_{0} and dv(σ(x)) = ϕ(x) for all x ∈ Var(G). Moreover, the narrowing positions in both derivations are identical, and the applied rules correspond via the transformation eev.

If R is an almost orthogonal normal CTRS and we want to apply our transformation in order to show the completeness of sophisticated narrowing strategies, we have to ensure that the transformed program eev(R) is also almost orthogonal (Theorem 3.7). The following proposition shows that this is always the case.

Proposition 3.8 If R is an almost orthogonal CTRS, then eev(R) is almost orthogonal.

We mentioned in Section 3.3 that simple narrowing has a huge search space and, therefore, sophisticated narrowing strategies are needed in practice. In general, a narrowing strategy restricts the number of possible narrowing steps, i.e., it can be seen as a mapping which assigns to each goal a set of pairs of positions and rules.^{5} However, a narrowing strategy should not destroy completeness, and completeness results are often known only for equational logic programs without extra variables. In order to overcome these problems, we can apply the results of this section to transfer completeness results for narrowing strategies from programs without extra variables to programs which may contain extra variables. The following main result shows the general method.

Theorem 3.9 Let R be an almost orthogonal normal CTRS (with extra variables) and N be a narrowing strategy which is complete for eev(R). Then N is also complete for R.

The following section contains concrete applications of this result.

3.5 Application of Extra Variable Elimination

3.5.1 Inductively Sequential Systems

Lazy narrowing is complete for almost orthogonal normal 2-CTRS [18]. However, it is well known that lazy narrowing may perform superfluous narrowing steps due to the interaction of redex selection and rule selection. As an alternative, needed narrowing is proposed in [1]. The needed narrowing strategy is optimal w.r.t. the length of the derivations and the number of computed solutions. Needed narrowing is defined for the class of inductively sequential systems. These are particular constructor-based orthogonal unconditional rewrite systems (see [1] for a precise definition). Roughly speaking, in inductively sequential systems all rules defining a function can be organized in a hierarchical structure, called definitional tree, which represents a unique selection of a rule by a case distinction on the arguments for each ground function call. For instance, the rules for append in Example 3.2 are inductively sequential, since a unique selection of a rule can be made by the first argument of append: if this argument is an empty list ([]), the first rule is selected, and the second rule is selected if this argument is a nonempty list ([·|·]). On the other hand, the rules of Example 1.1 are not inductively sequential, since the first as well as the second rule can be applied to the term ‘a’.

5An exception is the needed narrowing strategy [1] which additionally assigns a unifier because the unifier in a needed narrowing step is not necessarily a most general one.

We will use the results of the previous section to extend needed narrowing to conditional rewrite rules with extra variables in a simple way. A CTRS R is called inductively sequential if it is a constructor-based normal CTRS and its unconditional part R_{u} is inductively sequential. Since inductively sequential systems are orthogonal, we can use the method proposed in [4] to translate inductively sequential normal CTRS into an unconditional system. For this purpose, we introduce for each conditional rule R: l → r ⇐ s = u of R (where u is a ground constructor term) a new function symbol cond_{R} and replace R by the following unconditional rules:

l → cond_{R}(s, r)
cond_{R}(u, x) → x

We denote by uc(R) the new unconditional system obtained from R. Since u is a ground constructor term, the new unconditional system is inductively sequential if the original system is an inductively sequential CTRS without extra variables.^{6} Moreover, there is a strong correspondence between the rewrite derivations (see [4], Proposition 2.5.4). In order to deal with extra variables, we have to translate R by the transformation eev before applying uc. The following proposition is obvious since the introduction of extension arguments does not influence the non-overlapping of left-hand sides.

Proposition 3.10 If R is an inductively sequential CTRS, then uc(eev(R)) is an unconditional inductively sequential rewrite system.

Example 3.11 Consider the following inductively sequential CTRS R which defines the Boolean function member on the basis of the function append:

   append([],   L) → L
   append([E|R],L) → [E|append(R,L)]
   member(E,L) → true ⇐ append(L1,[E|L2]) ≡ L

Then the transformed system uc(eev(R)) consists of the following rules:

   append([],   L,v_{0})  → L
   append([E|R],L,v_{1}(X)) → [E|append(R,L,X)]
   member(E,L,v_{3}(L1,L2,X)) → cond(append(L1,[E|L2],X) ≡ L,true)
   cond(true,X) → X

□

6Proposition 2.5.3 in [4] is not true in the presence of extra variables.

Since needed narrowing is an optimal and complete strategy for inductively sequential unconditional systems, we can apply the results of the previous section (as summarized in Theorem 3.9), and we obtain the following new result.

Theorem 3.12 Needed narrowing is complete for inductively sequential CTRS (with extra variables). Moreover, it is optimal w.r.t. the length of the derivations and the number of computed solutions.

Since this result can be easily extended to overlapping rules with excluding conditions, we obtain with our translation method an optimal narrowing strategy for a large class of equational logic programs.

3.5.2 Extra Variables in Right-Hand Sides

Current functional logic languages like BABEL [18] and K-LEAF [10]) permit extra variables in conditions but not in the right-hand side of conditional rules. However, as observed by several authors [8, 15, 17], it makes good sense to allow extra variables also in right-hand sides if they occur in conditions (3-CTRS). Example 3.2 shows a sensible use of extra variables in right-hand sides. The following example [15] shows that such extra variables can be a replacement for the let construct of functional languages.

Example 3.13 The Fibonacci numbers can be computed by the following conditional rules:

   fib(0)  → <0,1>
   fib(s(X)) → <Z,Y+Z> ⇐ fib(X) ≡ <Y,Z>

□

However, an unrestricted use of extra variables in right-hand sides leads to nonconfluent rewrite relations even for non-overlapping normal CTRS. To ensure the confluence of the rewrite relation and completeness of narrowing, additional restrictions are needed. Middeldorp and Hamoen [17] showed that narrowing is complete for level-confluent and terminating 3-CTRS. In [5, 7, 19] 3-CTRS with a special rewrite relation are proposed, where extra variables are instantiated only to irreducible terms and all such instantiations of conditional rules must be decreasing (i.e., the left-hand side must greater than the conditions and right-hand side w.r.t. a termination ordering). Narrowing is complete for such rewrite systems. Since we do not want to restrict ourselves to terminating rewrite systems, we need other conditions. For this purpose, we call a CTRS R functional if the following conditions hold:

1. R is a normal CTRS.

2. The unconditional part R_{u} is almost orthogonal (where we use the same definition as in Section 3.1 but do not require Var(r) ⊆ Var(l) for all l → r ∈ R_{u}).

3. →_{R} is confluent.

Conditions 1 and 2 are necessary to extend Theorem 3.5 and Proposition 3.8 to functional CTRS. Since these conditions are not sufficient for the confluence of the rewrite relation, we have the explicit confluence condition 3. We will discuss sufficient conditions ensuring confluence below. Note that each almost orthogonal normal 2-CTRS is functional (by Theorem 3.1), while a 4-CTRS cannot be functional. Hence the class of functional CTRS lies between the classes of almost orthogonal normal 2-CTRS and 3-CTRS.

We want to apply our transformation to show the completeness of narrowing strategies for functional CTRS. Since functional CTRS are transformed by eev into almost orthogonal CTRS, it is easy to check that Theorem 3.9 is also valid for functional CTRS:

Theorem 3.14 Let R be a functional CTRS and N be a narrowing strategy which is complete for eev(R). Then N is also complete for R.

We can use this result to show the completeness of various narrowing strategies for equational logic programs with extra variables in right-hand sides. For instance, completeness results for lazy narrowing strategies are only known for constructor-based normal 2-CTRS [18]. Our transformation method yields new completeness results for functional CTRS by applying Theorem 3.14 to the completeness result of lazy narrowing [18] for constructor-based almost orthogonal normal 2-CTRS.

Corollary 3.15 Lazy narrowing is complete for constructor-based functional CTRS.

To obtain a further interesting result, we apply Theorem 3.14 to inductively sequential systems with extra variables in right-hand sides. For this purpose, we use the same translation techniques as introduced in Section 3.5.1 and we immediately obtain the following proposition.

Corollary 3.16 Let R be a functional CTRS such that the unconditional part R_{u} is inductively sequential.^{7} Then needed narrowing is complete for R, and it is an optimal strategy w.r.t. the length of the derivations and the number of computed solutions.

Thus needed narrowing is a complete and optimal strategy for the programs in Examples 3.2 and 3.13.

Due to these results, it is no problem to extend equational logic languages like BABEL [18] or K-LEAF [10] by permitting extra variables in right-hand sides. However, the use of these extra variables must be restricted so that the programs are functional. The first two conditions of functional CTRS are easy to check, but the confluence condition 3 is usually hard to verify. In some cases it is possible to show confluence by proving that the rewrite system R is level-confluent, i.e., we may show that each unconditional rewrite system R_{n} is confluent for all n ≥ 0. For instance, it is relatively easy to show that the rewrite system in Example 3.2 is level-confluent. However, from a practical point of view, it is desirable to have syntactic criteria to ensure the confluence of a 3-CTRS. Fortunately, for constructor-based programs there is an interesting subclass of functional CTRS which has a simple syntactic characterization.^{8} Note that in constructor-based systems each conditional rule can be written in the form l → r ⇐ s ≡ t.

7Since the property of inductive sequentiality depends only on the left-hand sides of the rewrite rules, the definition can simply be extended to rules with extra variables in right-hand sides.

8Recently, Suzuki et al. [21] have independently characterized a class of level-confluent 3-CTRS with similar restrictions.

Proposition 3.17 A constructor-based normal CTRS R is functional if the following conditions holds:

1. The unconditional part R_{u} is almost orthogonal.

2. For each rule l → r ⇐ s ≡ t with extra variables in r, t is a constructor term, Var(s) ⊆ Var(l), and Var(r) ⊆ Var(l) ∪ Var(t).

As a consequence of this proposition, the rewrite system in Example 3.13 is functional. It is straightforward to refine the proposition to conditional rules with more than one strict equation in the condition part.

4 Conclusions

In this paper we have discussed the necessity and problems of extra variables in pure logic programming and equational logic programming. In the first part, we have shown that extra variables are unnecessary for pure logic programming since all occurrences of extra variables during a computation can be moved into the initial goal. Although this transformation does not change the declarative and operational semantics of pure logic programs, it does not generally work for equational logic programs, since it is known that the presence of extra variables may cause incompleteness of narrowing, the standard operational semantics of equational logic programs. Nevertheless, we have shown that this transformation works for the important subclass of almost orthogonal normal programs. As a consequence of this result, we have provided a general method to lift completeness results for narrowing without extra variables to programs with extra variables. Using this method, we could prove various new completeness results like completeness and optimality of needed narrowing and completeness of lazy narrowing in the presence of extra variables. Programs with such properties often occur if programming techniques like infinite data structures (e.g., streams) and let constructs from functional programming are simultaneously used. Therefore, our results are a contribution to extend current functional logic languages in a practically useful way, since such extensions give the programmer more expressivity and allow a more efficient execution of programs. Our method can also be helpful to simplify completeness proofs for possibly more sophisticated narrowing strategies that will be developed in the future.

Acknowledgements. The author is grateful to Aart Middeldorp and Enno Ohlebusch for their comments on this paper. The research described in this paper was supported in part by the German Ministry for Research and Technology (BMFT) under grant ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics).

References

[1] S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proc. 21st ACM Symposium on Principles of Programming Languages, pp. 268–279, Portland, 1994.

[2] R. Barbuti, P. Mancarella, D. Pedreschi, and F. Turini. A Transformational Approach to Negation in Logic Programming. Journal of Logic Programming (8), pp. 201–228, 1990.

[3] H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer, and M.R. Sleep. Term Graph Rewriting. In Proc. Parallel Architectures and Languages Europe (PARLE’87), pp. 141–158. Springer LNCS 259, 1987.

[4] J.A. Bergstra and J.W. Klop. Conditional Rewrite Rules: Confluence and Termination. Journal of Computer and System Sciences, Vol. 32, No. 3, pp. 323–362, 1986.

[5] H. Bertling and H. Ganzinger. Completion-Time Optimization of Rewrite-Time Goal Solving. In Proc. of the Conference on Rewriting Techniques and Applications, pp. 45–58. Springer LNCS 355, 1989.

[6] N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pp. 243–320. Elsevier, 1990.

[7] N. Dershowitz and M. Okada. A Rationale for Conditional Equational Programming. Theoretical Computer Science, Vol. 75, pp. 111–138, 1990.

[8] N. Dershowitz, M. Okada, and G. Sivakumar. Confluence of Conditional Rewrite Systems. In Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, pp. 31–44. Springer LNCS 308, 1987.

[9] L. Fribourg. SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 172–184, Boston, 1985.

[10] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel LEAF: A Logic plus Functional Language. Journal of Computer and System Sciences, Vol. 42, No. 2, pp. 139–185, 1991.

[11] E. Giovannetti and C. Moiso. A completeness result for E-unification algorithms based on conditional narrowing. In Proc. Workshop on Foundations of Logic and Functional Programming, pp. 157–167. Springer LNCS 306, 1986.

[12] M. Hanus. Compiling Logic Programs with Equality. In Proc. of the 2nd Int. Workshop on Programming Language Implementation and Logic Programming, pp. 387–401. Springer LNCS 456, 1990.

[13] M. Hanus. Combining Lazy Narrowing and Simplification. In Proc. of the 6th International Symposium on Programming Language Implementation and Logic Programming, pp. 370–384. Springer LNCS 844, 1994.

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

[15] J.W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.

[16] J.W. Lloyd. Foundations of Logic Programming. Springer, second, extended edition, 1987.

[17] A. Middeldorp and E. Hamoen. Completeness Results for Basic Narrowing. Applicable Algebra in Engineering, Communication and Computing, Vol. 5, pp. 213–253, 1994.

[18] J.J. Moreno-Navarro and M. Rodríguez-Artalejo. Logic Programming with Functions and Predicates: The Language BABEL. Journal of Logic Programming, Vol. 12, pp. 191–223, 1992.

[19] P. Padawitz. Generic Induction Proofs. In Proc. of the 3rd Intern. Workshop on Conditional Term Rewriting Systems, pp. 175–197. Springer LNCS 656, 1992.

[20] M. Proietti and A. Pettorossi. Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables. In Proc. Eleventh International Conference on Logic Programming, pp. 714–729. MIT Press, 1994.

[21] T. Suzuki, A. Middeldorp, and T. Ida. Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides. Technical Report ISE-TR 94-116, Univ. of Tsukuba, 1994. To appear in Proc. RTA’95.