Bounding derivation lengths with functions from the slow growing hierarchy
type: Item
instance of: scholarly article
title: Bounding derivation lengths with functions from the slow growing hierarchy
zbMATH Open document ID: 0919.03036
author: Andreas Weiermann
published in: Archive for Mathematical Logic
publication date: 1999-08-19T00:00:00Z
review text: 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(\…
reviewed by: Benjamin Blankertz
Mathematics Subject Classification ID: 03D20
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03F15
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 1210626
zbMATH Keywords: term rewrite systems
zbMATH Keywords: termination ordering
zbMATH Keywords: derivation lengths
zbMATH Keywords: complexity characterizations
zbMATH Keywords: hierarchy comparison theorem
zbMATH Keywords: subrecursive hierarchies
zbMATH Keywords: growth rate
zbMATH Keywords: slow growing hierarchy
MaRDI profile type: Publication
full work available at URL: s001530050107
OpenAlex ID: W2092340582
DOI: 10.1007/S001530050107
Recommended article: Equational derivation vs. computation
Recommended article: Some interesting connections between the slow growing hierarchy and the Ackermann function
Recommended article: Q4447240
Recommended article: Q4541806
Recommended article: Termination proofs by multiset path orderings imply primitive recursive derivation lengths
Recommended article: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
Recommended article: Derivation lengths and order types of Knuth--Bendix orders
Recommended article: Q5297489
Recommended article: An upper bound on the derivational complexity of Knuth-Bendix orderings.
description: scientific article; zbMATH DE number 1210626