A complex example of a simplifying 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 : For a string rewriting system, it is known that termination by a simplification ordering implies multiply recursive complexity. This theoretical upper bound is, however, far from having been reached by known examples of rewrite systems. All known methods used to establish termination by simplification yield a primitive recursive bound. Furthermore, the study of the order types of simplification orderings suggests that the recursive path ordering is, in a broad sense, a maximal simplification ordering. This would imply that simplifying string rewrite systems cannot go beyond primitive recursion. Contradicting this intuition, we construct here a simplifying string rewriting system whose complexity is not primitive recursive. This leads to a new lower bound for the complexity of simplifying string rewriting systems
Type de document :
Communication dans un congrès
Kim G. Larsen and Sven Skyum and Glynn Winskel. International Colloquium on Automata, Languages, and Programming - ICALP'98, Jul 1998, Aalborg, Denmark, Springer, 1443, pp.507-517, 1998, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00098574
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-00098574, version 1

Collections

Citation

Hélène Touzet. A complex example of a simplifying rewrite system. Kim G. Larsen and Sven Skyum and Glynn Winskel. International Colloquium on Automata, Languages, and Programming - ICALP'98, Jul 1998, Aalborg, Denmark, Springer, 1443, pp.507-517, 1998, Lecture Notes in Computer Science. 〈inria-00098574〉

Partager

Métriques

Consultations de la notice

96