Lepper, Ingo: Simplification orders in term rewriting. 2001
Inhalt
- 1 Introduction
- 2 Preliminaries
- 2.1 Conventions
- 2.2 Basic definitions
- 2.3 Orders and Order types
- 2.4 Subrecursive Hierarchies
- 2.5 Complexity Classes
- 3 Term Rewriting
- 3.1 Basic Definitions
- 3.2 Abstract Orders on Terms
- 3.3 Semantic Orders on Terms
- 3.4 Syntactic Orders on Terms
- 3.5 Functions Computable by a TRS
- 4 Order Types
- 5 Derivation Lengths
- 5.1 omega-termination
- 5.2 Termination via KBO
- 5.3 Simple Termination is Complex
- 5.3.1 The Fixed Point Free Veblen Function
- 5.3.2 Fundamental Sequences and Hydrae below Delta_k
- 5.3.3 Encoding all Hydrae below Delta_k
- 5.3.4 Simulating all Hydra Battles below Delta_k
- 5.3.5 Proof of Total Termination
- 5.4 A Digression: LPO-Controlled Derivations
- 5.5 Another Digression: Ground Termination
- 6 Computability
- 6.1 Computability via PT
- 6.2 Computability via MPO and LPO
- 6.3 Computability via KBO
- 6.3.1 List Operations Compatible with KBO
- 6.3.2 Simulating a Timebounded RM
- 6.3.3 Long Linear Derivations
- 6.3.4 Hard Computation via KBO
- 6.4 Computability via Simple Termination
- 7 Very Long Size-Controlled Derivations
- 8 Conclusion
- Bibliography
- Glossary of Notation
- Index
- Curriculum Vitae