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


Problem #51 (Solved !)

Originator: Hubert Comon, Max Dauchet
Date: June 1993

Summary: Is the first order theory of one-step rewriting decidable?

For an arbitrary finite term rewriting system R, is the first order theory of one-step rewriting (→R) decidable? Decidability would imply the decidability of the first-order theory of encompassment (that is, being an instance of a subterm) [CCD93], as well as several known decidability results in rewriting. (It is well known that the theory of →R* is in general undecidable.)

Remark

This has been answered negatively in [Tre96, Tre98]. Sharper undecidability results have been obtained for the following subclasses of rewrite systems:

Decidbability results have been obtained for

References

[CCD93]
Anne-Cécile Caron, Jean-Luc Coquidé, and Max Dauchet. Encompassment properties and automata with constraints. In Claude Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 328–342, Montreal, Canada, June 1993. Springer-Verlag.
[Com97]
Hubert Comon, editor. 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, Barcelona, Spain, June 1997. Springer-Verlag.
[Jac96]
Florent Jacquemard. Automates d’arbres et Réécriture de termes. PhD thesis, Université de Paris-Sud, 1996. In French.
[Mar97]
Jerzy Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. In Comon [Com97], pages 241–253.
[NPR97]
Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg. On equality up-to constraints over finite trees, context unification and one-step rewriting. In William McClune, editor, 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Artificial Intelligence, pages 34–48, Townsville, Australia, July 1997. Springer-Verlag.
[STT97]
Franck Seynhaeve, Marc Tommasi, and Ralf Treinen. Grid structures and undecidable constraint theories. In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 357–368, Lille, France, April 1997. Springer-Verlag.
[STTT01]
Franck Seynhaeve, Sophie Tison, Marc Tommasi, and Ralf Treinen. Grid structures and undecidable constraint theories. Theoretical Computer Science, 258(1–2):453–490, May 2001.
[Tis90]
Sophie Tison. Automates comme outil de décision dans les arbres. Dossier d’habilitation à diriger des recherches, December 1990. In French.
[Tre96]
Ralf Treinen. The first-order theory of one-step rewriting is undecidable. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 276–286, New Brunswick, NJ, USA, July 1996. Springer-Verlag.
[Tre98]
Ralf Treinen. The first-order theory of linear one-step rewriting is undecidable. Theoretical Computer Science, 208(1–2):179–190, November 1998.
[Vor97]
Sergei Vorobyov. The first-order theory of one step rewriting in linear noetheran systems is undecidable. In Comon [Com97], pages 254–268.

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