[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #31

Originator: Albert Meyer
Date: April 1991

Summary: Is there a decidable uniform word problem for which there is no variant on the rewriting theme that can decide it—without adding new symbols?

Is there a decidable uniform word problem for which there is no variant on the rewriting theme (for example, rewriting modulo a congruence with a decidable matching problem, or ordered rewriting) that can decide it—without adding new symbols to the vocabulary? There are decidable theories that cannot be decided with ordinary rewriting (see, for example, [Squ87]); on the other hand, any theory with decidable word problem can be solved by ordered-rewriting with some ordered system for some conservative extension of the theory (that is, with new symbols) [DMT85], or with a two-phased version of rewriting, wherein normal forms of the first system are inputs to the second [Bau85].

References

[Bau85]

G. Bauer. n-level rewriting systems. Theoretical Computer Science, 40:85–99, 1985.

[DMT85]

Nachum Dershowitz, Leo Marcus, and Andrzej Tarlecki. Existence, uniqueness, and construction of rewrite systems. Technical Report ATR-85(8354)-7, Computer Science Laboratory, The Aerospace Corporation, El Segundo, CA, December 1985.

[Squ87]

Craig Squier. Word problems and a homological finiteness condition for monoids. J. of Pure and Applied Algebra, 49:201–217, 1987.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]