Termination of Abstract Reduction Systems

Jeremy E. Dawson and Rajeev Goré

Logic and Computation Program, NICTA^{∗}and

Automated Reasoning Group

Australian National University, Canberra, ACT 0200, Australia

Jeremy.Dawson@nicta.com.au  Rajeev.Gore@anu.edu.au

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 according to some formal syntax. 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 [4], or closed under context [15], in that if C[ ], a term with a “hole”, is the context, and l reduces to r, then C[l] reduces to C[r]. There are several general methods capturing termination of such term rewriting systems [2, 10, 6].

Recently, Jean Goubault-Larrecq [14] has proved termination results for the more general setting of an abstract reduction system (ARS) where objects need not have a term structure and so there is no monotonicity assumption or subterm relation. Where proofs for TRSs involve the subterm relation, he uses an arbitrary well-founded relation ◁ in a similar way. His Theorem 1 is the result of “chasing generalizations and simplifications” of earlier work and “subsumes … most path-orderings of the literature” [14].

While the theorems from [6] and [14] use remarkably similar ideas, it was frustrating to see that none actually subsumed the other, even though [6] applies to TRSs and [14] applies to ARSs. Indeed, there is something in common between the two results: a more general theorem that subsumes both.

We first present this more general theorem and its proof in §2. Then, in §3, we show that it generalises [14, Theorem 1] and [6, Theorem 2], and we discuss its application to constricting derivations. 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 [14, Theorem 1]. Thus, our theorem handles most path-orderings in the literature and the reducibility method typically used for typed combinators.

In the longer paper [7] we apply our theorem to the general path ordering of Dershowitz & Hoot [10], and adapt our theorem to show strong normalisation for the simply-typed λ-calculus. We also use our techniques to give a different proof of Goubault-Larrecq’s much more complicated Theorem 2 [14]. His theorem generalises [14, Theorem 1], handles the reducibility argument, and encompasses explicit reasoning about substitutions for handling the simply-typed λ-calculus.

Commonly, a rewrite system can be defined by taking a base system, known to be terminating, and adding new function symbols and rules to it. 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 [6]. A more complex variant of the result covers the example in [6, §3.6].

Our proofs were formalised and machine-checked in the theorem prover Isabelle/HOL: see [8], directories snabs,snlc. This was particularly valuable for §5, where our initial paper proofs turned out to be wrong, as the choice of ≪′_{2} was particularly difficult to get right. Further, the possible instantiation of a variable by a term headed by a symbol in either F_{0} or F_{1} complicated matters: see the discussion following [12, 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 τ.

∗National ICT Australia is funded by the Australian Government’s Dept of Communications, Information Technology and the Arts and the Australian Research Council through Backing Australia’s Ability and the ICT Research Centre of Excellence programs.

Copyright copyright 2007, Australian Computer Society, Inc.

This paper appeared at Computing: The Australasian Theory Symposium (CATS2007), Ballarat, Australia. Conferences in Research and Practice in Information Technology (CRPIT), Vol. 65. Joachim Gudmundsson and Barry Jay, Eds. Reproduction for academic, not-for profit purposes permitted provided this text is included.

1.1 Notation, Terminology, Definitions and Basic Lemmas

We assume 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 will 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 the relational composition of relations σ and ρ: 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 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 [6], on term rewriting systems, dealt with the well-founded-ness of the closure under context of a relation called ρ. In contrast, we are dealing here with an abstract reduction system, usually calling the reduction relation ρ. So concepts such as “strongly normalising”, “reduction”, etc, relate to ρ, and not, even when discussing structured terms, to the closure of ρ under context. Furthermore, in the ARS setting, we use an arbitrary relation where we used the immediate subterm relation in the TRS setting.

In [6] 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 [6, §2.2]. Clearly, SN ⊆ ISN. We now define gindy as a generalised notion of “inductively” for an arbitrary relation σ in place of the immediate subterm relation isubt. Use of gindy enables us to express the principle of well-founded induction succinctly: it says that 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 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 [14] for a more 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 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:

(a) S ⊆ gbars σ Q S

(b) 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 equivalent 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 [14].

Definition 4 (wfp, bars) (a) s ∈ bars σ S iff s ∈ gbars σ U S (“S bars s in σ”)

(b) s ∈ wfp σ iff s ∈ bars σ ∅ (“s accessible in σ ”).

Thus SN = wfp ρ and ISN = gindy isubt SN. Now from Lemma 1 we get the following characterisation of bars, which was given as a definition in [14]: s ∈ bars σ S if every infinite decreasing σsequence s_{0} >_{σ} s_{1} >_{σ} s_{2} >_{σ} … meets S, ie, for some k, s_{k} ∈ S.

Our Lemma 3 below generalises [6, Lemma 2]. It relies on the gbars-induction principle, which is analogous to the principles of well-founded induction, and of bars-induction (see [14, Proposition 1]). It is generated automatically by the Isabelle theorem prover from the inductive definition of gbars above. We write P s to mean that object s satisfies property P.

Proposition 2 (gbars-induction) For sets Q and S, and any property P, if

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

(b) for every s ∈ Q, if ∀t. (t, s) ∈ σ ⇒ P t, then P s

then every s ∈ gbars σ Q S satisfies P.

Lemma 3

(a) S = gbars σ (gindy σ S) S

(b) Q ⊆ gindy σ (gbars σ Q S)

Proof.

(a) ⊆: this is trivial, from Definition 3(a), by letting Q be gindy σ S. ⊇: Let P s = s ∈ S. We use Proposition 2 with Q = gindy σ S. Condition (a) of Proposition 2 holds trivially, and condition (b) is given by Definition 2.

(b) Follows directly from Definitions 2 and 3(b). □

Lemma 4

(a) if all objects are in gindy σ S, then bars σ S = S, whence, if σ is well-founded, then every object is in S, and (b) bars σ (wfp σ) = wfp σ

Proof.

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

(b) follows as every object is in gindy σ (wfp σ), which follows from Lemma 3(b).

2 The Termination Theorem

Given a reduction relation ρ, our general termination result requires relations ◁ and ≪ which satisfy certain properties. These relations play a role similar to the relations ◁ and ≪ in [14], and, where convenient, we express our conditions so as to enable easy comparisons with [14]. 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(a) below, but in practice we often use the simpler and stronger conditions (b) to (e). (Even weaker conditions than 1(a) are possible, since we could for example suppose that s also satisfies ∀u ≪ s. u ∈ gindy ◁ SN: see the proof of of Lemma 6 below).

Condition 1

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

(b) For all (t, s) ∈ ρ, if ∀s′ ◁ s. s′ ∈ SN, then t ∈ gbars ◁ {u | u ≪ s} SN

(c) For all (t, s) ∈ ρ, t ∈ gbars ◁ {u | u ≪ s} {v | (v, s) ∈ (◁ ∘ ρ)}

(d) ◁ is well-founded and, for all (t, s) ∈ ρ, if ∀s′ ◁ s. s′ ∈ SN, then, for all t′ ◁^{∗} t, either t′ ∈ SN or t′ ≪ s

(e) ◁ is well-founded and, for all (t, s) ∈ ρ and for all t′ ◁^{∗} t, either (t′, s) ∈ (◁ ∘ ρ^{∗}) or t′ ≪ s.

Lemma 5 Each of Conditions 1(b) to (e) implies Condition 1(a) for all s.

Proof. It is easy to see that Condition 1(b) implies Condition 1(a) for all s.

To show that Condition 1(d) implies Condition 1(b), assume (d) holds. Then, as ◁ is wellfounded, 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 (b) holds.

To show that Condition 1(e) implies Condition 1(d), and likewise, that Condition 1(c) implies Condition 1(b), 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(c) we could have (◁ ∘ ρ^{∗}) in place of (◁ ∘ ρ). □

Our key lemma, Lemma 6 below, corresponds to [6, Lemma 3], but is considerably simpler. We thank an unnamed referee for pointing out that our proof and that of [6, Lemma 3] resembles the proof by Buchholz [5] of the well-foundedness of the lexicographic path ordering, although it was obtained independently.

Lemma 6 If object s satisfies Condition 1(a), then

s ∈ gindy ≪ (gindy ◁ SN).

Proof. Given s, assume that ρ, ◁ and ≪ satisfy Condition 1(a) 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 4(b), it suffices to show s ∈ bars ρ SN.

The  antecedent  of  Condition  1(a)
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, we have gbars ◁ {u | u ≪ s} SN ⊆ gbars ◁ (gindy ◁ SN) SN = SN, by Lemma 3(a).

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 7 Relation ρ is well-founded if Condition 1(a) holds for all s and

(a) every object is in bars ≪ (gindy ◁ SN), and

(b) every object is in bars ◁ SN.

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

If Condition 1(b) holds, then it also holds if we augment ρ to contain ◁. Thus, for fixed ◁, Theorem 7 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 7 can be applied trivially. Let ≪ = ◁ = ρ^{+}, which is well-founded. Then even Condition 1(e) applies. Clearly also, conditions (a) and (b) of Theorem 7 apply as ≪ and ◁ are wellfounded. That is, Theorem 7 is, trivially, a universal result for proving termination (as are several other orderings in the literature).

3 Generalising Previous Results

3.1 Generalising Goubault-Larrecq’s General Theorem for ARSs

We show that Theorem 1 of Goubault-Larrecq [14], which itself generalizes many results in the literature, is a special case of our Theorem 7. Note that [14] uses < where we use ρ. We first require two lemmas.

Lemma 8 Given set S and object s, suppose for all t that, if (t, s) ∈ ρ, then

(a) t ∈ S, or

(b) 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 (a) and (b) as above. Firstly, if t ∈ S, then t ∈ gbars ◁ {x | x ≪ s} S by Definition 3(a). Secondly, if (b) holds, we show that t ∈ gbars ◁ {x | x ≪ s} S using Definition 3(b). We have t ≪ s, and for any u ◁ t, there are again two cases. In the first case, (u, s) ∈ ρ and so, by the inductive hypothesis, u ∈ gbars ◁ {x | x ≪ s} S. In the second case, u ∈ S and so u ∈ gbars ◁ {x | x ≪ s} S by Definition 3(a). □

Lemma 9 Suppose that, whenever (t, s) ∈ ρ, either

(a) for some object u, s ▷ u and u ≥_{ρ} t, or

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

Suppose also that ◁ is well-founded. Then Condition 1(b) holds.

Proof. We use Lemma 8 with S = {v | ∃x. s ▷ x and x ≥_{ρ} v}. To show Condition 1(b), let (t, s) ∈ ρ, and suppose that ∀s′ ◁ s. s′ ∈ SN. By Lemma 8, t ∈ gbars ◁ {x | x ≪ s} S. We show S ⊆ SN. Let 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(b). □

Corollary 10 Theorem 1 of [14] holds.

Proof. Theorem 1 of [14] says: if Property 1 and conditions (iii) and (iv) (as given in [14]) hold, then ρ is well-founded.

Condition (iv) of [14] is just condition (a) of our Theorem 7 because \underline{SN} of [14] is gindy ◁ SN, and if some u ◁ s ∉ SN, then s ∈ \underline{SN}. Thus the requirement that “if every u ◁ s is in SN” in the statement of Theorem 1 of [14] is redundant, although its counterpart is needed in the statement of Theorem 2 of [14].

Condition (iii) of [14] says that ◁ is well-founded. Then, for any object v and set S of objects, v ∈ bars ◁ S, and so condition (b) of Theorem 7 follows.

Property 1 of [14] says that for (t, s) ∈ ρ, either (a) or (b) of Lemma 9 holds. Finally, Lemma 9 shows that if ◁ is well-founded, as ensured by condition (iii) of [14], then Property 1 implies Condition 1(b), whence Condition 1(a) holds.

Thus all the conditions of Theorem 7 hold, so ρ is well-founded. □

We explore the extent to which, conversely, Theorem 1 of Goubault-Larrecq [14] implies our Theorem 7. We discuss in detail only whether our Conditions 1(a) to (e) imply Property 1 of [14]. First we note a sort of converse to Lemma 8: if (t, s) ∈ ρ ⇔ t ∈ gbars ◁ {x | x ≪ s} S then, by the definition of gbars, (a) or (b) of Lemma 8 hold, even after deleting “or u ∈ S” from (b).

Suppose Condition 1(c) 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 ρ so that Condition 1(c) holds as an equivalence, giving (a) and (b) of Lemma 9 (i.e. Property 1 of [14]).

That is, [14, Theorem 1] can be used to prove a weaker version of our Theorem 1 in which Condition 1(c), rather than Condition 1(a), is assumed, and it is assumed that ◁ is well-founded. On the other hand, in Sections 4.1 and 4.2, the proofs of termination use Theorem 7, and, in particular, use Condition 1(b). The difference between Condition 1(b) and Condition 1(c) is crucial to these proofs, which shows that [14, Theorem 1] is a special case of our Theorem 7.

3.2 Generalising our Previous Theorem for TRSs

We now apply Theorem 7 to the special case of a TRS on terms of a first-order language T (Σ, V) (see [3, §3.1]), thereby showing that our main result from [6] is a special case of Theorem 7. 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 [3, Definition 3.1.9]). So we define ctxt σ to be the “closure under contexts” of σ: that is, where C[ ] is a context, and (r, l) ∈ σ, then (C[r], C[l]) ∈ ctxt σ. Likewise we define pctxt (“proper context”): for (r, l) ∈ σ, if r and l are proper subterms of C[r] and C[l], then (C[r], C[l]) ∈ pctxt σ.

In [6] 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 [6] we used a relation <_{dt} = <_{cut} ∪ <_{sn1}, where <_{cut} was chosen by the user, but <_{sn1} was defined to be the set of those reductions where a strongly normalising immediate subterm is reduced [6, Definition 3]. Then we apply Theorem 7 by letting ≪ be the relation <_{dt}^{+}, which is well-founded if and only if <_{dt} is so. Also let ≪′ be <_{cut}, so ≪ = ≪′ ∪ <_{sn1}. We now reproduce Theorem 2 of [6] in our current notation, as Condition 2(a). Condition 2(b) implies Condition 2(a), is more generally useful, and will be used in §5.

Condition 2

(a) For all (t, s) ∈ σ, if ∀s′ ◁^{+} s. s′ ∈ SN then, for all t′ ◁^{∗} t, either t′ ∈ SN or t′ ≪ s.

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

Theorem 11 If σ satisfies Condition 2(a), ≪ contains <_{sn1} and ≪ is well-founded, then every term is strongly normalising [6].

Proof. We apply Theorem 7 to this situation. Since ◁ is well-founded and we assume ≪ is wellfounded, conditions (a) and (b) of Theorem 7 are satisfied. It remains only to check that Condition 1(a) holds. In fact we can show that the stronger Condition 1(d) 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 the case (t, s) ∈ σ, Condition 2(a) then implies that for t′ ◁^{∗} t, either t′ ∈ SN or t′ ≪ s, and so Condition 1(d) holds in this case.

We also need to 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(d) holds for this case also. □

3.3 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 [9].

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 ρ. As before, ◁ is the immediate subterm relation, and <_{sn1} is defined as in §3.2.

The following results are easily proved by methods similar to those of [11].

Lemma 12 For all binary relations σ and τ:

(a) σ ∘ τ is well-founded if and only if τ ∘ σ is wellfounded

(b) if τ is well-founded then wfp (τ^{∗}∘σ) = wfp (σ∪τ)

(c) if τ is well-founded and τ ∘ σ ⊆ σ ∘ τ^{∗}, then wfp (σ ∪ τ) = wfp σ.

The following theorem encapsulates mostly known results, for example Lemma 1 of Hirokawa & Middeldorp [15] resembles: “if (4) then (7)”, and Proposition 1 of Borralleras, Ferreira & Rubio [4] is: “if (7) then (6)”.

Theorem 13 The following are equivalent, where ρ = ctxt σ:

(constrict σ ∘ ◁^{∗}) ∪ <_{sn1}  is well-founded (1)
constrict σ ∘ ◁^{∗} ∘ <_{sn1}^{∗}  is well-founded (2)
◁^{∗} ∘ <_{sn1}^{∗} ∘ constrict σ  is well-founded (3)
<_{sn1}^{∗} ∘ constrict σ ∘ ◁^{∗}  is well-founded (4)
ρ ∘ ◁^{∗}  is well-founded (5)
ρ ∪ ◁  is well-founded (6)
ρ  is well-founded (7)
ρ^{+}  is well-founded (8)
ρ^{+}∪ ◁  is well-founded (9)

Proof. (3) ⇒ (7): 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 in the literature, eg, [2, Theorem 6], [15, Lemma 1].

(2) ⇔ (3) ⇔ (4): these follow from Lemma 12(a).

(1) ⇔ (4) : and (5) ⇔ (6) : follows from Lemma 12(b), since <_{sn1} is well-founded.

(7) ⇒ (6) : (and (8) ⇒ (9) is similar) : follows from Lemma 12(c), as ◁ ∘ ρ ⊆ ρ ∘ ◁, as ρ is monotonic.

(6) ⇒ (7) : trivial, as ρ ⊆ ρ ∪ ◁

(9) ⇒ (4) : similarly trivial, as <_{sn1}^{∗} ∘ constrict σ ⊆ ρ^{+}

(8) ⇔ (7) is a standard result

(6) ⇒ all others : since every other relation mentioned is contained in (ρ ∪ ◁)^{+}. □

We now link Theorem 13 with Theorem 11, by some simple proofs. Note that Condition 2(a) in §3.2 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 12(c), wfp ρ = wfp (ρ ∪ ◁).

Then, we can use Theorem 11 to prove (1) implies (7). Let ≪ = τ. Then Condition 2 holds trivially, ≪ ⊇ <_{sn1} and ≪ is well-founded, which is just (1) of Theorem 13. Hence, by Theorem 11, ρ is wellfounded.

The converse is also easy to prove, giving an alternative proof of Theorem 11. Assume (1) ⇒ (7); we will prove Theorem 11. Suppose the assumptions of Theorem 11 hold, and we want to show its conclusion, (7). We show (1), 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.

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 4(b), every s ∈ wfp τ, as required.

4 Application to Typed Combinators

In [14] Goubault-Larrecq concludes that “Theorem 1 seems to be insufficient to show that every simplytyped λ-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 [13] 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 well-typed 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 7 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 Theorem 2.2 of Akama [1], this is enough to show strong normalisation of β-reduction.

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

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 righthand-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 Theorem 7 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 (11), (12) and (13) are added only because the proof uses them: for clearly, if ρ ⊇ ρ′, and ρ terminates, then so does ρ′. These rules are motivated by the relation ◁^{∘} of [14, §5]:

Sfgx >_{σ} fx(gx)  (10)
Sfg >_{τ} fx(gx)  if x ∈ SN  (11)
Sf >_{τ} fx(gx)  if g, x ∈ SN  (12)
S >_{τ} fx(gx)  if f, g, x ∈ SN (13)

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

Note that “SN ” means with respect to ρ: that is, τ and ρ (but not σ) are being defined, indirectly, in terms of themselves. However the rule (10) 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 (12), 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 [14]. 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 14 Let ≪ = <_{ty} ∪ <_{sn1}, and let ◁ be the immediate subterm relation. Then Condition 1(b) holds.

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

If (t, s) ∈ τ ⊆ ρ via rule (13), 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 σ by rule (10), 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 15 Every term is strongly normalising.

Proof. We use Theorem 7. Apart from Lemma 14, we need conditions (a) and (b) of Theorem 7. Condition (b) holds as ◁ is well-founded. Finally, to show condition (a), we show that ≪ is well-founded. Clearly the “smaller type” relation < is well-founded, and it is easy to show that <_{sn1} is well-founded. Then, clearly, <_{ty} ∘ <_{sn1} ⊆ <_{ty}, and so, by [6, Lemma 1], <_{ty} ∪ <_{sn1} is well-founded. □ Our rules (11), (12) and (13) were suggested by the definition of ◁^{∘} given just below Remark 13 in [14]. As in [14], therefore, there is a resemblance between our proof and the classic reducibility argument: we have, for example, that 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 [13, §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 Theorem 7 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  (14)
M >_{ρ} MN if N ∈ SN  (15)
Sfgxy_{1} … y_{n} >_{σ} fx(gx)y_{1} … y_{n}  (16)
σ ⊆ ρ  (17)
\begin{matrix}(x′_{i}, x_{i}) ∈ ctxt σ ⇒ \\ fx_{1} … x_{i} … x_{n} & >_{ρ} fx_{1} … x′_{i} … x_{n} \end{matrix}  (18)

Note that rules (16) to (18) 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 (15), 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 16 Every term is strongly normalising.

Proof. We first show that Condition 1(b) holds. Let (t, s) ∈ ρ and assume that ∀u ≪ s. u ∈ gindy ◁ SN, and ∀v ◁ s. v ∈ SN. If (t, s) ∈ ρ via rule (16), 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 (15), 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 (18), 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(b) holds.

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

5 Incremental Proofs of Termination

A rewrite system can be defined by taking the union of two terminating systems. Obviously, it would be desirable to be able to reduce a proof of termination of such a system into two smaller proofs of termination of smaller systems. This is possible under certain conditions (see, eg, [12]), but not in general. We show how Theorem 2 of [6], as described in §3.2, can be used to prove termination incrementally in certain cases. The assumptions we require of the component systems are mentioned where they first become relevant, and all appear in Theorem 21.

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 a rewrite system ρ_{0} which has been proved terminating by any method, with only the extra condition that the rules R_{0} be right-linear: that is, no variable appears more than once on the righthand side of a rule. Thus we define the R_{0}-property, (in which (b) and (d) are obviously necessary for any terminating system), and assume throughout that R_{0} satisfies it. The R_{0}-property is important for the lemma which follows.

Definition 5 (R_{0}-property) A rule satisfies the R_{0}-property if

(a) its function symbols are in the set F_{0}

(b) its left-hand side is not a variable

(c) its right-hand side variables are not duplicated

(d) its right-hand side variables also appear on the left-hand side

Lemma 17 Let σ be the set of substitution instances of a set of rules satisfying the R_{0}-property. Then (a) For f ∉ F_{0} and (t, s) ∈ σ,

if t′ = f(\overline{t}) ◁^{∗} t then t′ ◁^{+} s.

(b) 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. The system ρ_{1} is assumed to have been proved terminating using Theorem 11 above (ie, using Theorem 2 of [6]): that is, by defining a relation ≪′_{1} such that ≪_{1} = ≪′_{1} ∪ <_{sn1} is well-founded, where <_{sn1} is defined in terms of ρ_{1} only.

In many examples of the use of Theorem 11, the argument went as follows. Firstly, 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. Secondly, using <_{sn2} in place of <_{sn1}, we prove that ≪′ ∪ <_{sn2} is wellfounded by proving that ≪′ is well-founded and then using [11] to prove that the union is well-founded, often by proving that ≪′ ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ ≪′ (see Theorem 1 and Lemma 1 of [6]).

We will use this proof method. The key point is to define a suitable relation ≪′: we will use ≪′ = ≪′_{0} ∪ ≪′_{1}, where ≪′_{0} is a suitable relation which we derive from R_{0}. To help prove ≪′ ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ ≪′ we will assume ≪′_{1} satisfies the ≪′_{1}-property:

Definition 6 (≪′_{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 [6, Lemma 1], and Theorem 21 still holds. Details will be in [7]. The example in [6, §3.6] satisfies only the weaker condition.

To define ≪′_{0} we first define ◁_{0} and ctxt_{0}, and then a set of rules R_{≪0}:

Definition 7 (◁_{0}) t ◁_{0} f(…, t, …) if f ∈ F_{0}.

Definition 8 (ctxt _{0}) For (t, s) ∈ σ, if the subterms of C[x] which are super-terms of x have head symbols in F_{0} then (C[t], C[s]) ∈ ctxt_{0} σ.

Definition 9 (R_{≪0}) (r′_{0}, l_{0}) ∈ R_{≪0} iff it satisfies the R_{0}-property and there exists r_{0} such that r′_{0} ◁_{0}^{∗} r_{0} and r′_{0} is not a variable, and (r_{0}, l_{0}) ∈ ctxt_{0} R_{0}.

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 define ≪ = ≪′ ∪ <_{sn2}. Since <_{sn2} is well-founded ([6, Theorem 1]), to show that ≪ is well-founded it would be enough to show ≪′ ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ ≪′. We cannot do this, but we can choose a suitable subset <′_{sn2} of <_{sn2} such that ≪ = ≪′ ∪ <′_{sn2} and we prove that ≪ is wellfounded 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 ρ). 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 ([8], file hier.ML), as have all these results.

Lemma 18 Let

<′_{sn2} = ctxt (τ_{1} ∩ pctxt (σ_{0} ∩ ρ_{SN})) ∪ pctxt (σ_{1} ∩ ρ_{SN})

Let R_{0} satisfy the R_{0}-property. Then

<′_{sn2} ⊆ <_{sn2} ⊆ ≪′_{0} ∪ <′_{sn2}.

Lemma 19 Assume hypotheses (a), (b) and (d) of Theorem 21 below. Then

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

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

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

Proof.

(a) This follows from [6, Lemma 1] as ≪′_{1} satisfies the ≪′_{1}-property.

(b) Recall that, for f(\overline{t}) ≪′_{0} s, f ∈ F_{0}. Then use Lemma 17(b).

(c) As ≪′_{0} and, by (a), ≪′_{1} ∪ <′_{sn2} are wellfounded, we can use (b) and [6, Lemma 1(a)] to get that ≪′_{0} ∪ (≪′_{1} ∪ <′_{sn2}) is wellfounded. Then, by Lemma 18, this is ≪′_{0} ∪ (≪′_{1} ∪ <_{sn2}) = ≪′ ∪ <_{sn2} = ≪. □

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

Proof. Let (t, s) ∈ σ_{0}, got by substituting 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 then, by Lemma 17(a), t′ ◁^{∗} f(\overline{t}) ◁^{+} s, as required. □

Theorem 21 Assume that

(a) rules R_{0} satisfy the R_{0}-property, and give a terminating rewrite system ρ_{0},

(b) relation ≪′_{1} is well-founded and satisfies the ≪′_{1}-property,

(c) σ_{1} and ≪′_{1} satisfy Condition 2(b),

(d) for (t, s) ∈ σ_{1} ∪ ≪′_{1}, s is of the form f(\overline{s}), with f ∉ F_{0}.

Then ρ_{0} ∪ ρ_{1} is well-founded.

Proof. From assumption (c) and Lemma 20, it can be seen that σ_{0} ∪ σ_{1} and ≪′_{0} ∪ ≪′_{1} satisfy Condition 2(b). Then, since, by Lemma 19(c), ≪ = ≪′_{0} ∪ ≪′_{1} ∪ <_{sn2} is well-founded, and <_{sn1} ⊆ <_{sn2}, the result follows from Theorem 11. □

6 An Incremental Path Ordering

We now use the previous results to describe an incremental generalisation of the general path ordering of Dershowitz & Hoot [10].

The incremental path ordering <_{ipo} (or ipo) is then defined as below, where \overline{s} = s_{1}, …, s_{m}, \overline{t} = t_{1}, …, t_{n}, and s = f(\overline{s}) and t = g(\overline{t}). Let Λ(ipo) (or <_{Λ}) be an ordering on lists of terms, derived from <_{ipo}, satisfying certain conditions given later: the common examples for Λ are the lexicographic or multiset extensions of <_{ipo}. As before we have a set of rules R_{0} satisfying the 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 wellfounded. Let < be a well-founded ordering on the function symbols.

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

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

\frac{f > g f ∉ F_{0} ∀i ∈ \{1, …, n\}. s >_{ipo} t_{i}}{s >_{ipo} t} (21)

\frac{(t, s) ∈ σ_{0}}{s >_{ipo} t}  (22)

\frac{(t, s) ∈ pctxt ipo}{s >_{ipo} t}  (23)

Rules (23) and (22) 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 (20) implies (23). 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, [10]). 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 [6], we define a function fwf (“from wellfounded”) which maps a binary relation σ to a binary relation fwf σ thus: (t, s) ∈ fwf σ iff (t, s) ∈ σ and s ∈ wfp σ.

We now list the conditions on Λ required at some point in the proof:

(a) Λ is a monotonic function

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

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

(d) if all s_{i} are in wfp τ and if (t, s) ∈ Λ(τ), then (t, s) ∈ Λ(fwf τ)

In practice, condition (d) means that the dependence of Λ(σ) upon σ is only as follows: whether (\overline{t}, \overline{s}) ∈ Λ(σ) depends solely upon σ-comparisons between the s_{i} and the t_{j}. The lexicographic and multiset extensions of an ordering satisfy these conditions.

The proof of termination consists mostly of combining the proof of Theorem 21 above with ideas from the proof of the termination of the recursive path ordering in [6, §3.7]. We omit the details, but note that it has been proved using the Isabelle theorem prover,

see [8], in snabs/hpodef.{thy,ML}.

Theorem 22 Assume that

(a) rules R_{0} satisfy the R_{0}-property, and give a terminating rewrite system ρ_{0} = ctxt σ_{0},

(b) the relation < on the function symbols (see rule (21)) is well-founded, and

(c) the ordering extension function Λ satisfies the conditions listed above

Then <_{ipo} is well-founded.

7 Observations and Conclusion

We have proved a theorem about termination of reduction rules which generalises the previous quite general theorems, in [6] and the first theorem in [14].

We use our main theorem to prove the termination of the reduction of well-typed combinator expressions. One of our proofs takes advantage of the abstract setting, using a relation ◁ which is not the usual immediate subterm relation.

The picture that emerges is the following. Goubault-Larrecq’s Theorem 1 [14] can handle ARSs but cannot handle reducibility arguments like those required for combinators or the simply-typed λcalculus. Our [6, Theorem 2] handles TRSs but also cannot handle such reducibility arguments. Our new Theorem 7 handles both TRSs and some reducibility arguments, but had to be be modified to reason indirectly about substitutions for the simply-typed λcalculus. An important goal is to find the exact relationship between [14, Theorem 2] and our Theorem 7.

Finally, we show how our main theorem can be used to prove termination of a rewrite system defined incrementally. We showed in [6] that our main theorem strictly subsumes the termination of the recursive path ordering. Since [12] contains a very general set of results which are nonetheless based on the recursive path ordering, neither it nor the work in §5 subsume each other. A goal of further work is to explore the relationship between their results and the work in §6.

Acknowledgements Finally, we thank some anonymous referees for very helpful comments.

References

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

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

[3] Franz Baader and Tobias Nipkow. Term Rewriting and All That. CUP, 1998

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

[5] Wilfried Buchholz. Proof-theoretic analysis of termination proofs. Annals of Pure and Applied Logic 75 (1995), 57–65.

[6] Jeremy E Dawson and Rajeev Goré. A General Theorem on Termination of Rewriting. In Proc. Computer Science Logic (CSL 2004), LNCS 3210, 100–114, 2004.

[7] J E Dawson and R Goré. Machine-checked Termination Proofs for Abstract Reduction Systems. In preparation.

[8] J E Dawson. Isabelle/HOL code, http://web.

rsise.anu.edu.au/~jeremy/isabelle

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

[10] N Dershowitz & C Hoot. Natural Termination. TCS 142 (1995), 179-207.

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

[12] Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio. Recursive Path Orderings Can Also Be Incremental. Proc. LPAR2005, LNCS 3835, 230– 245, Springer, 2005.

[13] Jean-Yves Girard, Yves Lafont and Paul Taylor. Proofs and Types. CUP, 1990.

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

[15] Nao Hirokawa and Aart Middeldorp. Dependency Pairs Revisited. In Proc. Rewriting Techniques and Applications (RTA-04), LNCS 3091, 249–268, Springer, 2004.