In this thesis the author approaches complexity problems of term rewriting theory using results and techniques from proof theory. The thesis contains 8 chapters.
Chapter 1 contains an introduction with a short presentation of the thesis.
In Chapter 2, Preliminaries, basic definition and results are presented. So the author consider orders, ordinals and order types, subrecursive hierarchies, ordinal notation systems, Bachmann systems. The introduction of complexity classes and various concept of computation are presented.
Term Rewriting is the subject of Chapter 3. First the basics are presented and then abstract orders on terms, Kruskal’s Tree Theorem for terms and simplification order. Semantic orders as induced by interpretations and \( \Sigma \)-algebras form the subject of Section 3.3. This section contains also the termination hierarchy of Zantema and a theorem of Touzet about connections between weak total termination and total termination. Section 3.4 introduces the syntactic simplification orders: multiset path order (MPO), lexicographic path order (LPO) and Knuth-Bendix orders (KBO). The final section is concerned with functions computable by a term rewriting system and computability via some termination proof method, in connection with computability on Turing machines.
Order Types is the subject of Chapter 4. The author presents results concerning MPO and LPO and proves a new characterization of the order types of KBO. So the author shows that the order types of the simplification orders (on terms) can get huge and that LPO exhausts these order types for terms as well as for strings. In contrast to this, any KBO has a surprisingly tiny order type, while MPO resides between the other two termination proof methods. As a main result he shows that KBO and MPO have to exchange positions.
Chapter 5, Derivation Lengths, is the most important part of this thesis. The subject of this chapter is the derivation complexity as one way to measure the strength of a termination proof method. First a review of complexity bounds occurring within \(\omega\)-termination, including termination via MPO and LPO, is presented. Section 5.2 is devoted to KBO, it contains the author’s interpretation of KBO into \(\mathbb N,\) which is then used to show termination via KBO implies \(\omega^2\)-termination. Simple termination in general is cared for in Section 5.3. The construction of totally terminating term rewriting systems (TRSs) with longest possible derivations is presented. Also he presents various principles concerning connections between order types, complexities, and subrecursive hierarchies. In Section 5.4 the constructed TRSs are used in the context of (generalized) LPO-controlled derivations, a concept introduced by Harvey Friedman (1999). The final section of this chapter is devoted to differences between closed and open versions of syntactic simplification orders.
The author treats computability via simple termination in Chapter 6, Computability. He presents his new results about computability via KBO and shows that function classes well known from complexity theory occur as classes of functions computable via the usual termination proof methods. The final section of this chapter is devoted to differences between closed and open versions of syntactic simplification orders.
Chapter 7, Very Long Size-Controlled Derivations, contains the construction of TRSs having very long size-controlled derivations. The author presents a closer look at results from Section 5.3 about TRSs simulating Hydra battles.
Chapter 8, Conclusions, contains a short summary, open problems, conjectures, and proposals for further research. We list here these problems:
Problem 1. Find and prove strong instances of the Hardy function principle.
Problem 2. What shortest complexities occur within simple termination?
Problem 3. What are the optimal complexity bounds for the ground versions of KBO, MPO, and LPO?
Problem 4. Construct syntactic simplification orders which reach beyond \(\omega^2\) -termination.
Problem 5. What complexity bounds are imposed by \(\alpha\)-termination?
Problem 6. What functions are computable via simple termination?
Problem 7. Consider triples \((n,m,r) \in \mathbb N \times \mathbb N \times\mathbb R.\) Over signatures containing \(n\) symbols, what maximal \(f_r\) -controlled derivation lengths are possible for TRSs containing \(m\) rules?