Problem #80
Originator: Hubert Comon
Date: April 1995
Summary:
Is strong sequentiality decidable for arbitrary rewrite systems?
Strong sequentiality is a property of rewrite systems introduced in
[HL78] (see [HL91a]), which ensures the existence of optimal
reduction strategies. Is strong sequentiality
decidable for arbitrary rewrite systems? What is the complexity of strong
sequentiality in the linear case? in the orthogonal case? Decidability
results for particular rewrite systems are given in
[HL91b, Toy92, JS94], among others.
References

[HL78]

Gérard Huet and Dallas S. Lankford.
On the uniform halting problem for term rewriting systems.
Rapport laboria 283, Institut de Recherche en Informatique et en
Automatique, Le Chesnay, France, March 1978.
 [HL79]

Gérard Huet and JeanJacques Lévy.
Call by need computations in nonambiguous linear term rewriting
systems.
Rapport Laboria 359, Institut National de Recherche en Informatique
et en Automatique, Le Chesnay, France, August 1979.
 [HL91a]

Gérard Huet and JeanJacques Lévy.
Computations in orthogonal rewriting systems, I and II.
In JeanLouis Lassez and Gordon Plotkin, editors, Computational
Logic: Essays in Honor of Alan Robinson, pages 395–443.
The MIT Press, Cambridge, MA, 1991.
This is a revision of [HL79].
 [HL91b]

Gérard Huet and JeanJacques Lévy.
Computations in orthogonal rewriting systems, II.
In JeanLouis Lassez and Gordon Plotkin, editors, Computational
Logic: Essays in Honor of Alan Robinson, chapter 12, pages 415–443.
The MIT Press, Cambridge, MA, 1991.
 [JS94]

JeanPierre Jouannaud and Walid Sadfi.
Strong sequentiality of leftlinear overlapping rewrite systems.
In Nachum Dershowitz and N. Lindenstrauss, editors, Proceedings
of the Fourth International Workshop on Conditional Rewriting Systems,
Jerusalem, Israel, July 1994.
SpringerVerlag.
 [Toy92]

Yoshihito Toyama.
Strong sequentiality of left linear overlapping term rewriting
systems.
In Andre Scedrov, editor, Seventh
Symposium on Logic in
Computer Science, Santa Cruz, CA, June 1992.
IEEE.