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, longstanding open problem (mentioned in [DJ90])
is decidability for one (lengthincreasing) monadic (string,
semiThue) rule. Termination is undecidable for nonlengthincreasing
monadic systems of rules [Car91]. For one monadic rule, confluence
is decidable [Kur90][Wra90]. What about confluence of one
nonmonadic 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]

AnneCé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.
SpringerVerlag.
 [Dau89]

Max Dauchet.
Simulation of Turing machines by a leftlinear 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.
SpringerVerlag.
 [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.
SpringerVerlag.
 [DJ90]

Nachum Dershowitz and JeanPierre Jouannaud.
Rewrite systems.
In J. van Leeuwen, editor, Handbook of Theoretical Computer
Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320.
NorthHolland, 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.
SpringerVerlag.
 [Kur90]

W. Kurth.
Termination und Konfluenz von SemiThueSystems mit nur einer
Regel.
PhD thesis, Technische Universitat Clausthal, Clausthal, Germany,
1990.
In German.
 [Wra90]

C. Wrathall.
Confluence of onerule 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.
SpringerVerlag.