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

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

Problem #35 (Solved !)

Originator: Nachum Dershowitz, L. Marcus
Date: April 1991

Summary: Can completion be incomplete when the ordering is changed en route?

Huet’s proof [Hue81] of the “completeness” of completion is predicated on the assumption that the ordering supplied to completion does not change during the process. Assume that at step i of completion, the ordering used is able to order the current rewriting relation →_Ri, but not necessarily →_Rk for k<i (since old rules may have been deleted by completion). Is there an example showing that completion is then incomplete (the persisting rules are not confluent)?

Remark

The answer is yes, even when completion terminates with finitely many rules [SK94].

References

[Hue81]

Gérard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Computer and System Sciences, 23(1):11–21, 1981.

[SK94]

Andrea Sattler-Klein. About changing the ordering during Knuth-Bendix completion. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 175–186, 1994.

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

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