Proof Transformations For Equational Theories^{∗}

Tobias Nipkow University of Cambridge Computer Laboratory Pembroke Street Cambridge CB2 3QG England

                          tnn@cl.cam.ac.uk

Abstract

This paper contrasts two kinds of proof systems for equational theories: the standard ones obtained by combining the axioms with the laws of equational logic, and alternative systems designed to yield decision procedures for equational problems.

Although new matching algorithms for (among other theories) associativity, associativity + commutativity, and associativity + commutativity + identity are presented, the emphasis is not so much on individual theories but on the general method of proof transformation as a tool for showing the equivalence of different proof systems.

After studying proof translations defined by rewriting systems, equivalence tests based on the notion of resolvant theories are used to derive new matching and in some cases unification procedures for a number of equational theories. Finally the combination of resolvant systems is investigated.

∗This work was supported by the Alvey Diamond project, SERC grants GR/E/02369 and GR/F/10811. At MIT the author was supported in part by NYNEX, NSF grant CCR-8706652, and by the Advanced Research Projects Agency of the DoD, monitored by the ONR under contract N00014-83-K-0125.

1 Introduction

We contrast two kinds of proof systems for a number of equational systems E. On the one hand there is the standard one obtained by combining E with the laws of equational logic. We know that the resulting system defines what we want it to define. However, it gives no indication how the word problem, matching, or unification can be solved in that theory. On the other hand we present proof systems that are not obviously complete for E but which immediately give rise to matching or even unification procedures.

Although new matching algorithms for associativity (A), associativity + commutativity (AC), and associativity + commutativity + identity (AC1) are presented, the emphasis is not so much on individual theories but on the general method of proof transformations as a tool for showing the equivalence of different proof systems. In particular a mechanizable equivalence test and its implementation are discussed. Although the test is not complete, it is powerful enough to deal with many equational systems.

The paper comes in two parts. Section 3 compares standard proof systems for the empty theory, commutativity, left/right-commutativity, A, and AC, with alternative ones. Equivalence is shown by presenting a terminating set of rewrite rules which translate proofs from one system into the other. However, these rewriting systems become more and more complex to construct and to prove terminating. Therefore Section 4 uses the notion of “resolvance” to present a uniform treatment of the theories in Section 3. It is shown that resolvant systems of equations directly yield alternative inference systems which, in certain cases, are terminating matching algorithms. Two powerful criteria for resolvance are developed and their implementation is discussed. This implementation is used to check a number of further equational systems for resolvance, which yields new matching algorithms for some of them. It is also shown that resolvance is a modular property, i.e. putting resolvant sets of equations together which do not have function symbols in common does again yield resolvant systems. Finally we discuss the relationship of our work with some recent results by Claude Kirchner.

The reader should be familiar with the basic notions of equational logic, as defined for example in [6].

2 Equational Theories, Unification, Matching, and Equality

Equational theories are defined by inference rules of the form

\frac{s_{1} = t_{1} … s_{n} = t_{n}}{s = t} .  (1)

A system of such rules inductively defines a predicate =. Furthermore, since all rules are Horn clauses, they constitute a logic program which can be used to solve unification, matching or word problems w.r.t. =. The only problem is termination. Since a set of Horn clauses merely yields a semidecision procedure, it depends on the particular set of rules whether they actually constitute a decision procedure for equality, matching or unification. Thus we can separate the question of correctness (does the given set of rules axiomatize the desired theory?) from that of termination.

Given a set of equations E, the equational theory induced by E is defined by E plus reflexivity, symmetry, transitivity and congruence. This system is denoted by E^{+} and the predicate it defines by =_{E}. Although E^{+} is by definition correct, i.e. defines the equational theory generated by E, it has a major termination problem: due to transitivity, any query (in the logic programming sense) will run forever even after all answer substitutions have been found.

The rest of the paper discusses alternative axiomatizations of various simple equational theories which yield decision procedures for matching and, in some trivial cases, even unification. Initially attention is focussed on correctness. In Section 4 the termination question is addressed and a fairly general answer is given.

Before we become technical, we have to fix some terminology. An arbitrary set of equations E is often called a presentation, in contrast to the equational theory =_{E}, which is closed under equational reasoning. We call an equational theory permutative if all its equivalence classes are finite. A set of equations is permutative if its equational theory is. An equation s = t is called regular if V(s) = V(t), where V returns the set of variables in a term. An equation s = t is called collapse-free if both s and t are proper terms. A presentation is called collapse-free if all its members are.

3 Proof Transformation by Rewriting

In the following we examine different formulations of some well known equational theories. Each alternative axiomatization D_{rk} of E^{+} consists of a collection of rules of the form (1), say D for “decomposition”, together with congruence rules and reflexivity. D_{rk} and E^{+} are shown to be equivalent by translating proofs from one into the other. The translation is expressed by rewrite rules on proof trees.

D and E are always chosen such that each element of D is a derived rule of E^{+} and each equation in E is a derived rule of D_{rk}. Thus the transformation of proofs in D_{rk} into E^{+} is trivial and is briefly described in Section 4. The translation in the opposite direction needs to get rid only of symmetry and transitivity, the two rules that cause termination problems and do not occur in D_{rk}.

3.1 The Empty Theory

We start with the basic laws of equational logic, reflexivity (r), symmetry (s), transitivity (t) and congruence (k) for a single binary function symbol (·). The choice of function symbols is immaterial.

r ≡  \overline{x = x}

s ≡  \frac{x = y}{y = x}

t ≡ \frac{x = y y = z}{x = z}

k ≡ \frac{x = u y = v}{x·y = u·v}

In the sequel this system is called B. B axiomatizes equality in the empty theory. Of course r alone suffices for that. A constructive proof of this fact can be given by a set of transformation rules which eliminate all other rules from a proof in B.

s\frac{r\overline{x = x}}{x = x} ⟶ r\overline{x = x}

t\frac{r\overline{x = x} r\overline{x = x}}{x = x} ⟶ r\overline{x = x}

k \frac{r\overline{x = x} r\overline{y = y}}{x·y = x·y} ⟶ r\overline{x·y = x·y}

These rules are obviously terminating and cover all cases, i.e. reduce any proof in B to reflexivity.

In the sequel E will be some set of equations and D a set of inference rules. We want to show that for given D and E, any proof in E^{+} = E ∪ B can be rewritten to one in D_{rk} = D ∪ {r, k}. This transformation can be done on a rule by rule basis.

Axioms from E can be eliminated in one step because E and D will always be chosen such that all axioms in E are equivalent to some combination of rules in D_{rk}.

To simplify elimination of s and t, we show that B has some further properties:

t\frac{x = y y = z}{s\frac{x = z}{z = x}} ⟶ t\frac{s\frac{y = z}{z = y} s\frac{x = y}{y = x}}{z = x}  (2)

s\frac{k \frac{x = u y = v}{x·y = u·v}}{u·v = x·y} ⟶ k \frac{s\frac{x = u}{u = x} s\frac{y = v}{v = y}}{u·v = x·y}  (3)

t\frac{r\overline{x = x} x = z}{x = z} ⟶ x = z  t \frac{x = z r\overline{z = z}}{x = z} ⟶ x = z  (4)

t\frac{k \frac{u = w v = x}{u·v = w·x} k \frac{w = y x = z}{w·x = y·z}}{u·v = y·z} ⟶ k \frac{t\frac{u = w w = y}{u = y} t\frac{v = x x = z}{v = z}}{u·v = y·z} (5)

Rules (2) and (3) show that symmetry can be pushed through transitivity and congruence. Therefore symmetry can be pushed to the leaves of any proof in B ∪ E, and hence can be eliminated altogether, provided that E is closed under s, i.e. s=t ∈ E implies t=s ∈ E. In the sequel E will always have that property, and elimination of s is automatic. This is the formal justification of the fact that equational proofs don’t need explicit symmetry if all axioms can be used in both directions.

The only remaining task is the elimination of t. Rules (4) and (5) show that it is sufficient to cover the cases t(ρ, k), t(k, ρ), and t(ρ, ρ′) for all rules ρ, ρ′ in D.

Before we look at particular systems D and E, we simplify our notation. Although the above rewrite rules rules are fairly involved already, they are not quite precise in that they don’t say how the subtrees are relocated. The proper formulation of, for example, rule (3) is

s\frac{k \frac{\frac{P}{x = u} \frac{Q}{y = v}}{x·y = u·v}}{u·v = x·y} ⟶ k \frac{s \frac{\frac{P}{x = u}}{u = x} s \frac{\frac{Q}{y = v}}{v = y}}{u·v = x·y}

where P and Q are the proof trees that prove x = u and y = v. However, this rule is more complicated than it needs to be. All that is required is the pattern of proof rules as in

s(k(P, Q)) ⟶ k(s(P), s(Q)).

We now assume that r, s, t, and k are functions on proof trees or skeletons. The actual formulae being proved are determined by these proof skeletons. Under this new interpretation the above rewrite rules translate to

\begin{matrix}s(r) & ⟶ & r \\ t(r, r) & ⟶ & r \\ k(r, r) & ⟶ & r \\ s(t(x, y)) & ⟶ & t(s(y), s(x)) \\ s(k(x, y)) & ⟶ & k(s(x), s(y)) \\ t(r, x) & ⟶ & x \\ t(x, r) & ⟶ & x \\ t(k(x, y), k(u, v)) & ⟶ & k(t(x, u), t(y, v)) \end{matrix} \} T

Notice that x, y, z, … stand for proof skeletons, not terms or formulae. The termination of T can now be shown by a mechanical system like LP [5].

3.2 Commutativity (C)

An alternative axiomatization of commutativity is obtained by adding

c ≡ \frac{x = v y = u}{x·y = u·v}.

to r and k. This system is trivial and well known. For example Claude Kirchner [8] derives c automatically from commutativity. Commutativity is proved from c by composing both premises with reflexivity, i.e. the conclusion of c(r, r) is x·y = y·x. The same device works for all subsequent equational theories.

The following further rewrite rules are needed to translate proofs:

t(c(x, y), c(u, v)) ⟶ k(t(x, v), t(y, u))
t(c(x, y), k(u, v)) ⟶ c(t(x, v), t(y, u))
t(k(x, y), c(u, v)) ⟶ c(t(x, u), t(y, v))

Again, LP manages to show that the union of T with the above rules is a terminating system.

It is interesting to note that both for the empty theory and for commutativity, the system D_{rk} could be derived from B ∪ E automatically using the CEC system [2, 4] which is a general purpose system for the completion of sets of conditional equations. The following equational theories are more complex and automatic tools failed to help.

3.3 Left/Right-Commutativity (C_{l/r})

The first non-trivial example is left/right-commutativity. For simplicity we consider only E = {(x·y)·z = (x·z)·y}, right-commutativity. Left-commutativity is symmetric.

It turns out that if D = {c_{r}}, where

c_{r} ≡ \frac{x = w·v w·y = u}{x·y = u·v},

then D_{rk} axiomatizes C_{r}. The elimination of t is achieved by the following rules:

t(k(x, y), c_{r}(u, v)) ⟶ c_{r}(t(x, u), t(k(r, y), v))  (6)
t(c_{r}(x, y), k(u, v)) ⟶ c_{r}(t(x, k(r, v)), t(y, u))  (7)
t(c_{r}(x, k(y_{1}, y_{2})), c_{r}(u, v)) ⟶ t(c_{r}(x, r), c_{r}(t(k(y_{1}, y_{2}), u), v))  (8)
t(c_{r}(x, c_{r}(y_{1}, y_{2})), c_{r}(u, v)) ⟶ t(c_{r}(x, r), c_{r}(t(c_{r}(y_{1}, y_{2}), u), v))  (9)
t(c_{r}(x, r), c_{r}(r, v)) ⟶ k(t(x, v), r)  (10)
t(c_{r}(x, r), c_{r}(k(u_{1}, u_{2}), v)) ⟶ k(t(x, t(k(u_{1}, r), v)), u_{2})  (11)
t(c_{r}(x, r), c_{r}(c_{r}(u_{1}, u_{2}), v)) ⟶ c_{r}(t(x, c_{r}(u_{1}, r)), t(c_{r}(r, u_{2}), v))  (12)

The first two rules cover the cases that either of t’s subtree is labelled with k. The next two rules translate from t(c_{r}(., .), c_{r}(., .)) to t(c_{r}(., r), c_{r}(x, .), and the last three rules translate the latter pattern, depending on the form of x.

The above set of rules is not easily proved to terminate, and systems like LP fail to do so. The point is that the termination argument is hidden in the equations that are being proved, which are not part of the proof skeletons. To exploit this information, we view t as a function defined on terms over {r, k, c_{r}}. Looking at the form of the transformation rules we can see that their termination, or equivalently totality of t, can be shown by proving that some measure function on the arguments of t decreases when going from left to right. This measure is the size of the equation (or either side of it) that forms the invisible conclusion of the proof tree rooted in t. One way to see that the measure decreases is to decorate the rewrite rules with the equations being proved. For example rule (10) becomes

t\frac{c_{r} \frac{x = u·v r\overline{u·y = u·y}}{x·y = (u·y)·v} c_{r} \frac{r\overline{u·y = u·y} u·v = z}{(u·y)·v = z·y}}{x·y = z·y} ⟶ k \frac{t \frac{_{x = u·v u·v = z}}{x = z} r\overline{y = y}}{x·y = z·y}

On the rhs t proves x = z, which is strictly smaller than x·y = z·y, the conclusion of the tree labelled by t on the lhs.

Alternatively, we notice that the size of the conclusion of k and c_{r} is strictly greater then the size of their hypotheses. Hence in any rule with lhs t(… k(x, y) …) or t(… c_{r}(x, y) …), the measure of x and y is smaller than the measure of the full lhs. Hence x and y are ok as arguments to t on the rhs.

If the termination proof is done in complete detail, one notices that in rules (8) and

(9) the outer occurrence of t on the rhs proves the same formula as the t on the lhs, i.e. the measure is not decreased. However, none of the two rules can be applied twice in a row. Therefore the complexity measure becomes a pair. Its first component is what we had before, which all other rules decrease. The second component indicates the applicability of rule (8) or (9). It is decreased by those two rules, which do not change the first component.

As we have seen, both the transformation rules and their termination proofs become quite complex even for very simple equational theories. For that reason, both are omitted in the following examples. I have carried them out by hand and found them very similar to what we saw in this section, only more tedious. This prompted me to look for automatic methods which are presented in Section 4.

3.4 Associativity (A)

Associativity can be axiomatized with k, r,

a_{1} ≡ \frac{x = u·w w·y = v}{x·y = u·v} and a_{2} ≡ \frac{x·w = u y = w·v}{x·y = u·v} .

A geometric interpretation of this fact can be given where terms are interpreted as strings or lines and · is concatenation. If the two lines x·y and u·v are equal, there are three cases:

[figure: x; y; a_{1} :; u; v; k :; u; v; a_{2} :; u; v]

It can be shown that Plotkin’s associative unification procedure [13] can be derived from the procedure embodied in the inference rules k, r, a_{1} and a_{2} by imposing a particular search strategy.

3.5 Associativity + Commutativity (AC)

For AC let D = {c, a_{1}, a_{2}, ac_{1}, ac_{2}, ac}, where

ac_{1} ≡ \frac{x = v·w w·y = u}{x·y = u·v} ac_{2} ≡ \frac{x·w = v y = w·u}{x·y = u·v}

ac ≡ \frac{x = x_{1}·x_{2} y = y_{1}·y_{2} x_{1}·y_{1} = u x_{2}·y_{2} = v}{x·y = u·v} .

Again there is a geometric interpretation of these rules, this time in terms of areas or multisets. If x·y is of the form

x y

and u·v is the same area, there are 7 ways in which they can cover each other:

k u v  c v u  a_{1} u v  ac_{1} v u  a_{2} u v  ac_{2} v u  ac vu

4 Resolvant Theories

The collection of equational theories presented above and the complexity of some of the completeness proofs raises the question whether there is some principle behind them all which might even be automated. For some of the simpler examples (C, C_{l/r}) this question was first answered by Claude Kirchner [7, 8] using the notion of resolvant presentation.

A set of equational axioms E is resolvant if s =_{E} t implies that there is an equational derivation of this fact which uses at most one application of an equation at the root of a term. Notice that by a derivation s =_{E} t we refer to a list of terms s = s_{0}, …, s_{n} = t such that s_{i+1} can be obtained from s_{i} by replacing a subterm which is an instance of one side of an equation in E by the corresponding instance of the other side. In particular we call the step s_{k} =_{E} s_{k+1} a peak if s_{k} is an instance of one side of an equation in E and s_{k+1} the corresponding instance of the other side. With this terminology we can say that E is resolvant if s =_{E} t implies that there is an equational derivation of this fact with at most one peak. For a formal definition of resolvance we need the following simple predicates:

s = . _{E} t ⇔ ∃f, s_{i}, t_{i}. s = f(s_{1}, …, s_{n}) ∧ t = f(t_{1}, …, t_{n}) ∧ s_{1} =_{E} t_{1} ∧ … ∧ s_{n} =_{E} t_{n}
s ≐_{E} t ⇔ ∃p=q ∈ E, σ. s = σp ∧ t = σq
s ≐ ; .._{E} t ⇔ ∃s′, t′. s = . _{E} s′ ≐_{E} t′ = . _{E} t
s ≐ ; ._{E} t ⇔ s = . _{E} t ∨ s ≐ ; .._{E} t

Notice that in general only ≐_{E} is decidable, provided E is finite. If E is also permutative, all four predicates are in principle decidable, although in practice a complexity theoretic barrier may quickly be reached.

Definition 4.1 E is called resolvant iff s =_{E} t implies s ≐ ; ._{E} t.

An equational theory is called syntactic by Kirchner [8] if it is generated by a finite set of resolvant axioms. In the sequel we tacitly restrict ourselves to collapse-free equational presentations. The theory can be made to work without that restriction but that requires some further case distinctions.

The point is that each equational theory presented above is syntactic but only C and C_{l/r} are resolvant. Although [8] gives some sufficient conditions for syntacticness, they are not met by C_{l/r}, A or AC. The aim of this section is to present a more refined criterion for resolvance, its implementation, and its application to both the examples above and some further theories.

For resolvant presentations there is a simple translation from equational axioms to inference rules: an equation f(s_{1}, …, s_{m}) = g(t_{1}, …, t_{n}) yields

\frac{x_{1} = s_{1} … x_{m} = s_{m} t_{1} = y_{1} … t_{n} = y_{n}}{f(x_{1}, …, x_{m}) = g(y_{1}, …, y_{n})}  (13)

where the x_{i} and y_{j} are new variables. In [8] this translation is called Gen. All the inference rules presented above can be generated this way. However, in many cases this leads to rules with trivial equations of the form x = y among the hypotheses. These can be deleted without loss of generality if x is replaced by y everywhere else.

Starting with C, C_{l/r}, or A we obtain the rules shown in Sections 3.2 to 3.4. For AC we needed three more rules. Those are generated by the equations

P = {(x·y)·z = (x·z)·y, x·(y·z) = y·(x·z), (x·y)·(u·v) = (x·u)·(y·v)}

The reason is that AC by itself is not resolvant but AC^{+} = AC ∪ P is. Note that all elements of P are equational consequences of AC.

In the sequel let D be the set of inference rules obtained from E as above, let K be the set of all congruence rules, and let D_{rk} = D ∪ {r} ∪ K. In particular let k_{f} be the congruence rule for function symbol f.

We can now give a general scheme for translating proofs in D_{rk} to those in E^{+}, the direction that had not been tackled in Section 3. For every rule ρ ∈ D, ρ(r, …, r) is the proof of some equation e ∈ E. If ρ is rule (13), we have the following translation from D_{rk} to E^{+}:

ρ(p_{1}, …, p_{m}, q_{1}, …, q_{n}) ⟶ t(k_{f}(p_{1}, …, p_{m}), t(e, k_{g}(q_{1}, …, q_{n})))  (14)

The importance of resolvant presentations stems from the following theorem.

Theorem 4.2 If E is resolvant, D_{rk} is a sound and complete inference system for =_{E}. Proof Soundness of D_{rk} follows from the fact that each rule in D is a derived rule in E^{+}, as witnessed by (14). The completeness proceeds by induction on the length of equational proofs. Let s =_{E} t and distinguish 3 cases.

If s = t, this has an immediate proof by reflexivity.

If s = . _{E} t, it follows that s = f(s_{1}, …, s_{n}), t = f(t_{1}, …, t_{n}), and s_{i} =_{E} t_{i} for all i. Since the derivation of the latter equations are shorter than the derivation of s =_{E} t, there is a proof skeleton p_{i} in D_{rk} for each of them. Hence there is a proof of s =_{E} t with the skeleton k_{f}(p_{1}, …, p_{n}).

If s ≐ ; .._{E} t, it follows that there is an equation f(s_{1}, …, s_{m}) = g(t_{1}, …, t_{n}) in E and

s = f(r_{1}, …, r_{m}) = . _{E} f(s′_{1}, …, s′_{m}) ≐_{E} g(t′_{1}, …, t′_{n}) = . _{E} g(u_{1}, …, u_{n}) = t

such that s′_{i} and t′_{j} are instances of s_{i} and t_{j} respectively and that s_{i} =_{E} s′_{i} and t′_{j} =_{E} t_{j} for all i and j. Since the derivation of the latter equations are shorter than the derivation of s =_{E} t, there are proof skeletons p_{i} and q_{j} for each of them. Hence the skeleton ρ(p_{1}, …, p_{m}, q_{1}, …, q_{n}), where ρ is the rule (13) derived from f(s_{1}, …, s_{m}) = g(t_{1}, …, t_{n}), proves s =_{E} t. □

In addition, we have:

Theorem 4.3 If E is permutative, the interpretation of D_{rk} as a Prolog program yields a terminating matching algorithm. Proof An equation l = r is called a matching problem if V(l) = {}. Because E is permutative, it must be regular, and hence any solution σ to a matching problem l = r must be such that V(σr) = {}.

Interpreting D_{rk} as a Prolog program means that the order of the goals is important and they are kept as a list (of equations). We use the ML notation for lists, i.e. [e_{1}, …, e_{n}] is a list of length n, and @ denotes list concatenation.

First we establish that the current goal is always a matching problem if it was one initially. Resolution of a rule in D_{rk} with a matching problem l = r will always lead to a list of subgoals of the form

H = H_{l}@H_{r} = [l_{1} = s_{1}, …, l_{m} = s_{m}, t_{1} = r_{1}, …, t_{n} = r_{n}]  (15)

such that each l_{i} = s_{i} is a matching problem, and ⋃_{j=1}^{n} V(t_{j}) ⊆ ⋃_{i=1}^{m} V(s_{i}). The first property follows from the form of the rules, the second one is a consequence of the fact that E is regular. Both properties together imply that during execution the current goal will always be a matching problem: either it was one to start with (l_{i} = s_{i}), or a solution of the goals to the left of it have instantiated all variables on its lhs by ground terms (t_{j} = r_{j}).

To prove termination, we need some more definitions. If S ⊆ IN, max(S) = m if m ∈ S and all elements in S are less or equal m, and max(S) = 0 if there is no such m. The function depth computes the depth of a term, where the depth of variables and constants is 1. The function

maxd_{E}(s) = max{depth(t) | s =_{E} t}

computes the maximal depth of any E-equivalent term. Since E is permutative, maxd_{E}(s) is never 0. The ordering < on IN is extended to multisets over IN in the canonical way [3]. Multiset union is written ⊔. The function C takes two lists of equations and produces a multiset of natural numbers:

C([], L) = {}
C([l = r]@R, L) = {max{maxd_{E}(σl) | σ ⊢_{E} L}} ⊔ C(R, L@[l = r])})

where σ ⊢_{E} L means that σ solves all equations s = t in L, i.e. σs =_{E} σt.

Finally we define the complexity of a list of equational goals G by C(G, []). In words: each goal l = r in G is assigned the maximal depth of l under instantiations resulting from a solution of all goals to the left; the overall complexity is the multiset of all these integers.

Some important facts about C are

1. C(σR, σL) ≤ C(R, L)

2. If σ ⊢_{E} H implies σ ⊢_{E} H′ for all σ, then C(R, H) ≤ C(R, H′).

Each resolution step transforms the list of goals from [l = r]@G to H@G′, where G′ = θG, θ is the unifying substitution, and H is defined in (15) above. Since C(H@G′, []) = C(H_{l}, []) ⊔ C(H_{r}, H_{l}) ⊔ C(G′, H) and C([l = r]@G, []) = C([l = r], []) ⊔ C(G, [l = r]), it suffices to show C(G′, H) ≤ C(G, [l = r]), C(H_{l}, []) < C([l = r], []), and C(H_{r}, H_{l}) < C([l = r], []) in order to prove C(H@G′, []) < C([l = r]@G, []).

C(G′, H) ≤ C(G, [l = r]) follows from the two facts about C above because the rules in D_{rk} guarantee that σ ⊢_{E} H implies σl =_{E} σr.

To show C(H_{l}, []) < C([l = r], []) and C(H_{r}, H_{l}) < C([l = r], []) we notice that C([l = r], []) = maxd_{E}(l) ≠ 0. Looking at the equations in H_{l}, we find that all l_{i} are proper subterms of l and hence that maxd_{E}(σl_{i}) = maxd_{E}(l_{i}) < maxd_{E}(l), which establishes C(H_{l}, []) < C([l = r], []). If H_{r} is nonempty, resolution must have taken place with a rule in D derived from an equation s = t in E. Thus σ ⊢_{E} H_{l} implies l =_{E} σs =_{E} σt. Hence σt_{j} is ground and a proper subterm of σt, and therefore maxd_{E}(σt_{j}) < maxd_{E}(σt) = maxd_{E}(l). This proves C(H_{r}, H_{l}) < C([l = r], []) and concludes the termination proof. □

Theorem 4.3 is important because it is the first time that a subclass of resolvant presentations has been identified which yield terminating matching algorithms. On the other hand, there is a trivial terminating matching algorithm for permutative theories: in trying to match the pattern r to the variable free term s, enumerate the finite set of t’s with s =_{E} t and try to match r and t in the empty theory. The time and space complexity of these algorithms remains to be investigated.

We will now stop to think in terms of inference rules and confine our attention to equations.

4.1 A Generalized Criterion

Given a set of equations E we want to test whether E is resolvant. Our criterion actually shows how to go from an arbitrary derivation s =_{E} t to one with at most one peak. The transformation is an inductive process which combines adjacent peaks.

If we write e, e′ ∈ E in the sequel, we really mean that there are two equations e and e_{1} in E, such that e′ = σe_{1}, where σ is a renaming of the variables in e_{1} away from those in e. We also assume that E is closed under symmetry, i.e. s=t ∈ E, implies t=s ∈ E.

Defining

p=q ⇓_{E} u=v ⇔ ∀σ. σq = . _{E} σu ⇒ σp ≐ ; ._{E} σv

we get

Lemma 4.4 E is resolvant iff p=q ⇓_{E} u=v holds for all equations p=q, u=v ∈ E where q = f(…) and u = f(…). Proof We concentrate on the “if”-part as the “only if”-part is trivial. For E to be resolvant, s =_{E} t must imply s ≐ ; ._{E} t. We show that under the given assumptions any derivation s =_{E} t can be reduced to s ≐ ; ._{E} t. The reduction merges adjacent peaks. This means we translate a derivation s_{0} ≐_{E} s_{1} = . _{E} s_{2} ≐_{E} s_{3} into one of the form s_{0} ≐ ; ._{E} s_{3}. By induction the number of peaks in any derivation can always be reduced to 0 or 1.

A derivation s_{0} ≐_{E} s_{1} = . _{E} s_{2} ≐_{E} s_{3} must be of the form σp ≐_{E} σq = . _{E} σu ≐_{E} σv for some p=q, u=v ∈ E with q = f(…) and u = f(…). By assumption this implies σp ≐ ; ._{E} σv, which is the required reduction. □

We will now concentrate on ways of turning the resolvance criterion embodied in this lemma into a finite test.

In the sequel let s̄ denote the instantiation of every variable in s by a unique free constants. Thus s̄ is equivalent to τs, where τ is a fixed injective substitution from variables to free constants. Therefore any first-order formula P̄ holds iff σP holds for all σ.

Lemma 4.5 Let p=q, u=v ∈ E such that q = f(q_{1}, …, q_{n}), and u = f(u_{1}, …, u_{n}), and

let E′ = E ∪ \{\overline{q_{1}} = \overline{u_{1}}, …, \overline{q_{n}} = \overline{u_{n}}\}. Then p̄ ≐ ; ._{E′} v̄ implies p=q ⇓_{E} u=v.

Proof In the following we make use of the fact that if A ⊢ P ⇒ Q then A ⊢ P implies A ⊢ Q.

p̄ ≐ ; ._{E′} v̄
⇔ E ∪ \{\overline{q_{1}} = \overline{u_{1}}, …, \overline{q_{n}} = \overline{u_{n}}\} ⊢ p̄ ≐ ; . v̄
⇔ E ⊢ \overline{q_{1}} = \overline{u_{1}} ∧ … ∧ \overline{q_{n}} = \overline{u_{n}} ⇒ p̄ ≐ ; . v̄
⇔ E ⊢ q̄ = ū ⇒ p̄ ≐ ; . v̄
⇒ q̄ =_{E} ū ⇒ p̄ ≐ ; ._{E} v̄
⇔ ∀σ. σq =_{E} σu ⇒ σp ≐ ; ._{E} σv
⇔ p=q ⇓_{E} u=v
□

Example 4.6 In the presence of commutativity in E, we need to test x·y=y·x ⇓_{E} u·v=v·u. By Lemma 4.5 it suffices to show x̄·ȳ ≐ ; ._{E′} v̄·ū where E′ = E ∪ {ȳ = ū, x̄ = v̄}: x̄·ȳ = . _{E′} v̄·ū.

If E contains x·y = y·x, (x·y)·z = x·(y·z), and (x·y)·z = (x·z)·y we need to show

(x·y)·z=x·(y·z) ⇓_{E} u·v=v·u and hence (x̄·ȳ)·z̄ ≐ ; ._{E′} v̄·ū where E′ = E ∪ {x̄ = ū, ȳ·z̄ = v̄}:

(x̄·ȳ)·z̄ = . _{E′} (ȳ·x̄)·z̄ ≐_{E′} (ȳ·z̄)·x̄ = . _{E′} v̄·ū

However, Lemma 4.5 is not necessary for resolvance:

Example 4.7 Right-commutativity is resolvant and (x·y)·z=(x·z)·y ⇓_{C_{r}} (u·v)·w=(u·w)·v holds although Lemma 4.5 is not applicable: (x̄·ȳ)·z̄ ≐ ; ._{E′} (ū·w̄)·v̄, where E′ = C_{r} ∪{x̄·z̄ = ū·v̄, ȳ = w̄}, does not hold.

The problem stems from the fact that in E′ we only assume that \overline{q_{i}} = \overline{r_{i}}, without any further distinctions. We have to take into account what the derivation of q_{i} =_{E} r_{i} looks like. For right-commutativity it is sufficient to take a closer look at x·z =_{E} u·v. We can assume that this derivation has at most one peak.

If x·z = . _{E} u·v, we have E′_{1} = E′ ∪ {x̄ = ū, z̄ = v̄} and therefore (x̄·ȳ)·z̄ = . _{E′_{1}} (ū·w̄)·v̄. Otherwise there are terms r,s,t such that x·z = . _{E} (r·s)·t ≐_{E} (r·t)·s = . _{E} u·v, which gives

rise to E′_{2} = E′ ∪ {x̄ = r̄·s̄, z̄ = t̄, r̄·t̄ = ū, s̄ = v̄}. Therefore (x̄·ȳ)·z̄ = . _{E′_{2}} ((r̄·w̄)·s̄)·t̄ ≐_{E′_{2}} ((r̄·w̄)·t̄)·s̄ = . _{E′_{2}} (ū·w̄)·v̄.

Thus we have shown that (x̄·ȳ)·z̄ ≐ ; ._{E′_{i}} (ū·w̄)·v̄ holds for i = 1, 2.

The case distinction of the previous example can be formalized as follows:

C_{E}(f(s_{1}, …)=f(t_{1}, …)) = {{s_{1} = t_{1}, …}} ∪

{{s_{1} = u_{1}, …, v_{1} = t_{1}, …} | f(u_{1}, …)=f(v_{1}, …) ∈ E}

C_{E}(f(s_{1}, …)=g(t_{1}, …)) = {{s_{1} = u_{1}, …, v_{1} = t_{1}, …} | f(u_{1}, …)=g(v_{1}, …) ∈ E}
C_{E}(x=y) = {{x = y}}

The three clauses that define C_{E} are ordered in the sense of ML or Prolog. For example the last one, which is the default case, applies only if the first two do not. The next two facts show that the definition of C_{E}(s = t) returns exactly those equalities between subterms that can arise if s′ ≐ ; ._{E} t′ for some instances s′ and t′ of s and t respectively.

C ∈ C_{E}(s = t) ⇒ s̄ ≐ ; ._{E∪C̄} t̄  (16)
σs ≐ ; ._{E} σt ⇒ ∃C ∈ C_{E}(s = t).∀p=q ∈ C. σp =_{E} σq  (17)

With these facts we can prove the following lemma which formalizes the procedure outlined in Example 4.7.

Lemma 4.8 If p̄ ≐ ; ._{E∪C̄} v̄ holds for all p=q, u=v ∈ E such that q = f(q_{1}, …, q_{n}) and u = f(u_{1}, …, u_{n}), and all C ∈ M = {E_{1} ∪ … ∪ E_{n} | E_{i} ∈ C_{E}(q_{i}=u_{i})}, then p=q ⇓_{E} u=v holds for all p=q, u=v ∈ E, i.e. E is resolvant. Proof The proof is similar to the one of Lemma 4.4 in that it proceeds by reducing peaks. However, we are more specific about the order in which adjacent peaks are removed from a derivation and its subderivations: we reduced a derivation σp ≐_{E} σq = . _{E} σu ≐_{E} σv, where p=q, u=v ∈ E, q = f(q_{1}, …, q_{n}) and u = f(u_{1}, …, u_{n}), only if all subderivations σq_{i} =_{E} σu_{i} are normalized, i.e. of the form σq_{i} ≐ ; ._{E} σu_{i}. In that case we know from (17) that there is a C_{i} ∈ C_{E}(q_{i} = u_{i}) such that σs =_{E} σt holds for all s=t ∈ C_{i}. Letting C = C_{1} ∪ … ∪ C_{n} ∈ M we obtain

p̄ ≐ ; ._{E∪C̄} v̄ ⇔ E ⊢ (∀i, s=t ∈ C_{i}. s̄ = t̄) ⇒ p̄ ≐ ; . v̄
⇒ (∀i, s=t ∈ C_{i}. s̄ =_{E} t̄) ⇒ p̄ ≐ ; ._{E} v̄
⇒ (∀i, s=t ∈ C_{i}. σs =_{E} σt) ⇒ σp ≐ ; ._{E} σv
⇔ σp ≐ ; ._{E} σv

the required reduction. □

This concludes the exposition of the theoretical basis for our resolvance checker.

4.2 Automating It

The procedures suggested by Lemmas 4.5 and 4.8 lead to a fairly large number of cases that have to be examined. The principal problem with automating this procedure is the undecidability of the concepts involved, i.e. the predicates = . _{E} etc. As remarked above, these predicates, and hence Lemmas 4.5 and 4.8, become decidable for permutative E. However, in practice it turns out that the resulting search space is far too large for a naive enumeration procedure.

A prototype system for automating these tests has been implemented in Prolog. To overcome the problems just mentioned, a number of heuristics for testing ≐ ; ._{E} were implemented. If these turn out to be insufficient (as they have for a number of presentations) the predicate ≐ ; ._{E} can be implemented separately for each E.

4.3 More Theories

Using the implementation described in the previous section, the following list of presentations was shown to be resolvant:

AC1^{+} = {(x·y)·(u·v) = (x·u)·(y·v), 1·x = x, x·1 = x}

D = {x·(y + z) = x·y + x·z}
I = {x·x = x}
CI = C ∪ I
DC = D ∪ {x + y = y + x}
DC_{r} = D ∪ {(x + y) + z = (x + z) + y}
DA = D ∪ {(x + y) + z = x + (y + z)}
C_{S} = {(x·x)·y = y·(x·x)}
C_{P} = {(x·y)·z = z·(x·y)}

I and CI yield terminating unification algorithms, the rest only terminating matching algorithms. For D this has already been exploited by Mzali [11].

We also conjecture that ACI^{+} = AC^{+} ∪ I and ACI1^{+} = AC1^{+} ∪ I are resolvant presentations. However, the methods of this paper seem inadequate to prove it.

4.4 Combining Resolvant Theories

In this section we investigate the combination of resolvant presentations. We are given a collection of equational presentations E_{i}, i ∈ I, over pairwise disjoint signatures Σ_{i}. Let E = ⋃_{i∈I} E_{i} and Σ = ⋃_{i∈I} Σ_{i}. Adapting the terminology of [10] we call a property P of equational presentations modular if E has property P iff all E_{i} have property P.

As an immediate consequence of Lemma 4.4 we obtain that

Lemma 4.9 Resolvance is modular. Proof Assume that all E_{i} are resolvant. Given two equations p=q, u=v ∈ E such that q = f(…) and u = f(…), disjointness of the Σ_{i} implies that both equations must come from the same E_{k}. Hence p=q ⇓_{E_{k}} u=v and thus p=q ⇓_{E} u=v must hold, which implies resolvance of E.

Now assume that E is resolvant and let s, t be two terms over Σ_{k} with s =_{E_{k}} t and thus in particular s =_{E} t. Resolvance of E implies s ≐ ; ._{E} t. Using disjointness of the signatures and Fact 1 in [12] s ≐ ; ._{E_{k}} t follows. Thus E_{k} is resolvant. □

This lemma does for the combination of resolvant presentations what [15, 14, 12] do for the combination of arbitrary unification or matching algorithms. The simplicity of its proof is partly due to the fact that it says nothing about termination: even if each E_{i} yields a terminating unification or matching algorithm, E might not. For permutative theories however we are able to show that termination carries over. The reason is that

Lemma 4.10 Permutativity is modular. Proof This proof relies heavily on notions defined in [12] which appear in quotation marks.

Assume that all E_{i} are permutative. The proof is by induction on the “theory height” of terms over Σ, i.e. the maximum number of alternations of signature along some path in a mixed term considered as a DAG. Any term s over Σ can be written as C[s_{1}, …, s_{m}], where C is a proper “context” over some Σ_{k} and the s_{i} are the “immediate alien subterms”. By induction hypothesis each s_{i} has a finite E-equivalence class. Since E is both regular and collapse-free, Fact 2 in [12] shows that any term t with s =_{E} t is of the form D[t_{1}, …, t_{n}] such that each t_{j} is E-equivalent to some s_{i} (and vice versa), and C[[s_{1}]_{=_{E}}, …] =_{E_{k}} D[[t_{1}]_{=_{E}}, …]. Thus there are only finitely many different t_{j} and D, and therefore only a finite number of t with s =_{E} t, i.e. E is also permutative.

The reverse implication is trivial. □

Thus we can safely combine permutative resolvant presentations to obtain a matching algorithm for the joint theory.

5 Related Work

As was mentioned earlier on, this paper is strongly related to the work of Claude Kirchner, who coined the term “resolvant” [8]. He also suggested some criteria for checking resolvance and a completion procedure which turns a non-resolvant theory into a resolvant one. However, for most equational theories discussed above his criteria are too weak to determine that they are resolvant. This prompted the development of the improved tests in this paper. Recently, Claude Kirchner and Francis Klay have given a nice and simple characterization of resolvant theories:

Theorem 5.1 (Kirchner, Klay [9]) If E is a collapse-free set of equations over the signature Σ, the set

{σf(x_{1}, …) = σg(y_{1}, …) | f, g ∈ Σ, σ ∈ cU_{E}(f(x_{1}, …) = g(y_{1}, …))}

is a resolvant set of axioms which generates the same equational theory as E. (The x_{i} and y_{j} are all distinct and cU_{E} denotes a complete set of E-unifiers).

Thus any equational theory with a finitary unification problem has a finite resolvant presentation. This presentation can be computed by means of a unification algorithm for the theory.

Although this theorem yields very short proofs for the resolvance of the theories in Sections 3.1 to 3.5, it is not easy to apply to some of the theories in Section 4.3. For example D has a fairly involved unification algorithm (see [1]), and the author is not aware of a published unification algorithm for DC or DA. The problem is that a notion that was conceived to explain and automate the generation of unification algorithms, namely resolvance, is itself reduced to unification.

If a complete unification algorithm for some theory E is not known, it may still be possible to compute a resolvant presentation by combining Theorem 5.1 with the results of this paper: instead of computing a complete set of unifiers, enumerate all unifiers one by one and keep on testing whether the resulting presentation is yet resolvant. Of course this procedure may still not succeed because we can reach a resolvant presentation without realizing it, due to the incompleteness of the test we described.

Acknowledgements

Part of this research was carried out at the Laboratory for Computer Science at MIT. I would like to express my gratitude to both John Guttag and Larry Paulson for giving me the freedom to pursue this line of research. Larry Paulson and David Wolfram helped to improve the presentation.

References

[1] S. Arnborg, E. Tidén: Unification Problems with One-Sided Distributivity, Proc. 1st Conf. Rewriting Techniques and Applications, LNCS 202 (1985), 398-406.

[2] H. Bertling, H. Ganzinger, R. Schäfer: CEC: A System for Conditional Equational Completion, PROSPECTRA-Report M.1.3-R-7.0, Universität Dortmund (1988).

[3] N. Dershowitz, Z. Manna: Proving Termination with Multiset Orderings, CACM 22 (1979), 465-476.

[4] H. Ganzinger, Private system demonstration, June 1989.

[5] S.J. Garland, J.V. Guttag: An Overview of LP, The Larch Prover, in: Proc. 3rd Intl. Conf. Rewriting Techniques and Applications, LNCS 355 (1989), 137-151.

[6] G. Huet, D.C. Oppen: Equations and Rewrite Rules - A Survey, in: Formal Languages: Perspectives and Open Problems, R. Book (ed.), Academic Press (1982).

[7] C. Kirchner: Méthodes et outils de conception systématique d’algorithmes d’unification dans les théories équationnelles, Thèse d’état de l’Université de Nancy I (1985).

[8] C. Kirchner: Computing Unification Algorithms, Proc. Symp. on Logic in Computer Science (1986), Cambridge, MA, 206-216.

[9] C. Kirchner, F. Klay: A Note on Syntacticness, Presentation at the 3rd Intl. Workshop on Unification, Lambrecht, FRG, June 1989.

[10] A. Middeldorp: Modular Aspect of Properties of Term Rewriting Systems Related to Normal Forms, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications, LNCS 355 (1989), 263-277.

[11] J. Mzali: Matching with Distributivity, Proc. 8th Intl. Conf. on Automated Deduction, LNCS 230 (1986), 496-505.

[12] T. Nipkow: Combining Matching Algorithms: The Regular Case, Proc. 3rd Intl. Conf. Rewriting Techniques and Applications, LNCS 355 (1989), 343-358.

[13] G.D. Plotkin: Building-in Equational Theories, in: Machine Intelligence, Vol. 7, Halsted Press (1972), 73-90.

[14] E. Tidén: Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols, in: Proc. CADE-8, LNCS 230 (1986), 431-449.

[15] K. Yelick: Unification in Combinations of Collapse-Free Regular Theories, JSC 3 (1987), 153-181.