Termination of Abstract Reduction Systems

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

∗

∗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.

2007 1

Overview and Motivation

Term Rewriting: Structured first-order terms — rewrite may be at any subterm Termination Proof: Earlier paper (CSL’04) gave conditions and termination

proof (based on our result on termination of a cut-elimination procedure) Abstract reduction systems: Goubault-Larrecq’s (first) termination theorem

resembles ours, but in a more general setting (but doesn’t subsume ours) We generalised our result to abstract reduction systems:

We found that this also generalised Goubault-Larrecq’s result. An example using the generality: Our new result (following

Goubault-Larrecq) uses a relation ◁ in place of subterm relation.

We prove termination of typed combinators, using a different relation as ◁

2007 2

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. NB: as pairs, (r_{1}, l_{1}), etc 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 3

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 4

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 5

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 6

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 7

Inductive Strong Normalisation

Recall t ∈ SN iff t is strongly normalising. We define ISN: t ∈ ISN if t is in SN provided that its immediate subterms are. 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 8

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 9

Generalisation to Abstract Terms

The Termination Conditions

Condition 3 (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) …

(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) … Think of s′ ◁ s as like s′ is an immediate subterm of s. Note: Each of (b) to (e) implies (a)

2007 10

Definitions: gbars

Definition 4 (gbars) (Generalises bars) For sets 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. Lemma 4 (gbars-alternative) 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.

2007 11

Definitions: bars, wfp, gindy

Definition 5 (wfp, bars) Let U be the universal set of objects. Then

(a) s ∈ bars σ S iff s ∈ gbars σ U S (“S bars s in σ”)

(b) s ∈ wfp σ iff s ∈ bars σ ∅ (“s is accessible in σ ”). Definition 6 (gindy) (Generalises ISN) For a relation σ and set S, an object t ∈ gindy σ S iff: if ∀u. (u, t) ∈ σ ⇒ u ∈ S, then t ∈ S. Lemma 5 S = gbars σ (gindy σ S) S Lemma 6 (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 σ

2007 12

The Termination Theorem

Lemma 7 If object s satisfies Condition 3(a), then

s ∈ gindy ≪ (gindy ◁ SN).

Proof. Given s, assume that ρ, ◁ and ≪ satisfy Condition 3(a) and that (a) ∀u ≪ s. u ∈ gindy ◁ SN. We then need to show s ∈ gindy ◁ SN, so we assume that

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

2007 13

The Termination Theorem — proof (ctd)

The antecedent of Condition 3(a) holds by assumption (b), and so s ∈ bars ρ (gbars ◁ {u | u ≪ s} SN).

As bars is monotonic in its second argument, to show s ∈ bars ρ SN, 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, by Lemma 5,

gbars ◁ {u | u ≪ s} SN ⊆ 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).

2007 14

The Termination Theorem — wrapping up the proof

Theorem 2 Relation ρ is well-founded if Condition 3(a) holds for all s and

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

(b) every object is in bars ◁ SN. Note: enough that ◁ and ≪ are well-founded. Proof. If ρ and ≪ satisfy Condition 3(a), then every s ∈ gindy ≪ (gindy ◁ SN) by Lemma 7. Then, for any u, if u ∈ bars ≪ (gindy ◁ SN) then Lemma 6(a) gives u ∈ gindy ◁ SN. Thus every u ∈ gindy ◁ SN. Then, for any v, if v ∈ bars ◁ SN then Lemma 6(a) gives v ∈ SN. Thus every v ∈ SN: that is, ρ is well-founded.

2007 15

Goubault-Larrecq’s Theorem 1

Suppose that, whenever s >_{ρ} t, either

(i) for some object u, s ▷ u and u ≥_{ρ} t, or (ii) s ≫ t and, for every u ◁ t, s >_{ρ} u. Assume also that (iii) ◁ is well-founded (whence (b) of Theorem 2) (iv) every object is in bars ≪ (gindy ◁ SN) (ie, (a) of Theorem 2) Then ρ is well-founded. Proved that this follows from Theorem 2: key step is to use (i) and (ii), and well-founded induction on ◁ (by (iii)), to get Condition 3(b).

2007 16

Typed Combinators

Sfgx = fx(gx)  W fx = fxx

Untyped, these do not terminate: (SII)(SII) ⟶^{+} (SII)(SII) (W I)(W I) ⟶^{+} (W I)(W I) W W W ⟶ W W W

2007 17

Typed Combinators — first proof

Define reduction relations σ, τ, and let ρ = ctxtσ ∪ τ. Note that “SN” is wrt ρ.

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)

where S : (α→β →γ)→(α→β)→α→γ, f : α→β →γ, g : α→β, x : α. Now τ and ρ (but not σ) are defined, indirectly, in terms of themselves. But recursive definitions are in terms of “smaller” types (checked in Isabelle!) t <_{sn1} s if (t, s) ∈ ctxtσ by reducing an immediate subterm in wfp(ctxtσ) t <_{ty} s if t has smaller type than s. Lemma 8 Let ≪ = <_{ty} ∪ <_{sn1}, and let ◁ be the immediate subterm relation. Then Condition 3(b) holds. Finally show ◁ and ≪ well-founded to complete the proof.

2007 18

Typed Combinators — second proof

Uses a different relation as ◁ (not the immediate subterm relation!)

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} and σ ⊆ ρ (7)
(x′_{i}, x_{i}) ∈ ctxtσ ⇒ fx_{1} … x_{i} … x_{n} >_{ρ} fx_{1} … x′_{i} … x_{n}  (8)

From (7) and (8), ctxtσ ⊆ ρ. Again, definitions sound, as a reduction preserves or reduces 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σ).

2007 19

Typed Combinators — second proof, ctd

Let ≪ = <_{ty} ∪ <_{sn1}. We show Condition 3(b) holds. Rule (6), M >_{ρ} MN if N ∈ SN: M >_{ty} MN. For K ◁ MN, K = N ∈ SN, or K ◁ M and so K ∈ SN. Rule (7): as we can assume f, g, x, y_{i} ∈ SN, so fx(gx)y_{1} … y_{n} ∈ SN Rule (8): lhs >_{sn1} rhs, and each ◁-subterm of rhs is a ◁-subterm of lhs, or a reduction thereof, and so is in SN. So Condition 3(b) holds, and vtl and ≪ are well-founded, so ρ is well-founded, by Theorem 2.

2007 20

Incremental Proofs of Termination

Terminating system of rewrite rules R_{0}, head symbols in F_{0}. Additional rules, head symbols in F_{1}. If additional rules satisfy conditions similar to main theorem, then whole system is terminating: subject to some restrictions. Most significant restriction is that rules R_{0} be right linear.

Incremental Path Ordering

Like recursive path ordering, but built on top of rewrite system based on R_{0}. Same restriction on R_{0}. Proofs in Isabelle only!

2007 21