About changing the ordering during Knuth-Bendix completion | SpringerLink
Skip to main content
Springer Nature Link
Log in

About changing the ordering during Knuth-Bendix completion

  • Conference paper
  • First Online:
STACS 94 (STACS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 775))

Included in the following conference series:

  • 148 Accesses

Abstract

We will answer a question posed in [5], and will show that Huet's completion algorithm [9] 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, 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 nonterminating but locally confluent system (see e.g. [11]). Our examples will show that this assumption is not true.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. R.V. Book. Thue systems as rewriting systems. Journal Symbolic Computation 3 (1987), 39–68.

    Google Scholar 

  2. R.V. Book, F. Otto. String-Rewriting Systems. Texts and Monographs in Computer Science (Springer, New York, 1993).

    Google Scholar 

  3. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science 17(3) (1982), 279–301.

    Google Scholar 

  4. N. Dershowitz. Completion and its applications. In: H. Ait-Kaci and M. Nivat(eds.): Resolution of Equations in Algebraic Structures, Vol. II: Rewriting Techniques (Academic Press, New York, 1989), 31–86.

    Google Scholar 

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

    Google Scholar 

  6. N. Dershowitz, J.-P. Jouannaud, J.W. Klop. More Problems in Rewriting. In: Proc. Fifth International Conference on Rewriting Techniques and Applications, Montreal, Canada, Lecture Notes in Computer Science 690 (Springer, Berlin, 1993), 468–487.

    Google Scholar 

  7. M. Hermann. Vademecum of divergent term rewriting systems. CRIN Report 88-R-082 (Centre de Recherche en Informatique de Nancy, 1988).

    Google Scholar 

  8. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27(4) (1980), 797–821.

    Google Scholar 

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

    Google Scholar 

  10. M. Jantzen. Confluent String Rewriting. EATCS Monographs on Theoretical Computer Science Vol. 14 (Springer, Berlin—Heidelberg, 1988).

    Google Scholar 

  11. 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).

    Google Scholar 

  12. D.E. Knuth, P. Bendix. Simple word problems in universal algebras. In: J. Leech (ed.): Computational Problems in Abstract Algebra (Pergamon, New York, 1970), 263–297.

    Google Scholar 

  13. D.A. Plaisted. A simple non-termination test for the Knuth-Bendix method. In: Proc. Eighth International Conference on Automated Deduction, Oxford, England, Lecture Notes in Computer Science 230 (Springer, Berlin, 1986), 79–88.

    Google Scholar 

  14. P. Purdom. Detecting loop simplifications. In: Proc. Second International Conference on Rewriting Techniques and Applications, Bordeaux, France, Lecture Notes in Computer Science 256 (Springer, Berlin, 1987), 54–61.

    Google Scholar 

  15. A. Sattler-Klein. About changing the ordering during Knuth-Bendix completion. Internal report (Universität Kaiserslautern, 1993). To appear.

    Google Scholar 

  16. J. Steinbach. Comparing on Strings: Iterated Syllable Ordering and Recursive Path Orderings. SEKI Report SR-89-15 (Universität Kaiserslautern, 1989).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Kaiserslautern, D-67653, Kaiserslautern, Germany

    Andrea Sattler-Klein

Authors
  1. Andrea Sattler-Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Patrice Enjalbert Ernst W. Mayr Klaus W. Wagner

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sattler-Klein, A. (1994). About changing the ordering during Knuth-Bendix completion. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds) STACS 94. STACS 1994. Lecture Notes in Computer Science, vol 775. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57785-8_140

Download citation

  • DOI: https://doi.org/10.1007/3-540-57785-8_140

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57785-0

  • Online ISBN: 978-3-540-48332-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation