Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths

DOI10.1016/0304-3975(94)00135-6zbMath0874.68156OpenAlexW2049865932MaRDI QIDQ673975

Andreas Weiermann

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00135-6

zbMATH Keywords

lexiographic path orderingterm rewriting system

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (25)

How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study ⋮ Proving consistency of equational theories in bounded arithmetic ⋮ KBO orientability ⋮ Proof-theoretic analysis of termination proofs ⋮ Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones ⋮ On the Computational Content of Termination Proofs ⋮ The hierarchy of terminating recursive programs over N ⋮ Analyzing Innermost Runtime Complexity Through Tuple Interpretations ⋮ An upper bound on the derivational complexity of Knuth-Bendix orderings. ⋮ Proving Quadratic Derivational Complexities Using Context Dependent Interpretations ⋮ Unnamed Item ⋮ Automated Complexity Analysis Based on the Dependency Pair Method ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Term rewriting theory for the primitive recursive functions ⋮ Some interesting connections between the slow growing hierarchy and the Ackermann function ⋮ Quasi-interpretations. A way to control resources ⋮ Derivation lengths and order types of Knuth--Bendix orders ⋮ The Hydra battle and Cichon's principle ⋮ Complexity Analysis by Rewriting ⋮ A lexicographic path order with slow growing derivation bounds ⋮ Applications and extensions of context-sensitive rewriting ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results ⋮ Some results on cut-elimination, provable well-orderings, induction and reflection

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Bounding derivation lengths with functions from the slow growing hierarchy
• Slow growing versus fast growing
• A Uniform Approach to Fundamental Sequences and Hierarchies
• Incremental termination proofs and the length of derivations
• Eine Klassifikation der ε₀‐Rekursiven Funktionen

This page was built for publication: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths