[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #81 (Solved !)

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?

Remark

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]).

References

[Lep01]
Ingo Lepper. Simplification Orders in Term Rewriting. PhD thesis, Universität Münster, Germany, 2001. Available at http://wwwmath.uni-muenster.de/logik/publ/diss/9.html.
[Lep04]
Ingo Lepper. Simply terminating rewrite systems with long derivations. Archive for Mathematical Logic, 43(1):1–18, 2004.
[Tou97]
Hélène Touzet. Propriétés combinatoires pour la terminaison de systèmes de réécriture. PhD thesis, Université Henri Poincaré – Nancy 1, Nancy, France, September 1997. In French.
[Tou98]
Hélène Touzet. Encoding the Hydra battle as a rewrite system. In Lubos Brim, Jozef Gruska, and Jirí Zlatuska, editors, Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 267–276, Brno, Czech Republic, August 1998. Springer-Verlag.
[Tou99]
Hélène Touzet. A characterization of multiply recursive functions with Higman’s lemma. In Paliath Narendran and Michael Rusinowitch, editors, 10th International Conference on Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, pages 163–174, Trento, Italy, July 1999. Springer-Verlag.
[Wei93]
Andreas Weiermann. Bounding derivation lengths with functions from the slow growing hierarchy. Preprint Münster, 1993.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]