Bounding derivation lengths with functions from the slow growing hierarchy (Q1267850)

A problem in complexity theory is the classification of term rewrite systems according to it worst-case running length. The latter is given by the derivation lengths function that maps a natural number \(m\) to the maximum length of a reduction sequence starting from a term of complexity \(\leq m\). In the article under review the Buchholz-Cichon-Weiermann approach to subrecursive hierarchies is employed to characterize the growth rate of the derivation lengths function for a certain class of rewrite systems in terms of the slow growing hierarchy. This is done in a direct way via (a version of) Buchholz's \(\succ_k\)-relation -- in contrast to the meta-mathematical approach via profound ordinal analyses of \textit{W. Buchholz} [Ann. Pure Appl. Logic 75, 57-65 (1995; Zbl 0844.03031)]. The paper consists of three parts. The first part gives a comprehensive introduction to the presented approach and a good motivation for the technique. The second part is devoted to the proof of the main theorem of the paper, the Bounding Theorem. It shows that the \(\succ_k\)-relation is compatible with Wainer's pointwise collapsing functions \(\lambda\alpha.C_k(\alpha)\) [\textit{S. S. Wainer}, J. Symb. Logic 54, 608-614 (1989; Zbl 0701.03029)]. This part is presented in a syntactical way to achieve maximum precision within minimum space. The proofs are given in full detail and are carefully worked out. The last part shows how the Bounding Theorem can be applied to derive classifications of rewrite systems. The termination of such a system \(\mathcal R\) is typically shown by constructing an embedding of the reduction rules into a well-founded termination ordering. A general corollary of the Bounding Theorem states that, if this termination ordering is of ordertype \(\leq\bar{\theta}\alpha 0\) (\(\bar{\theta}\) of Schütte's notation system) and if some additional moderate assumptions are satisfied, then the \(\mathcal R\) derivation lengths are bounded in terms of \((k\mapsto F_{C_k(\alpha)}(k))\). According to the hierarchy comparison theorem this is a function from the slow growing hierarchy. Another application shows that the derivation lengths function of a rewrite system that can be embedded into the multiset resp. lexicographic path ordering is bounded by some primitive resp. multiply recursive function. So this paper gives a short and uniform proof of these well-known results, first established by \textit{D. Hofbauer} [Theor. Comput. Sci. 105, 129-140 (1992; Zbl 0759.68045)] for the multiset path ordering and by \textit{A. Weiermann} [ibid. 139, 355-362 (1995; Zbl 0874.68156)] for the lexicographic path ordering.