Encoding the Hydra battle as a rewrite system

Hélène Touzet 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In rewriting theory, termination of a rewrite system by Kruskal's theorem implies a theoretical upper bound on the complexity of the system. This bound is, however, far from having been reached by {\em known} examples of rewrite systems. All known orderings used to establish termination by Kruskal's theorem yield a multiply recursive bound. Furthermore, the study of the order types of such orderings suggests that the class of multiple recursive functions constitutes the least upper bound. Contradicting this intuition, we construct here a rewrite system which reduce by Kruskal's theorem and whose complexity is not multiply recursive. This system is even totally terminating. This leads to a new lower bound for the complexity of totally terminating rewrite systems and to rewrite systems that reduces by Kruskal's theorem. Our construction relies on the Hydra battle using classical tools from ordinal theory and subrecursive functions. It can be extended to exhaust the provably total functions of Peano arithmetic.
Type de document :
Communication dans un congrès
Lubos Brim and Jozef Gruska and Jiri Zlatuska. International Symposium on the Mathematical Foundations of Computer Science - MFCS'98, Aug 1998, Brno, Czech Republic, Springer, 1450, pp.267-276, 1998, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00098575
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:37
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00098575, version 1

Collections

Citation

Hélène Touzet. Encoding the Hydra battle as a rewrite system. Lubos Brim and Jozef Gruska and Jiri Zlatuska. International Symposium on the Mathematical Foundations of Computer Science - MFCS'98, Aug 1998, Brno, Czech Republic, Springer, 1450, pp.267-276, 1998, Lecture Notes in Computer Science. 〈inria-00098575〉

Partager

Métriques

Consultations de la notice

192