[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Andreas Weiermann
Date: April 1995
Summary: Is it possible to bound the derivation lengths of simply terminating rewrite systems by a multiply recursive function?
If the termination of a finite rewrite system over a finite signature can be proved using a simplification ordering, then the derivation lengths are bounded by a Hardy function of ordinal level less than the small Veblen number φ_{Ωω}0. (See [Wei93].) Is it possible to lower this bound by replacing the Hardy function by a slow growing function? That is, is it possible to bound the derivation lengths by a multiply recursive function?
Hélène Touzet [Tou97] has shown in her thesis that the answer is negative, exhibiting a simplifying rewrite system which has derivation bounds "longer" than multiply recursive. This work leaves open the question about what complexity can be achieved using simpifying rewrite systems. An improved version of the proof is given in [Tou98].
In [Tou99], Touzet has shown that for any multiple recursive function f there is a simplifying string rewriting system whose derivation length function dominates f.
The complete solution to the problem is contained in [Lep04], where it is shown that the upper bound from Weiermann is tight, hence for any Hardy function h of ordinal level below the small Veblen ordinal there is a simplifying term rewrite system whose derivation length function dominates h (see also [Lep01]).
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |