MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Lazy Unification with Inductive Simplification

Michael Hanus

MPI–I–93–215 April 1993

[figure: I N F O R M A T I K]

Im Stadtwald W 6600 Saarbrücken

Germany Author’s Address

Michael Hanus Max-Planck-Institut für Informatik Im Stadtwald W-6600 Saarbrücken Germany

michael@mpi-sb.mpg.de

Acknowledgements

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). The responsibility for the contents of this publication lies with the author.

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 with inductive axioms into the unification process. Inductive simplification reduces the search space so that in some case infinite search spaces are reduced to finite ones. Consequently, more efficient unification algorithms can be achieved. We prove soundness and completeness of our method for equational theories represented by ground confluent and terminating rewrite systems.

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 [Plo72] or if functions should be integrated into a logic language [GR89]. Therefore the development of E-unification algorithms is an active research topic during recent years (see, for instance, [Sie90]).

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 the addition and multiplication on natural numbers which are represented by terms of the form s(⋯ s(0) ⋯):

\begin{matrix}0 + y ≈ & y \\ s(x) + y ≈ & s(x + y) \\ 0 ∗ y ≈ & 0 \\ 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 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.

[MRM89] 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 [GS89] 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 [Red85] as the operational principle of functional logic languages. You [You89] has shown completeness of outer narrowing for confluent and terminating constructor-based axioms. Echahed [Ech92] has proved completeness of any narrowing strategy but with strong requirements on the equational theory.

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 [Fay79, Fri85, Rét87, Höl89, NRS89, Han92b]. In this paper we propose to include simplification into lazy unification, i.e., equations are simplified to a normal form before the application of a unification step. Since it seems that lazy unification avoids many unnecessary nondeterministic computations due its outermost behavior (especially, if dynamic tests for variable instantiations are added [LW91]), we will allow simplification with inductive axioms. An inductive axiom is an equation which is valid for all ground instances of it. For instance, the equation x + 0 ≈ x is an inductive axiom of the above specification. Using this inductive axiom, the equation z + 0 ≈ z is simplified to z ≈ z which means that the identity is a solution to the initial equation. Note that without this simplification an E-unification procedure would enumerate the solutions z ↦ 0, z ↦ s(0), z ↦ s(s(0)) and so on. Of course, this is also true for any other narrowing strategy like Fribourg’s innermost narrowing with inductive simplification [Fri85]. However, we will give in Section 5 an example which shows that our lazy unification calculus with inductive simplification terminates where other eager narrowing strategies with the identical inductive simplification axioms have an infinite search space. Hence the integration of lazy unification with inductive simplification has practical advantages.

Simplification with inductive axioms has also been proposed by other researchers. Fribourg [Fri85] has integrated it into an innermost narrowing strategy. This has the important effect that the efficiency of programs can be dramatically improved (see also [Han92a]). Echahed [Ech92] has shown the completeness of any narrowing strategy with inductive simplification but only under strong requirements (uniformity of specifications). Dershowitz et al. [DMS90] have proposed to combine lazy unification with simplification and demonstrated the usefulness of inductive axioms 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 with inductive simplification and give a rigorous completeness proof. The distinguishing features of our framework are:

• We consider a 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 the use of inductive consequences for simplification.

In the next section we recall basic notions from term rewriting. Section 3 presents our basic lazy unification calculus. In Section 4 we show how to include a deterministic simplification process into the lazy unification calculus. Finally, we show in Section 5 some important optimizations for constructor-based specifications.

2 Computing in equational theories

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

A signature F is a set of function symbols. Every operation f ∈ F is associated with an arity.^{1} Let X be a countably infinite set of variables. In this paper we write x, y, z for elements of X. Then the set T (F, X) of terms built from F and X is the smallest set containing X such that f(t_{1}, …, t_{n}) ∈ T (F, X) whenever f ∈ F has arity n and t_{1}, …, t_{n} ∈ T (F, X). We write f instead of f() whenever f has arity 0. The set of variables occurring in a term t is denoted by Var(t) (similarly for the other syntactic constructions defined below, like equation, rewriting rule etc.). A ground term t is a term without variables, i.e., Var(t) = ∅. In the following we assume that F is a signature with at least one constant.

The computation w.r.t. equational theories requires notions like substitution, unifier and subterm which will be defined next. 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. The union of two substitutions ϕ and σ is defined by

(ϕ ∪ σ)(x) = \{ \begin{matrix}ϕ(x) & if x ∈ Dom(ϕ) \\ σ(x) & if x ∈ Dom(σ) \\ x & otherwise \end{matrix}

only if Dom(ϕ) ∩ Dom(σ) = ∅.

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 [DJ90] for details).

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 exist 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 substitution σ is called irreducible or normalized if σ(x) is in normal form for all variables x ∈ X. 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}.

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

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 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 ⇝_{[p,l→r,σ]} t′ or simply t ⇝_{σ} t′. If there is a narrowing sequence t_{1} ⇝_{σ_{1}} t_{2} ⇝_{σ_{2}} ⋯ ⇝_{σ_{n−1}} t_{n}, we write t_{1} ⇝_{σ}^{∗} t_{n} with σ = σ_{n−1} ∘ ⋯ ∘ σ_{2} ∘ σ_{1}.

Narrowing is able to solve equations w.r.t. R. For this purpose we introduce two new function symbols =^{?} and true and add the rewrite rule x =^{?} x → true to R. Then narrowing is sound and complete in the following sense.

Theorem 2.1 ([Hul80]) Let R be a term rewriting system so that →_{R} is confluent and terminating.

1. If s =^{?} t ⇝_{σ}^{∗} true, then σ(s) =_{R} σ(t).

2. If σ′(s) =_{R} σ′(t), then there exist a narrowing derivation s =^{?} t ⇝_{σ}^{∗} true and a substitution ϕ with ϕ(σ(x)) =_{R} σ′(x) for all x ∈ Var(s) ∪ Var(t).

Since this simple narrowing procedure (enumerating all narrowing derivations) is very inefficient, several authors have proposed restrictions on the admissible narrowing derivations. For instance, Hullot [Hul80] has introduced basic narrowing where narrowing steps in positions introduced by substitutions are forbidden. Fribourg [Fri85] has proposed innermost narrowing where narrowing is applied only at innermost positions, and Hölldobler [Höl89] has combined innermost and basic narrowing. Krischer and Bockmayr [KB91] have proposed additional tests during narrowing derivations to eliminate redundant derivations. Narrowing at outermost positions is only complete if the term rewrite system satisfies strong restrictions [Ech88]. Lazy narrowing [Red85, DG89, MKLR90] 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 [BGL^{+}87, MR92]. 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 [MRM89, DMS90].

From a practical point of view the most essential improvement of simple narrowing is normalizing narrowing [Fay79] 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) whereas different narrowing steps may lead to different solutions and therefore all admissible narrowing steps must be considered. Hence in a sequential implementation rewriting can be efficiently implemented like reductions in functional languages whereas narrowing steps need costly backtracking management like in Prolog. For instance, if s =_{R} t, normalizing narrowing will prove the validity by a pure deterministic computation (reducing s and t to the same normal form) whereas simple narrowing would compute the normal form of s and t by costly narrowing steps. As shown in [Fri85, Han92a], normalizing narrowing has the important effect that equational logic programs (which can be seen as an integration of functional and logic programming languages) are more efficiently executable than pure logic programs.

The idea of normalizing narrowing can also be combined with other narrowing restrictions. Rety [Rét87] has proved completeness of normalizing basic narrowing, Fribourg [Fri85] has proposed normalizing innermost narrowing and Hölldobler [Höl89] has combined innermost basic narrowing with normalization. Because of these important advantages, normalizing narrowing is the foundation of several programming languages which combines functional and logic programming like SLOG [Fri85] or ALF [Han90]. However, normalization has not been included in narrowing strategies with a lazy behavior, i.e., which compute functions only if their values are needed.^{2} Therefore we will present a lazy unification calculus which includes a normalization process where the term rewrite rules as well as additional inductive axioms 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 [MM82] 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

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. 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 Lazy narrowing

2Except for [DMS90, Ech92], but see the remarks in Section 1.

3We are interested in ground solutions since later we will include inductive axioms which are valid in the ground models of R. As pointed out in [NRS89], this ground approach subsumes the conventional narrowing approaches where also non-ground solutions are taken into account (as in Theorem 2.1).

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 rewrite 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})} (where x_{i} new variable)

Figure 1: The lazy unification calculus

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 [GS89]), we perform only a partial binding which is also called “root imitation” in [GS89].

It is possible to add further rules to simplify equation systems like the elimination of trivial equations:

t ≈ t, E ⟹^{lu} E

However, these rules are not really necessary and therefore we omit them in our first approach. Later we will see how to add deterministic (failure) rules to reduce the search space of the calculus.

At first sight our lazy unification calculus has many similarities with the lazy unification rules presented in [Pad88, GS89, MRM89, DMS90]. 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 3.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  (lazy narrowing)
⟹^{lu} t ≈ x, 0 ≈ 0  (decomposition)
⟹^{lu} t ≈ x  (decomposition)

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

The conventional transformation rules for unification w.r.t. an empty equational theory [MM82] 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 3.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 prove 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 [MM82, GS89] we call an equation x ≈ t of an equation system 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 no 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 quasisolved 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 justified by the following propositions.

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

Proposition 3.3 Let E and E′ be equation systems with E⟹^{var}E′. Then E and E′ have the same solutions.

Proof: It is obvious that E and E′ have the same solutions if the transformation rule “Trivial” is applied. In case of the rule “Coalesce” E has the form x ≈ y, E_{0} and E′ has the form x ≈ y, ϕ(E_{0}) with ϕ = {x ↦ y}. Let σ be a solution of E. Then σ(x) ↔_{R}^{∗} σ(y) = σ(ϕ(x)). By definition of ϕ and the congruence property of ↔_{R}^{∗}, σ(t) ↔_{R}^{∗} σ(ϕ(t)) for all terms t. Let s ≈ t ∈ E_{0}. Since σ is a solution of E, σ(s) ↔_{R}^{∗} σ(t). Moreover, σ(s) ↔_{R}^{∗} σ(ϕ(s)) and σ(t) ↔_{R}^{∗} σ(ϕ(t)) which implies σ(ϕ(s)) ↔_{R}^{∗} σ(ϕ(t)). Therefore σ is also a solution of ϕ(E_{0}).

If σ is a solution of E′, it can be shown in a similar way that σ is also a solution of E_{0}.

Due to this proposition, the transformation ⟹^{var} preserves solutions. Moreover, it is a terminating relation:

Proposition 3.4 The relation ⟹^{var} on equation systems is terminating.

Proof: Define the complexity of an equation system as the total number of occurrences of unsolved variables in this system. Obviously, both transformation rules of ⟹^{var} reduce this number.

If an equation system is quasi-solved, we can always transform it into a solved system:

Proposition 3.5 Let E be a quasi-solved equation system. Then there exists a solved equation system E′ with E⟹^{var}^{∗}E′.

Proof: Let E be a quasi-solved equation system which is not solved. Then there exists an equation x ≈ y ∈ E which is unsolved. Hence x = y or x, y ∈ Var(E − {x ≈ y}). In the first case we apply the rule “Trivial” and in the second case we apply the rule “Coalesce”. The result of both cases is a new equation system in quasi-solved form. Since there are no infinite derivations w.r.t. ⟹^{var} (Proposition 3.4), successive transformation steps w.r.t. ⟹^{var} will end in a solved equation system.

The solutions of an equation system in solved form can be obtained as follows:

Proposition 3.6 Let E be an equation system in solved form, i.e.,

E = {x_{1} ≈ t_{1}, …, x_{n} ≈ t_{n}}

where x_{1}, …, x_{n} are different variables with x_{i} ∉ Var(t_{j}) for i, j ∈ {1, …, n}. Then the substitution set

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

is a complete set of solutions for E.

Proof: First we show that θ : = γ ∘ {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} is a solution of E for an arbitrary ground substitution γ. Consider the equation x_{i} ≈ t_{i} ∈ E. Since x_{1}, …, x_{n} do not occur in any t_{i}, θ(x_{i}) = γ(t_{i}) = θ(t_{i}), i.e., θ is a solution of x_{i} ≈ t_{i}. Hence θ is a solution of E.

Next we show that every solution of E is covered by some substitution from the substitution set defined above. Let ξ be a solution of E. Then ξ(x_{i}) =_{R} ξ(t_{i}) for i = 1, …, n. Since ξ is a ground substitution, the substitution

θ : = ξ ∘ {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}

is contained in the above substitution set. We have to show ξ(x) =_{R} θ(x) for all x ∈ Var(E):

• By definition of θ and ξ, θ(x_{i}) = ξ(t_{i}) =_{R} ξ(x_{i}) for i = 1, …, n.

• If x ∈ Var(t_{j}) for some j ∈ {1, …, n}, then θ(x) = ξ(x) by definition of θ (note that x is different from any x_{i} since no x_{i} occurs in t_{j}).

Altogether, θ(x) =_{R} ξ(x) for all x ∈ Var(E).

Due to Propositions 3.3, 3.5 and 3.6 it is sufficient to transform an equation system into a quasisolved form in order to compute its solutions. Hence we can state soundness and completeness results by concentrating on quasi-solved forms. The next lemma shows the soundness if a transformation rule of the lazy unification calculus is applied.

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

Proof: Assume that σ is a solution of E′. There are three cases corresponding to the applied transformation rule:

1. The lazy narrowing rule has been applied. Then E = f(t_{1}, …, t_{n}) ≈ t, E_{0}, f(l_{1}, …, l_{n}) → r is a variant of a rewrite rule and E′ = t_{1} ≈ l_{1}, …, t_{n} ≈ l_{n}, r ≈ t, E_{0}. Since σ is a solution of E′, σ(t_{i}) ↔_{R}^{∗} σ(l_{i}) (for i = 1, …, n) and σ(r) ↔_{R}^{∗} σ(t). These equivalences imply σ(f(t_{1}, …, t_{n})) ↔_{R}^{∗} σ(f(l_{1}, …, l_{n})) by the congruence property of ↔_{R}^{∗}. Since f(l_{1}, …, l_{n}) → r is a variant of a rewrite rule, σ(f(l_{1}, …, l_{n})) →_{R} σ(r) ↔_{R}^{∗} σ(t). Hence σ(f(t_{1}, …, t_{n})) ↔_{R}^{∗} σ(t), i.e., σ is a solution of E.

2. The decomposition rule has been applied. Then E = f(t_{1}, …, t_{n}) ≈ f(t′_{1}, …, t′_{n}), E_{0} and E′ = t_{1} ≈ t′_{1}, …, t_{n} ≈ t′_{n}, E_{0}. Since σ is a solution of E′, σ(t_{i}) ↔_{R}^{∗} σ(t′_{i}) (for i = 1, …, n). Hence σ(f(t_{1}, …, t_{n})) ↔_{R}^{∗} σ(f(t′_{1}, …, t′_{n})) by the congruence property of ↔_{R}^{∗}.

3. The partial binding rule has been applied. Then E = x ≈ f(t_{1}, …, t_{n}), E_{0} and E′ = x ≈ f(x_{1}, …, x_{n}), x_{1} ≈ ϕ(t_{1}), …, x_{n} ≈ ϕ(t_{n}), ϕ(E_{0}) where ϕ = {x ↦ f(x_{1}, …, x_{n})}. Since σ is a solution of E′, we have (a) σ(x) ↔_{R}^{∗} σ(f(x_{1}, …, x_{n}))

(b) σ(x_{i}) ↔_{R}^{∗} σ(ϕ(t_{i})) (for i = 1, …, n)

(c) σ solution of ϕ(E_{0})

By definition of ϕ, (a) and the congruence property of ↔_{R}^{∗},

σ(ϕ(t)) ↔_{R}^{∗} σ(t) for all terms t  (∗)

Hence σ is also a solution of E_{0}. Moreover,

σ(x) ↔_{R}^{∗} σ(f(x_{1}, …, x_{n}))  (by (a))
↔_{R}^{∗} σ(f(ϕ(t_{1}), …, ϕ(t_{n}))) (by (b))
↔_{R}^{∗} σ(f(t_{1}, …, t_{n}))  (by (∗))

Hence σ is a solution of x ≈ f(t_{1}, …, t_{n}).

The following soundness theorem can be proved by a simple induction on the transformation steps using the previous lemma.

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

The completeness proof is more difficult since we have to consider all possible transformation sequences. Therefore 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 additional new variables are generated during the derivation (by lazy narrowing and partial binding transformations). But this is no problem since we are interested in solutions w.r.t. the variables of the initial equation system.

Theorem 3.9 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 quasi-solved 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 [JK86].^{4} Now we define the following ordering on pairs (σ, E): (σ, E) ≻ (σ′, E′) iff

{σ(s), σ(t) | s ≈ t ∈ E is unsolved in E} ≻≻_{mul} {σ′(s′), σ′(t′) | s′ ≈ t′ ∈ E′ is unsolved in E′} (∗)

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

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 quasi-solved, 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 the 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}

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

5The 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. ≻ ≻ [Der87].

We combine σ and θ to a new substitution σ′ = σ ∪ θ (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 the 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.

(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 inductive simplification as we will see in the next section.

Propositions 3.3, 3.5, 3.6 and Theorems 3.8 and 3.9 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 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 Lazy unification with inductive simplification

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 4.1 Consider the rewrite rules

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

and the equation f(g(b)) ≈ d. Then there are the following four different derivations in our lazy narrowing calculus:

\begin{matrix}f(g(b)) ≈ d & ⟹^{lu} & g(b) ≈ a, c ≈ d & ⟹^{lu} & b ≈ a, a ≈ a, c ≈ d & ⟹^{lu} & b ≈ a, c ≈ d \\ f(g(b)) ≈ d & ⟹^{lu} & g(b) ≈ a, c ≈ d & ⟹^{lu} & b ≈ b, b ≈ a, c ≈ d & ⟹^{lu} & b ≈ a, c ≈ d \\ f(g(b)) ≈ d & ⟹^{lu} & g(b) ≈ b, d ≈ d & ⟹^{lu} & b ≈ a, a ≈ b, d ≈ d & ⟹^{lu} & b ≈ a, a ≈ b \\ f(g(b)) ≈ d & ⟹^{lu} & g(b) ≈ b, d ≈ d & ⟹^{lu} & b ≈ b, b ≈ b, d ≈ d & ⟹^{lu}^{∗} & ∅ \end{matrix}

The first three derivations do not end in a quasi-solved form, only the last 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 [Fri85, Han92a] that the inclusion of inductive axioms for normalization may have an essential effect on the search space reduction in normalizing narrowing strategies. Therefore we will also allow inductive axioms for normalization. A rewrite rule l → r is called inductive axiom or 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

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

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 axiom 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.^{6}

In the following we assume that I is a set of inductive consequences of R so that the rewrite relation →_{I} is terminating. We will use rules from R for lazy narrowing and rules from I for normalization. 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 for narrowing.

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

The following lemma shows the soundness of one rewrite step with an inductive axiom:

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

Proof: Let s →_{I} s′ and σ be a solution of s′ ≈ t, i.e., σ(s′) =_{R} σ(t). Obviously, σ(s) →_{I} σ(s′) using the same rewrite rule from I. Hence σ(s) =_{R} σ(s′) since I consists of inductive consequences of R and σ is a ground substitution. By σ(s′) =_{R} σ(t), this implies σ(s) =_{R} σ(t), i.e., σ is a solution of s ≈ t.

Now we can state the soundness of the calculus ⟹^{lui}:

Theorem 4.3 Let E and E′ be equation systems with E⟹^{lui}^{∗}E′ where E′ is in quasi-solved form. Then each solution σ of E′ is a solution of E.

Proof: By Lemma 4.2, we can show the soundness of ⇒_{I} with a simple induction on the sequence of rewrite steps. Combining this result with Lemma 3.7 shows the soundness of one ⟹^{lui} step. Then the theorem follows by another simple induction on the number of ⟹^{lui} steps.

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

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

Proof: Let s ≈ t ∈ E, σ(s) =_{R} σ(t) and s ≈ t ⇒_{I} s′ ≈ t′. Hence s →_{I}^{∗} s′ and t →_{I}^{∗} t′ which implies σ(s) →_{I}^{∗} σ(s′) and σ(t) →_{I}^{∗} σ(t′). Since σ is a ground substitution and I are inductive axioms, σ(s) =_{R} σ(s′) and σ(t) =_{R} σ(t′). Hence σ(s′) =_{R} σ(t′), i.e., σ is a solution of all equations in E′.

6In larger single-sorted term rewriting systems it would be difficult to find inductive axioms. 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 axioms 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.

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

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

Theorem 4.5 Let I be a set of inductive consequences of the ground confluent and terminating term rewriting system R such that →_{R∪I} is terminating. Let E be a solvable equation system with solution σ. Then there exists a derivation E ⟹^{lui}^{∗} 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.9 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 ⟹^{lui} since Lemma 4.4 shows that normalization steps preserve solutions. The only difference concerns the ordering where we use →_{R∪I} instead of →_{R}, i.e., ≻≻ is now defined to be the transitive closure of the relation →_{R∪I} ∪ ≻_{sst}. Clearly, this does not change anything in the proof of Theorem 3.9. Moreover, the relation ⇒_{I} does not increase the complexity w.r.t. this ordering but reduce it if inductive axioms are applied since →_{I} is contained in ≻≻.

Theorems 4.3 and 4.5 show that we can integrate the deterministic normalization into the lazy unification calculus without loosing soundness and completeness. Note that the rules from I 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.6 Consider the rules

\begin{matrix}zero(s(x)) → & zero(x) \\ zero(0) → & 0 \end{matrix}

(these rules are contained in R as well as in I) 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 [GS89, MRM89]):

zero(x) ≈ 0, x ≈ 0

⟹^{lui} x ≈ s(x_{1}), zero(x_{1}) ≈ 0, x ≈ 0  (lazy narrowing with first rule)
⟹^{lui} x ≈ s(x_{1}), x_{1} ≈ s(x_{2}), zero(x_{2}) ≈ 0, x ≈ 0  (lazy narrowing with first rule)
⟹^{lui} x ≈ s(x_{1}), x_{1} ≈ s(x_{2}), x_{2} ≈ s(x_{3}), zero(x_{3}) ≈ 0, x ≈ 0 (lazy narrowing with first rule)
⟹^{lui} ⋯

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

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

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

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

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 SLOG [Fri85], K-LEAF [BGL^{+}87], BABEL [MR92], ALF [Han90]). 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 means that these transformations are applied as long as possible before any transformation ⟹^{lu} is used. Hence they can be integrated into the deterministic normalization process ⇒_{I}. 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 4.5 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 Clash of constructor equations

c(t_{1}, …, t_{n}) ≈ d(t′_{1}, …, t′_{m}), E ⟹^{luc} fail

if c, d ∈ C and c ≠ d or m ≠ n

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

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:

cvar(x) = {x}
cvar(c(t_{1}, …, t_{n})) = ⋃_{i=1}^{n} cvar(t_{i}) if c ∈ C
cvar(f(t_{1}, …, t_{n})) = ∅  if f ∈ D

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} ⋯

It is obvious that an equation of the form x ≈ c(t_{1}, …, t_{n}) with x ∈ cvar(c(t_{1}, …, t_{n})) is unsolvable.

A further optimization can be introduced if all functions are reducible on ground constructor terms, i.e., there exists a term t with f(t_{1}, …, t_{n}) →_{R} t for all f ∈ D and t_{1}, …, t_{n} ∈ T (C, ∅). 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 means that these transformations are 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.

The next example shows the improved computational power of our lazy unification calculus with rewriting.

Example 5.1 Consider the following rewrite rules for the addition and multiplication on natural numbers where C = {0, s} and D = {+, ∗}:

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

If we use this confluent and terminating set of rewrite rules for lazy narrowing (R) as well as for normalization (I) and add the inductive consequence x ∗ 0 → 0 to I, then our lazy unification calculus with rewriting 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 axiom 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})
⇒_{I} 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 axiom. Consequently, an infinite derivation would occur in our basic unification calculus of Section 3.

Note that other lazy unification calculi [GS89, MRM89] or lazy narrowing calculi [Red85, MKLR90] have an infinite search space for this equation. It is also interesting to note that a normalizing innermost narrowing strategy as in [Fri85, Han91] has also an infinite search space even if the same inductive axioms are available. This shows the advantage of combining a lazy strategy with a normalization process including inductive axioms. □

6 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 where inductive consequences can be used. 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. Therefore our calculus is qualified as the operational principle of efficient functional logic languages.

Acknowledgements. The author is grateful to Harald Ganzinger for his pointer to a suitable termination ordering.

References

[BGL^{+}87] P.G. Bosco, E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. A complete semantic characterization of K-LEAF, a logic language with partial functions. In Proc. 4th IEEE Internat. Symposium on Logic Programming, pp. 318–327, San Francisco, 1987.

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

[DG89] 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.

[DJ90] 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.

[DMS90] N. Dershowitz, S. Mitra, and G. Sivakumar. Equation Solving in Conditional AC-Theories. In Proc. of the 2nd International Conference on Algebraic and Logic Programming, pp. 283–297. Springer LNCS 463, 1990.

[Ech88] R. Echahed. On Completeness of Narrowing Strategies. In Proc. CAAP’88, pp. 89–101. Springer LNCS 299, 1988.

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

[Fay79] 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.

[Fri85] 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.

[GR89] 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.

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

[Han90] 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.

[Han91] M. Hanus. Efficient Implementation of Narrowing and Rewriting. In Proc. Int. Workshop on Processing Declarative Knowledge, pp. 344–365. Springer LNAI 567, 1991.

[Han92a] M. Hanus. Improving Control of Logic Programs by Using Functional Logic Languages. In Proc. of the 4th International Symposium on Programming Language Implementation and Logic Programming, pp. 1–23. Springer LNCS 631, 1992.

[Han92b] M. Hanus. Incremental Rewriting in Narrowing Derivations. In Proc. of the 3rd International Conference on Algebraic and Logic Programming, pp. 228–243. Springer LNCS 632, 1992.

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

[Hul80] J.-M. Hullot. Canonical Forms and Unification. In Proc. 5th Conference on Automated Deduction, pp. 318–334. Springer LNCS 87, 1980.

[JK86] 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.

[KB91] S. Krischer and A. Bockmayr. Detecting Redundant Narrowing Derivations by the LSE-SL Reducibility Test. In Proc. RTA’91. Springer LNCS 488, 1991.

[LW91] R. Loogen and S. Winkler. Dynamic Detection of Determinism in Functional Logic Languages. In Proc. of the 3rd Int. Symposium on Programming Language Implementation and Logic Programming, pp. 335–346. Springer LNCS 528, 1991.

[MKLR90] J.J. Moreno-Navarro, H. Kuchen, R. Loogen, and M. Rodríguez-Artalejo. Lazy Narrowing in a Graph Machine. In Proc. Second International Conference on Algebraic and Logic Programming, pp. 298–317. Springer LNCS 463, 1990.

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

[MR92] 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.

[MRM89] 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.

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

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

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

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

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

[Sie90] J.H. Siekmann. An Introduction to Unification Theory. In R.B. Banerji, editor, Formal Techniques in Artificial Intelligence, pp. 369–425. Elsevier Science Publishers, 1990.

[You89] J.-H. You. Enumerating Outer Narrowing Derivations for Constructor-Based Term Rewriting Systems. Journal of Symbolic Computation, Vol. 7, pp. 319–341, 1989.