Propositional Modal First-Order Higher-Order

Termination of rewriting

Jeremy Dawson

                    Jeremy.Dawson@nicta.com.au

Propositional Modal First-Order Higher-Order

Rewriting

Using rewrite rule (x + 0) ⟶ x (a + 0) × b ⟶ a × b ((a + 0) + 0) × (b + 0) ⟶ a × b (3 steps)

Does this procedure always finish ?

In this case, yes — terms get smaller each time Add the rule (x + y) × z ⟶ (x × z) + (y × z)

(a + b + c) × d × e ⟶ a × d × e + b × d × e + c × d × e Can we prove that this terminates?

Propositional Modal First-Order Higher-Order

A tricky one

Single rule (integer values, not expressions)

if n odd, n ≥ 2, n ⟶ 3n + 1 if n even, n ≥ 2, n ⟶ n/2

Can express this using term rewrite rules

Not known whether this rewriting always terminates

Example: starting at 27, get the sequence

27 82 41 124 62 31 94 47 142 71 214 107 322 161 484 242 121 364 182 91 274 137 412 206 103 310 155 466 233 700 350 175 526 263 790 395 1186 593 1780 890 445 1336 668 334 167 502 251 754 377 1132 566 283 850 425 1276 638 319 958 479 1438 719 2158 1079 3238 1619 4858 2429 7288 3644 1822 911 2734 1367 4102 2051 6154 3077 9232 4616 2308 1154 577 1732 866 433 1300 650 325 976 488 244 122 61 184 92 46 23 70 35 106 53 160 80 40 20 10 5 16 8 4 2 1

Propositional Modal First-Order Higher-Order

Why does this matter?

Assume the rules are true as equalities Then we can prove (a + 0) × b = a × b by rewriting (a + 0) × b to a × b We can also add logical rules, eg add the rule x = x ⟶ T rue Anything that can be rewritten to T rue is thereby proved

eg, (a + 0) × b = a × b ⟶ a × b = a × b ⟶ T rue Rewriting much used in automated theorem proving For automation, must know that it will terminate

Propositional Modal First-Order Higher-Order

Cut-elimination a special case

Logical system (set of rules) S Additional rule, Cut Automated proof much easier using S than S ∪ {Cut}

Want to show that anything which can be proved using S ∪ {Cut} can also be proved using S

Method is to take an arbitrary proof using S ∪ {Cut}, and transform (rewrite) it to a proof using S This transformation is done in several steps, called cut-reduction steps Need to show

So long as proof still uses Cut there is still a rewrite step available the rewriting terminates

Propositional Modal First-Order Higher-Order

My work

There is a published proof of strong normalisation (ie, that any sequence of cut-reduction steps terminates)

Tried to implement this in the Isabelle theorem prover discovered a “bug” in the proof one case not dealt with

Devised a new proof, implemented in Isabelle, now published

Realized that this new proof could be expressed as a proof of rewriting termination generally

Of course it depends on assumptions about the system of rewrite rules

Am now working on using my proof to show termination of various examples of rewrite systems, in Isabelle

Termination of rewriting – p.6/6