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

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

Problem #49

Originator: Miki Hermann
Date: December 1991

Summary: Can completion always be made terminating when limiting the depth of occurrences of critical pairs?

Suppose ordinary completion (as in [DJ90], for example, is non-terminating for some initial set of equations E, completion strategy, and reduction ordering. Must there be a finite depth N for E such that for any n > N restricting the generation of critical pairs to overlaps at positions that are no deeper than n in the overlapped left-hand side (but otherwise not changing the strategy) also produces a non-terminating completion sequence?

References

[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.

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

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