International Journal of Foundations of Computer Science \begin{matrix}c \\ ◯ \end{matrix} World Scientific Publishing Company

TERMINATION OF ABSTRACT REDUCTION SYSTEMS

JEREMY E DAWSON

Logic and Computation Program, NICTA, Locked Bag 8001, Canberra ACT 2601,

AUSTRALIA,

RSISE (Bldg 115) Australian National University Canberra ACT 0200 AUSTRALIA

and

RAJEEV GORÉ

RSISE (Bldg 115) Australian National University Canberra ACT 0200 AUSTRALIA

Received (received date) Revised (revised date) Communicated by Editor’s name

ABSTRACT We present a general theorem capturing conditions required for the termination

of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

Keywords: rewriting, termination, well-founded ordering, strong normalisation

1. Introduction

We address the general problem of termination of rewriting which can be informally posed as follows. Assume that we have a fixed set of “objects” defined in some way. Suppose we are given a binary relation ρ on these objects, where (t, s) ∈ ρ expresses that object s may be transformed into object t. Let us call such a transformation a reduction. Consider repeatedly reducing an object in any way possible. We are interested to know whether such repeated reduction necesarily terminates – formally, whether or not there is an infinite sequence t = t_{0}, t_{1}, …, where each (t_{i+1}, t_{i}) ∈ ρ. If there is not, we say that t is strongly normalising: t ∈ SN. The difficulty of the problem arises from the totally general notion of “reduction”.

In the common special case of a term rewriting system (TRS), an object is a term of some first-order language, and the reduction relation is described by a set of “rewrite rules” l_{i} → r_{i}, where l_{i} and r_{i} are terms containing variables for which terms may be substituted. Here, rewriting is also usually monotonic [5], or closed under context [22], in that if C[ ], a term with a “hole”, is the context, and l reduces to r, then C[l] reduces to C[r]. Several general methods capturing termination of such term rewriting systems exist [3, 13, 8]. For a detailed survey see [11]. A discussion of methods for proving termination, including structural induction on terms, is found in [21]. Term rewriting systems with specific rewriting strategies such as innermost, outermost (see, eg, [17], [20], and works cited therein) also are cases of this general problem.

Jean Goubault-Larrecq [21] has proved termination results for an abstract reduction system (ARS) where objects need not have a term structure and so there is no monotonicity assumption or subterm relation. Whereas proofs for TRSs involve the subterm relation, his proofs use an arbitrary well-founded relation ◁ instead. His Theorem 1, call it JGL1, is the result of “chasing generalizations and simplifications” of earlier work and “subsumes … most path-orderings of the literature”.

We first proved our Theorem 8 as [8, Theorem 2]. While Theorem 8 and JGL1 use remarkably similar ideas, neither JGL1 (even if restricted to TRSs) nor our Theorem 8 subsumed the other. Our new more general theorem subsumes both.

We first present this more general theorem and its proof in §2. In §3, we show that it generalises JGL1, and in §3.2 we show directly how it implies the termination of the general path ordering of Dershowitz & Hoot [13]. In §4, we show how to use our new theorem to obtain two different proofs of strong normalisation for well-typed combinator terms. In these cases, although the objects have a term structure, our proofs use the ARS setting and show the well-foundedness of larger, non-monotonic, relations. The combinator case suggests that our theorem properly generalises JGL1. Thus, our theorem handles most path-orderings in the literature and the reducibility method typically used for typed combinators.

In §5 we show how the main theorem implies a similar result for TRSs [8, Theorem 2], and relate that result to work on constricting derivations. We consider applications of the theorem for TRSs, showing how it gives well-known results for the Knuth-Bendix Ordering, and results relating to dependency pairs. By an analogue of §3.2 (see [8, §3.7]), the termination of the recursive path ordering [11, Defn 4.22, 4.24] follows. We also apply our theorem to numerous specific examples.

Commonly, a rewrite system is defined by taking a base system, known to be terminating, and adding new function symbols and rules to it. In §6 we show how our theorem can be used to prove termination in certain such cases, for example, where the new symbols and rules are those of the examples in §3.3 to §3.5 of [8]. A more complex variant of the result covers the example in [8, §3.6]. We then derive a path-ordering result in this context of incrementally defined systems.

The history of our work is this. In [7] we described a proof of strong normalisation for a cut-elimination procedure in display logic. Since the procedure involved repeated transformation (or “rewriting”) of a derivation tree, we realised that if we described a derivation tree as a term in a first-order language, we would get a proof of termination of a particular rewriting system. Finding the crucial properties of this rewriting system gave us [8, Theorem 2]. Tracing the similarities and differences between this result and JGL1 led us to our main result, Theorem 1.

Our proofs were machine-checked in Isabelle/HOL: [9], directories snabs,snlc.

1.1. Notation, Terminology, Definitions and Basic Lemmas

Assume we are given a set U: in a TRS this would be the set of terms, but in the ARS setting we just call them “objects”. For an irreflexive binary relation ρ, we write (r, t) ∈ ρ, (r, t) ∈ <_{ρ}, r <_{ρ} t or t >_{ρ} r interchangeably. We prefer >_{ρ} over the more traditional →_{ρ} because the latter is typically used in TRSs, our setting is more abstract than TRSs, and when we deal with TRSs we need to carefully distinguish between a relation and its closure under contexts. For a symbol that suggests a direction such as <, ◁, ≺, ≾ or ≪ we will write (r, t) ∈ ◁, (t, r) ∈ ▷, r ◁ t or t ▷ r interchangeably. 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 objects, and ρ is well-founded (or Noetherian) if every r ∈ SN. We write ≤_{ρ} or ρ^{=}, <_{ρ}^{+} or ρ^{+}, and <_{ρ}^{∗} or ρ^{∗} for the reflexive closure, the transitive closure and the reflexive transitive closure, respectively, of <_{ρ}. We write σ ∘ ρ for relational composition: that is, (r, s) ∈ σ ∘ ρ if there exists t such that (r, t) ∈ ρ and (t, s) ∈ σ.

In our formal treatment in Isabelle/HOL we used the following inductive definition (also used in the Isabelle libraries) for the set SN of strongly normalising objects, and we proved, in the HOL logic, which is classical and contains the Axiom of Choice, that this definition is equivalent to the standard definition given above. Definition 1 (Strongly Normalising – HOL) For a reduction relation ρ, the set SN of strongly normalising objects is the (unique) smallest set of objects such that: if every object t to which s reduces is in SN then s ∈ SN.

Our previous work [8] on term rewriting was on the well-foundedness of the closure under context of a relation ρ. In contrast, we deal here with an abstract reduction system, usually calling the reduction relation ρ. So concepts like “strongly normalising”, “reduction”, etc, relate to ρ, and not, even when discussing structured terms, to the closure of ρ under context. For structured terms, ρ may be the closure under contexts of another relation σ, which may itself be the set of substitution instances of a set R of rewriting rules. In the ARS setting, we use an arbitrary relation where we used the immediate subterm relation in the TRS setting.

In [8, §2.2] we defined the set ISN of “inductively strongly normalising” terms as the set of terms that are in SN if their immediate subterms are in SN. This is same idea as \underline{SN} of [21]. Clearly, SN ⊆ ISN. We now define gindy as a generalised notion of “inductively” for an arbitrary relation σ in place of the immediate subterm relation, which we call isubt. The concept “gindy” enables us to express the principle of well-founded induction succinctly as: if every object is in gindy σ S, and σ is well-founded, then every object is in S. Definition 2 (gindy) For a relation σ and set S, an object t ∈ gindy σ S iff: if ∀u. (u, t) ∈ σ ⇒ u ∈ S, then t ∈ S.

The notion of well-foundedness is generalised to that of a particular object being accessible, or in the well-founded part, of a binary relation: the constructive definition is that s is in the well-founded part of a relation < if there is no infinite downward chain … < s_{2} < s_{1} < s starting from s. This is generalised to the notion that s bars S in < if every infinite downward chain, starting from s, contains a member of S. See [21] for a detailed discussion of this. We now generalise bars to a function gbars where the members of a downward chain, until it meets S, must be in some set Q. The inductive definition of gbars is: Definition 3 (gbars) For sets of objects Q and S, and relation σ, gbars σ Q S is the (unique) smallest set such that:

(i) S ⊆ gbars σ Q S

(ii) if t ∈ Q and ∀u. (u, t) ∈ σ ⇒ u ∈ gbars σ Q S, then t ∈ gbars σ Q S. The next lemma gives another characterisation of gbars which is provably equiva-

lent in classical logic using the Axiom of Choice: t ∈ gbars σ Q S iff every downward σ-chain starting from t is within Q until it hits S or it terminates. Lemma 1 (gbars-alternative) For sets of objects Q and S, and relation σ, object t ∈ gbars σ Q S iff: for every downward σ-chain t = t_{0} >_{σ} t_{1} >_{σ} t_{2} >_{σ} …, either the chain is finite and all t_{i} ∈ Q, or for some member t_{n} of the chain, both t_{n} ∈ S and {t_{0}, t_{1}, t_{2}, …, t_{n−1}} ⊆ Q.

Definition 4 records how gbars generalises the notions of “S bars s in σ” and of “s is accessible in σ, or s is in the well-founded part of σ” as defined in [21]. Definition 4 (wfp, bars)

(i) s ∈ bars σ S iff s ∈ gbars σ U S (“S bars s in σ”) (ii) s ∈ wfp σ iff s ∈ bars σ ∅ (“s accessible in σ ”). Thus SN = wfp ρ and ISN = gindy isubt SN. Lemma 1 gives the following

characterisation of bars, which was given in [21]: s ∈ bars σ S if every infinite decreasing σ-sequence s_{0} >_{σ} s_{1} >_{σ} s_{2} >_{σ} … meets S, ie, for some k, s_{k} ∈ S.

The gbars-induction principle is analogous to the principles of well-founded induction, and of Brouwer’s bars-induction (see [21, Proposition 1]). Like Lemma 1, it follows easily from the inductive definition of gbars in Isabelle’s Higher Order Logic. In fact it is generated automatically by the Isabelle theorem prover from the inductive definition of gbars above. However in weaker logics these do not necessarily hold: see [23, Ch 1, §6] or [15, Ch 3] for discussions of this topic. We write P s to mean that s satisfies property P. Proposition 1 (gbars-induction) For sets Q and S, and any property P, if

(i) for every s ∈ S, we have P s, and

(ii) for every s ∈ Q, if ∀t. (t, s) ∈ σ ⇒ P t, then P s then every s ∈ gbars σ Q S satisfies P. Lemma 2

(i) S = gbars σ (gindy σ S) S (ii) Q ⊆ gindy σ (gbars σ Q S) Proof.

(i) ⊆: this is trivial, from Definition 3(i), by letting Q be gindy σ S.

⊇: Let P s = s ∈ S. We use Proposition 1 with Q = gindy σ S. Condition (i) of Proposition 1 holds trivially, and condition (ii) is given by Definition 2.

(ii) Follows directly from Definitions 2 and 3(ii). □ Lemma 3

(i) if all objects are in gindy σ S, then bars σ S = S, whence, if σ is wellfounded, then every object is in S, and (ii) bars σ (wfp σ) = wfp σ Proof.

(i) As U = gindy σ S, this follows from Lemma 2(i) and Definition 4(i). If σ is well-founded, then U = wfp σ = bars σ ∅ ⊆ bars σ S.

(ii) By Lemma 2(ii), U ⊆ gindy σ (gbars σ U ∅), that is (by Definition 4) every object is in gindy σ (wfp σ). The result now follows from part (i). □

2. The Termination Theorem

Given a reduction relation ρ, our general termination result utilises two relations ◁ and ≪, which, together with ρ, must satisfy a number of properties given below. These relations play a role similar to the relations ◁ and ≪ in [21], and, where convenient, we express our conditions so as to enable easy comparisons with [21]. Most commonly, the relation ◁ is instantiated to the immediate subterm relation, and ≪ is often some sort of approximation to the rewrite relation itself. The most general version of the properties that ◁ and ≪ must satisfy is Condition 1(i) below, but in practice we often use the simpler and stronger conditions (ii) to (v). (Even weaker conditions than 1(i) are possible, since we could for example suppose that s also satisfies ∀u ≪ s. u ∈ gindy ◁ SN: see the proof of Lemma 5 below). Condition 1

(i) If ∀s′ ◁ s. s′ ∈ SN, then s ∈ bars ρ (gbars ◁ {u | u ≪ s} SN)

(ii) For all (t, s) ∈ ρ, if ∀s′ ◁ s. s′ ∈ SN, then t ∈ gbars ◁ {u | u ≪ s} SN (iii) For all (t, s) ∈ ρ, t ∈ gbars ◁ {u | u ≪ s} {v | (v, s) ∈ (◁ ∘ ρ)} (iv) ◁ is well-founded and, for all (t, s) ∈ ρ, if ∀s′ ◁ s. s′ ∈ SN, then, for all t′ ◁^{∗} t, either t′ ∈ SN or t′ ≪ s

(v) ◁ is well-founded and, for all (t, s) ∈ ρ and all t′ ◁^{∗} t,

either (t′, s) ∈ (◁ ∘ ρ^{∗}) or t′ ≪ s. Lemma 4 Each of Conditions 1(ii) to (v) implies Condition 1(i) for all s.

Proof. Clearly, for any set X, ∀(t, s) ∈ ρ. t ∈ X implies s ∈ bars ρ X. Thus it follows that Condition 1(ii) implies that Condition 1(i) holds for all s.

To show that Condition 1(iv) implies Condition 1(ii), assume (iv) holds. Then, as ◁ is well-founded, there is no infinite descending ◁-chain. Any descending ◁- chain from t is contained in {t′ | t′ ≪ s} ∪ SN. A fortiori, members of such a chain are contained in {t′ | t′ ≪ s} until the chain reaches a member of SN. That is, t ∈ gbars ◁ {u | u ≪ s} SN, and so (ii) holds.

To show that Condition 1(v) implies Condition 1(iv), and likewise, that Condition 1(iii) implies Condition 1(ii), assume that ∀s′ ◁ s. s′ ∈ SN. Then, if (t′, s) ∈ (◁ ∘ ρ^{∗}) because t′ <_{ρ}^{∗} s′ ◁ s, then we have s′ ∈ SN and so t′ ∈ SN. Note that in Condition 1(iii) we could have (◁ ∘ ρ^{∗}) in place of (◁ ∘ ρ). □

Our key lemma is Lemma 5. We thank an unnamed referee for pointing out that our proof resembles the proof by Buchholz [6] of the well-foundedness of the lexicographic path ordering, although it was obtained independently. Lemma 5 If object s satisfies Condition 1(i), then s ∈ gindy ≪ (gindy ◁ SN).

Proof. Given s, assume that ρ, ◁ and ≪ satisfy Condition 1(i) and that

(a) ∀u ≪ s. u ∈ gindy ◁ SN. We then need to show s ∈ gindy ◁ SN, so we assume

(b) ∀s′ ◁ s. s′ ∈ SN and we show that s ∈ SN. By Lemma 3(ii), it suffices to show s ∈ bars ρ SN.

The antecedent of Condition 1(i) holds by assumption (b), and so s ∈ bars ρ (gbars ◁ {u | u ≪ s} SN). As bars is monotonic in its second argument, it is enough to show gbars ◁ {u | u ≪ s} SN ⊆ SN. As {u | u ≪ s} ⊆ gindy ◁ SN by assumption (a), and as gbars is monotonic in its second argument, gbars ◁ {u | u ≪ s} SN ⊆ gbars ◁ (gindy ◁ SN) SN. By Lemma 2(i), gbars ◁ (gindy ◁ SN) SN = SN.

So we have s ∈ SN. Thus, discharging assumptions (b) and then (a), we have s ∈ gindy ◁ SN, and then s ∈ gindy ≪ (gindy ◁ SN). □

We now identify the conditions that guarantee that every object is in SN. Theorem 1 Suppose that ρ, ◁ and ≪ satisfy Condition 1(i) for all s and

(i) every object is in bars ≪ (gindy ◁ SN), and (ii) every object is in bars ◁ SN.

Then ρ is well-founded.

Proof. As ρ, ◁ and ≪ satisfy Condition 1(i), every s ∈ gindy ≪ (gindy ◁ SN) by Lemma 5. Then, for any u, if u ∈ bars ≪ (gindy ◁ SN) then Lemma 3(i) gives u ∈ gindy ◁ SN. Thus every u ∈ gindy ◁ SN. Then, for any v, if v ∈ bars ◁ SN then Lemma 3(i) gives v ∈ SN. Thus every v ∈ SN: that is, ρ is well-founded. □

If Condition 1(ii) holds, then it also holds if we augment ρ to contain ◁. Thus, for fixed ◁, Theorem 1 does not provide a universal method of proving termination because it is possible that ρ is well-founded but ρ ∪ ◁ is not.

However, if ρ is well-founded and we can choose ◁ so that ◁ ⊆ ρ, then Theorem 1 can be applied trivially. Let ≪ = ◁ = ρ^{+}, which is well-founded. Then even Condition 1(v) applies. Clearly also, conditions (i) and (ii) of Theorem 1 apply as ≪ and ◁ are well-founded. That is, Theorem 1 is, trivially, a universal result for proving termination (as are several other orderings in the literature).

Most commonly the conditions of Theorem 1 will be satisfied by choosing ≪ and ◁ to be well-founded relations. At this point we mention a lemma which we will use several times, for proving that a relation is well-founded. Lemma 6 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 [14], and is implied by each of the others, which are in earlier results discussed and cited in [14].

3. Applications to Abstract Rewrite Systems

3.1. Generalising Goubault-Larrecq’s General Theorem for ARSs

We show that JGL1, ie, Goubault-Larrecq’s [21, Theorem 1], which itself generalizes many results in the literature, is a special case of our Theorem 1. Note that [21] uses < where we use ρ, uses T where we use U and uses \underline{SN} where we use gindy ◁ SN. We reproduce JGL1, using our notation. Property 1 For every s, t ∈ U, if s >_{ρ} t then either:

(i) for some u ∈ U, s ▷ u and u ≥_{ρ} t, or

(ii) s ≫ t and for every u ◁ t, s >_{ρ} u

Theorem 2 (JGL1: [21], Theorem 1) Assume that Property 1 holds, and (iii) ▷ is well-founded on U, and (iv) for every s ∈ U, if every u ◁ s is in SN, then gindy ◁ SN bars s in ≫.

Then >_{ρ} is well-founded on U.

We first require two lemmas. Lemma 7 Given set S and object s, suppose that for all t, if (t, s) ∈ ρ, then

(i) t ∈ S, or

(ii) s ≫ t and, for every u ◁ t, either (u, s) ∈ ρ or u ∈ S.

Assume ◁ is well-founded. Then (t, s) ∈ ρ implies t ∈ gbars ◁ {x | x ≪ s} S.

Proof. Let (t, s) ∈ ρ. We prove this result for t by well-founded induction on ◁, so assume that, for all v ◁ t, if (v, s) ∈ ρ then v ∈ gbars ◁ {x | x ≪ s} S.

We consider the two cases (i) and (ii) as above.

• First, if t ∈ S, then t ∈ gbars ◁ {x | x ≪ s} S by Definition 3(i).

• Second, if (ii) holds, we show that t ∈ gbars ◁ {x | x ≪ s} S using Defini-

tion 3(ii). We have t ≪ s, and for any u ◁ t, there are two cases. • If (u, s) ∈ ρ then by the inductive hypothesis, u ∈ gbars ◁ {x | x ≪ s} S.

• If u ∈ S then u ∈ gbars ◁ {x | x ≪ s} S by Definition 3(i). □ Lemma 8 Suppose that Property 1 holds, and that ◁ is well-founded. Then Condition 1(ii) holds.

Proof. We use Lemma 7 with S = {v | ∃x. s ▷ x and x ≥_{ρ} v}. To show Condition 1(ii), let (t, s) ∈ ρ, and suppose that ∀s′ ◁ s. s′ ∈ SN. By Lemma 7, t ∈ gbars ◁ {x | x ≪ s} S. We show S ⊆ SN. Let v ∈ S, say s ▷ x and x ≥_{ρ} v. Then x ∈ SN = wfp ρ and so v ∈ SN. Thus, by the obvious monotonicity of gbars, t ∈ gbars ◁ {x | x ≪ s} SN, as required for Condition 1(ii). □

Proof of Theorem 2 (JGL1)

Condition (iv) of Theorem 2 is just condition (i) of our Theorem 1, for if some u ◁ s ∉ SN, then trivially s ∈ gindy ◁ SN. Thus the requirement that “if every u ◁ s is in SN” in (iv) of the statement of JGL1 is redundant, although its counterpart is needed in the statement of [21, Theorem 2].

As ◁ is well-founded, for any object v and set S of objects, v ∈ bars ◁ S, and so condition (ii) of our Theorem 1 follows.

Finally, Lemma 8 shows that, as ◁ is well-founded, Property 1 implies Condition 1(ii), whence Condition 1(i) holds.

Thus all the conditions of our Theorem 1 hold, so ρ is well-founded. □ We now explore the extent to which, conversely, JGL1 implies our Theorem 1. Suppose both ◁ and ≪ are well-founded, and that Condition 1(iii) holds: that

is, with S = {v | (v, s) ∈ (◁ ∘ ρ)}, we have (t, s) ∈ ρ ⇒ t ∈ gbars ◁ {x | x ≪ s} S. Since gbars is monotonic in its third argument and S is monotonic in ρ, we can enlarge ρ to get equivalence, so that (t, s) ∈ ρ ⟺ t ∈ gbars ◁ {x | x ≪ s} S ; then it can be seen that (i) and (ii) of Property 1 hold.

That is, JGL1 can be used to prove a weaker version of our Theorem 1 in which Condition 1(iii), rather than Condition 1(i), is assumed, and it is assumed that ◁ and ≪ are well-founded. On the other hand, in Sections 4.1 and 4.2, the proofs of termination use our Theorem 1, and, in particular, use Condition 1(ii). The difference between Condition 1(ii) and Condition 1(iii) is crucial to these proofs, which suggests that JGL1 is a special case of our Theorem 1.

3.2. Application to the General Path Ordering

The definition of the general path ordering of Dershowitz & Hoot [13] presupposes terms in a first-order language, but the ordering is not necessarily monotonic. Therefore we deal with it in the context of an ARS. As noted by Goubault-Larrecq [21], JGL1 can be used to show that the general path ordering is well-founded. We now show how that ordering fits our Condition 1 for termination of an ARS presented earlier. The following treatment is similar to that of the recursive path orderings in our [8, §3.7], but that applied only to the cases where the derived ordering is monotonic (ie, closed under context).

The general path ordering <_{gpo} is defined as below where s = f(s_{1}, …, s_{m}) and t = g(t_{1}, …, t_{n}), and Λ(<_{gpo}) (or <_{Λ}) is an ordering derived from <_{gpo}, where Λ satisfies conditions given later. We omit defining <_{gpo}-equivalent terms.

\frac{s_{i} ≥_{gpo} t}{s >_{gpo} t}(G1)  \frac{s >_{Λ} t  ∀i ∈ \{1, …, n\}. s >_{gpo} t_{i}}{s >_{gpo} t} (G2)

In practice, <_{Λ}, which is derived from <_{gpo}, depends on <_{gpo} applied only to smaller terms, ie, determining whether s >_{Λ} t depends on whether s′ >_{gpo} x only for proper subterms s′ of s (and arbitrary terms x). Thus the above rules can be seen as mutually recursive definitions of <_{gpo} and <_{Λ}.

However in the formal Isabelle proof a different approach was taken to ensure a consistent definition: <_{gpo} is an inductively defined set, which means that s >_{gpo} t if and only if it can be shown so using the rules above. This approach requires that <_{Λ} be a monotonic function of <_{gpo}.

As in [8], we define an auxiliary function fwf for “from well-founded” which maps a binary relation σ to a binary relation fwf σ as below: Definition 5 Given a relation σ, (t, s) ∈ fwf σ iff (t, s) ∈ σ and s ∈ wfp σ.

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

We can let ◁ be either the immediate subterm relation or the proper subterm relation — in the latter case, the required condition (c) below is weaker. We now list the conditions on Λ required for the Isabelle proof:

(a) Λ is a monotonic function

(b) if σ is well-founded then Λ(σ) is well-founded

(c) if all s′ ◁ s are in wfp σ and if (t, s) ∈ Λ(σ), then (t, s) ∈ Λ(fwf σ).

In practice, condition (c) means that Λ(σ) depends on σ only as follows: whether (t, s) ∈ Λ(σ) depends solely upon whether (x, s′) ∈ σ for s′ ◁ s, and arbitrary x, although Λ(σ) can also depend on, for example, a well-founded ordering on the function symbols {f, g, …}. Lemma 9 If s >_{gpo} t and t′ is a subterm of t then s >_{gpo} t′. Proof. It is enough to show that if s >_{gpo} t = g(t_{1}, …, t_{n}) then s >_{gpo} t_{j} for any j ∈ {1, …, n}. We show it by induction on the size of s.

• If s >_{gpo} t via rule (G2), then it is immediate that s >_{gpo} t_{j}.

• If s = f(s_{1}, …, s_{m}) >_{gpo} t via rule (G1), then for some s_{i}, s_{i} ≥_{gpo} t. • If s_{i} >_{gpo} t then s_{i} >_{gpo} t_{j} by induction.

• If s_{i} = t then, as rule (G1) gives t >_{gpo} t_{j}, so s_{i} >_{gpo} t_{j}. In either of these cases, s >_{gpo} t_{j} by rule (G1). □

Theorem 3 The general path ordering <_{gpo} is well-founded.

Proof. Define ≪ = Λ(fwf (<_{gpo})). Then, as fwf (<_{gpo}) is well-founded, ≪ is well-founded by condition (b) above. As ◁ is well-founded, conditions (i) and (ii) of our Theorem 1 are satisfied.

Then, to show Condition 1(iv), suppose for all s′ ◁ s that s′ ∈ SN = wfp (<_{gpo}), t <_{gpo} s, and t′ is a subterm of t. Then Lemma 9 gives t′ <_{gpo} s. If t′ <_{gpo} s by rule (G1), then s_{i} ◁ s and t′ <_{gpo}^{∗} s_{i}, so s_{i} and t′ are in SN. If t′ <_{gpo} s by rule (G2), then (t′, s) ∈ Λ(<_{gpo}). By condition (c), (t′, s) ∈ Λ(fwf (<_{gpo})) = ≪. Thus Condition 1(iv) is satisfied, and so <_{gpo} is well-founded. □

An appropriate choice of Λ can give us either the lexicographic or multiset path orderings for structured terms [11, Defn 4.22, 4.24]. To do so we let f(s_{1}, …, s_{m}) >_{Λ} g(t_{1}, …, t_{n}) iff either f > g (according to a given well-founded ordering on function symbols) or (s_{1}, …, s_{m}) > (t_{1}, …, t_{n}) in the derived lexicographic or multiset ordering derived from >_{gpo}. Such a Λ satisfies properties (a) to (c) above.

These examples of Λ also have the property that:

if (s′_{i}, s_{i}) ∈ σ then (f(s_{1}, …, s′_{i}, …, s_{n}), f(s_{1}, …, s_{i}, …, s_{n})) ∈ Λ(σ) which ensures that Λ(σ) is closed under context, but is not needed for this more general treatment.

4. Application to Typed Combinators

In [21] Goubault-Larrecq concludes that “Theorem 1 seems to be insufficient to show that every simply-typed λ-term terminates”. He therefore takes notions like “reducibility” and “the substitution of terms for variables” from the classical strong normalisation proof of the simply-typed λ-calculus [19] and generalises them to obtain his Theorem 2 for termination of higher-order path orderings.

As the λ-calculus can be imitated by using the combinators S, K, I a related problem is to prove the strong normalisation for well-typed combinator terms. This result follows easily from the strong normalisation of β-reduction. But to prove the converse, that strong normalisation of β-reduction follows from that of welltyped combinator terms, is not so easy: one needs a translation from λ-terms to combinator terms that preserves reducibility, such as of Akama [1].

We now describe two ways to use our Theorem 1 to prove strong normalisation of well-typed combinator terms. These proofs resemble classic “reducibility” arguments, but do not handle substitution of terms for variables. By Akama [1, Theorem 2.2], this is enough to show strong normalisation of β-reduction.

Thus, the full power of the much more complex [21, Theorem 2] is not necessary for these tasks. However, we have been unable to prove termination of typed combinators using our [8, Theorem 2] as suggested by a referee. Also, although we could prove strong normalisation of the simply-typed λ-calculus by adapting the proof of our Theorem 1, we could not prove it as a corollary of our Theorem 1.

In the examples of this section, we use some of the concepts and notation applicable to term rewriting systems (§5). In particular, we define ctxt σ to be the “closure under contexts” of σ: that is, where C[ ] is a context, and (t, s) ∈ σ, then (C[t], C[s]) ∈ ctxt σ. Likewise we define pctxt (“proper context”): for (t, s) ∈ σ, if t and s are proper subterms of C[t] and C[s], then (C[t], C[s]) ∈ pctxt σ.

4.1. Reduction of Typed Combinator Expressions

Of the usual combinators, the problematic ones are S f g x = f x (g x) and W f x = f x x, since their right-hand-sides duplicate x. Thus, in the untyped setting, these do not satisfy strong normalisation: for example, (SII)(SII) ⟶^{+} (SII)(SII), (W I)(W I) ⟶^{+} (W I)(W I), and W W W ⟶ W W W.

In the typed setting, we can use our Theorem 1 to prove strong normalisation for combinators like S, I, K, B, C, W, but we must actually add extra rules to do so. Note that some rules are only applied to the whole term, whereas others can also be applied to any subterm. We use α, β, γ, … for types, and the notation < on types for the transitive relation given by: α < (α → β) and β < (α → β). Let tyof t denote the type of t, and let t <_{ty} s mean tyof t < tyof s.

We show in detail how to handle only the S combinator, but many other combinators like I, K, B, C, W can be dealt with similarly, and the proof holds for the single system containing all these combinators. We define the relations σ and τ (as inductively defined sets) by rules, as shown below for the combinator S. Then let ρ = ctxt σ ∪ τ. Note that the extra rules (2), (3) and (4) are added only because the proof uses them: for clearly, if ρ ⊇ ρ′, and ρ terminates, then so does ρ′. These rules are motivated by the relation ◁^{∘} of [21, §5]:

Sfgx >_{σ} fx(gx)  (1)
Sfg >_{τ} fx(gx)  if x ∈ SN  (2)
Sf >_{τ} fx(gx)  if g, x ∈ SN  (3)
S >_{τ} fx(gx)  if f, g, x ∈ SN  (4)

with types S : (α→β →γ)→(α→β)→α→γ, f : α→β →γ, g : α→β, x : α.

Note that “SN ” means with respect to ρ: that is, SN = wfp ρ. Thus τ and ρ (but not σ) are being defined, indirectly, in terms of themselves. However the rule (1) preserves the type of a term: so, when it is applied to a subterm, the whole term remains well-typed. The rules for τ change a well-typed term into a well-typed term of <-smaller type. Further, where a rule for reducing a term s depends on another term s′ being in SN, then s′ <_{ty} s. For example, in rule (3), we have Sf : (α→β)→α→γ, where g and x have <-smaller types, g : α→β and x : γ.

That is, for s : α, the set {t | (t, s) ∈ ρ} depends on σ and on {t | (t, s) ∈ τ}, which depends on {s′ ∈ SN | tyof s′ < α}. For given β < α, the set {s′ ∈ SN | s′ : β} depends on {(x, s′′) ∈ ρ | tyof s′ ≤ β}. This ensures a consistent definition, as for ◁^{∘} in [21]. In effect, whether (t, s) ∈ ρ, (t, s) ∈ τ and u ∈ SN are defined inductively on the types of s and of u.

We say t <_{sn1} s if (t, s) ∈ ctxt σ via a reduction in an immediate subterm which is itself in wfp (ctxt σ): that is, where t and s differ only in corresponding immediate subterms t′ and s′ with (t′, s′) ∈ ctxt σ and s′ ∈ wfp (ctxt σ). (Note that the immediate subterms of f x y are f x and y). Lemma 10 Let ≪ = <_{ty} ∪ <_{sn1}, and let ◁ be the immediate subterm relation. Then Condition 1(ii) holds.

Proof. Let (t, s) ∈ ρ and assume ∀s′ ◁ s. s′ ∈ SN. If (t, s) ∈ ρ via rule (2) (where s = Sfg), we have g ∈ SN, so (t, Sf) ∈ ρ by rule (3). As Sf ◁ s, we have Sf ∈ SN, so t ∈ SN ⊆ gbars ◁ {u | u ≪ s} SN. Similar arguments hold where (t, s) ∈ σ ⊆ ρ by rule (1), and where (t, s) ∈ τ ⊆ ρ via rule (3).

If (t, s) ∈ τ ⊆ ρ via rule (4), then we see that the subterms f, g and x of t are in SN, while the subterms fx : β → γ, gx : β and t = fx(gx) : γ are of <-smaller type than S. Thus any ◁-descending chain from t consists of terms in {u | u ≪ s} until reaching a term in SN. That is, t ∈ gbars ◁ {u | u ≪ s} SN.

Finally, in the case where (t, s) ∈ pctxt σ, we have t′ ◁ t and s′ ◁ s such that (t′, s′) ∈ ctxt σ. Since s′ ∈ SN ⊆ wfp (ctxt σ), we have t <_{sn1} s and t ≪ s. Now consider any t′′ ◁ t. Either t′′ = t′ and (t′, s′) ∈ ctxt σ as just discussed, in which case s′ ∈ SN and so t′ ∈ SN, or t′′ is an immediate subterm of s not affected by the reduction from s to t, whence t′′ ∈ SN.

Therefore t ∈ gbars ◁ {u | u ≪ s} SN. □ Theorem 4 Every term is strongly normalising.

Proof. We use our Theorem 1, and Lemmas 4 and 5. Apart from Lemma 10, we need conditions (i) and (ii) of our Theorem 1. Condition (ii) holds as ◁ is wellfounded. Finally, to show condition (i), we show that ≪ is well-founded. Clearly the “smaller type” relation < is well-founded, and it is easy to show (analogously to Theorem 7) that <_{sn1} is well-founded. Then, clearly, <_{ty} ∘ <_{sn1} ⊆ <_{ty}, and so, by Lemma 6(a), <_{ty} ∪ <_{sn1} is well-founded. □

Our rules (2), (3) and (4) were suggested by the definition of ◁^{∘} given just below Remark 13 in [21] (where λx. M ▷^{∘} M[x := N] for N strongly normalising). As in [21], therefore, there is a resemblance between our proof and the classic reducibility argument: for example, for S f g to be in SN, it is necessary that for all x ∈ SN, S f g x ∈ SN, which resembles the condition for reducibility in [19, §6.1]. Likewise, reducibility and our SN are both defined by induction on the type.

4.2. A Second Proof for Typed Combinator Expressions

We now present another way of using our Theorem 1 to prove the same result. This proof was suggested by a presentation of the classic reducibility argument given us by an unnamed referee. It is of independent interest since, unlike the proof in §4.1, it uses a relation ◁ which is distinct from the usual immediate subterm relation. We define ◁ and the reduction relation ρ. Again, it is understood that terms are well-typed. Combinators other than S could be included also.

N_{i} ◁ MN_{1} … N_{i} … N_{n} for 1 ≤ i ≤ n  (5)
M >_{ρ} MN if N ∈ SN  (6)
Sfgxy_{1} … y_{n} >_{σ} fx(gx)y_{1} … y_{n}  (7)
σ ⊆ ρ  (8)
(x′_{i}, x_{i}) ∈ ctxt σ ⇒ fx_{1} … x_{i} … x_{n} >_{ρ} fx_{1} … x′_{i} … x_{n}  (9)

Note that rules (7) to (9) together give ctxt σ ⊆ ρ. These definitions are sound as before, since again, a reduction preserves type or gives a result of <-smaller type, and reduction from s is defined involving SN terms of <-smaller type. Note that, by rule (6), if M, N ∈ SN then MN ∈ SN.

For this proof we define fx_{1} … x_{i} … x_{n} >_{sn1} fx_{1} … x′_{i} … x_{n} where (x′_{i}, x_{i}) ∈ ctxt σ and x_{i} ∈ wfp (ctxt σ). That is, as before, t <_{sn1} s if (t, s) ∈ ctxt σ by means of reduction in a “◁-subterm” which is itself in wfp (ctxt σ).

Also as before, let ≪ = <_{ty} ∪ <_{sn1}. Theorem 5 Every term is strongly normalising.

Proof. We first show that Condition 1(ii) holds. Let (t, s) ∈ ρ and assume that ∀u ≪ s. u ∈ gindy ◁ SN, and ∀v ◁ s. v ∈ SN. If (t, s) ∈ ρ via rule (7), we have f, g, x and each y_{i} ∈ SN, so the combination fx(gx)y_{1} … y_{n} ∈ SN.

If (t, s) = (MN, M) ∈ ρ via rule (6), then t <_{ty} s, so t ≪ s, and, for K ◁ MN, either K = N which is in SN, or K ◁ M and so K ∈ SN.

Finally, where (t, s) ∈ ρ via rule (9), the argument is similar to that before: t <_{sn1} s, and for y ◁ t, there is x ◁ s such that y ≤_{ρ} x, so y ∈ SN.

That is, in each case, t ∈ gbars ◁ {u | u ≪ s} SN, so Condition 1(ii) holds.

From Condition 1(ii), we prove that every term is in SN as in Theorem 4. □

4.3. Strong Normalization for System T

We can also develop the previous proofs to handle the strong normalization of System T, though in each case there is a complication. System T [2] consists of the system of typed combinators as above, with a distinguished type nat, the usual two constructors for this type, Zero : nat and Succ : nat → nat, and the general recursive function R defined by

R Zero f z = z R (Succ n) f z = f n (R n f z)

So to extend the first proof to this situation we add the rules

R Zero f z >_{σ} z  (10)
R (Succ n) f z >_{σ} f n (R n f z)  (11)
R (Succ n) f >_{τ} f n (R n f z)  if z ∈ SN  (12)
R (Succ n) >_{τ} f n (R n f z)  if f, z ∈ SN  (13)
Succ n >_{τ} n  (14)

We now prove Lemma 10 for this extended system. Lemma 11 Consider the system of §4.1, extended by rules (10) to (14). Let ≪ be <_{ty} ∪ <_{sn1}, and ◁ the immediate subterm relation. Then Condition 1(ii) holds.

Proof. Let (t, s) ∈ ρ and assume ∀s′ ◁ s. s′ ∈ SN.

If (t, s) ∈ ρ via rule (10) then t = z ◁ s, so t ∈ SN.

If (t, s) ∈ ρ via rule (11) or rule (12) the argument is as for rules (1) to (3). If (t, s) ∈ ρ via rule (13) then first note that as Succ n ∈ SN, and Succ n >_{τ} n

by rule (14), so n ∈ SN. We now need to consider any ◁-descending chain from t = f n (R n f z), and consider the subterms t′ on such a chain. Since s = R (Succ n) is of type (nat → α → α) → α → α), we see that t : α and its subterms f n : α → α, R n f z : α and R n f : α → α are of <-smaller type than S. Also R n <_{sn1} R (Succ n), since R n is obtained by reducing the strongly normalizing subterm (Succ n). So for all these subterms t′, we have t′ ≪ s. Finally, we have that f, z, n and R are in SN. Thus any ◁-descending chain from t consists of terms in {u | u ≪ s} until meeting a term in SN ; that is, t ∈ gbars ◁ {u | u ≪ s} SN. □

Finally, every term is strongly normalising, proved exactly as in Theorem 4.

4.4. Adapting the second proof to System T

We now show how to adapt the proof of §4.2 to System T. We add the following rules to those given earlier, ie, to rules (6) to (9):

R Zero f z y_{1} … y_{k} >_{σ} z y_{1} … y_{k}  (15)
R (Succ n) f z y_{1} … y_{k} >_{σ} f n (R n f z) y_{1} … y_{k}  (16)
Succ n >_{τ} n  (17)

We define ◁ as before, ie, by rule (5), but we need a different definition of ≪, as follows where <_{sn1} is defined as in §4.2, f \overline{x′} means fx_{1} … x′_{i} … x_{m}, f \overline{x} means fx_{1} … x_{i} … x_{m}, f \overline{x} \overline{y} means f \overline{x} y_{1} … y_{k}, and applications are well-typed.

MN ≪ M  (18)
f \overline{x′} ≪ f \overline{x} \overline{y}  where f \overline{x′} <_{sn1} f \overline{x}  (19)

Lemma 12 ≪ is well-founded.

Proof. We use Lemma 6(d), with ϕ and ψ being the relations given by (18) and (19) respectively. Then we have the following cases for u >_{ϕ} v >_{ψ} w:

• f \overline{x} >_{ϕ} f \overline{x} y >_{ψ} f \overline{x} y′, when u >_{ϕ} w

• f \overline{x} >_{ϕ} f \overline{x} y >_{ψ} f \overline{x′} y, when u >_{ψ} v′ >_{ϕ} w

• f \overline{x} \overline{w} >_{ϕ} f \overline{x} \overline{w} y >_{ψ} f \overline{x′} when u >_{ψ} w so in each case (w, u) ∈ (ψ ∘ (ϕ ∪ ψ)^{∗}) ∪ ϕ.

Since <_{sn1} is well-founded it follows easily that ψ is well-founded, and ϕ is well-founded since M N <_{ty} M. Thus ϕ ∪ ψ = ≪ is well-founded. □ Theorem 6 Every term is strongly normalising.

Proof. In this case we cannot show that Condition 1(ii) holds, but we can show that every term is in gindy ≪ (gindy ◁ SN). Let (t, s) ∈ ρ and assume that ∀u ≪ s. u ∈ gindy ◁ SN, and ∀v ◁ s. v ∈ SN. If (t, s) ∈ ρ via rule (7), then, as in the proof of Theorem 5 we have f, g, x and each y_{i} ∈ SN, so the combination fx(gx)y_{1} … y_{k} ∈ SN.

If (t, s) = (MN, M) ∈ ρ via rule (6), then t ≪ s, so t ∈ gindy ◁ SN. Then for K ◁ MN, either K = N which is in SN, or K ◁ M and so K ∈ SN. Thus t ∈ SN.

If (t, s) ∈ ρ via rule (15), then z and each y_{i} ∈ SN, so t = z y_{1} … y_{k} ∈ SN.

If (t, s) ∈ ρ via rule (16), then we have f, z, Succ n and each y_{i} ∈ SN, and so by rule (17), n ∈ SN. Thus, to get t = f n (R n f z) y_{1} … y_{k}, we need only show R n f z ∈ SN. Now R n f z ≪ R (Succ n) f z y_{1} … y_{k} = s, so R n f z ∈ gindy ◁ SN. Now, for t′ ◁ R n f z, t′ = n, f or z and so t′ ∈ SN. Therefore R n f z ∈ SN.

If (t, s) ∈ ρ via rule (17), then we have t = n ∈ SN.

Finally, where (t, s) ∈ ρ via rule (9), t <_{sn1} s, so t ∈ gindy ◁ SN. Then for y ◁ t, there is x ◁ s such that y ≤_{ρ} x, so y ∈ SN. Thus t ∈ SN.

That is, in each case, t ∈ SN, and, discharging the assumptions as in the proof of Lemma 5 we get s ∈ SN and s ∈ gindy ≪ (gindy ◁ SN). Then we prove that every term is in SN as in our Theorem 1, as both ≪ and ◁ are well-founded. □

5. Application to Term Rewriting Systems

We now apply our Theorem 1 to the special case of a TRS on terms of a firstorder language T (Σ, V) (see [4, §3.1]), thereby showing that our main result from [8] is a special case of our Theorem 1. We consider a binary relation σ, which is the set of substitutional instances of a set of rewrite rules, and so is closed under substitutions. However σ itself is typically not monotonic, ie, compatible with Σcontexts (see [4, Definition 3.1.9]). So we define ctxt σ and pctxt σ as in §4.

In [8] we dealt with the termination of such rewrite relations. In discussing that work we will use “σ” for the relation there called “ρ”, which is the set of substitutional instances of the rewrite rules. Then the rewrite relation is ctxt σ, which here we will call ρ. So SN = wfp ρ = wfp (ctxt σ). The relation ◁ of the previous sections will now be interpreted as the immediate subterm relation.

Recall that in [8] we used a relation <_{dt} = <_{cut} ∪ <_{sn1}, where <_{cut} was chosen by the user, but <_{sn1} was defined as below [8, Definition 3].

Definition 6 ( <_{sn1}, <_{sn2}) Given ρ and <_{cut} we define two further binary relations on terms, <_{sn1} and <_{sn2}.

• t_{1} <_{sn1} t_{0} if t_{0} and t_{1} are the same except that an immediate subterm t′_{0} of t_{0} is in SN and reduces to the corresponding immediate subterm t′_{1} of t_{1}.

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

(that is, in both cases, (t′_{1}, t′_{0}) ∈ ctxt σ).

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. Theorem 7 The relations <_{sn1} and <_{sn2} are each well-founded [7].

Then we apply our Theorem 1 by letting ≪ be the relation <_{dt}^{+}, which is wellfounded if and only if <_{dt} is so. Also let ≪′ be <_{cut}, so ≪ = ≪′ ∪ <_{sn1}. We now reproduce Theorem 2 of [8] in our current notation, as Theorem 8 and Condition 2(i). Condition 2(ii) implies Condition 2(i), is more generally useful, and is used in §6. Condition 2 For all (t, s) ∈ σ,

(i) If ∀s′ ◁^{+} s. s′ ∈ SN then, for all t′ ◁^{∗} t, either t′ ∈ SN or t′ ≪ s.

(ii) For all t′ ◁^{∗} t, either (t′, s) ∈ ◁ ∘ (ρ ∪ ◁)^{∗} or t′ ≪′ s.

Theorem 8 If σ satisfies Condition 2(i) or (ii), ≪ contains <_{sn1} and ≪ is wellfounded, then every term is strongly normalising [8].

Proof. We apply our Theorem 1. Since ◁ is well-founded and we assume ≪ is well-founded, conditions (i) and (ii) of our Theorem 1 are satisfied. It remains only to check that Condition 1(i) holds. In fact, the stronger Condition 1(iv) holds.

Consider (t, s) ∈ ρ, and assume that ∀s′ ◁ s. s′ ∈ SN. As ρ = ctxt σ is closed under context, it follows that any subterm of a strongly normalising term is strongly normalising, so we can assume that ∀s′ ◁^{+} s. s′ ∈ SN. For (t, s) ∈ ρ, there are two cases: (t, s) ∈ σ or (t, s) ∈ ρ \ σ. For the case (t, s) ∈ σ, Condition 2(i) then implies that for t′ ◁^{∗} t, either t′ ∈ SN or t′ ≪ s, and so Condition 1(iv) holds in this case.

We now consider the case (t, s) ∈ ρ \ σ: that is, where a proper subterm of s is reduced, using σ, to the corresponding proper subterm of t. Consider any subterm t′ of t. We show that either t′ ∈ SN or t′ <_{sn1} s, whence t′ ≪ s.

If t′ = t, then t′ <_{sn1} s by definition of <_{sn1}. If t′ is a proper subterm of t, then if there is a corresponding subterm s′ of s such that either t′ = s′ or (t′, s′) ∈ ctxt σ, then s′ and t′ are in SN. Otherwise, there is a proper subterm s′ of s, where s′ is reduced to t′′, so (t′′, s′) ∈ ctxt σ, and t′ is a subterm of t′′. Then s′, t′′ and t′ are all in SN. So Condition 1(iv) holds for this case also. □

We next relate this theorem to known results on constricting derivations, and show how it implies known results relating to the the Knuth-Bendix Ordering, and to dependency pairs. Note that we have already discussed, in §3.2, how the termination of the recursive path orderings [11, Defn 4.22, 4.24] follows from our Theorem 1. We did in fact show, in [8, §3.7], that this also follows from Theorem 8.

We then show how the theorem can be used in a number of specific examples. Further examples may be found in [8]. In these examples, the crux is to find an appropriate definition of ≪′, for this determines ≪ as ≪′ ∪ <_{sn1}. Since we need to choose ≪′ so that ≪ is well-founded, we choose ≪′ well-founded, and such that ≪′ and <_{sn1} satisfy one of the conditions of Lemma 6. Since <_{sn1} is necessarily well-founded, this ensures that ≪ is well-founded.

In many examples of the use of Theorem 8, the argument went as follows. We let <_{sn2} be the set of those reductions where a strongly normalising proper subterm is reduced, so <_{sn1} ⊆ <_{sn2}, and <_{sn2} is also necessarily well-founded, by Theorem 7. Then, using <_{sn2} in place of <_{sn1}, we prove that ≪′ ∪ <_{sn2} is well-founded by proving that ≪′ is well-founded and then using Lemma 6 to prove that the union is well-founded, often by proving that ≪′ ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ ≪′.

5.1. Constricting Derivations

For a rewrite system on a first-order language (where the reduction relation is closed under context), a “constricting derivation” has been defined as an infinite reduction sequence where each reduction occurs at a subterm t whose proper subterms are all strongly normalising [12]. For a rewrite relation ρ = ctxt σ, we define a constricting reduction by: (t, s) ∈ constrict σ iff (t, s) ∈ σ and the proper subterms of s are in wfp ρ. Here, ◁ is the immediate subterm relation, and <_{sn1} is defined as in §5. The following results are easily proved by methods similar to those of [14]. Lemma 13 For all binary relations σ and τ:

(i) σ ∘ τ is well-founded if and only if τ ∘ σ is well-founded (ii) if τ is well-founded then wfp (τ^{∗} ∘ σ) = wfp (σ ∪ τ) (iii) if τ is well-founded and τ ∘ σ ⊆ σ ∘ τ^{∗}, then wfp (σ ∪ τ) = wfp σ. The following theorem encapsulates mostly known results, for example Lemma 1

of [22] resembles: “if (23) then (26)”, and Proposition 1 of [5] is: “if (26) then (25)”. Theorem 9 The following are equivalent, where ρ = ctxt σ:

(constrict σ ∘ ◁^{∗}) ∪ <_{sn1}  is well-founded  (20)
constrict σ ∘ ◁^{∗} ∘ <_{sn1}^{∗}  is well-founded  (21)
◁^{∗} ∘ <_{sn1}^{∗} ∘ constrict σ  is well-founded  (22)
<_{sn1}^{∗} ∘ constrict σ ∘ ◁^{∗}  is well-founded  (23)
ρ ∘ ◁^{∗}  is well-founded  (24)
ρ ∪ ◁  is well-founded  (25)
ρ  is well-founded  (26)

Proof. (22) ⇒ (26): If t_{0} is not in SN = wfp ρ, then let t′_{0} be a minimal subterm of t_{0} which is not in SN — so the proper subterms of t′_{0} are in SN. Consider any infinite sequence of reductions from t′_{0} — these cannot all be reductions of proper subterms as the latter are in SN, so find t′′_{0} and t_{1} in this infinite sequence such that (t′′_{0}, t′_{0}) ∈ (ctxt σ \ σ)^{∗} and (t_{1}, t′′_{0}) ∈ σ. Now all proper subterms of t′_{0}, of t′′_{0} and of all terms between them in the reduction sequence are in SN. So (t_{1}, t_{0}) ∈ ◁^{∗} ∘ <_{sn1}^{∗} ∘ constrict σ, and as t_{1} ∉ SN, a (◁^{∗} ∘ <_{sn1}^{∗} ∘ constrict σ)- sequence can be continued. Similar proofs are at, eg, [3, Theorem 6], [22, Lemma 1].

(21) ⇔ (22) ⇔ (23): these follow from Lemma 13(i).

(20) ⇔ (23) and (24) ⇔ (25): use Lemma 13(ii) since <_{sn1} is well-founded.

(26) ⇒ (25) : follows from Lemma 13(iii), as ◁ ∘ ρ ⊆ ρ ∘ ◁, as ρ is monotonic.

(25) ⇒ all others : since every relation mentioned is contained in (ρ ∪ ◁)^{+}. □ We now link Theorem 9 with Theorem 8, by some simple proofs. Note that

Condition 2(i) in §5 simply says: if (t′, s) ∈ constrict σ ∘ ◁^{∗} then t′ ∈ SN or t′ ≪ s.

Let τ = (constrict σ ∘ ◁^{∗}) ∪ <_{sn1}. We show SN = wfp ρ ⊆ wfp τ. Since τ ⊆ (ρ ∪ ◁)^{+}, so wfp (ρ ∪ ◁) ⊆ wfp τ. By Lemma 13(iii), wfp ρ = wfp (ρ ∪ ◁).

Then, we can use Theorem 8 to prove (20) implies (26). Assume (20) of Theorem 9, that is, τ is well-founded. Let ≪ = τ. Then Condition 2(i) holds trivially, ≪ ⊇ <_{sn1} and ≪ is well-founded. Hence, by Theorem 8, ρ is well-founded.

The converse is also easy to prove, giving an alternative proof of Theorem 8. Assume (20) ⇒ (26); we will prove Theorem 8. Suppose the assumptions of Theorem 8 hold, and we want to show its conclusion, (26). We show (20), ie, that τ is well-founded. Let (t, s) ∈ τ. Then, if (t, s) ∈ <_{sn1}, then t ≪ s. Otherwise, (t, s) ∈ constrict σ ∘ ◁^{∗} and so t ∈ SN or t ≪ s by Condition 2(i). Now SN ⊆ wfp τ, as shown above, so (t, s) ∈ τ implies t ∈ wfp τ or t ≪ s, where ≪ is well-founded. Thus any τ-descending chain either terminates or hits a member of wfp τ: that is, every s ∈ bars τ (wfp τ). So, by Lemma 3(ii), every s ∈ wfp τ, as required.

5.2. 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)  (27)
s = k^{n}(t) for some n > 0  (28)
s = f(\overline{s}) and t = g(\overline{t}) where f > g  (29)
s = f(\overline{s}), t = f(\overline{t}) and (\overline{t}, \overline{s}) ∈ lex (<_{kb})  (30)

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

Proof. We define s ≫′ t iff w(s) ≥ w(t) and either one of the rules (27) or (29) holds, or s >_{kw1} t, where <_{kw1} is defined by:

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

To show ≪′ is well-founded, we have that each of rules (27), (29) and (31) provides a well-founded relation and we can apply Lemma 6 repeatedly to show that their union is well-founded, noting that if s >_{kw1} t then w(s) ≥ w(t). Further, <_{sn1} ⊆ <_{kw1}, so ≪ = ≪′ ∪ <_{sn1} = ≪′ is well-founded.

To show Condition 2(ii), suppose that l >_{kb} r and that r′ is a subterm of r.

• First, let r′ = r. Assume that all proper subterms of l are in SN, in which case, if l >_{kb} r by rule (30), then l >_{kw1} r, so l ≫′ r. If l >_{kb} r by rules (27) or (29), then l ≫′ r, and if l >_{kb} r by rule (28) then l ▷^{+} r.

• Now suppose r′ is a proper subterm of r, so w(r) ≥ w(r′).

• If w(r′) < w(r) or w(r) < w(l) then w(l) > w(r′), so l ≫′ r′ by rule (27).

• If w(l) = w(r) = w(r′) then r = k^{n}(r′) for some n > 0, and so l >_{kb} r

by either (28) or (30) (as the g of (29) cannot be k). • If l >_{kb} r by (28) then l ▷^{+} r′.

• If l >_{kb} r by (30), then, for some l_{1}, r_{1}, we must have l = k(l_{1}), r = k(r_{1}), l_{1} >_{kb} r_{1} and r′ is a subterm of r_{1}, so (r′, l) ∈ ◁ ∘ <_{kb} ∘ ◁^{∗}, so satisfying Condition 2(ii). □

5.3. Dependency Pairs

Arts & Giesl [3] 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 “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. Here 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. In [3], the relations ≾ and ≺ below were a quasi-order and its strict part, but in subsequent papers [18], [22] these relations needed only to be a reduction pair, as defined next. Definition 7 A reduction pair (≿, ≻) consists of a quasi-ordering (ie, a reflexive and transitive relation) ≿, which is closed under contexts (monotonic), and a wellfounded ordering ≻, where both are closed under substitutions and ≻ is compatible with ≿, ie either ≿ ∘ ≻ ⊆ ≻ or ≻ ∘ ≿ ⊆ ≻. (Some papers say ≿ ∘ ≻ ⊆ ≻ \underline{and} ≻ ∘ ≿ ⊆ ≻ here, apparently because it makes some proofs simpler). We now state and prove the analogue, for reduction pairs, of the “sufficiency” part of [3, Theorem 7]. Theorem 11 If there is a reduction pair (≿, ≻) 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 that ≿ and ≻ 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 (either with or without ♯), as neither (a) nor (b) nor the requirement that ≿ be closed under context require it, whence the compatibility condition cannot require it.

For a constructor symbol c and defined symbol d, we define ≪′:

s^{♯} ≺ t^{♯} ⟹ s ≪′ t  (32)
c(x) ≪′ d(y)  (33)

Because ≺ is well-founded and, by the remark above, rule (32) does not give any case of c(x) ≫′ d(y), it follows that ≪′ is well-founded.

To show that ≪′ ∪ <_{sn1} is well-founded, in the case ≺ ∘ ≾ ⊆ ≺, we use Lemma 6(a), showing that ≪′ ∘ <_{sn1} ⊆ ≪′ ; in the case ≾ ∘ ≺ ⊆ ≺, we use Lemma 6(b), showing <_{sn1} ∘ ≪′ ⊆ ≪′.

In the case that ≺ ∘ ≾ ⊆ ≺, suppose that t ≫′ u >_{sn1} v. If t ≫′ u by rule (33) then t ≫′ v by the same rule. If t ≫′ u by rule (32) then t^{♯} ≻ u^{♯}, and a proper subterm u′ of u is rewritten to a corresponding subterm v′ of v. As ≾ is closed under substitution, assumption (a) gives us that u′ ≿ v′. Then, since ≿ is closed under context, u^{♯} ≿ v^{♯}, and so t^{♯} ≻ v^{♯} and t ≫′ v.

In the case that ≾ ∘ ≺ ⊆ ≺, suppose that t >_{sn1} u ≫′ v. If u ≫′ v by rule (33) then t ≫′ v by the same rule. If u ≫′ v by rule (32) then u^{♯} ≻ v^{♯}, where a proper subterm t′ of t is rewritten to a corresponding subterm u′ of u, and we have t′ ≿ u′, t^{♯} ≿ u^{♯}, t^{♯} ≻ v^{♯} and t ≫′ v.

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

• the head of r′ is a constructor symbol in r, in which case lσ ≫′ r′ by (33)

• 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 so l^{♯} ≻ r_{1}^{♯} ; then l^{♯}σ ≻ r_{1}^{♯}σ (since ≻ is closed under substitution), and lσ ≫′ r_{1}σ = r′ by (32)

• 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. □

5.4. A non simplification ordering

Example 5 of [10], 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. That is, as f(f(x)) is embedded in f(g(f(x))), and the embedding is included in every simplification ordering, every simplification ordering orients that rule in the reverse direction.

But Theorem 8 is not limited to simplification orderings. We define ≪′ 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 [10]. Thus f(f(x)) ≫′ f(g(y)), f(f(x)) ≫′ g(y), and f(f(x)) ≫′ f(x). Finally, any subterm of x is a proper subterm of f(f(x)). Thus Condition 2(ii) is satisfied. Clearly also, rewriting a subterm cannot increase the number of consecutive f symbols, so <_{sn1} ∘ ≪′ ⊆ ≪′ (and likewise ≪′ ∘ <_{sn1} ⊆ ≪′). Thus ≪ = ≪′ ∪ <_{sn1} is well-founded by Lemma 6. Therefore the system terminates, by Theorem 8.

5.5. The factorial example

Example 21 of [10] 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} where terms are compared by comparing their head symbols, using the following ordering: F > × > + > S, and also F > P. But we need to define ≪′ to be the union of <_{h} and the following additional cases

F (S(x)) ≫′ F (P (S(x))) F (S(x)) ≫′ 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 [10, Examples 21, 25] are based on interpreting arguments to the function symbols as natural numbers.

To verify Condition 2(ii), it is reasonably easy to see that for each (r′, l) where l → r is a rewrite rule and r′ is a subterm of r, 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′ ≪′ l).

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

Suppose t ≫′ u >_{sn2} v. We consider the cases for t ≫′ u.

• If t >_{h} u then clearly t >_{h} v, as u and v have the same head symbol.

• 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′)) ≫′ v.

• Otherwise we need to consider specific cases:

u = F (P (S(x))), S(x) ⟶ x where S(x) ∈ SN, v = F (P (x)):

in this case, t ≫′ v u = F (P (S(x))), P (S(x)) ⟶ x where P (S(x)) ∈ SN, v = F (x):

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): as S(y) ⟶ y and S(y) ∈ SN, so t = F (S(S(y)) >_{sn2} F (S(y)) >_{sn2} F (y) = v.

Thus ≪′ ∪ <_{sn2} is well-founded and the system terminates by Theorem 8.

6. Modular Proofs of Termination

A rewrite system can be defined by taking the union of two terminating systems. It is desirable to reduce a proof of termination of such a system into two smaller proofs of termination of smaller systems, which is possible under certain conditions (see, eg, [4, §9.2], [24], [16]), but not in general. We show how to use Theorem 8 in certain cases to obtain modular proofs of termination. The assumptions required of the component systems appear where they first become relevant, and in Theorem 12.

Let R_{0} be a set of rewrite rules, in a first-order language, where the function symbols appearing in the rules are from the set F_{0}. Note, however, that the variables appearing in those rules may be replaced by any term (which may contain function symbols outside F_{0}). The set of substitution instances of the rules in R_{0} is the relation σ_{0}, with corresponding rewrite relation ρ_{0} = ctxt σ_{0}.

We consider the case where the rewrite relation ρ_{0} has been proved terminating by any method, with only the extra condition that the rules of R_{0} be right-linear: that is, no variable appears more than once on the right-hand side of a rule. This is a similar but stronger condition than the “non-duplicating” requirement of some modularity theorems (eg, [4, Thm 9.2.4]). Thus we define the R_{0}-property, (in which (ii) and (iv) are obviously necessary for any terminating system), and assume throughout that R_{0} satisfies it. The R_{0}-property is important for the next lemma. Definition 8 (R_{0}-property) A rule satisfies the R_{0}-property if

(i) its function symbols are in the set F_{0} (ii) its left-hand side is not a variable (iii) no variable appears more than once in the right-hand side (iv) its right-hand side variables also appear on the left-hand side.

Lemma 14 Let σ be the set of substitution instances of a set of rules satisfying the R_{0}-property. Then

(i) For f ∉ F_{0} and (t, s) ∈ σ, if t′ = f(\overline{t}) ◁^{∗} t then t′ ◁^{+} s. (ii) Let τ be a relation such that for (t, f(\overline{t})) ∈ τ, f ∉ F_{0}. Then σ ∘ pctxt τ ⊆ (pctxt τ)^{∗} ∘ σ.

We then consider a second rewrite system ρ_{1} = ctxt σ_{1} whose “defined symbols” are from a set of new symbols F_{1}, where F_{0} ∩ F_{1} = ∅. That is, for (t, s) ∈ σ_{1}, s is of the form f(\overline{s}), for some f ∈ F_{1} and some sequence \overline{s} of terms. Note that, unlike in some modularity theorems (eg, [4, Thm 9.2.4]), rules used to define ρ_{1} may contain symbols from F_{0}. The system ρ_{1} is assumed to have been proved terminating using Theorem 8 above: that is, by defining a relation ≪′_{1} such that ≪_{1} = ≪′_{1} ∪ <_{sn1} is well-founded, where <_{sn1} is defined in terms of ρ_{1} only. Then let ρ = ρ_{0} ∪ ρ_{1}.

Our proof involves <_{sn2}, as described after Theorem 8. The key is to define a relation ≪′: we use ≪′ = ≪′_{0} ∪ ≪′_{1}, where ≪′_{0} is a relation derived from R_{0}. To help prove ≪′ ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ ≪′ we assume ≪′_{1} satisfies the ≪′_{1}-property: Definition 9 (≪′_{1}-property) A relation ≪′_{1} satisfies the ≪′_{1}-property if, for any relation σ, ≪′_{1} ∘ pctxt σ ⊆ (pctxt σ)^{∗} ∘ ≪′_{1}.

In fact, the ≪′_{1}-property could be weakened, to apply only to certain choices of σ, and to match (d) instead of (a) of Lemma 6, and Theorem 12 still holds. The example in §5.5 satisfies only the weaker condition.

To define ≪′_{0} we first define ◁_{0} and ctxt_{0}, and then a set of rules R_{≪0}: Definition 10 (◁_{0}) t ◁_{0} f(…, t, …) if f ∈ F_{0}. Definition 11 (ctxt _{0}) For (t, s) ∈ σ, if the subterms of C[x] which contain x have head symbols in F_{0} then (C[t], C[s]) ∈ ctxt_{0} σ. Definition 12 (R_{≪0}) (r′_{0}, l_{0}) ∈ R_{≪0} iff r′_{0} is not a variable and there exists r_{0} such that r′_{0} ◁_{0}^{∗} r_{0}, (r_{0}, l_{0}) ∈ ctxt_{0} R_{0} and (r_{0}, l_{0}) satisfies the R_{0}-property.

Then let ≪′_{0} be the set of substitution instances of the rules in R_{≪0}. Clearly ≪′_{0} ⊆ (ρ_{0} ∪ ◁)^{+} so ≪′_{0} is well-founded.

We now can define ≪′ = ≪′_{0} ∪ ≪′_{1}. If we assume that for t ≪′_{1} f(\overline{t}), f ∈ F_{1}, and that ≪′_{1} is well-founded, then ≪′ is well-founded as ≪′_{0} ∘ ≪′_{1} = ∅. Then let ≪ = ≪′ ∪ <_{sn2}. Since <_{sn2} is well-founded (Theorem 7), to show that ≪ is well-founded it would suffice to show ≪′ ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ ≪′, but this does not actually hold. Instead, we can choose a suitable subset <′_{sn2} of <_{sn2} such that ≪ = ≪′ ∪ <′_{sn2} and prove that ≪ is well-founded in two steps.

We define τ_{1}: (t, f(\overline{t})) ∈ τ_{1} iff f ∉ F_{0}. Recall that SN means the set of strongly normalising terms, ie SN = wfp (ctxt ρ), where ρ = ρ_{0} ∪ ρ_{1}. We define ρ_{SN}: (t, s) ∈ ρ_{SN} iff s ∈ SN. Thus <_{sn2} = pctxt (σ ∩ ρ_{SN}). Then the required relation <′_{sn2} is given in the following lemma, whose proof is detailed but tedious, and which has been proved in Isabelle ([9], file hier.ML), as have all these results. Lemma 15 Let <′_{sn2} = ctxt (τ_{1} ∩ pctxt (σ_{0} ∩ ρ_{SN})) ∪ pctxt (σ_{1} ∩ ρ_{SN}). Let R_{0} satisfy the R_{0}-property. Then <′_{sn2} ⊆ <_{sn2} ⊆ ≪′_{0} ∪ <′_{sn2}. Lemma 16 Assume hypotheses (i), (ii) and (iv) of Theorem 12 below. Then

(i) ≪′_{1} ∪ <_{sn2} is well-founded; so ≪′_{1} ∪ <′_{sn2} is well-founded.

(ii) ≪′_{0} ∘ τ_{1} = ∅ (so ≪′_{0} ∘ ≪′_{1} = ∅) and ≪′_{0} ∘ <′_{sn2} ⊆ <′_{sn2}^{∗} ∘ ≪′_{0}.

(iii) ≪′_{0} ∪ (≪′_{1} ∪ <′_{sn2}), that is, ≪, is well-founded.

Proof.

(i) This follows from Lemma 6(a) as ≪′_{1} satisfies the ≪′_{1}-property. (ii) Recall that, for f(\overline{t}) ≪′_{0} s, f ∈ F_{0}, so ≪′_{0} ∘ τ_{1} = ∅. Then we use the fact

that <′_{sn2} is of the form (τ_{1} ∩ X) ∪ pctxt Y ∪ pctxt Z and Lemma 14(ii). (iii) As ≪′_{0} and, by (i), ≪′_{1} ∪ <′_{sn2} are well-founded, we can use (ii) and Lemma 6(a)

to get that ≪′_{0} ∪ (≪′_{1} ∪ <′_{sn2}) is well-founded. Then, by Lemma 15, this is ≪′_{0} ∪ (≪′_{1} ∪ <_{sn2}) = ≪′ ∪ <_{sn2} = ≪. □

Lemma 17 If R_{0} satisfies the R_{0}-property, σ_{0} and ≪′_{0} satisfy Condition 2(ii).

Proof. Let (t, s) ∈ σ_{0}, an instance of the rule (t_{0}, s_{0}) ∈ R_{0}, and let t′ ◁^{∗} t. If t′ ◁_{0}^{∗} t, then (t′, s) ∈ ≪′_{0}. Otherwise, there must be f ∉ F_{0} and a sequence \overline{t} of terms with t′ ◁^{∗} f(\overline{t}) ◁^{∗} t, and so, by Lemma 14(i), t′ ◁^{∗} f(\overline{t}) ◁^{+} s, as required.□ Theorem 12 Assume that

(i) rules R_{0} satisfy the R_{0}-property, and give a terminating rewrite system ρ_{0}, (ii) relation ≪′_{1} is well-founded and satisfies the ≪′_{1}-property, (iii) σ_{1} and ≪′_{1} satisfy Condition 2(ii), (iv) for (t, s) ∈ σ_{1} ∪ ≪′_{1}, s is of the form f(\overline{s}), with f ∉ F_{0}.

Then ρ = ρ_{0} ∪ ρ_{1} is well-founded where ρ_{1} = ctxt σ_{1}.

Proof. From assumption (iii) and Lemma 17, we can see that σ_{0} ∪ σ_{1} and ≪′_{0} ∪ ≪′_{1} satisfy Condition 2(ii). Then, since, by Lemma 16(iii), ≪ = ≪′_{0} ∪ ≪′_{1} ∪ <_{sn2} is well-founded, and <_{sn1} ⊆ <_{sn2}, the result follows from Theorem 8. □

7. An Incremental Path Ordering

We now use the previous results to describe a generalisation to an incrementally defined ordering of the general path ordering of Dershowitz & Hoot [13].

The incremental path ordering <_{ipo} or ipo (“modular path ordering” could be used but mpo also stands for “multiset path ordering”) is then defined as below, where \overline{s} = s_{1}, …, s_{m}, \overline{t} = t_{1}, …, t_{n}, s = f(\overline{s}) and t = g(\overline{t}). Let Λ(ipo) (or <_{Λ}) be an ordering on lists of terms, derived from <_{ipo}, satisfying conditions given later: the common examples for Λ are the lexicographic or multiset extensions of <_{ipo}. As before, the rules R_{0} satisfy the R_{0}-property. Again, let σ_{0} be the set of substitution instances of the rules in R_{0}, and let the corresponding rewrite relation ρ_{0} = ctxt σ_{0} be well-founded. Let < be a well-founded ordering on the function symbols.

\frac{f ∉ F_{0}  s_{i} ≥_{ipo} t}{s >_{ipo} t}  (34)

\frac{f = g \overline{s} >_{Λ} \overline{t} f ∉ F_{0} ∀i ∈ \{1, …, n\}. s >_{ipo} t_{i}}{s >_{ipo} t}  (35)
\frac{f > g f ∉ F_{0} ∀i ∈ \{1, …, n\}. s >_{ipo} t_{i}}{s >_{ipo} t}  (36)
\frac{(t, s) ∈ σ_{0}}{s >_{ipo} t}  (37)
\frac{(t, s) ∈ pctxt ipo}{s >_{ipo} t}  (38)

Rules (38) and (37) imply ρ_{0} = ctxt σ_{0} ⊆ <_{ipo} and that ipo is closed under contexts. In the Isabelle formulation ipo is an inductively defined set, where ipo is the set of all pairs whose inclusion in ipo is established by the rules given.

Note that if F_{0}, and so R_{0} and σ_{0} are empty, then this reduces to the recursive path ordering. In that case, if Λ is the lexicographic or multiset ordering, then rule (35) implies (38). Also, in that case, the rules themselves imply that the defined path ordering is transitive, and this fact is used in some proofs of well-foundedness (see, eg, [13]). But when F_{0}, R_{0} and σ_{0} are non-empty, it does not seem clear whether <_{ipo} is transitive, and our proof of termination does not depend on it.

As in [8], we define a function fwf (“from well-founded”) which maps a binary relation σ to a binary relation fwf σ thus: (t, s) ∈ fwf σ iff (t, s) ∈ σ and s ∈ wfp σ.

Our proof needed the following conditions on Λ. Related conditions are discussed in §3.2. All are satisfied by the lexicographic and multiset extensions of an ordering.

(a) Λ is a monotonic function

(b) if σ is well-founded then Λ(σ) is well-founded (c) if all s_{i} are in wfp τ and if (t, s) ∈ Λ(τ), then (t, s) ∈ Λ(fwf τ)

(d) if (s′_{i}, s_{i}) ∈ τ then ((s_{1}, …, s′_{i}, … s_{m}), (s_{1}, …, s_{i}, … s_{m})) ∈ Λ(τ).

The termination proof combines the proof of Theorem 12 above with ideas from the termination proof of the recursive path ordering in [8, §3.7]. We omit details, but note that it has been checked using Isabelle, see [9], in snabs/ipodef.{thy,ML}. Theorem 13 The relation <_{ipo} is well-founded if:

(i) rules R_{0} satisfy the R_{0}-property, and give a terminating rewrite system ρ_{0} = ctxt σ_{0}, (ii) the relation < on the function symbols (see rule (36)) is well-founded, and (iii) the ordering extension function Λ satisfies conditions (a)-(d) listed above.

8. Observations and Conclusion

Our main Theorem 1 about termination of reduction rules generalises two previous quite general theorems in [8] and the first theorem (JGL1) in [21].

The following picture emerges. JGL1, i.e. Goubault-Larrecq’s Theorem 1 [21], can handle ARSs but cannot handle reducibility arguments like those required for combinators or the simply-typed λ-calculus. Our Theorem 8, i.e. [8, Theorem 2], handles TRSs but also cannot handle such reducibility arguments. Our new Theorem 1 handles both TRSs and some reducibility arguments such as those involved in the proofs of termination of the typed combinator systems. One of our proofs takes advantage of the abstract setting, using a relation ◁ which is not the usual immediate subterm relation. However our theorem had to be modified to reason indirectly about substitutions for the simply-typed λ-calculus. What is the exact relationship between [21, Theorem 2] and our Theorem 1 ?

Our Theorem 1 can be used to prove termination of a rewrite system defined incrementally. We showed in [8] that our Theorem 1 strictly subsumes the termination of the recursive path ordering. Since [16] contains a very general set of results which are nonetheless based on the recursive path ordering, neither [16] nor the work in §7 subsume each other. A goal is to unify the work in §7 and [16].

Our proofs were machine-checked in Isabelle/HOL. This was particularly valuable for §6, where our initial paper proofs turned out to be wrong, as the correct choice of ≪′_{2} was particularly difficult to find. Further, the possible instantiation of a variable by a term headed by a symbol in either F_{0} or F_{1} complicated matters as discussed following [16, Proposition 1]. Also, in §4.1 the Isabelle proof confirmed the validity of the rather tricky argument for the soundness of the mutually recursive definitions of SN, ρ and τ.

Acknowledgements

We thank Linda Postniece for researching the criteria for well-foundedness of a union of well-founded orderings, Jean Goubault-Larrecq and Hubert Comon for pointers to the literature, and Thorsten Altenkirch and Jürgen Giesl for helpful discussions. Finally, we thank some anonymous referees for very helpful comments.

References

1. Y Akama. A λ-to-CL Translation for Strong Normalization. In Proc. Typed Lambda Calculi and Applications (TLCA’97), LNCS 1210, 1–10, Springer, 1997.

2. T Altenkirch and J Chapman. Tait in one big step. In Proc. MSFP 2006, Electronic Workshops in Computing, British Computer Society, 2006.

3. T Arts and J Giesl. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236 (2000), 133–178, 2000.

4. F Baader and T Nipkow. Term Rewriting and All That. CUP, 1998

5. C Borralleras, M Ferreira and A Rubio. Complete Monotonic Semantic Path Orderings. In Proc. CADE-17, LNCS 1831, 346–364, Springer, 2000.

6. W Buchholz. Proof-theoretic analysis of termination proofs. Annals of Pure and Applied Logic 75 (1995), 57–65.

7. J E Dawson and R 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.

8. J E Dawson and R Goré. A General Theorem on Termination of Rewriting. In Proc. Computer Science Logic (CSL 2004), LNCS 3210, 100–114, 2004.

9. J E Dawson. Isabelle code, http://web.rsise.anu.edu.au/^{∼}jeremy/isabelle

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

11. N Dershowitz & D A Plaisted. Rewriting. In Alan Robinson & Andrei Voronkov, eds, Handbook of Automated Reasoning, 535–610, Elsevier, 2001.

12. N Dershowitz. Termination Dependencies (Extended Abstract). In Proc. Sixth Int’l Workshop on Termination (WST ’03), A Rubio, ed., Valencia, Spain, pp. 27–30.

13. N Dershowitz & C Hoot. Natural Termination. TCS 142 (1995), 179–207.

14. H Doornbos & B Von Karger. On the Union of Well-Founded Relations. L. J. of the IGPL 6 (1998), 195–201.

15. M A E Dummett. Elements of intuitionism. Clarendon Press, 1977.

16. M-L Fernández, G Godoy, A Rubio. Recursive Path Orderings Can Also Be Incremental. In Proc. LPAR2005, LNCS 3835, 230–245, Springer, 2005.

17. O Fissore, I Gnaedig and H Kirchner. Termination of Rewriting with Local Strategies. Electronic Notes in Theoretical Computer Science 58, 2001.

18. J Giesl, T Arts, and E Ohlebusch. Modular Termination Proofs for Rewriting Using Dependency Pairs. Journal of Symbolic Computation 34(1):21–58, 2002.

19. J-Y Girard, Y Lafont and P Taylor. Proofs and Types. CUP, 1990.

20. I Gnaedig and H Kirchner. Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations, LNCS 4600, 44–67, Springer, 2007.

21. J Goubault-Larrecq. Well-founded recursive relations. In Proc. CSL’2001, LNCS 2142, 484–497, Springer, 2001.

22. N Hirokawa and A Middeldorp. Dependency Pairs Revisited. In Proc. Rewriting Techniques and Applications (RTA-04), LNCS 3091, 249–268, Springer, 2004.

23. S C Kleene and R E Vesley. The foundations of intuitionistic mathematics: especially in relation to recursive functions. North-Holland, 1965.

24. Y Toyama and J W Klop and H P Barendregt. Termination for direct sums of left-linear complete term rewriting systems. J of the ACM 42(6):1275–1304, 1995.