About Changing the Ordering during Knuth-Bendix Completion

Andrea Sattler-Klein
Fachbereich Informatik, Universitaet Kaiserslautern
D-67653 Kaiserslautern, GERMANY
E-mail: sattler@informatik.uni-kl.de


Abstract
We will answer a question posed in [DJK91] and will show  that
Huet's completion algorithm [Hu81] becomes incomplete, i.e. it
may generate a term rewriting system that is not confluent, if
it is modified in a way that the reduction ordering  used  for
completion can be changed during completion provided that  the
new ordering is compatible with the actual rules.
In particular, we will show that this  problem  may  not  only
arise if the modified completion algorithm does not terminate:
Even if the algorithm terminates  without  failure,  then  the
generated finite noetherian term rewriting system may be  non-
confluent. Most existing implementations of  the  Knuth-Bendix
algorithm provide the user with help in choosing  a  reduction
ordering: If an unorientable equation is encountered, then the
user has many  options, especially, the   one  to  orient  the
equation manually. The integration of this feature is based on
the widespread assumption that, if equations are  oriented  by
hand during completion and the completion  process  terminates
with success, then the generated finite system is a maybe non-
terminating but  locally  confluent  system (see e.g. [KZ89]).
Our examples will show that this assumption is not true.

References

[DJK91] N. Dershowitz, J.-P. Jouannaud, J.W. Klop.
	Open Problems in Rewriting.
	Proc. Fourth International Conference on Rewriting
	Techniques and Applications, Como, Italy,  Lecture
	Notes in Computer Science 488 (Springer, Berlin,
	1991), 445-456.

[Hu81]  G. Huet.
	A complete proof of correctness of the Knuth-
	Bendix completion algorithm.
	Journal Computer and System Science 23(1) (1981),
	11-21.

[KZ89]  D. Kapur, H. Zhang.
	RRL: Rewrite Rule Laboratory - User's Manual.
	GE Corporate Research and Development Report,
	Schenectady, New York, 1987
	(revised version: May 1989).

Keywords

Knuth-Bendix completion, term rewriting systems, string
rewriting systems

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1993/papers/
file: Sattler.SR-93-19.ps.Z