A General Theorem on Termination of Rewriting

Jeremy E. Dawson and Rajeev Goré

Logic and Computation Program, NICTA ^{⋆} and Automated Reasoning Group Australian National University, Canberra, ACT 0200, Australia

                  http://users.rsise.anu.edu.au/^{∼}jeremy/
                   http://users.rsise.anu.edu.au/^{∼}rpg/

Abstract. We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which can be handled by ours. Finally, we show that our method can also prove the termination of the Knuth-Bendix ordering and of dependency pairs. Keywords: rewriting, termination, well-founded ordering, recursive path ordering

1 Introduction

The traditional method for proving the termination of a rewriting systems uses well-founded orderings [7]. The traditional method for proving strong-normalisation of λ-calculi is to use structural induction on lambda terms and their types, backed by auxiliary well-founded inductions. Recently, structural induction on derivations have been used to prove cut-elimination [12] and to prove strongnormalisation of the generalised sequent framework of display calculi [3].

We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We then show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which can be handled by ours. Finally, we show that our method can also prove the termination of the Knuth-Bendix ordering and of dependency pairs.

The results in this paper have been machine-checked using the logical frame-

work Isabelle, see http://web.rsise.anu.edu.au/^{∼}jeremy/isabelle/snabs/

⋆ National ICT Australia is funded by the Australian Government’s Department of Communications, Information Technology and the Arts and the Australian Research Council through Backing Australia’s Ability and the ICT Centre of Excellence program

Related Work: Important methods for proving termination of rewrite systems often use simplification orderings. These include the recursive path orderings ([7], [11]) and the Knuth-Bendix ordering. In §3.7 and §3.8 we use our theorem to prove the well-foundedness of these orderings.

These orderings have been generalised by Ferreira & Zantema [9], Dershowitz & Hoot [6] and Borralleras, Ferreira & Rubio [2]. Their theorems, like ours, are not limited to simplification orderings, but they prove the well-foundedness of larger relations which satisfy the subterm property, so if they were closed under context (rewrite relations), they would also be simplification orderings. Jean Goubault-Larrecq [10] has proved results which are more general in that they replace the notion of subterm with an arbitrary well-founded relation. He also generalises methods for dealing with the λ-calculus, where the notion of substitution creates difficulties for techniques such as ours.

Arts & Giesl [1] describe a method of proving termination using “dependency pairs”. They give key theorems and extensive development of resulting techniques. Their method does not require a simplification ordering or the subterm property. In §3.9 we use our theorem to prove one of their key theorems.

1.1 Notation and Terminology

Assume that we have fixed some syntax for defining “terms” like r, s and t. We deliberately leave this notion vague for now.

For an irreflexive binary relation ρ on terms, we will write (r, t) ∈ ρ, (r, t) ∈ <_{ρ}, r <_{ρ} t or t >_{ρ} r interchangeably. Relations will be assumed irreflexive unless the contrary is stated, but are not assumed transitive even when written <_{ρ}. We say r is strongly normalising, or is ∈ SN, (with respect to ρ) if there is no infinite descending sequence r = r_{0} >_{ρ} r_{1} >_{ρ} r_{2} >_{ρ} … of terms, and ρ is well-founded (or Noetherian) if every r ∈ SN. We write ≤_{ρ}, <_{ρ}^{+} and <_{ρ}^{∗} for the reflexive closure, the transitive closure and the reflexive transitive closure, respectively, of <_{ρ}. We write σ ∘ ρ for the relational composition of relations σ and ρ, in the sense that (r, s) ∈ σ ∘ ρ if there exists t such that (r, t) ∈ ρ and (t, s) ∈ σ.

Often (see our examples) such a relation is described by giving a finite set of “rewrite rules” l_{i} → r_{i}, where l_{i} and r_{i} are terms containing (meta-)variables for which terms may be substituted.

When a relation is defined by a set of rewrite rules, it is also usually taken that it is closed under context, ie, that where C[ ] is a context (a term with a “hole”), and l rewrites to r, then C[l] rewrites to C[r]. Often such a relation is called a reduction, such as the “β-reduction” of the lambda calculus.

The setting of our main theorem is that we are given a binary relation ρ which may or may not consist of the substitution instances of a finite set of rewrite rules, and which is not necessarily closed under context. Then we define ctxt ρ to be the closure under context of ρ and prove that ctxt ρ is well-founded. When ρ consists of the substitution instances of a finite set of rewrite rules the well-foundedness of ctxt ρ proves that the associated rewrite system terminates.

To formalise “closure under context”, we must specify a language of terms. This is a first-order language, with a fixed set of function symbols, or term constructors, of fixed or variable (finite) arity, whose arguments and results are terms. This language may or may not contain term variables. The meta-language used to express rewrite rules and to discuss rewrites does contain term variables.

Given a term like t = f(a, b, g(c, d)), its immediate subterms are a, b and g(c, d), its proper subterms are these and c and d, and its subterms are these and also t itself. We write \overline{s} for a sequence of terms s_{1}, …, s_{m}, such that these are the immediate subterms of f(\overline{s}). We define the “closure of ρ under context”, ctxt ρ: for example, if (c′, c) ∈ ρ, then (f(a, g(c′)), f(a, g(c))) ∈ ctxt ρ.

Definition 1 (closure under context). Given an irreflexive relation ρ and terms t_{0} and t_{1}, the pair (t_{1}, t_{0}) ∈ ctxt ρ (say “t_{0} reduces to t_{1}”) if either (a) (t_{1}, t_{0}) ∈ ρ, or (b) t_{0} and t_{1} are identical except that exactly one immediate subterm of t_{0} reduces to the corresponding immediate subterm of t_{1}.

We also define, inductively, the set SN of strongly normalising terms. This definition is equivalent, at least in classical logic, to that given in §1.1.

Definition 2 (strongly normalising). The set SN of strongly normalising terms is the smallest set of terms such that if every term t_{1} to which t_{0} reduces is in SN then t_{0} ∈ SN. It follows that if t_{0} cannot be reduced then t_{0} ∈ SN.

It is to be understood that concepts such as “strongly normalising”, “reduction”, etc, relate to ctxt ρ, which is, itself, closed under context. It follows therefore that if t ∈ SN then all subterms of t are in SN.

2 A Proof of Termination

We now re-express our theorem about strong-normalisation for display calculi from [3] to make it applicable to term rewriting.

2.1 Various Well-Founded Orderings

To prove that ctxt ρ is well-founded, we use a binary relation <_{dt} on terms, and show that it is well-founded. The relation <_{dt} depends on a relation <_{cut}, which we have the freedom to define. The relation <_{cut} must be well-founded, and invariably it is a superset of ρ. It will normally, but not necessarily, depend on the parts of the terms at or near its head (ie the roots of the corresponding abstract syntax trees).

Definition 3 ( <_{sn1}, <_{sn2}, <_{dt}). Given ρ and <_{cut} we define three further binary relations on terms, <_{sn1}, <_{sn2} and <_{dt}:

(a) t_{1} <_{sn1} t_{0} if t_{0} and t_{1} are the same except that one of the immediate subterms of t_{0} is in SN and reduces to the corresponding immediate subterm of t_{1}.

(b) t_{1} <_{sn2} t_{0} if t_{0} and t_{1} are the same except that a proper subterm of t_{0} is in SN and reduces to the corresponding proper subterm of t_{1}.

(c) t_{1} <_{dt} t_{0} iff either t_{1} <_{cut} t_{0} or t_{1} <_{sn1} t_{0}.

Note that t_{1} <_{sn1} t_{0} implies t_{1} <_{sn2} t_{0}, and our main theorem uses only <_{sn1}. However <_{sn2} is sometimes easier to work with because it is closed under context. We also define an auxiliary function fwf for “from well-founded” which maps a binary relation ρ to a binary relation fwf ρ as below: Definition 4. Given a relation ρ, the pair (r, t) ∈ fwf ρ if and only if (r, t) ∈ ρ and t is strongly normalising (for ρ).

Clearly fwf ρ is well-founded, regardless of whether ρ is. We then prove

Theorem 1. The relations <_{sn1} and <_{sn2} are each well-founded [3].

Despite the notation, these relations need not be transitive. Intuitively, t_{1} <_{dt} t_{0} means that t_{1} is closer to being “normalised” (in some sense) than is t_{0}.

Recall that we require <_{cut} to be well-founded. We also need <_{dt} to be well-founded. Given that <_{cut} and <_{sn1} are well-founded, to prove that <_{dt} is well-founded, we need one of a number of sufficient conditions on the interaction between <_{cut} and <_{sn1}.

Lemma 1. Assume that τ and σ are well-founded relations. Then each of the following conditions is sufficient for τ ∪ σ to be well-founded:

(a) τ ∘ σ ⊆ σ^{∗} ∘ τ,

(b) τ ∘ σ ⊆ σ ∘ τ^{∗},

(c) τ ∘ σ ⊆ τ ∪ σ,

(d) τ ∘ σ ⊆ (σ ∘ (τ ∪ σ)^{∗}) ∪ τ.

Of these, the last is from Doornbos & von Karger [8], and is implied by each of the others, which are in earlier results discussed and cited in [8].

Clearly <_{sn1}⊆<_{sn2}, so to prove that <_{dt} is well-founded it is enough to prove that <_{cut} ∪ <_{sn2} is well-founded. Sometimes it is easier to prove one of the above conditions for <_{sn2} than for <_{sn1}.

2.2 Strong Normalisation Induced from Immediate Subterms

We next define the set ISN, for “inductively strongly normalising”, as the set of terms that are in SN if their immediate subterms are in SN. Clearly, SN ⊆ ISN.

Definition 5 (ISN ). A term t ∈ ISN iff: if all the immediate subterms of t are in SN then t ∈ SN.

The next lemma follows from this definition. We use only the ⟸ part.

Lemma 2. A term t ∈ SN iff every subterm of t is in ISN.

Proof. ⟹: Assume t ∈ SN and let u be a subterm of t, where t = C[u]. Consider any infinite sequence u = u_{0}, u_{1}, … of reductions starting with u. Since the reduction relation is closed under context, t = C[u_{0}], C[u_{1}], … is also an infinite sequence of reductions, contradicting t ∈ SN. Therefore u ∈ SN and so u ∈ ISN.

⟸: By induction on the structure of term t — assume that the result holds for each immediate subterm t′ of t. Assume that every subterm of t, including t itself, is in ISN. Therefore each immediate subterm t′ of t has the property that every subterm of t′ is in ISN, and so, by the inductive hypothesis, t′ ∈ SN. As each t′ ∈ SN, and t ∈ ISN, so t ∈ SN. ⊓ ⊔ 2.3 Properties we require of ρ

Finally, given a rewrite system, our result requires that the relation ρ satisfy certain properties. The most general version of these is

Condition 1 For all (r, l) ∈ ρ, if all proper subterms of l are in SN then, for all subterms r′ of r, either

(a) r′ ∈ SN or

(b) r′ <_{dt}^{+} l.

In practice we use a simpler condition which implies Condition 1, such as

Condition 2 For all (r, l) ∈ ρ, for all subterms r′ of r, either

(a) r′ is a proper subterm of l or is a subterm of a reduction of a proper subterm of l

(b) r′ <_{cut} l

(c) r′ is obtained from l by reduction of l at a proper subterm.

For if we assume that all proper subterms of l are in SN as required in the precondition of Condition 1, then Condition 2(a) implies that r′ ∈ SN, and 2(c) implies that r′ <_{sn1} l, which implies that r′ <_{dt}^{+} l.

Note that sometimes, as in Example 3.3, we enlarge the relation ρ to satisfy Conditions 1 and 2.

2.4 Strong-Normalisation

Lemma 3. Suppose ρ satisfies Condition 1, and let t_{0} be any term. If all terms t′ <_{dt}^{+} t_{0} are in ISN, then t_{0} ∈ ISN.

Proof. Given t_{0}, assume that ρ satisfies Condition 1 and that

(a): all terms t′ such that t′ <_{dt}^{+} t_{0} are in ISN. We need to show t_{0} ∈ ISN, so we assume that

(b): all immediate subterms of t_{0} are in SN, and we show that t_{0} ∈ SN.

To show that t_{0} ∈ SN, we show that every term t_{1} that can be obtained from t_{0} by a single reduction is in SN. We consider the two possible cases: whether the reduction occurs in a proper subterm of t_{0}, or is a reduction of t_{0} as a whole.

Firstly, consider a reduction in a proper subterm of t_{0}: that is, (t_{1}, t_{0}) ∈ ctxt ρ \ ρ. Then the reduction is in an immediate (strongly normalising) subterm of t_{0}. So t_{1} <_{sn1} t_{0} and hence t_{1} <_{dt} t_{0} by Definition 3(c). Therefore t_{1} ∈ ISN by assumption (a). Now each immediate subterm of t_{1} is equal to, or is a reduction of, an immediate subterm of t_{0}, which itself is in SN by assumption (b). All immediate subterms of t_{1} are therefore in SN. Therefore, as t_{1} ∈ ISN, t_{1} ∈ SN.

Secondly, consider a reduction of the whole term t_{0}: that is, (t_{1}, t_{0}) ∈ ρ. Thus we get the new term t_{1} whose subterms are either in SN because of Condition 1(a) or are subterms which are <_{dt}^{+}-smaller than t_{0}, by Condition 1(b). That is, every subterm t_{1}^{s} of t_{1} (including t_{1} itself) satisfies one of the following:

(c): t_{1}^{s} ∈ SN (d): t_{1}^{s} <_{dt}^{+} t_{0}

Then t_{1}^{s} ∈ ISN, in case (c) because SN ⊆ ISN, and in case (d) by assumption (a). Since t_{1}^{s} is an arbitrary subterm of t_{1}, Lemma 2 implies that t_{1} ∈ SN.

In either case t_{1} ∈ SN. Since t_{1} was obtained via an arbitrary reduction from t_{0}, it follows that t_{0} ∈ SN. Thus we have t_{0} ∈ ISN. ⊓ ⊔

Theorem 2. If ρ satisfies Condition 1 and <_{dt} is well-founded, then every term is strongly normalising.

Proof. As <_{dt} and hence <_{dt}^{+} are well-founded, it follows from Lemma 3 by wellfounded induction that every term is in ISN ; now use Lemma 2. ⊓ ⊔

We now have a way of proving termination of a suitable rewrite system. Given the relation ρ, normally the rewrite rules and their substitutional instances, we define a well-founded relation <_{cut} such that, when <_{sn1} and <_{dt} are defined as in Definition 3, the resulting <_{dt} is well-founded and Condition 1 is satisfied. This is enough to show the well-foundedness of ctxt ρ. In the following section we show some examples using this procedure.

3 Examples using the theorem

As explained above, the crux is to find an appropriate definition of <_{cut}.

3.1 Multiset order

Given an irreflexive relation ρ on a set E, we can define the multiset order derived from ρ on multisets of elements of E. We use A, B and C for finite multisets of elements of E, by which we mean both that they contain only finitely many distinct elements and that they contain only finitely many copies of each such element. We use A⊔B to stand for the multiset union. We consider the irreflexive relation <_{m1} defined on finite multisets:

≤_{m1}: ∀C, ∀b ∈ E. if, for all c ∈ C, c <_{ρ} b, then C ⊔ A <_{m1} {b} ⊔ A

If ρ is a strict order (an irreflexive, transitive relation), then <_{m1}^{+} is equal to the multiset order derived from ρ.

We represent a multiset as a tree, with two sorts of node, “inner” nodes (I) and “leaf” nodes (L). Viewing such a tree as a term, the function symbols are I and, for each e ∈ E, L(e), where I has arbitrary arity and each L(e) is nullary. The “leaf multiset” of a tree is the multiset of its leaf nodes, but with each L(e) changed to e. Note that different trees can have the same leaf multiset.

We define a rewrite relation on such trees (terms) as follows. For every (finite) multiset C = [c_{1}, c_{2}, …, c_{k}] and every element b ∈ E such that for all c_{i} ∈ C, c_{i} <_{ρ} b (as in the definition of <_{m1}) we have a rule

L(b) ⟶ I(L(c_{1}), L(c_{2}), …, L(c_{k}))

Theorem 3. Given a well-founded order ρ, the derived multiset order (on finite multisets) is well-founded.

Proof. Clearly, whenever A <_{m1} B, any tree whose leaf multiset is B can be reduced to a tree whose leaf multiset is A using the rewrite relation defined above. Since for a given finite multiset B there always is a tree whose corresponding multiset is B, when we show that rewriting terminates we have shown that the multiset order is well-founded.

We prove that this rewrite system terminates. We define <_{cut} by the rules

L(x) >_{cut} I(y) L(x) >_{cut} L(y) iff x >_{ρ} y

It is clear that <_{cut} is well-founded when ρ is. To show that <_{cut} ∪ <_{sn1} is well-founded, we use Lemma 1, by showing that in fact <_{sn1} ∘ <_{cut}= ∅. For suppose t >_{sn1} u >_{cut} v. Then u must be of the form L(x), and a proper subterm of t must reduce to a proper subterm of u – but u has no proper subterms.

To show that Condition 2 is satisfied, when L(b) ⟶ I(L(c_{1}), …, L(c_{k})), we have L(b) >_{cut} I(L(c_{1}), …, L(c_{k})) by the first rule for <_{cut}, and, for every subterm L(c_{i}) of the reduced subterm, L(b) >_{cut} L(c_{i}) by the second rule.

3.2 A non simplification ordering

Example 5 of [5], with the single rule f(f(x)) ⟶ f(g(f(x))) is one for which a simplification ordering cannot be used, because a simplification ordering would take g(f(x)) to f(x) and so f(g(f(x))) to f(f(x)), giving a cycle.

But Theorem 2 is not limited to simplification orderings. We define <_{cut} according to the number of consecutive f symbols starting from the head of a term. Alternatively, we could use the total number of pairs of adjacent f symbols, as suggested in [5]. Thus f(f(x)) >_{cut} f(g(y)), f(f(x)) >_{cut} g(y), and f(f(x)) >_{cut} f(x). Finally, any subterm of x is a proper subterm of f(f(x)). Thus Condition 2 is satisfied. Clearly also, rewriting a subterm cannot increase the number of consecutive f symbols, so <_{sn1} ∘ <_{cut} ⊆ <_{cut} (and likewise <_{cut} ∘ <_{sn1} ⊆ <_{cut}). Thus <_{dt} = <_{cut} ∪ <_{sn1} is well-founded by Lemma 1. Therefore the system terminates, by Theorem 2.

3.3 A recursive path ordering example

We now consider a typical example whose termination is shown by the recursive path ordering (see, for example, [6] or [7]).

D(x + y) ⟶ Dx + Dy  (x × y) × z ⟶ x × (y × z)
D(x × y) ⟶ x × Dy + Dx × y  (x + y) + z ⟶ x + (y + z)
x × (y + z) ⟶ x × y + x × z

The recursive path ordering is a simplification ordering. To prove termination we must actually add the following simplification rules as rewrite rules:

x + y ⟶ x  x + y ⟶ y  x × y ⟶ x  x × y ⟶ y

Clearly, if additional rules R′ are added to a rewrite system R, and the resulting system R ∪ R′ terminates, then the original system R terminates.

We define <_{cut} as below by first defining the relation <_{h}, which depends on the head symbol, and then defining the relations <_{×} and <_{+} which are for the rewrite rules capturing associativity:

– D(x) >_{h} y × z  D(x) >_{h} y + z  x × y >_{h} z + w

– if x′ is an immediate subterm of x, then x + y >_{+} x′ + z and x × y >_{×} x′ × z – <_{cut}= (<_{h} ∪ <_{×} ∪ <_{+}).

We now prove that this rewrite system terminates. Clearly <_{cut} is wellfounded, since the immediate subterm relation is well-founded.

To show that <_{cut} ∪ <_{sn1} is well-founded, we in fact show that <_{cut} ∪ <_{sn2} is well-founded, using Lemma 1(a). First we show that <_{cut} ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ <_{cut}. For suppose t >_{cut} u >_{sn2} v. If t >_{h} u then clearly t >_{h} v. Suppose t >_{×} u, say t = x × y, u = x′ × z and x′ is an immediate subterm of x. There are two cases for u >_{sn2} v, namely that a strongly normalising subterm of either x′ or z reduces to a corresponding subterm of v. Firstly, if z ⟶ w, then we also have v = x′ × w and t >_{cut} v. Secondly, if x′ ⟶ w′, then v = w′ × z. As x′ is a subterm of x, let w be the term obtained from x by rewriting its subterm x′ to w′. Then t = x × y >_{sn2} w × y: but note that this step of the argument would not hold for >_{sn1}. Then w′ is an immediate subterm of w, so we have w × y >_{cut} w′ × z = v. That is, (v, t) ∈ <_{sn2} ∘ <_{cut}.

So, in each case, (v, t) ∈ <_{sn2}^{∗} ∘ <_{cut}, and so <_{cut} ∪ <_{sn2} is well-founded, by Lemma 1(a).

Finally, we need to consider all pairs (r′, l), where l → r is a rewrite rule and r′ is a subterm of r. In many cases l >_{h} r′: for example D(x + y) >_{h} Dx + Dy. In other cases, r′ is a proper subterm of l: for example whenever a (meta-)variable appears on the right-hand side of a rule, and r′ is the term the variable stands for, or any subterm of it. In the case of the associative rewrite rule l = (x × y) × z ⟶ r = x × (y × z), we have that l >_{×} r, by definition; the rule for the associativity of + is similar.

Finally, we have cases for (r′, l) such as (D(x), D(x+y)) or (y×z, (x×y)×z). Here, since a proper subterm l′ of l is assumed to be strongly normalising, and x + y ⟶ x (likewise x × y ⟶ y) we have D(x + y) >_{sn1} D(x) and (x × y) × z >_{sn1} y × z.

Thus in all cases either r′ is a proper subterm of l or (assuming proper subterms of l are in SN ) l >_{dt} r′, so the system terminates by Theorem 2.

3.4 Ackermann’s function

Ackermann’s function on the natural numbers can be defined by the following rewrite rules [5, Example 29]

A(0, y) ⟶ S(y)
A(S(x), 0) ⟶ A(x, S(0))
A(S(x), S(y)) ⟶ A(x, A(S(x), y))

It can be shown to terminate using the lexicographic path ordering. This is reflected in the relation >_{cut} we use, which is defined by the following cases:

A(x, y) >_{cut} S(z)  (1)
A(S(x), y) >_{cut} A(x, z)  (2)
A(x, S(y)) >_{cut} A(x, y)  (3)

We now prove that this rewrite system terminates. It is clear that >_{cut} is well-founded using the lexicographic ordering on arguments. It is also clear that for each (r′, l), where l → r is a rewrite rule and r′ is a subterm of r, either l >_{cut} r′ or r′ is a proper subterm of l.

It remains to show that <_{cut} ∪ <_{sn1} is well-founded. Again we show that <_{cut} ∪ <_{sn2} is well-founded, using Lemma 1(a). We show that <_{cut} ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ <_{cut}. For suppose t >_{cut} u >_{sn2} v. If t >_{cut} u by rule (1), ie t = A(x, y) and u = S(z), then v = S(z′) and so t >_{cut} v. If t >_{cut} u by rule (2), then t = A(S(x), y) and u = A(x, z). There are two cases for u >_{sn2} v: v = A(x, z′) where z ⟶ z′, in which case t >_{cut} v, or v = A(x′, y) where x ⟶ x′ by reducing a strongly normalising subterm of x, in which case t = A(S(x), y) >_{sn2} A(S(x′), y) >_{cut} A(x′, z) = v. The case for rule (3) is similar.

So in all cases (v, t) ∈ <_{sn2}^{∗} ∘ <_{cut}, and so <_{cut} ∪ <_{sn2} is well-founded, by Lemma 1(a). Therefore the system terminates by Theorem 2.

3.5 Insertion sort

This example [5, Example 32] is more difficult than the previous two, though the approach is similar. The rules are

sort(nil) ⟶ nil
sort(cons(x, y)) ⟶ insert(x, sort(y))
insert(x, nil) ⟶ cons(x, nil)
insert(x, cons(v, w)) ⟶ choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) ⟶ cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) ⟶ cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) ⟶ choose(x, cons(v, w), y, z)

To define >_{cut}, we start by defining an order >_{h}, contained in >_{cut}, which depends on the head symbol, using this (transitive) order on symbols: sort > {insert, choose} > cons. We notice that the rules (considered as definitions) define insert and choose in terms of each other, so we continue by defining

insert(x, w) >_{cut} choose(y, w, a, b) >_{cut} insert(x, w′)
choose(y, w, a, b) >_{cut} choose(y′, w, a′, b′)

where >_{cut} is transitive and w′, a′ are immediate subterms of w, a. It is easy to see that >_{cut} is well-founded. As in §3.3, we add a simplification rule

cons(x, y) ⟶ y

Then, for every (r′, l) where l → r is a rewrite rule and r′ is a subterm of r, either l >_{cut} r′, l >_{sn1} r′ or r′ is a proper subterm of l.

Again we show that <_{cut} ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ <_{cut}, using the same technique as in the previous two examples. Therefore the system terminates by Theorem 2.

The ordering <_{cut} is similar to that used in [5, Example 32], and [6].

3.6 The factorial example

Example 21 of [5] is almost the usual definition of the factorial function, but modified so that we can not use a simplification ordering. The rules are

P (S(x)) ⟶ x  F (0) ⟶ 0
F (S(x)) ⟶ S(x) × F (P (S(x)))  0 × y ⟶ 0
S(x) × y ⟶ x × y + y  x + 0 ⟶ x
x + S(y) ⟶ S(x + y)

As usual we define a (transitive) ordering <_{h} of terms based on the following ordering of head symbol: F > × > + > S. But we need to define <_{cut} to be the union of <_{h} and the following additional cases

F (S(x)) >_{cut} F (P (S(x))) F (S(x)) >_{cut} F (P (x))

We can not use a simplification ordering because if we allowed P (x) ⟶ x the system would not terminate, but would “cycle” between terms containing F (S(x)) and terms containing F (P (S(x))). We do, however, need to add the rule S(x) ⟶ x. The proofs of termination given in [5, Examples 21, 25] are based on interpreting arguments to the function symbols as natural numbers.

Now for each (r′, l) where l → r is a rewrite rule and r′ is a subterm of r, it is reasonably easy to see that we have one of the following cases:

– r′ is a proper subterm of l

– r′ <_{h} l

– r′ is l, but with S removed from a subterm (to give r′ <_{sn1} l)

– r′ is F (P (S(x))) and l is F (S(x)) (so r′ <_{cut} l).

It is easy to see that <_{cut} is well-founded. To show that <_{cut} ∪ <_{sn2} is wellfounded we need to use a more general case of Lemma 1 than hitherto. In fact we show <_{cut} ∘ <_{sn2} ⊆ (<_{sn2}^{∗} ∘ <_{cut})∪ <_{sn2}^{+}, which implies (d) of Lemma 1.

Suppose t >_{cut} u >_{sn2} v. If t >_{h} u then clearly t >_{h} v. Suppose t = F (S(x)) and u = F (P (S(x))) or u = F (P (x)). If u >_{sn2} v by way of reducing the x in u to x′ (reducing a strongly normalising subterm of x), then t = F (S(x)) >_{sn2} F (S(x′)) >_{cut} v. Otherwise we need to consider specific cases:

– u = F (P (S(x))), S(x) ⟶ x where S(x) ∈ SN, v = F (P (x)): then t >_{cut} v – u = F (P (S(x))), P (S(x)) ⟶ x where P (S(x)) ∈ SN, v = F (x): here, as

S(x) ⟶ x and S(x) ∈ SN, we have t >_{sn2} v

– u = F (P (x)), where x = S(y), P (S(y)) ⟶ y and P (S(y)) ∈ SN, v = F (y): here, as S(y) ⟶ y and S(y) ∈ SN, we have t = F (S(S(y)) >_{sn2} F (S(y)) >_{sn2} F (y) = v.

Thus <_{cut} ∪ <_{sn2} is well-founded and the system terminates by Theorem 2.

3.7 Recursive Path Orderings

To show that our theorem is at least as general as the recursive path orderings we now derive their termination.

Given a well-founded ordering <_{σ}, we use the derived lexicographic ordering lex σ, which is restricted to fixed-length sequences, and so is well-founded.

Given a well-founded ordering <_{ρ} on function symbols, the lexicographic path ordering lpo ρ, also written <_{lpo} [7, Defn 4.22], is then defined as below (omitting reference to lpo-equivalent terms, and where <_{lex} is lex (lpo ρ)

\frac{s_{i} ≥_{lpo} t}{f(s_{1}, …, s_{m}) >_{lpo} t}  \frac{f >_{ρ} g  ∀i ∈ \{1, …, n\}. f(s_{1}, …, s_{m}) >_{lpo} t_{i}}{f(s_{1}, …, s_{m}) >_{lpo} g(t_{1}, …, t_{n})}

\frac{(s_{1}, …, s_{m}) >_{lex} (t_{1}, …, t_{m}) ∀i ∈ \{1, …, m\}. f(s_{1}, …, s_{m}) >_{lpo} t_{i}}{f(s_{1}, …, s_{m}) >_{lpo} f(t_{1}, …, t_{m})}

We note that the definition of the multiset path ordering, and the proof that it is well-founded, correspond closely to what follows.

The following lemma is actually an easy consequence of the transitivity of >_{lpo}, but that result is much more difficult to prove.

Lemma 4. If s >_{lpo} t and t′ is a subterm of t then s >_{lpo} t′.

Proof. It is enough to show that if s >_{lpo} t = g(t_{1}, …, t_{n}) then s >_{lpo} t_{j} where j ∈ {1, …, n}. We show this by induction on the size (or structure) of s. If s >_{lpo} t by the second or third rules, then it is immediate that s >_{lpo} t_{j}. If s = f(s_{1}, …, s_{m}) >_{lpo} t by the first rule, then for some s_{i}, either s_{i} >_{lpo} t and so s_{i} >_{lpo} t_{j} by induction, or s_{i} = t >_{lpo} t_{j} by the first rule, and then s >_{lpo} t_{j} by the first rule. ⊓ ⊔

Theorem 4. For a well-founded ordering <_{ρ} on function symbols, the derived lexicographic path ordering is well-founded.

Proof. We first define <_{cut} using <_{h} as the ordering of terms according to the head symbol and defining another relation <_{lw1} as below:

– f(\overline{s}) >_{h} g(\overline{t}) iff f >_{ρ} g

– if ((\overline{t}), (\overline{s})) ∈ lex (fwf (lpo r)), then f(\overline{t}) <_{lw1} f(\overline{s})

– <_{cut} = (<_{h} ∪ <_{lw1}).

The idea behind the definition is similar to the way the definition of <_{sn1} requires the <_{sn1}-greater term to be strongly normalising. As fwf (lpo r) is well-founded, lex (fwf (lpo r)) and so <_{lw1} are well-founded. Clearly also <_{h} ∘ <_{lw1} ⊆ <_{h}, so <_{cut} is well-founded, by Lemma 1. Further, <_{sn1} ⊆<_{lw1}, so <_{cut} ∪ <_{sn1} = <_{cut} is well-founded.

To show that the rewrite relation <_{lpo} satisfies Condition 1, suppose (r′, l) is given, where r <_{lpo} l and r′ is a subterm of r. Then, by Lemma 4, r′ <_{lpo} l.

If l = f(s_{1}, …, s_{m}) >_{lpo} r′ by the first rule, then some s_{i} >_{lpo} r′. Now assuming that s_{i} ∈ SN, we have r′ ∈ SN.

Now suppose l >_{lpo} r′ by the second or third rules. Again, we are assuming that all proper subterms of l are strongly normalising, and then r′ <_{cut} l. ⊓ ⊔

It may be noted that using our theorem as above actually proves that ctxt (lpo ρ) is well-founded — in fact, since lpo ρ is closed under context this point is of no significance. The proof that the multiset path ordering <_{mpo} [7, Defn 4.24] is well-founded is very similar. In the “status-based” recursive path ordering, lists of arguments to a function symbol are compared using the lexicographic, multiset or other derived ordering ϕ( ), depending on the function symbol. This is well-founded also, by a similar proof. The necessary properties for such an ordering ϕ( ) are the following: that ϕ(σ) is well-founded if σ is, and that if s′_{i} <_{σ} s_{i} then (s_{1}, …, s′_{i}, …, s_{m}) <_{ϕ(σ)} (s_{1}, …, s_{i}, …, s_{m}). This second property is used above in the step <_{sn1} ⊆<_{lw1}.

3.8 The Knuth-Bendix Ordering

For a rewrite system (with rules containing variables), the Knuth-Bendix ordering <_{kb} is based on a strict well-founded order < on function symbols and, additionally, a weight function w on function symbols and variables. Since our approach is based on a relation ρ (which amounts to the rewrite rules after all possible substitutions for variables), we describe the Knuth-Bendix ordering in this context. Weights are natural numbers, and the weight of any constant or object language variable is positive: thus every subterm has positive weight. At most one unary function symbol (call it k) can have zero weight, and then k > f for any other function symbol f. The weight of a term is the sum of the weights of the function symbols and variables in it. Then we have that s >_{kb} t iff w(s) ≥ w(t) and one of

w(s) > w(t)  (4)
s = k^{n}(t) for some n > 0  (5)
s = f(\overline{s}) and t = g(\overline{t}) where f > g  (6)
s = f(\overline{s}), t = f(\overline{t}) and (\overline{t}, \overline{s}) ∈ lex (<_{kb})  (7)

Theorem 5. The Knuth-Bendix ordering is well-founded.

Proof. The proof that <_{kb} is well-founded is similar to that in §3.7, and so is somewhat abbreviated here. We define s >_{cut} t iff w(s) ≥ w(t) and either one of the rules (4), (5), (6) holds or s >_{kw1} t holds, where <_{kw1} is defined by:

f(\overline{t}) <_{kw1} f(\overline{s}) iff (\overline{t}, \overline{s}) ∈ lex (fwf (<_{kb}))  (8)

To show <_{cut} is well-founded, we have that each individual rule provides a well-founded relation and it is easy to apply Lemma 1 to show that their union is well-founded, noting that if (6) applies then g ≠ k. As in the case of the lexicographic path order <_{sn1}⊆<_{kw1}.

To show that Condition 1 is satisfied, suppose that l >_{kb} r and that r′ is a subterm of r. Assume that all proper subterms of l are in SN, in which case, if l >_{kb} r′ then l >_{cut} r′. We show by induction on the structure of l, that r′ <_{kb} l′ for some subterm l′ of l. Then if l′ is a proper subterm of l, Condition 2(a) is satisfied; if l′ = l then r′ <_{kb} l and so r′ <_{cut} l, so Condition 2(b) is satisfied.

If w(r′) < w(r) or w(r) < w(l) then w(l) > w(r′) and l >_{kb} r′. If r′ = r then l >_{kb} r′. If w(l) = w(r) = w(r′) and r′ is a proper subterm of r, then r = k^{n}(r′) for some n > 0, and so l >_{kb} r by either (5) or (7) (as the g of (6) cannot be k). If l >_{kb} r by (5) then l >_{kb} r′ by (5). If l >_{kb} r by (7), then, for some l_{1}, r_{1}, l = k(l_{1}), r = k(r_{1}), l_{1} >_{kb} r_{1} and r′ is a subterm of r_{1}, so by induction we have that r′ <_{kb} l′ for some l′ which is a subterm of l_{1} and so of l. ⊓ ⊔

3.9 Dependency Pairs

Arts & Giesl [1] describe a method of establishing termination using “dependency pairs”. They distinguish function symbols which appear at the head of the left-hand side of a rewrite rule (“defined symbols”) and those which do not (“constructor symbols”). They follow the convention that for a rule l → r of a rewrite system, l is not a lone variable, and any variable in r is also in l. For each defined symbol d they introduce a new corresponding “tuple symbol” d^{♯}. From a term t we obtain a term t^{♯} by changing the head symbol of t to the corresponding tuple symbol.

Previously we have considered a “rule” l → r after substitution, and the variables in our analyses have been metavariables where, for example, we might have considered a rule g(x) → x with l = g(x), r = x, and r′ a proper subterm of x. This approach no longer holds: l → r will mean a rule before substitution, and we will use σ for a substitution.

For a rewrite rule l → r, and subterm r′ of r, if the head of r′ is a defined symbol then l^{♯} → r^{′♯} is a dependency pair. We now state and prove the “sufficiency” part of Theorem 7 of [1].

Theorem 6. If there is a well-founded quasi-ordering ≤ which is closed under context and where both ≤ and < are closed under substitution, such that

(a) l ≥ r for all rules l → r, and

(b) s > t for all dependency pairs s → t

then the rewrite system terminates.

Proof. Assume > is minimal such that the conditions hold. Then there is no instance of c^{♯}(x) > d^{♯}(y) or c(x) > d(y) where c is a constructor symbol and d is a defined symbol, as neither (a) nor (b) nor the requirement that ≤ be closed under context require it, whence the transitivity of ≤ cannot require it.

We define <_{cut} by

s^{♯} < t^{♯} ⟹ sσ <_{cut} tσ  (9)
c(x) <_{cut} d(y)  (10)

for any substitution σ, constructor symbol c and defined symbol d.

Then <_{cut} is well-founded because < is and because, as remarked above, there is no instance of c^{♯}(x) > d^{♯}(y) or c(x) > d(y).

To show that <_{cut} ∪ <_{sn1} is well-founded, we use Lemma 1(a), showing that <_{cut} ∘ <_{sn1} ⊆ <_{cut}. Suppose that t >_{cut} u >_{sn1} v. If t >_{cut} u by rule (10) then t >_{cut} v by the same rule. If t >_{cut} u by rule (9) then t^{♯} > u^{♯}, where a proper subterm u′ of u is rewritten to a corresponding subterm v′ of v. Since u′ ≥ v′ by assumption (a) because ≤ is closed under substitution, we have u^{♯} ≥ v^{♯} since ≤ is closed under context, and so t^{♯} > v^{♯} and t >_{cut} v.

Finally, we show that Condition 2 is satisfied. For a rule l → r and substitution σ, so (rσ, lσ) ∈ ρ, and subterm r′ of rσ, there are three cases for r′:

– the head of r′ is a constructor symbol in r, in which case lσ >_{cut} r′ by (10)

– the head of r′ is a defined symbol in r, in which case r′ = r_{1}σ for some subterm r_{1} of r, l^{♯} → r_{1}^{♯} is a dependency pair, and lσ >_{cut} r_{1}σ = r′ by (9)

– r′ is a subterm of xσ for some variable x in r, in which case r′ is a proper subterm of lσ, since any variable in r appears as a proper subterm of l.

4 Observations and Conclusion

In §3.3 we had the somewhat paradoxical situation that it was necessary to add additional rewrite rules to enlarge the relation ρ to prove termination. An interesting question is whether we can reformulate Theorem 2 to avoid this need since, the larger ρ is, the more difficult it should be to prove termination.

It is interesting to consider further questions of a similar nature. We prove the well-foundedness of ctxt ρ based on certain conditions on ρ. Since ctxt (ctxt ρ) = ctxt ρ and assuming we can apply Theorem 2 to ρ, can we also apply it to ctxt ρ using the same or a different choice of <_{cut} ? In fact, we can, and with the same choice of <_{cut}. Suppose ρ satisfies Condition 1. Consider (C[r], C[l]) ∈ ctxt ρ \ ρ, where (r, l) ∈ ρ, and let r′ be a subtree of C[r]. If r′ = C[r], then r′ <_{sn1} C[l] under the assumption that all proper subtrees of C[l] are in SN. If r′ is a subtree of r, then Condition 2(a) holds for (r′, C[l]) because l is a proper subtree of C[l], l reduces to r, and r′ is a subtree of r. Thus l, r and r′ are in SN. Finally, r′ could be C′[r], where C′[l] is a proper subterm of C[l]. If C′[r] = C′[l] then l is in a different part of C[l] from C′[l] so r′ = C′[l] is a proper subterm of C[l]; otherwise r′ is the reduction of C′[l], and Condition 2(a) holds.

Likewise, rewriting with ρ terminates if and only if rewriting with ρ^{+} terminates: this is because ctxt ρ ⊆ ctxt ρ^{+} ⊆ (ctxt ρ)^{+} and ctxt ρ is well-founded if and only if (ctxt ρ)^{+} is. Now, when we can apply Theorem 2 to ρ, can we also apply it to ρ^{+} ? So far we have shown that if ctxt ρ satisfies Condition 2, then so does (ctxt ρ)^{+} (with the same <_{cut}), provided that ctxt ρ is well-founded. The proof is a complex triple induction.

If we ask how powerful Theorem 2 is, that is, which terminating rewrite systems can it handle, then we find that it can handle all of them, but this result is unhelpful. For given ρ, where ctxt ρ is well-founded, then, writing ≤_{sub} for the subterm relation, we can define <_{cut}= ρ ∘ <_{sub}. Then Condition 2(a) holds, trivially. Further, it can be shown that ctxt ρ ∪ <_{sub} is well-founded: though, as we have seen, ctxt (ρ ∪ <_{sub}) need not be. Since <_{dt}⊆ (ctxt ρ ∪ <_{sub})^{+}, we have <_{dt} is well-founded. That is, where ctxt ρ is well-founded, we can always find an appropriate relation <_{cut}. But it may be no easier to show <_{cut} well-founded than to show ctxt ρ well-founded.

We have described a proof of the termination of a rewrite system (or any relation closed under context) which provides simple proofs of the termination of a range of rewrite systems. It provides a reasonably easy proof of the wellfoundedness of the lexicographic and multiset path orderings (which are simplification orderings), but it is not limited to simplification orderings. It can also be used to prove the termination of Knuth-Bendix orderings and a key theorem for the method of dependency pairs.

There are several termination results for orderings which are not necessarily closed under context, but contain a rewrite ordering, such as the results of Ferreira & Zantema [9], Dershowitz & Hoot [6] and Borralleras, Ferreira & Rubio [2]. We are currently exploring the linkage between our results and these termination results.

Acknowledgements We wish to thank Linda Buisman for investigating some of the examples, and researching the criteria for well-foundedness of a union of wellfounded orderings. We also wish to thank Jean Goubault-Larrecq and Hubert Comon for pointers to the literature. Finally, we thank some anonymous referees for very helpful comments.

References

1. Thomas Arts and Jürgen Giesl. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236 (2000), 133-178, 2000.

2. Cristina Borralleras, Maria Ferreira and Albert Rubio. Complete Monotonic Semantic Path Orderings. In Proc. 17th Conference on Automated Deduction (CADE-17), LNCS 1831, 346–364, Springer, 2000.

3. Jeremy E. Dawson and Rajeev Goré. A New Machine-checked Proof of Strong Normalisation for Display Logic. In Computing: The Australasian Theory Symposium, 2003, Electronic Notes in Theoretical Computer Science 78, 16–35, Elsevier.

4. Jeremy E. Dawson and Rajeev Goré. Formalised cut admissibility for display logic. In Proc. 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs02), LNCS 2410, 131–147, Springer, 2002.

5. Nachum Dershowitz. 33 Examples of Termination. Proc. French Spring School of Theoretical Computer Science (1993), LNCS 909, 16–25, Springer 1995.

6. Nachum Dershowitz & Charles Hoot. Natural Termination. Theoretical Computer Science 142 (1995), 179-207.

7. Nachum Dershowitz & David A. Plaisted. Rewriting. In Alan Robinson & Andrei Voronkov, eds, Handbook of Automated Reasoning, 535–610, Elsevier, 2001.

8. Henk Doornbos & Burghard Von Karger. On the Union of Well-Founded Relations. L. J. of the IGPL 6 (1998), 195-201.

9. M C F Ferreira and H Zantema. Well-foundedness of Term Orderings. In Conditional Term Rewriting Systems (CTRS-94) ed N. Dershowitz, LNCS 968, 106–123, 1995.

10. Jean Goubault-Larrecq. Well-founded recursive relations. In Computer Science Logic (CSL’2001), LNCS 2142, 484–497, 2001.

11. Sam Kamin & Jean-Jacques Lévy. Two generalizations of the recursive path ordering. Unpublished, Department of Computer Science, University of Illinois, 1980.

12. Frank Pfenning. Structural Cut Elimination, Proc. LICS 94, 1994.