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


Problem #21

Originator: Max Dauchet
Date: April 1991

Summary: Is termination of one linear rule decidable?

Is termination of one linear (left and right) rule decidable? Left linearity alone is not enough for decidability [Dau89].

Remark

A less ambitious, long-standing open problem (mentioned in [DJ90]) is decidability for one (length-increasing) monadic (string, semi-Thue) rule. Termination is undecidable for non-length-increasing monadic systems of rules [Car91]. For one monadic rule, confluence is decidable [Kur90][Wra90]. What about confluence of one non-monadic rule?

Partial results for string rewrite rules have been obtained in [Ges03].

The history of the problem and the attempts to solve it are told in [Der05].

References

[Car91]
Anne-Cécile Caron. Linear bounded automata and rewrite systems: Influence of initial configurations on decision properties. In Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 1: Colloquium on Trees in Algebra and Programming (Brighton, U.K.), volume 493 of Lecture Notes in Computer Science, pages 74–89, Berlin, April 1991. Springer-Verlag.
[Dau89]
Max Dauchet. Simulation of Turing machines by a left-linear rewrite rule. In Nachum Dershowitz, editor, Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 109–120, Chapel Hill, NC, USA, April 1989. Springer-Verlag.
[Der05]
Nachum Dershowitz. Open. Closed. Open. In Jürgen Giesl, editor, 16th International Conference on Rewriting Techniques, volume 3467 of Lecture Notes in Computer Science, Nara, Japan, April 2005. Springer-Verlag.
[DJ90]
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.
[Ges03]
Alfons Geser. Termination of string rewriting rules that have one pair of overlaps. In Robert Nieuwenhuis, editor, 14th International Conference on Rewriting Techniques, volume 2706 of Lecture Notes in Computer Science, pages 410–423, Valencia, Spain, June 2003. Springer-Verlag.
[Kur90]
W. Kurth. Termination und Konfluenz von Semi-Thue-Systems mit nur einer Regel. PhD thesis, Technische Universitat Clausthal, Clausthal, Germany, 1990. In German.
[Wra90]
C. Wrathall. Confluence of one-rule Thue systems. In Proceedings of the First International Workshop on Word Equations and Related Topics (Tubingen), volume 572 of Lecture Notes in Computer Science, pages 237–246, Berlin, 1990. Springer-Verlag.

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