Book contents
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Termination orderings and complexity characterisations
Published online by Cambridge University Press: 05 November 2011
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Summary
INTRODUCTION
This paper discusses proof theoretic characterisations of termination orderings for rewrite systems and compares them with the proof theoretic characterisations of fragments of first order arithmetic.
Rewrite systems arise naturally from systems of equations by orienting the equations into rules of replacement. In particular, when a number theoretic function is introduced by a set of defining equations, as is the case in first order systems of arithmetic, this set of equations can be viewed as a rewrite system which computes the function.
A termination ordering is a well-founded ordering on terms and is used to prove termination of a term rewriting system by showing that the rewrite relation is a subset of the ordering and hence is also well founded thus guaranteeing the termination of any sequence of rewrites.
The successful use of a specific termination ordering in proving termination of a given rewrite system, R, is necessarily a restriction on the form of the rules in R, and, as we show here in specific cases, translates into a restriction on the proof theoretical complexity of the function computed by R. We shall mainly discuss two termination orderings. The first, the so-called recursive path ordering (recently re-christened as the multiset path ordering) of [Der79], is widely known and has been implemented in various theorem provers. The second ordering is a derivative of another well known ordering, the lexico-graphic path ordering of [KL80]. This derivative we call the ramified lexicographic path ordering. We shall show that the recursive path ordering and the ramified lexicographic path ordering prove termination of different algorithms yet characterise the same class of number-theoretic functions, namely the primitive recursive functions.
- Type
- Chapter
- Information
- Proof TheoryA selection of papers from the Leeds Proof Theory Programme 1990, pp. 171 - 194Publisher: Cambridge University PressPrint publication year: 1993
- 6
- Cited by