Lazy Unification with Simplification

Michael Hanus

Max-Planck-Institut für Informatik Im Stadtwald, D-66123 Saarbrücken, Germany.

                           michael@mpi-sb.mpg.de

In Proc. 5th European Symposium on Programming Edinburgh, April 1994, Springer LNCS 788, pp. 272–286

Abstract. Unification in the presence of an equational theory is an important problem in theorem-proving and in the integration of functional and logic programming languages. This paper presents an improvement of the proposed lazy unification methods by incorporating simplification into the unification process. Since simplification is a deterministic computation process, more efficient unification algorithms can be achieved. Moreover, simplification reduces the search space so that in some case infinite search spaces are reduced to finite ones. We show soundness and completeness of our method for equational theories represented by ground confluent and terminating rewrite systems which is a reasonable class w.r.t. functional logic programming.

1 Introduction

Unification is not only an important operation in theorem provers but also the most important operation in logic programming systems. Unification in the presence of an equational theory, also known as E-unification, is necessary if the computational domain in a theorem prover enjoys certain equational properties [26] or if functions should be integrated into a logic language [10]. Therefore the development of Eunification algorithms is an active research topic during recent years (see, for instance, [29]).

Since E-unification is a complex problem even for simple equational axioms, we are interested in efficient E-unification methods in order to incorporate such methods into functional logic programming languages. One general method to improve the efficiency of implementations is the use of a lazy strategy. “Lazy” means that evaluations are performed only if it is necessary to compute the required solutions. In the context of unification this corresponds to the idea that terms are manipulated at outermost positions. Hence lazy unification means that equational axioms are applied to outermost positions of equations. For instance, consider the following equations for addition and multiplication on natural numbers which are represented by terms of the form s(⋯ s(0) ⋯):

\begin{matrix}0 + y ≈ & y & 0 ∗ y ≈ & 0 \\ s(x) + y ≈ & s(x + y) & s(x) ∗ y ≈ & y + x ∗ y \end{matrix}

If we have to unify the terms 0 ∗ (s(0) + s(z)) and 0, we could apply equational axioms to inner subterms starting with s(0)+s(z) (innermost or eager strategy) or to outermost subterms (outermost or lazy strategy). This will lead to the following two derivations (the subterms manipulated in the next step are underlined):

\begin{matrix}0 ∗ (\underline{s(0) + s(z)}) ≈ 0 ⇒ 0 ∗ (s(\underline{0 + s(z)})) ≈ 0 ⇒ \underline{0 ∗ (s(s(z)))} ≈ 0 ⇒ 0 ≈ 0 \\ \underline{0 ∗ (s(0) + s(z))} ≈ 0 ⇒ 0 ≈ 0 \end{matrix}

Obviously, the second lazy unification derivation should be preferred.

There are many proposals for such lazy unification strategies. For instance, Martelli et al. [22] have proposed a lazy unification algorithm for confluent and terminating equational axioms. Due to the confluence requirement, equations are only applied in one direction. However, their method is not pure lazy since equations are applied to inner subterms in equations of the form x ≈ t where the variable x occurs in t. Gallier and Snyder [11] have proved the completeness of a lazy unification method for arbitrary equational theories where equations can be applied in both directions. Narrowing is a method to compute E-unifiers in the presence of confluent axioms. It is a combination of the reduction principle of functional languages with syntactic unification in order to instantiate variables. Lazy narrowing were proposed by Reddy [27] as the operational principle of functional logic languages. Recently, Antoy, Echahed and Hanus [1] have proposed a narrowing strategy for programs where the functions are defined by case distinctions over the data structures. This strategy reduces only needed redexes, computes no redundant solutions, and is optimal w.r.t. the length of narrowing derivations.

From a practical point of view the disadvantage of E-unification is its inherent nondeterminism. In the area of narrowing there are many proposals for the inclusion of a deterministic simplification process in order to reduce the nondeterminism [8, 9, 19, 24, 28], but all these proposals are based on an eager narrowing strategy. On the other hand, only little work has been done to improve the efficiency of outermost or lazy strategies. Echahed [7] has shown the completeness of any narrowing strategy with simplification under strong requirements (uniformity of specifications). Dershowitz et al. [6] have proposed to combine lazy unification with simplification and demonstrated the usefulness of inductive consequences for simplification. However, they have not proved completeness of their lazy unification calculus if all terms are simplified to their normal form after each unification step. In fact, their completeness proof for lazy narrowing does not hold if eager rewriting is included since rewriting in their sense does not reduce the complexity measure used in their completeness proof and may lead to infinite instead of successful derivations. Therefore we will formulate a calculus for lazy unification which includes simplification and give a rigorous completeness proof. The distinguishing features of our framework are:

– We consider a ground confluent and terminating equational specification in order to apply equations only in one direction and to ensure the existence of normal forms. This is reasonable if one is interested in declarative programming rather than theorem proving.

– The unification calculus is lazy, i.e., functions are not evaluated if their value is not required to decide the unifiability of terms. Consequently, we may compute reducible solutions as answers according to the spirit of lazy evaluation. For instance, in contrast to other “lazy” unification methods we do not allow any evaluation of t in the equation x ≈ t if x occurs only once.

– We include a deterministic simplification process in our unification calculus. In order to restrict nondeterministic computations as much as possible, we allow to use additional inductive consequences for simplification which has been proved to be useful in other calculi [7, 9, 24].

After recalling basic notions from term rewriting, we present in Section 3 our basic lazy unification calculus. In Section 4 we include a deterministic simplification process into the lazy unification calculus. Finally, we show in Section 5 some important optimizations for constructor-based specifications. Due to lack of space we omit the details of some proofs, but the interested reader will find them in [17].

2 Computing in equational theories

In this section we recall the notations for equations and term rewriting systems [5] which are necessary in our context.

Let the signature F be a set of function symbols^{1} and X be a countably infinite set of variables. Then T (F, X) denotes the set of terms built from F and X. Var(t) is the set of variables occurring in t. A ground term t is a term without variables, i.e., Var(t) = ∅. A substitution σ is a mapping from X into T (F, X) such that its domain Dom(σ) = {x ∈ X | σ(x) ≠ x} is finite. We frequently identify a substitution σ with the set {x ↦ σ(x) | x ∈ Dom(σ)}. Substitutions are extended to morphisms on T (Σ, X) by σ(f(t_{1}, …, t_{n})) = f(σ(t_{1}), …, σ(t_{n})) for every term f(t_{1}, …, t_{n}). A substitution σ is called ground if σ(x) is a ground term for all x ∈ Dom(σ). The composition of two substitutions ϕ and σ is defined by ϕ ∘ σ(x) = ϕ(σ(x)) for all x ∈ X. A unifier of two terms s and t is a substitution σ with σ(s) = σ(t). A unifier σ is called most general (mgu) if for every other unifier σ′ there is a substitution ϕ with σ′ = ϕ ∘ σ. A position p in a term t is represented by a sequence of natural numbers, 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 [5] for details). The outermost position Λ is also called root position.

Let → be a binary relation on a set S. Then →^{∗} denotes the transitive and reflexive closure of the relation →, and ↔^{∗} denotes the transitive, reflexive and symmetric closure of →. → is called terminating if there are no infinite chains e_{1} → e_{2} → e_{3} → · · ·. → is called confluent if for all e, e_{1}, e_{2} ∈ S with e →^{∗} e_{1} and e →^{∗} e_{2} there exists an element e_{3} ∈ S with e_{1} →^{∗} e_{3} and e_{2} →^{∗} e_{3}.

An equation s ≈ t is a multiset containing two terms s and t. Thus equations to be unified are symmetric. In order to compute with equational specifications, we will use the specified equations only in one direction. Hence we define a rewrite rule l → r as a pair of terms l, r satisfying l ∉ X and Var(r) ⊆ Var(l) where l and r are called left-hand side and right-hand side, respectively. A rewrite rule is called a variant of another rule if it is obtained by a unique replacement of variables by other variables. A term rewriting system R is a set of rewrite rules. In the following we assume a given term rewriting system R.

A rewrite step is an application of a rewrite rule to a term, i.e., t →_{R} s if there exists a position p, a rewrite rule l → r and a substitution σ with t|_{p} = σ(l) and s = t[σ(r)]_{p}. A term t is called reducible if we can apply a rewrite rule to it, and t is called irreducible or in normal form if there is no term s with t →_{R} s. A term rewriting system is ground confluent if the restriction of →_{R} to the set of all ground terms is confluent. If R is ground confluent and terminating, then each ground term t has a unique normal form which is denoted by t↓_{R}.

We are interested in proving the validity of equations. Hence we call an equation s ≈ t valid (w.r.t. R) if s ↔_{R}^{∗} t. By Birkhoff’s Completeness Theorem, this is equivalent to the validity of s ≈ t in all models of R. In this case we also write s =_{R} t. If R is ground confluent and terminating, we can decide the validity of a ground equation s ≈ t by computing the normal form of both sides using an arbitrary sequence of rewrite steps since s ↔_{R}^{∗} t iff s↓_{R} = t↓_{R}. In order to compute solutions to a non-ground equation s ≈ t, we have to find appropriate instantiations for the variables in s and t. This can be done by narrowing. A term

1 In this paper we consider only single-sorted programs. The extension to many-sorted signatures is straightforward [25]. Since sorts are not relevant to the subject of this paper, we omit them for the sake of simplicity.

t is narrowable into a term t′ if there exist a non-variable position p (i.e., t|_{p} ∉ X), a variant l → r of a rewrite rule and a substitution σ such that σ is a mgu of t|_{p} and l and t′ = σ(t[r]_{p}). In this case we write t ⇝_{σ} t′.

Narrowing is able to solve equations w.r.t. R by deriving both sides of an equation to syntactically unifiable terms. Due to the huge search space of simple narrowing, several authors have proposed restrictions on the admissible narrowing derivations (see [18] for a detailed survey). Lazy narrowing [3, 23, 27] is influenced by the idea of lazy evaluation in functional programming languages. Lazy narrowing steps are only applied at outermost positions with the exception that arguments are evaluated by narrowing to their head normal form if their values are required for an outermost narrowing step. Since lazy strategies are important in the context of non-terminating rewrite rules, these strategies have been proved to be complete w.r.t. domain-based interpretations of rewrite rules [13, 23]. Lazy unification is very similar to lazy narrowing but manipulates sets of equations rather than terms. It has been proved to be complete for canonical term rewriting systems w.r.t. standard semantics [6, 22].

From a practical point of view the most essential improvement of simple narrowing is normalizing narrowing [8] where the term is rewritten to its normal form before a narrowing step is applied. This optimization is important since it prefers deterministic computations: rewriting a term to normal form can be done in a deterministic way since every rewriting sequence gives the same result (if R is confluent and terminating). As shown in [9, 16], normalizing narrowing has the important effect that equational logic programs are more efficiently executable than pure logic programs. Normalization can also be combined with other narrowing restrictions [9, 19, 28]. Because of these important advantages, normalizing narrowing is the foundation of several programming languages which combines functional and logic programming like ALF [15], LPG [2] or SLOG [9]. However, normalization has not been included in lazy narrowing strategies.^{2} Therefore we will present a lazy unification calculus which includes a normalization process where the term rewrite rules as well as additional inductive consequences are used for normalization.

3 A calculus for lazy unification

In the rest of this paper we assume that R is a ground confluent and terminating term rewriting system. This section presents our basic lazy unification calculus to solve a system of equations. The inclusion of a normalization process will be shown in Section 4. The “laziness” of our calculus is in the spirit of lazy evaluation in functional programming languages, i.e., terms are evaluated only if their values are needed.

Our lazy unification calculus manipulates sets of equations in the style of Martelli and Montanari [21] rather than terms as in narrowing calculi. Hence we define an equation system E to be a multiset of equations (in the following we write such sets without curly brackets if it is clear from the context). A solution of an equation system E is a ground substitution σ such that σ(s) =_{R} σ(t) for all equations s ≈ t ∈ E.^{3} An equation system E is solvable if it has at least one solution. A set S of substitutions is a complete set of solutions for E iff

2 Except for [6, 7], but see the remarks in Section 1. 3 We are interested in ground solutions since later we will include inductive consequences

which are valid in the ground models of R. As pointed out in [24], this ground approach subsumes the conventional narrowing approaches where also non-ground solutions are Lazy narrowing

f(t_{1}, …, t_{n}) ≈ t, E ⟹^{lu} t_{1} ≈ l_{1}, …, t_{n} ≈ l_{n}, r ≈ t, E

if t ∉ X or t ∈ Var(f(t_{1}, …, t_{n})) ∪ Var(E) and f(l_{1}, …, l_{n}) → r new variant of a rule

Decomposition of equations

f(t_{1}, …, t_{n}) ≈ f(t′_{1}, …, t′_{n}), E ⟹^{lu} t_{1} ≈ t′_{1}, …, t_{n} ≈ t′_{n}, E

Partial binding of variables

x ≈ f(t_{1}, …, t_{n}), E ⟹^{lu} x ≈ f(x_{1}, …, x_{n}), x_{1} ≈ ϕ(t_{1}), …, x_{n} ≈ ϕ(t_{n}), ϕ(E)

if x ∈ Var(f(t_{1}, …, t_{n})) ∪ Var(E) and ϕ = {x ↦ f(x_{1}, …, x_{n})} (x_{i} new variable)

Figure 1. The lazy unification calculus

1. for all σ ∈ S, σ is a solution of E;

2. for every solution θ of E, there exists some σ ∈ S with θ(x) =_{R} σ(x) for all x ∈ Var(E).

In order to compute solutions of an equation system, we transform it by the rules in Figure 1 until no more rules can be applied. The lazy narrowing transformation applies a rewrite rule to a function occurring outermost in an equation.^{4} Actually, this is not a narrowing step as defined in Section 2 since the argument terms may not be unifiable. Narrowing steps can be simulated by a sequence of transformations in the lazy unification calculus but not vice versa since our calculus also allows the application of rewrite rules to the arguments of the left-hand sides. The decomposition transformation generates equations between the argument terms of an equation if both sides have the same outermost symbol. The partial binding of variables can be applied if the variable x occurs at different positions in the equation system. In this case we instantiate the variable only with the outermost function symbol. A full instantiation by the substitution ϕ = {x ↦ f(t_{1}, …, t_{n})} may increase the computational work if x occurs several times and the evaluation of f(t_{1}, …, t_{n}) is costly. In order to avoid this problem of eager variable elimination (see [11]), we perform only a partial binding which is also called “root imitation” in [11].

At first sight our lazy unification calculus has many similarities with the lazy unification rules presented in [6, 11, 22, 25]. This is not accidental since these systems have inspired us. However, there are also essential differences. Since we are interested in reducing the computational costs in the E-unification procedure, our rules behave “more lazily”. In our rules it is allowed to evaluate a term only if its value is needed (in several positions). Otherwise, the term is left unevaluated.

Example 1. Consider the rewrite rule 0 ∗ x → 0. Then the only transformation sequence of the equation 0 ∗ t ≈ 0 (where t is a costly function) is

0 ∗ t ≈ 0 ⟹^{lu} 0 ≈ 0, t ≈ x, 0 ≈ 0 ⟹^{lu} t ≈ x, 0 ≈ 0 ⟹^{lu} t ≈ x

Thus the term t is not evaluated since its concrete value is not needed. Consequently, we may compute solutions with reducible terms which is a desirable property in the presence of a lazy evaluation mechanism. □

taken into account. 4 Similarly to logic programming, we have to apply rewrite rules with fresh variables in

order to ensure completeness.

Coalesce x ≈ y, E ⟹^{var} x ≈ y, ϕ(E)  if x, y ∈ Var(E) and ϕ = {x ↦ y}
Trivial  x ≈ x, E ⟹^{var} E

Figure 2. The variable elimination rules

The conventional transformation rules for unification w.r.t. an empty equational theory [21] bind a variable x to a term t only if x does not occur in t. This occur check must be omitted in the presence of evaluable function symbols. Moreover, we must also instantiate occurrences of x in the term t which is done in our partial binding rule. The following example shows the necessity of these extensions.

Example 2. Consider the rewrite rule f(c(a)) → a. Then we can solve the equation x ≈ c(f(x)) by the following transformation sequence:

x ≈ c(f(x)) ⟹^{lu} x ≈ c(x_{1}), x_{1} ≈ f(c(x_{1}))  (partial binding)
⟹^{lu} x ≈ c(x_{1}), c(x_{1}) ≈ c(a), x_{1} ≈ a  (lazy narrowing)
⟹^{lu} x ≈ c(x_{1}), x_{1} ≈ a, x_{1} ≈ a  (decomposition)
⟹^{lu} x ≈ c(a), x_{1} ≈ a, a ≈ a  (partial binding)
⟹^{lu} x ≈ c(a), x_{1} ≈ a  (decomposition)

In fact, the initial equation is solvable and {x ↦ c(a)} is a solution of this equation. This solution is also an obvious solution of the final equation system if we disregard the auxiliary variable x_{1}. □

In the rest of this section we will show soundness and completeness of our lazy unification calculus. Soundness simply means that each solution of the transformed equation system is also a solution of the initial equation system. Completeness is more difficult since we have to take into account all possible transformations. Therefore we will show that a solvable equation system can be transformed into another very simple equation system which has “an obvious solution”. Such a final equation system is called in “solved form”. According to [11, 21] we call an equation x ≈ t ∈ E solved (in E) if x is a variable which occurs neither in t nor anywhere else in E. In this case variable x is also called solved (in E). An equation system is solved or in solved form if all its equations are solved. A variable or equation is unsolved in E if it occurs in E but is not solved.

The lazy unification calculus in the present form cannot transform each solvable equation system into a solved form since equations between variables are not simplified. For instance, the equation system

x ≈ f(y), y ≈ z_{1}, y ≈ z_{2}, z_{1} ≈ z_{2}

is irreducible w.r.t. ⟹^{lu} but not in solved form since the variables y, z_{1}, z_{2} have multiple occurrences. Fortunately, this is not a problem since a solution can be extracted by merging the variables occurring in unsolved equations. Therefore we call this system quasi-solved. An equation system is quasi-solved if each equation s ≈ t is solved or has the property s, t ∈ X. In the following we will show that a quasi-solved equation system has solutions which can be easily computed by applying the rules in Figure 2 to it. The separation between the lazy unification rules in Figure 1 and the variable elimination rules in Figure 2 has technical reasons that will become apparent later (e.g., applying variable elimination to the equation y ≈ z_{1} may not reduce the complexity measure used in our completeness proofs). However, it is obvious to obtain the solutions of a quasi-solved equation system E. For this purpose we transform E by the rules in Figure 2 into a solved equation system which has a direct solution. This is always possible because ⟹^{var} is terminating, preserves solutions, and transforms each quasi-solved system into a solved one (see [17] for details). Moreover, the solutions of an equation system in solved form can be obtained as follows:

Proposition 1. Let E = {x_{1} ≈ t_{1}, …, x_{n} ≈ t_{n}} be an equation system in solved form. Then the substitution set

{γ ∘ {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} | γ is a ground substitution}

is a complete set of solutions for E.

Therefore it is sufficient to transform an equation system into a quasi-solved form. The soundness of the lazy unification calculus is implied by the following theorem which can be proved by a case analysis on the applied transformation rule [17].

Theorem 2. Let E and E′ be equation systems with E⟹^{lu}E′. Then each solution σ of E′ is also a solution of E.

For the completeness we show that for each solution of an equation system there is a derivation into a quasi-solved form that has the same solution. Note that the solution of the quasi-solved form cannot be identical to the required solution since new additional variables are generated during the derivation (by lazy narrowing and partial binding transformations). But this is not a problem since we are interested in solutions w.r.t. the variables of the initial equation system.

Theorem 3. Let E be a solvable equation system with solution σ. Then there exists a derivation E⟹^{lu}^{∗}E′ with E′ in quasi-solved form such that E′ has a solution σ′ with σ′(x) =_{R} σ(x) for all x ∈ Var(E). Proof. We show the existence of a derivation from E into a quasi-solved equation system by the following steps:

1. We define a reduction relation ⇒ on pairs of the form (σ, E) (where E is an equation system and σ is a solution of E) with the property that (σ, E) ⇒ (σ′, E′) implies E⟹^{lu}E′ and σ′(x) = σ(x) for all x ∈ Var(E).

2. We define a terminating ordering ≻ on these pairs.

3. We show: If E has a solution σ but E is not in quasi-solved form, then there exists a pair (σ′, E′) with (σ, E) ⇒ (σ′, E′) and (σ, E) ≻ (σ′, E′).

2 and 3 implies that each solvable equation system can be transformed into a quasisolved form. By 1, the solution of this quasi-solved form is the required solution of the initial equation system.

In the sequel we will show 1 and 3 in parallel. First we define the terminating ordering ≻. For this purpose we use the strict subterm ordering ≻_{sst} on terms defined by t ≻_{sst} s iff there is a position p in t with t|_{p} = s ≠ t. Since R is a terminating term rewriting system, the relation →_{R} on terms is also terminating. Let ≻≻ be the transitive closure of the relation →_{R} ∪ ≻_{sst}. Then ≻≻ is also terminating [20].^{5} Now we define the following ordering on pairs (σ, E): (σ, E) ≻ (σ′, E′) iff {σ(s), σ(t) | s ≈ t ∈ E unsolved} ≻≻_{mul} {σ′(s′), σ′(t′) | s′ ≈ t′ ∈ E′ unsolved} (∗)

5 Note that the use of the relation →_{R} instead of ≻ ≻ (as done in [6]) is not sufficient for the completeness proof since →_{R} has not the subterm property [4] in general.

where ≻≻_{mul} is the multiset extension^{6} of the ordering ≻≻ (all sets in this definition are multisets). ≻≻_{mul} is terminating (note that all multisets considered here are finite) since ≻≻ is terminating [4].

Now we will show that we can apply a transformation step to a solvable but unsolved equation system such that its complexity is reduced. Let E be an equation system not in quasi-solved form and σ be a solution of E. Since E is not quasisolved, there must be an equation which has one of the following forms:

1. There is an equation E = s ≈ t, E_{0} with s, t ∉ X: Let s = f(s_{1}, …, s_{n}) with n ≥ 0 (the other case is symmetric). Consider an innermost derivation of the normal forms of σ(s) and σ(t):

(a) No rewrite step is performed at the root of σ(s) and σ(t): Then t has the form t = f(t_{1}, …, t_{n}) and σ(s)↓_{R} = σ(t)↓_{R} = f(u_{1}, …, u_{n}). Since σ(s) and σ(t) are not reducible at the root, σ(s_{i})↓_{R} = u_{i} = σ(t_{i})↓_{R} for i = 1, …, n. Now we apply the decomposition transformation and obtain the equation system

E′ = s_{1} ≈ t_{1}, …, s_{n} ≈ t_{n}, E_{0}

Obviously, σ is a solution of E′. Moreover, the complexity of the new equation system is reduced because the equation s ≈ t is unsolved in E and each σ(s_{i}) and σ(t_{i}) is smaller than σ(s) and σ(t), respectively, since ≻≻ contains the strict subterm ordering ≻_{sst}. Hence (σ, E) ≻ (σ, E′).

(b) A rewrite step is performed at the root of σ(s), i.e., the innermost rewriting sequence of σ(s) has the form

σ(s) →_{R}^{∗} f(s′_{1}, …, s′_{1}) →_{R} θ(r) →_{R}^{∗} σ(s)↓_{R}

where f(l_{1}, …, l_{n}) → r is a new variant of a rewrite rule, θ(l_{i}) = s′_{i} and σ(s_{i}) →_{R}^{∗} s′_{i} for i = 1, …, n. An application of the lazy narrowing transformation yields the equation system

E′ = s_{1} ≈ l_{1}, …, s_{n} ≈ l_{n}, r ≈ t, E_{0}

We extend σ to a new substitution σ′ with σ′(x) = θ(x) for all x ∈ Dom(θ) (this is always possible since θ does only work on the variables of the new variant of the rewrite rule). σ′ is a solution of E′ since

σ′(s_{i}) = σ(s_{i}) →_{R}^{∗} s′_{i} = θ(l_{i}) = σ′(l_{i})

and σ′(r) = θ(r) →_{R}^{∗} σ(s)↓_{R} ↔_{R}^{∗} σ(t) = σ′(t)

Since the transitive closure of →_{R} is contained in ≻≻, σ(s_{i}) ≻≻ σ′(l_{i}) (if σ(s_{i}) ≠ σ′(l_{i})) and σ(s) ≻≻ σ′(r). Since s ≈ t is unsolved in E, the term σ(s) is contained in the left multiset of the ordering definition (∗), and it is replaced by the smaller terms σ(s_{1}), …, σ(s_{n}), σ′(l_{1}), …, σ′(l_{n}), σ′(r) (σ(s) ≻≻ σ(s_{i}) since ≻≻ contains the strict subterm ordering). Therefore the new equation system is smaller w.r.t. ≻, i.e., (σ, E) ≻ (σ′, E′).

2. There is an equation E = x ≈ t, E_{0} with t = f(t_{1}, …, t_{n}) and x unsolved in E: Hence x ∈ Var(t) ∪ Var(E_{0}). Again, we consider an innermost derivation of the normal form of σ(t):

(a) A rewrite step is performed at the root of σ(t). Then we apply a lazy narrowing step and proceed as in the previous case.

6 The multiset ordering ≻ ≻_{mul} is the transitive closure of the replacement of an element by a finite number of elements that are smaller w.r.t. ≻ ≻ [4].

(b) No rewrite step is performed at the root of σ(t), i.e., σ(t)↓_{R} = f(t′_{1}, …, t′_{n}) and σ(t_{i})↓_{R} = t′_{i} for i = 1, …, n. We apply the partial binding transformation and obtain the equation system

E′ = x ≈ f(x_{1}, …, x_{n}), x_{1} ≈ ϕ(t_{1}), …, x_{n} ≈ ϕ(t_{n}), ϕ(E_{0}) where ϕ = {x ↦ f(x_{1}, …, x_{n})} and x_{i} are new variables. We extend σ to a substitution σ′ by adding the bindings σ′(x_{i}) = t′_{i} for i = 1, …, n. Then σ′(f(x_{1}, …, x_{n})) = f(t′_{1}, …, t′_{n}) = σ(t)↓_{R} ↔_{R}^{∗} σ(t) ↔_{R}^{∗} σ(x) = σ′(x) Moreover, σ′(ϕ(x)) = σ′(x)↓_{R} which implies σ′(s) ↔_{R}^{∗} σ′(ϕ(s)) for all terms s. Hence σ′(ϕ(t_{i})) ↔_{R}^{∗} σ′(t_{i}) ↔_{R}^{∗} t′_{i} = σ′(x_{i}). Altogether, σ′ is a solution of E′. It remains to show that this transformation reduces the complexity of the equation system. Since σ′(ϕ(x)) = σ(x)↓_{R}, we have σ(x) →_{R}^{∗} σ′(ϕ(x)). Hence σ(E_{0}) is equal to σ′(ϕ(E_{0})) (if σ(x) = σ′(ϕ(x))) or σ′(ϕ(E_{0})) is smaller w.r.t. ≻≻_{mul}. Therefore it remains to check that σ(t) is greater than each σ′(x_{1}), …, σ′(x_{n}), σ′(ϕ(t_{1})), …, σ′(ϕ(t_{n})) w.r.t. ≻≻ (note that the equation x ≈ t is unsolved in E, but the equation x ≈ f(x_{1}, …, x_{n}) is solved in E′). First of all, σ(t) ≻≻ σ(t_{i}) since ≻≻ includes the strict subterm ordering. Moreover, σ(t_{i}) →_{R}^{∗} σ′(x_{i}), i.e., σ′(x_{i}) is equal or smaller than σ(t_{i}) w.r.t. ≻≻ for i = 1, …, n. This implies σ(t) ≻≻ σ′(x_{i}). Similarly, σ′(ϕ(t_{i})) is equal or smaller than σ(t_{i}) w.r.t. ≻≻ since σ′(ϕ(x)) = σ(x)↓_{R}. Thus σ(t) ≻≻ σ′(ϕ(t_{i})). Altogether, (σ, E) ≻ (σ′, E′). ⊓ ⊔

We want to point out that there exist also other orderings on substitution/equation system pairs to prove the completeness of our calculus. However, the ordering chosen in the above proof is tailored to a simple proof for the completeness of lazy unification with simplification as we will see in the next section.

The results of this section imply that a complete set of solutions for a given equation system E can be computed by enumerating all derivations in the lazy unification calculus from E into a quasi-solved equation system. Due to the nondeterminism in the lazy unification calculus, there are many unsuccessful and often infinite derivations. Therefore we will show in the next section how to reduce this nondeterminism by integrating a deterministic simplification process into the lazy unification calculus. More determinism can be achieved by dividing the set of function symbols into constructors and defined functions. This will be the subject of Section 5.

4 Integrating simplification into lazy unification

The lazy unification calculus admits a high degree of nondeterminism even if there is only one reasonable derivation. This is due to the fact that functional expressions are processed “too lazy”.

Example 3. Consider the rewrite rules

\begin{matrix}f(a) → & c & g(a) → & a \\ f(b) → & d & g(b) → & b \end{matrix}

and the equation f(g(b)) ≈ d. Then there are four different derivations in our lazy unification calculus, but only one derivation is successful. If we would first compute the normal form of f(g(b)), which is d, then there is only one possible derivation: d ≈ d ⟹^{lu} ∅. Hence we will show that the lazy unification calculus remains to be sound and complete if the (deterministic!) normalization of terms is included. □

It is well-known [9, 16] that the inclusion of inductive consequences for normalization may have an essential effect on the search space reduction in normalizing narrowing strategies. Therefore we will also allow the use of additional inductive consequences for normalization. A rewrite rule l → r is called inductive consequence (of R) if σ(l) =_{R} σ(r) for all ground substitutions σ. For instance, the rule x + 0 → x is an inductive consequence of the term rewriting system

0 + y → y  s(x) + y → s(x + y)

If we want to solve the equation s(x)+0 ≈ s(x), our basic lazy unification calculus would enumerate the solutions x ↦ 0, x ↦ s(0), x ↦ s(s(0)) and so on, i.e., this equation has an infinite search space. Using the inductive consequence x + 0 → x for normalization, the equation s(x) + 0 ≈ s(x) is reduced to s(x) ≈ s(x) and then transformed into the quasi-solved form x ≈ x representing the solution set where x is replaced by any ground term.^{7}

In the following we assume that S is a set of inductive consequences of R (the set of simplification rules) so that the rewrite relation →_{S} is terminating. We will use rules from R for lazy narrowing and rules from S for simplification. Note that each rule from R is also an inductive consequence and can be included in S. But we do not require that all rules from R must be used for normalization. This is reasonable if there are duplicating rules where one variable of the left-hand side occurs several times on the right-hand side, like f(x) → g(x, x). If we normalize the equation f(s) ≈ t with this rule, then the term s is duplicated which may increase the computational costs if the evaluation of s is necessary and costly. In such a case it would be better to use this rule only in lazy narrowing steps.

In order to include simplification into the lazy unification calculus, we define a relation ⇒_{S} on systems of equations. s ≈ t ⇒_{S} s′ ≈ t′ iff s′ and t′ are normal forms of s and t w.r.t. →_{S}, respectively. E ⇒_{S} E′ iff E = e_{1}, …, e_{n} and E′ = e′_{1}, …, e′_{n} where e_{i} ⇒_{S} e′_{i} for i = 1, …, n. Note that ⇒_{S} describes a deterministic computation process.^{8} E⟹^{lus}E′ is a derivation step in the lazy unification calculus with simplification if E ⇒_{S} \overline{E}⟹^{lu}E′ for some \overline{E}.

The soundness of the calculus ⟹^{lus} can be shown by a simple induction on the computation steps using Theorem 2 and the following lemma which shows the soundness of one rewrite step with a simplification rule:

Lemma 4. Let s ≈ t be an equation and s →_{S} s′ be a rewrite step. Then each solution of s′ ≈ t is also a solution of s ≈ t.

For the completeness proof we have to show that solutions are not lost by the application of inductive consequences:

Lemma 5. Let E be an equation system and σ be a solution of E. If E ⇒_{S} E′, then σ is a solution of E′.

7 In larger single-sorted term rewriting systems it would be difficult to find inductive consequences. E.g., x + 0 → x is not an inductive consequence if there is a constant a since a + 0 =_{R} a is not valid. However, in practice specifications are many-sorted and then inductive consequences must be valid only for all well-sorted ground substitutions. Therefore we want to point out that all results in this paper can also be extended to many-sorted term rewriting systems in a straightforward way.

8 If there exist more than one normal form w.r.t. →_{S}, it is sufficient to select don’t care one of these normal forms.

This lemma would imply the completeness of the calculus ⟹^{lus} if a derivation step with ⇒_{S} does not increase the ordering used in the proof of Theorem 3. Unfortunately, this is not the case in general since the termination of →_{R} and →_{S} may be based on different orderings (e.g., R = {a → b} and S = {b → a}). In order to avoid such problems, we require that the relation →_{R∪S} is terminating which is not a real restriction in practice.

Theorem 6. Let S be a set of inductive consequences of the ground confluent and terminating term rewriting system R such that →_{R∪S} is terminating. Let E be a solvable equation system with solution σ. Then there exists a derivation E ⟹^{lus}^{∗} E′ such that E′ is in quasi-solved form and has a solution σ′ with σ′(x) =_{R} σ(x) for all x ∈ Var(E).

Proof. In the proof of Theorem 3 we have shown how to apply a transformation step to an equation system not in quasi-solved form such that the solution is preserved. We can use the same proof for the transformation ⟹^{lus} since Lemma 5 shows that normalization steps preserve solutions. The only difference concerns the ordering where we use →_{R∪S} instead of →_{R}, i.e., ≻≻ is now defined to be the transitive closure of the relation →_{R∪S} ∪ ≻_{sst}. Clearly, this does not change anything in the proof of Theorem 3. Moreover, the relation ⇒_{S} does not increase the complexity w.r.t. this ordering but reduces it if inductive consequences are applied since →_{S} is contained in ≻≻. ⊓ ⊔

These results show that we can integrate the deterministic simplification process into the lazy unification calculus without loosing soundness and completeness. Note that the rules from S can only be applied if their left-hand sides can be matched with a subterm of the current equation system. If these subterms are not sufficiently instantiated, the rewrite rules are not applicable and hence we loose potential determinism in the unification process.

Example 4. Consider the rules

zero(s(x)) → zero(x)  zero(0) → 0

(assume that these rules are contained in R as well as in S) and the equation system zero(x) ≈ 0, x ≈ 0. Then there exists the following derivation in our calculus (this derivation is also possible in the unification calculi in [11, 22]):

zero(x) ≈ 0, x ≈ 0
⟹^{lus} x ≈ s(x_{1}), zero(x_{1}) ≈ 0, x ≈ 0  (lazy narrowing)
⟹^{lus} x ≈ s(x_{1}), x_{1} ≈ s(x_{2}), zero(x_{2}) ≈ 0, x ≈ 0  (lazy narrowing)
⟹^{lus} ⋯

This infinite derivation could be avoided if we apply the partial binding rule in the first step:

zero(x) ≈ 0, x ≈ 0 ⟹^{lus} zero(0) ≈ 0, x ≈ 0  (partial binding)
⇒_{S} 0 ≈ 0, x ≈ 0  (rewriting with second rule)
⟹^{lus} x ≈ 0  (decomposition)

In the next section we will present an optimization which prefers the latter derivation and avoids the first infinite derivation. □

Decomposition of constructor equations

c(t_{1}, …, t_{n}) ≈ c(t′_{1}, …, t′_{n}), E ⟹^{luc} t_{1} ≈ t′_{1}, …, t_{n} ≈ t′_{n}, E if c ∈ C

Full binding of variables to ground constructor terms

x ≈ t, E ⟹^{luc} x ≈ t, ϕ(E) if x ∈ Var(E), t ∈ T (C, ∅) and ϕ = {x ↦ t}

Partial binding of variables to constructor terms

x ≈ c(t_{1}, …, t_{n}), E ⟹^{luc} x ≈ c(x_{1}, …, x_{n}), x_{1} ≈ ϕ(t_{1}), …, x_{n} ≈ ϕ(t_{n}), ϕ(E)

if x ∈ Var(c(t_{1}, …, t_{n}))∪Var(E), x ∉ cvar(c(t_{1}, …, t_{n})) and ϕ = {x ↦ c(x_{1}, …, x_{n})} (x_{i} new variable)

Figure 3. Deterministic transformations for constructor-based rewrite systems

5 Constructor-based systems

In practical applications of equational logic programming a distinction is made between operation symbols to construct data terms, called constructors, and operation symbols to operate on data terms, called defined functions (see, for instance, the functional logic languages ALF [15], BABEL [23], K-LEAF [13], SLOG [9], or the RAP system [12]). Such a distinction allows to optimize our unification calculus. Therefore we assume in this section that the signature F is divided into two sets F = C ∪ D, called constructors and defined functions, with C ∩ D = ∅. A constructor term t is built from constructors and variables, i.e., t ∈ T (C, X). The distinction between constructors and defined functions comes with the restriction that for all rewrite rules l → r the outermost symbol of l is always a defined function.

The important property of such constructor-based term rewriting systems is the irreducibility of constructor terms. Due to this fact we can specialize the rules of our basic lazy unification calculus. Therefore we define the deterministic transformations in Figure 3. Deterministic transformations are intended to be applied as long as possible before any transformation ⟹^{lu} is used. Hence they can be integrated into the deterministic normalization process ⇒_{S}. It is obvious that this modification preserves soundness and completeness. The decomposition transformation for constructor equations must be applied in any case in order to obtain a quasi-solved equation system since a lazy narrowing step R cannot be applied to constructor equations. The full binding of variables to ground constructor terms is an optimization which combines subsequent applications of partial binding transformations. This transformation decreases the complexity used in the proof of Theorem 6 since a constructor term is always in normal form. The partial binding transformation for constructor terms performs an eager (partial) binding of variables to constructor terms since a lazy narrowing step cannot be applied to the constructor term. Moreover, this binding transformation is combined with an occur check since it cannot be applied if x ∈ cvar(c(t_{1}, …, t_{n})) where cvar denotes the set of all variables occurring outside terms headed by defined function symbols. This restriction avoids infinite derivations of the following kind:

x ≈ c(x) ⟹^{lu} x ≈ c(x_{1}), x_{1} ≈ c(x_{1})  (partial binding)
⟹^{lu} x ≈ c(x_{1}), x_{1} ≈ c(x_{2}), x_{2} ≈ c(x_{2})  (partial binding)
⟹^{lu} ⋯

A further optimization can be added if all functions are reducible on ground constructor terms, i.e., for all f ∈ D and t_{1}, …, t_{n} ∈ T (C, ∅) there exists a term t

Clash  c(t_{1}, …, t_{n}) ≈ d(t′_{1}, …, t′_{m}), E ⟹^{luc} fail if c, d ∈ C and c ≠ d
Occur check x ≈ c(t_{1}, …, t_{n}), E ⟹^{luc} fail  if x ∈ cvar(c(t_{1}, …, t_{n}))

Figure 4. Failure rules for constructor-based rewrite systems

with f(t_{1}, …, t_{n}) →_{R} t. In this case all ground terms have a ground constructor normal form and therefore the partial binding transformation of ⟹^{lu} can be completely omitted which increases the determinism in the lazy unification calculus.

If we invert the deterministic transformation rules, we obtain a set of failure rules shown in Figure 4. Failure rules are intended to be tried during the deterministic transformations. If a failure rule is applicable, the derivation can be safely terminated since the equation system cannot be transformed into a quasi-solved system.

6 Examples

In this section we demonstrate the improved computational power of our lazy unification calculus with simplification by means of two examples. The first example shows that simplification reduces the search space in the presence of rewrite rules with overlapping left-hand sides.

Example 5. Consider the following ground confluent and terminating rewrite system defining the Boolean operator ∨ and the predicate even on natural numbers:

\begin{matrix}true ∨ b → & true & even(0) → & true \\ b ∨ true → & true & even(s(0)) → & false \\ false ∨ false → & false & even(s(s(x))) → & even(x) \end{matrix}

If we want to solve the equation even(z)∨true ≈ true, the lazy unification calculus without simplification could apply a lazy narrowing step with the first ∨-rule. This yields the equation system

even(z) ≈ true, true ≈ b, true ≈ true

Now there are infinitely many solutions to the new equation even(z) ≈ true by instantiating the variable z with the values s^{2∗i}(0), i ≥ 0, i.e., the lazy unification calculus without simplification (cf. Section 3) has an infinite search space. The same is true for other lazy unification calculi [11, 22] or lazy narrowing calculi [23, 27]. Moreover, in a sequential implementation of lazy narrowing by backtracking [14] only an infinite set of specialized solutions would be computed without ever trying the second ∨-rule. But if we use our lazy unification calculus with simplification where all rewrite rules are used for simplification (i.e., R = S), then the initial equation even(z) ∨ true ≈ true is first simplified to true ≈ true by rewriting with the second ∨-rule. Hence our calculus has a finite search space. □

If the left-hand sides of the rewrite rules do not overlap, i.e., if the functions are defined by a case distinction on one argument, then there exists a lazy narrowing strategy (needed narrowing [1]) which is optimal w.r.t. the length of derivations. However, unsuccessful infinite derivations can be avoided also in this case by our lazy unification calculus with simplification if inductive consequences are added to the set of simplification rules.

Example 6. Consider the following rewrite rules for the addition and multiplication on natural numbers where C = {0, s} are constructors and D = {+, ∗} are defined functions:

\begin{matrix}0 + y → & y & (1) & 0 ∗ y → & 0 & (3) \\ s(x) + y → & s(x + y) & (2) & s(x) ∗ y → & y + x ∗ y & (4) \end{matrix}

If we use this confluent and terminating set of rewrite rules for lazy narrowing (R) as well as for normalization (S) and add the inductive consequence x ∗ 0 → 0 to S, then our lazy unification calculus with simplification has a finite search space for the equation x ∗ y ≈ s(0). This is due to the fact that the following derivation can be terminated using the inductive consequence and the clash rule: x ∗ y ≈ s(0)

⟹^{lu} x ≈ s(x_{1}), y ≈ y_{1}, y_{1} + x_{1} ∗ y_{1} ≈ s(0)  (lazy narrowing, rule 4)
⟹^{lu} x ≈ s(x_{1}), y ≈ y_{1}, y_{1} ≈ 0, x_{1} ∗ y_{1} ≈ y_{2}, y_{2} ≈ s(0) (lazy narrowing, rule 1)
⟹^{luc} x ≈ s(x_{1}), y ≈ 0, y_{1} ≈ 0, x_{1} ∗ 0 ≈ y_{2}, y_{2} ≈ s(0) (bind variable y_{1})
⟹^{luc} x ≈ s(x_{1}), y ≈ 0, y_{1} ≈ 0, x_{1} ∗ 0 ≈ s(0), y_{2} ≈ s(0) (bind variable y_{2})
⇒_{S} x ≈ s(x_{1}), y ≈ 0, y_{1} ≈ 0, 0 ≈ s(0), y_{2} ≈ s(0)  (reduce x_{1} ∗ 0)
⟹^{luc} fail  (clash between 0 and s)

The equation x_{1} ∗ 0 ≈ s(0) could not be transformed into the equation 0 ≈ s(0) without the inductive consequence. Consequently, an infinite derivation would occur in our basic unification calculus of Section 3.

Note that other lazy unification calculi [11, 22] or lazy narrowing calculi [23, 27] have an infinite search space for this equation. It is also interesting to note that a normalizing innermost narrowing strategy as in [9] has also an infinite search space even if the same inductive consequences are available. This shows the advantage of combining a lazy strategy with a simplification process. □

7 Conclusions

In this paper we have presented a calculus for unification in the presence of an equational theory. In order to obtain a small search space, the calculus is designed in the spirit of lazy evaluation, i.e., functions are not evaluated if their result is not required to solve the unification problem. The most important property of our calculus is the inclusion of a deterministic simplification process. This has the positive effect that our calculus is more efficient (in terms of the search space size) than other lazy unification calculi or eager narrowing calculi (like basic narrowing, innermost narrowing) with simplification. We think that our calculus is the basis of efficient implementations of future functional logic languages.

Acknowledgements. The author is grateful to Harald Ganzinger for his pointer to a suitable termination ordering and to two anonymous referees for their helpful remarks. 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 Symp. on Principles of Programming Languages, pp. 268–279, Portland, 1994.

2. D. Bert and R. Echahed. Design and Implementation of a Generic, Logic and Functional Programming Language. In Proc. ESOP’86, pp. 119–132. Springer LNCS 213, 1986.

3. J. Darlington and Y. Guo. Narrowing and unification in functional programming - an evaluation mechanism for absolute set abstraction. In Proc. of the Conference on Rewriting Techniques and Applications, pp. 92–108. Springer LNCS 355, 1989.

4. N. Dershowitz. Termination of Rewriting. J. Symbolic Computation, Vol. 3, pp. 69–116, 1987.

5. 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.

6. N. Dershowitz, S. Mitra, and G. Sivakumar. Equation Solving in Conditional AC-Theories. In Proc. ALP’90, pp. 283–297. Springer LNCS 463, 1990.

7. R. Echahed. Uniform Narrowing Strategies. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 259–275. Springer LNCS 632, 1992.

8. M.J. Fay. First-Order Unification in an Equational Theory. In Proc. 4th Workshop on Automated Deduction, pp. 161–167, Austin (Texas), 1979. Academic Press.

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. J.H. Gallier and S. Raatz. Extending SLD-Resolution to Equational Horn Clauses Using E-Unification. Journal of Logic Programming (6), pp. 3–43, 1989.

11. J.H. Gallier and W. Snyder. Complete Sets of Transformations for General E-Unification. Theoretical Computer Science, Vol. 67, pp. 203–260, 1989.

12. A. Geser and H. Hussmann. Experiences with the RAP system – a specification interpreter combining term rewriting and resolution. In Proc. ESOP 86, pp. 339– 350. Springer LNCS 213, 1986.

13. 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.

14. W. Hans, R. Loogen, and S. Winkler. On the Interaction of Lazy Evaluation and Backtracking. In Proc. PLILP’92, pp. 355–369. Springer LNCS 631, 1992.

15. M. Hanus. Compiling Logic Programs with Equality. In Proc. PLILP’90, pp. 387– 401. Springer LNCS 456, 1990.

16. M. Hanus. Improving Control of Logic Programs by Using Functional Logic Languages. In Proc. PLILP’92, pp. 1–23. Springer LNCS 631, 1992.

17. M. Hanus. Lazy Unification with Inductive Simplification. Technical Report MPI-I-93-215, Max-Planck-Institut für Informatik, Saarbrücken, 1993.

18. M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. To appear in Journal of Logic Programming, 1994.

19. S. Hölldobler. Foundations of Equational Logic Programming. Springer LNCS 353, 1989.

20. J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, Vol. 15, No. 4, pp. 1155–1194, 1986.

21. A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, Vol. 4, No. 2, pp. 258–282, 1982.

22. A. Martelli, G.F. Rossi, and C. Moiso. Lazy Unification Algorithms for Canonical Rewrite Systems. In Hassan Aït-Kaci and Maurice Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2, Rewriting Techniques, chapter 8, pp. 245–274. Academic Press, New York, 1989.

23. 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.

24. W. Nutt, P. Réty, and G. Smolka. Basic Narrowing Revisited. Journal of Symbolic Computation, Vol. 7, pp. 295–317, 1989.

25. P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer, 1988.

26. G.D. Plotkin. Building-in Equational Theories. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pp. 73–90, 1972.

27. U.S. Reddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. IEEE Internat. Symposium on Logic Programming, pp. 138–151, Boston, 1985.

28. P. Réty. Improving basic narrowing techniques. In Proc. of the Conference on Rewriting Techniques and Applications, pp. 228–241. Springer LNCS 256, 1987.

29. J.H. Siekmann. An Introduction to Unification Theory. In Formal Techniques in Artificial Intelligence, pp. 369–425. Elsevier Science Publishers, 1990.