A General Theorem on Termination of Rewriting

Jeremy E. Dawson and Rajeev Goré

Logic & Computation Programme  Automated Reasoning Group
National ICT Australia  Computer Sciences Laboratory

Res. Sch. of Inf. Sci. and Eng. Australian National University

http://rsise.anu.edu.au/∼jeremy    http://rsise.anu.edu.au/∼rpg

2007 1

Overview and Motivation

Display Calculi: Generalised sequent framework due to Nuel Belnap

Single cut-elimination proof if rules satisfy 8 easily checked conditions Isabelle/HOL: Logical framework that allows us to formalise mathematics Cut elimination: We used Isabelle/HOL to check the cut-elimination theorem

of Belnap: repeatedly transform derivation, focusing on a top-most cut Strong Normalisation: You can attack a cut other than a top-most cut – must

it terminate? We tried to check a published proof of strong normalisation. Actual outcome: problem with proof, found and checked a new proof, tricky as

each step changes or removes one cut, but can duplicate others Rewriting: can formulate this proof in terms of a set of rewriting rules, proving

strong normalisation (termination) of the rewriting procedure 2007 2

Reducing a Left-and-Right Principal Cut

A cut on A is left- [right-] principal if the left [right] inference immediately above the cut introduces A via a logical rule, written (⊢ A) [(A ⊢)]

Π_{L} (⊢ A) X ⊢ A ^{Π_{R} (A ⊢) A ⊢ Y} X ⊢ Y

C8: All left-and-right principal cuts can be replaced by cuts on strictly smaller subformulae of A

Base Case: (cut) \frac{p ⊢ p p ⊢ p}{p ⊢ p}reduced to just p ⊢ p

Similar cases for ⊤, ⊥

2007 3

Example of a Principal reduction (C8 condition)

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (⊢ ∨) Z ⊢ A ∨ B ^{\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix} \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (∨ ⊢) A ∨ B ⊢ X, Y} (cut) Z ⊢ X, Y

Principal cut on formula A ∨ B

\begin{matrix}Π_{ZAB} \\ Z ⊢ A, B \end{matrix} (dp) ∗A, Z ⊢ B \begin{matrix}Π_{BY} \\ B ⊢ Y \end{matrix} (cut) ∗A, Z ⊢ Y

(dp) Z ⊢ A, Y

(dp) Z, ∗Y ⊢ A

\begin{matrix}Π_{AX} \\ A ⊢ X \end{matrix}

(cut)
Z, ∗Y ⊢ X

(dp) Z ⊢ X, Y

Transformed derivation uses cuts only on A and B

Must exhibit and hard-wire such transformations for every logical connective

So if cut is not left-and-right principal then we try to make it so ...

2007 4

A Parametric Reduction — making a cut left-right-principal

Given a derivation ending in a non left-and-right principal cut on formula A,

we trace the ancestor occurrences of this A up Π_{L}: Let Π[A := Y] mean “replace all (non-principal) ancestors of A with Y ”

\begin{aligned}Π_{L}^{1} & (⊢ A) & V ⊢ A \\ & (π) \\ Π_{L}^{2} \end{aligned} ; (ρ) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}^{Π_{L}^{1} (⊢ A) V ⊢ A} & \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (cut) & V ⊢ Y \\ & (π) \\ Π_{L}^{2}[A := Y] \end{aligned} ; (ρ) ; X ⊢ Y

New cut is left-principal (similarly make it also right principal) If Π_{L} branches (A introduced at multiple places), more complex (!)

If Π_{L}^{1} is empty, A introduced by A ⊢ A, no new cuts needed. 2007 5

Strong Normalisation

Cut-admissibility proceeds by eliminating the top-most cut Strong normalisation: define reduction steps, eliminate any cut that can be reduced, and prove that this cut-elimination procedure terminates: Π_{n} < Π_{n−1} < ⋯ < Π_{2} < Π_{0} Π_{n} is cut-free n is finite weak-normalisation (attacking top most cut) is an instance of this method Usually define reductions as either a parametric or principal move, with proviso that we must not cross a cut in a parametric move

2007 6

Why Formalise (in Isabelle) ?

Strong-normalisation proofs are notoriously difficult involving many cases We tried to formalise Heinrich Wansing’s proof of strong-normalisation for display logic, but got stuck at one particular case Found a problem ... Wansing assumes that Π_{L}^{1} is unchanged!

V_{A} is (∗A , X) V_{Y} is (∗Y , X)

\begin{matrix}Π_{L}^{1} & (⊢ A) & V_{A} ⊢ A \\ (dp) \\ X ⊢ A, A \end{matrix} ; (ctr) ; X ⊢ A \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X ⊢ Y  \begin{aligned}^{Π_{L}^{′1} (⊢ A) V_{Y} ⊢ A} & \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} & (cut) & V_{Y} ⊢ Y \\ & (dp) \\ X ⊢ Y, Y \end{aligned} ; (ctr) ; X ⊢ Y

2007 7

Branch in left subtree — before and after

Π′ (intro-A) X′ ⊢ A ^{Π′′ (intro-A) X′′ ⊢ A} (π) Π_{L}

(ρ) X ⊢ A

\begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix}

(cut)
X ⊢ Y

\begin{matrix}Π′ \\ X′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′ ⊢ Y ^{\begin{matrix}Π′′ \\ X′′ ⊢ A \end{matrix} \begin{matrix}Π_{R} \\ A ⊢ Y \end{matrix} (cut) X′′ ⊢ Y} (π) Π_{L}[A := Y]

(ρ) X ⊢ Y

2007 8

Two successive introductions – before and after

\begin{aligned}Π & (ρ) & X, B ⊢ ∗B \\ & (⊢ ¬) \\ X, B ⊢ ¬B \end{aligned} ; (dp) ; ∗¬B, X ⊢ ∗B ; (⊢ ¬) ; ∗¬B, X ⊢ ¬B ; (dp) ; X ⊢ ¬B, ¬B (⊢ cont) X ⊢ ¬B \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} (cut) X ⊢ Y

\begin{matrix}\begin{aligned}Π & (ρ) & X, B ⊢ ∗B \\ & (⊢ ¬) \\ X, B ⊢ ¬B \end{aligned} & \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} & (cut) & X, B ⊢ Y \\ (dp) \\ ∗Y, X ⊢ ∗B \end{matrix} ; (⊢ ¬) ; ∗Y, X ⊢ ¬B \begin{matrix}Π_{R} \\ ¬B ⊢ Y \end{matrix} (cut) ∗Y, X ⊢ Y

(dp) X ⊢ Y, Y

(⊢ cont) X ⊢ Y

2007 9

Various Binary Orderings – <_{cut}

We define a well-founded ordering <_{cut}. For cut-elimination, Π_{1} <_{cut} Π_{0} iff (informally, the cut at the bottom of Π_{1} is closer to being eliminated than that at the bottom of Π_{0}) iff any of

(a) the bottom inference of Π_{1} is not cut, but that of Π_{0} is

(b) the size of the cut-formula of Π_{1} is smaller than that of Π_{0}, or

(c) Π_{1} and Π_{0} have the same cut-formula, and either (i) the cut in Π_{1} is left- or right-principal, and the cut in Π_{0} is neither, or (ii) the cut in Π_{1} is both left- and right-principal, and the cut in Π_{0} is not.

Clearly <_{cut} is well-founded.

2007 10

Generalise to Term Rewriting

Have a language for defining first-order “terms”, such as f(a, g(b, c)) Have a collection of rewrite rules: {l_{1} → r_{1}, ⋯, l_{n} → r_{n}} in which can substitute for variables We consider the rewrite relation after substitution – call it ρ closure under contexts of relation ρ (eg, if l ⟶^{ρ} r then C[l] ⟶ C[r]) Question: Does this rewriting process terminate for all terms? An ordering <_{cut} must be defined, depending on the problem. Typically, it looks at or near the head of the term (root of the tree)).

2007 11

Defining Reductions and Strongly Normalising Terms

Definition 1 Assuming a relation ρ, term t_{0} reduces to term t_{1} if either

(a) (t_{1}, t_{0}) ∈ ρ, or

(b) t_{0} and t_{1} are identical except that exactly one proper subterm of t_{0} reduces to the corresponding proper subterm of t_{1}. (this is the closure of ρ under context) Definition 2 The set SN is the smallest set of terms such that:

(a) if t_{0} cannot be reduced then t_{0} ∈ SN

(b) if every term t_{1} to which t_{0} reduces is in SN then t_{0} ∈ SN A term is strongly normalising iff it is a member of SN. Usual definition is: a term t is in SN iff there is no infinite sequence of reductions starting with t. These two definitions are equal in classical logic.

2007 12

Various Binary Orderings – <_{sn1}, etc

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

(b) t_{1} <_{sn2} t_{0} – as above, except put proper for immediate

(c) t_{1} <_{dt} t_{0} iff t_{1} <_{cut} t_{0} or t_{1} <_{sn1} t_{0}. Despite notation, these relations need not be transitive. Intuitively, t_{1} <_{dt} t_{0} means that t_{1} is closer to a normal form (being cut-free) (in some sense) than is t_{0}. Necessarily, <_{sn1}⊆<_{sn2}, both are well-founded. We need to be able to prove that <_{dt} = <_{cut} ∪ <_{sn1} is well-founded. Use lemma on the union of well-founded orderings.

2007 13

Union of Well-Founded Relations

Lemma 1 Let τ and σ be well-founded relations. Then each of the following implies that τ ∪ σ is well-founded:

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

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

(c) τ ∘ σ ⊆ τ ∪ σ,

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

(d) is from Doornbos & von Karger; other conditions imply (d)

2007 14

Conditions on the rewrite relation ρ

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

(a) r′ ∈ SN or (b) r′ <_{dt}^{+} l Condition 2 is simpler and implies Condition 1 Condition 2 For all (r, l) ∈ ρ, for all subterms r′ of r, either

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

(b) r′ <_{cut} l

(c) r′ is obtained from l by reduction of l at a proper subterm. For assuming that all proper subterms of l are in SN then Condition 2(a) implies that r′ ∈ SN, and 2(c) implies that r′ <_{sn1} l, so r′ <_{dt}^{+} l. Note that sometimes we enlarge the relation ρ to satisfy Conditions 1 and 2.

2007 15

Key Properties of Cut-Elimination Reductions

When we apply a reduction to a cut at the bottom of a tree Π_{0}, obtaining Π_{1}, then every subtree Π_{1}^{s} of Π_{1} which has cut at the bottom satisfies one of

Π_{1}^{s} is a proper subtree of Π_{0} (any cut-formula, any number of copies), (Condition 2(a)) or

Π_{1}^{s} <_{cut} Π_{0} (Condition 2(b)), because

(principal reduction) the cut-formula of Π_{1}^{s} is smaller than that of Π_{0}

(parametric reduction) Π_{1}^{s} and Π_{0} have the same cut-formula and Π_{1}^{s} is principal on more sides than Π_{0} .

2007 16

Inductive Strong Normalisation

Recall t ∈ SN iff t is strongly normalising. We define ISN: t ∈ ISN if t inherits strong normalisation from its immediate subterms. Definition 3 t ∈ ISN iff: if all the immediate subterms of t are strongly normalising then t is strongly normalising. Lemma 2 A term t is in SN iff every subterm of t is in ISN. Proof: The immediate subterm relation is well-founded. The result is proved using well-founded induction.

2007 17

Strong-Normalisation Proof – outline

Lemma 3 Assume that the rewrite relation satisfies Condition 1 or 2. For a given term t_{0}, if all terms t′ <_{dt}^{+} t_{0} are in ISN, then so is t_{0}. Proof: Given t_{0}, assume that ρ satisfies Condition 1 and that (a): all terms t′ <_{dt}^{+} t_{0} are in ISN. We need to show t_{0} ∈ ISN, so we assume that (b): all immediate subterms of t_{0} are in SN, and we show that t_{0} ∈ SN. To show this, let t_{0} reduce to t_{1}, show t_{1} ∈ SN. … Theorem 1 If ρ satisfies Condition 1 and <_{dt} = <_{cut} ∪ <_{sn1} is well-founded, then every term is strongly normalising. Proof: By well-founded induction, it follows from Lemma 3 that every term is in ISN; the result follows from Lemma 2.

2007 18

Strong-Normalisation Proof

Lemma 4 Assume that the rewrite relation satisfies Condition 1 or 2. For a given term t_{0}, if all terms t′ <_{dt} t_{0} are in ISN, then so is t_{0}. Proof: Given t_{0}, assume that ρ satisfies Condition 1 and that (a): all terms t′ <_{dt}^{+} t_{0} are in ISN. We need to show t_{0} ∈ ISN, so we assume that (b): all immediate subterms of t_{0} are in SN, and we show that t_{0} ∈ SN. To show this, let t_{0} reduce to t_{1}, show t_{1} ∈ SN. Two cases: reduction occurs in a proper subterm of t_{0}, or of t_{0} as a whole. Reduction in a proper subterm of t_{0} (which is in SN, by (b)): So t_{1} <_{sn1} t_{0} and t_{1} <_{dt} t_{0}. Therefore t_{1} ∈ ISN by assumption (a).

2007 19

Strong-Normalisation Proof (ctd)

Now each immediate subterm of t_{1} is equal to, or is a reduction of, an immediate subterm of t_{0}, which itself is in SN by assumption (b). All immediate subterms of t_{1} are therefore in SN. Then, as t_{1} ∈ ISN, we have t_{1} ∈ SN. (t_{1}, t_{0}) ∈ ρ: By Condition 1, subterms of t_{1} are either in SN or are <_{dt}^{+}-smaller than t_{0} (and so in ISN, by (a)). That is, every subterm t_{1}^{s} of t_{1} (including t_{1} itself) is in ISN, so t_{1} ∈ SN by Lemma 2. Theorem 2 If ρ satisfies Condition 1 and <_{dt} = <_{cut} ∪ <_{sn1} is well-founded, then every term is strongly normalising. Proof: By well-founded induction, it follows from Lemma 4 that every term is in ISN; the result follows from Lemma 2.

2007 20

Multiset Order

ρ: is an irreflexive relation on some given set E A, B, C: finite multisets of elements of E A ⊔ B: means multiset union <_{m1}: if ∀c ∈ C, c <_{ρ} b, then C ⊔ A <_{m1} {b} ⊔ A Multisets as trees: two types of nodes Internal and Leaf nodes Rewrite: L(b) ⟶ I(L(c_{1}), ⋯, L(c_{k})) <_{cut}: L(x) >_{cut} L(y) iff x >_{ρ} y L(x) >_{cut} I(y) Theorem: For ρ well-founded, derived <_{m1} is well-founded on finite multisets.

2007 21

Example - Ackermann’s function

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

We define <_{cut} by

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

Clearly >_{cut} is well-founded using the lexicographic ordering on arguments. For l → r and r′ a subterm of r, either l >_{cut} r′ or r′ is a proper subterm of l.

2007 22

Ackermann’s function – <_{cut} ∪ <_{sn2} is well-founded

To show <_{cut} ∪ <_{sn1} is well-founded, we show <_{cut} ∪ <_{sn2} (larger) is well-founded, using Lemma 1(a) – we show <_{cut} ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ <_{cut}. For suppose t >_{cut} u >_{sn2} v. If t >_{cut} u by rule (1), t = A(x, y) >_{cut} S(z) >_{sn2} S(z′) = v and so t >_{cut} v (by rule (1)) If t >_{cut} u by rule (2), t = A(S(x), y) >_{cut} A(x, z) = u. Cases for u >_{sn2} v: u = A(x, z) >_{sn2} A(x, z′) = v where z ⟶ z′, in which case t >_{cut} v, or u = A(x, z) >_{sn2} A(x′, z) = v where x ⟶ x′ by reducing a SN subterm of x, in which case t = A(S(x), y) >_{sn2} A(S(x′), y) >_{cut} A(x′, z) = v. The case for rule (3) is similar. So <_{cut} ∪ <_{sn2} is well-founded, by Lemma 1(a). Therefore the system terminates by Theorem 2.

2007 23

Example - Distributive and Associative laws

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

To use our proof, add the following simplification rules as rewrite rules:

x + y ⟶ x x + y ⟶ y x × y ⟶ x x × y ⟶ y Define <_{cut} by <_{cut} = <_{h} ∪ <_{×} ∪ <_{+} , where

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

• for an immediate subterm x′ of x, x + y >_{+} x′ + z and x × y >_{×} x′ × z Clearly <_{cut} is well-founded.

2007 24 To show <_{cut} ∪ <_{sn1} is well-founded, we show <_{cut} ∪ <_{sn2} (larger) is well-founded, using Lemma 1(a) – we show <_{cut} ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ <_{cut}. Suppose t >_{cut} u >_{sn2} v. If t >_{h} u then clearly t >_{h} v. If x × y >_{×} x′ × z >_{sn2} x′ × w, then x × y >_{×} x′ × w. If x × y >_{×} x′ × z >_{sn2} w′ × z, then, for some w,

x × y >_{sn2} w × y >_{×} w′ × z (would not hold for >_{sn1}) So (v, t) ∈ <_{sn2}^{∗} ∘ <_{cut}, and so <_{cut} ∪ <_{sn2} is well-founded, by Lemma 1(a). Look at all pairs (r′, l), where l → r is a rewrite rule and r′ is a subterm of r. Mostly l >_{h} r′, or r′ is a proper subterm of l. For the associative rewrite rules l >_{×} r or l >_{+} r, by definition. Cases like (r′, l) = (D(x), D(x + y)) : Since x + y ⟶ x, and proper subterm x + y of l is assumed SN, have D(x + y) >_{sn1} D(x). Thus the system terminates by Theorem 2.

2007 25

Example - insertion sort

sort ([ ]) ⟶ [ ]
sort (x : y) ⟶ insert (x, sort (y))
insert (x, [ ]) ⟶ x : [ ]
insert (x, v : w) ⟶ choose (x, v : w, x, v)
choose (x, v : w, y, 0) ⟶ x : v : w
choose (x, v : w, 0, s(z)) ⟶ v : insert (x, w)
choose (x, v : w, s(y), s(z)) ⟶ choose (x, v : w, y, z)

To define >_{cut}, first define >_{h} ⊆ >_{cut}, depending on the head symbol, using this (transitive) order on symbols: sort > {insert, choose } >.

As the rules define insert and choose in terms of each other, we define

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

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

where w′, a′ are immediate subterms of w, a.

2007 26

Example - insertion sort, ctd

It is easy to see that >_{cut} is well-founded. We add a simplification rule x : y ⟶ y Then, for every (r′, l) where l → r is a rewrite rule and r′ is a subterm of r, either l >_{cut} r′, l >_{sn1} r′ or r′ is a proper subterm of l. Again we show that <_{cut} ∘ <_{sn2} ⊆ <_{sn2}^{∗} ∘ <_{cut}, using the same technique as in the previous two examples. Therefore the system terminates by Theorem 2. Compare the ordering <_{cut} with Example 13 in Hirokawa & Middeldorp, Dependency Pairs Revisited, RTA-04.

2007 27

Example - the modified factorial example

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)

>_{h} (transitive), on terms, based on head symbol: F > × > + > S. If s >_{h} t, then s >_{cut} t; also

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

Cannot use simplification ordering as rule P (x) ⟶ x gives non-termination. We do, however, add the rule S(x) ⟶ x.

2007 28

modified factorial – checking the rules

\begin{matrix}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) & S(x) & ⟶ & x \end{matrix}

Now for each (r′, l) where l → r and r′ is a subterm of r, r′ is a proper subterm of l r′ <_{h} l r′ is l, but with S removed from a subterm (to give r′ <_{sn1} l) r′ is F (P (S(x))) and l is F (S(x)) (so r′ <_{cut} l).

2007 29

modified factorial – <_{cut} ∪ <_{sn2} is well-founded

Clearly <_{cut} is well-founded. To show that <_{cut} ∪ <_{sn2} is well-founded use Lemma 1(d). We show <_{cut} ∘ <_{sn2} ⊆ (<_{sn2}^{∗} ∘ <_{cut})∪ <_{sn2}^{+}. Suppose t >_{cut} u >_{sn2} v. If t >_{h} u then clearly t >_{h} v. Otherwise: Suppose t = F (S(x)) and u = F (P (S(x))) or u = F (P (x)). If u >_{sn2} v by reducing x in u to x′, then t = F (S(x)) >_{sn2} F (S(x′)) >_{cut} v. Otherwise we need to consider specific cases:

t  >_{cut}  u  >_{sn2} v
F (S(x))  F (P (S(x)))  F (P (x)) t >_{cut} v
F (S(x))  F (P (S(x)))  F (x)  t >_{sn2} v
F (S(S(y)))  F (P (S(y)))  F (y)  t >_{sn2}^{+} v

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

Recursive Path Orderings

Lexicographic ordering lex σ (fixed-length sequences), well-founded if σ is. Given well-founded partial order ρ on function symbols, the lexicographic path ordering lpo ρ or <_{lpo} defined by (where <_{lex} is lex (lpo ρ))

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

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

Definition and proof for the multiset path ordering similar. Lemma 5 If s >_{lpo} g(t_{1}, …, t_{n}) then s >_{lpo} t_{j}, for all j ∈ {1, … n}. (follows from transitivity of >_{lpo}, but we don’t prove that) Proof: Induction on the size (or structure) of s.

2007 31 Theorem 3 If ρ (on function symbols) is well-founded, then so is <_{lpo}. Proof: We first define <_{cut} using <_{h} as usual, and defining <_{lw1}: f(\overline{s}) >_{h} g(\overline{t}) iff f >_{ρ} g if ((\overline{t}), (\overline{s})) ∈ lex (fwf (lpo r)), then f(\overline{t}) <_{lw1} f(\overline{s}) <_{cut} = (<_{h} ∪ <_{lw1}). fwf (lpo r) means reducing only SN terms, like in <_{sn1}, so fwf (lpo r), lex (fwf (lpo r)) and <_{lw1} are well-founded. As <_{h} ∘ <_{lw1} ⊆ <_{h}, <_{cut} is well-founded, by Lemma 1. Further, <_{sn1} ⊆<_{lw1}, so <_{cut} ∪ <_{sn1} = <_{cut} is well-founded.

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

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

Now suppose l >_{lpo} r′ by the second or third rules. Assuming that proper subterms of l are in SN, we have r′ <_{cut} l.

Thus the system terminates by Theorem 2.

2007 33

Applications of the theorem

Can use the theorem to prove termination of recursive path orderings of Knuth-Bendix orderings where dependency pairs method applies (conversely, lemmas used in

dependency pairs work give short proof of our result)

2007 34

Extension to non-monotonic orderings

Consider a relation ρ not necessarily monotonic (closed under contexts). So “strongly normalising” and “SN” mean for ρ, not its closure under contexts. Condition 3 For all (r, l) ∈ ρ, if all proper subterms of l are in SN then, for all subterms r′ of r, either

(a) r′ ∈ SN (eg, (r′, l′) ∈ ρ^{∗} for some proper subterm l′ of l)

(b) r′ <_{cut} l Theorem 4 If ρ satisfies Condition 3 and <_{cut} is well-founded, then ρ is well-founded.

2007 35