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:
-
linear, shallow, ∃*∀*-fragment ([STT97],
[STTT01]);
- linear, terminating, ∃*∀*∃*-fragment
([Vor97]),
∃*∀*-fragment ([Mar97]).
- right-ground, terminating, ∃*∀*-fragment
([Mar97]).
Decidbability results have been obtained for
-
the positive existential theory ([NPR97])
- unary signatures ([Jac96])
- left-linear right-ground systems ([Tis90])
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.