Skip to main content
SpringerLink
Log in

Infinite, canonical string rewriting systems generated by completion

  • Session 15: Unification and Equality II
  • Conference paper
  • First Online:
Logic Programming and Automated Reasoning (LPAR 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 624))

  • 140 Accesses

Abstract

Most versions of the Knuth-Bendix completion ’procedure’ are designed to compute when possible a canonical rewriting system. We show that even for string rewriting systems (SRSs) canonical systems may be generated by completion which are not recursively enumerable. This may happen also if the SRS has decidable word problem. We analyze how this phenomenon depends on the ordering used for completion. It turns out that in general if a SRS is completed with respect to a length-lexicographic ordering divergence sequences encoding the input/output behaviour of any primitive recursive function as well as any recursively enumerable set and some non recursively enumerable sets may be generated. But, if a SRS with decidable word problem is completed with such an ordering, then the generated canonical system will be recursive.

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.

References

  1. Avenhaus, J.: Transforming infinite rewrite systems into finite rewrite systems by embedding techniques. SEKI-Report SR-89-21, Universität Kaiserslautern (1989)

    Google Scholar 

  2. Avenhaus, J.: Proving equational and inductive theorems by completion and embedding techniques. Proc. RTA '91, Como (1991) 361–373

    Google Scholar 

  3. Book, R.V.: Thue systems as rewriting systems. Proc. RTA '85, Dijon (1985) 63–94

    Google Scholar 

  4. Chen, H. and Hsiang, J. and Kong, H.-C: On finite representations of infinite sequences of terms. Preprint, Extended abstract in: Proc. CTRS '90, Montreal (1990) 37–44

    Google Scholar 

  5. Gramlich, B.: Unification of term schemes — Theory and Applications. SEKI-Report SR-88-18, Universität Kaiserslautern (1988)

    Google Scholar 

  6. Hermann, M.: Vademecum of divergent term rewriting systems. Research report 88-R-082, Centre de Recherche en Informatique de Nancy (1988)

    Google Scholar 

  7. Hermann, M.: Chain properties of rule closures. Proc. STAGS '89, Paderborn (1989) 339–347

    Google Scholar 

  8. Hermann, M.: Crossed term rewriting systems. Research report 89-R-003, Centre de Recherche en Informatique de Nancy (1989)

    Google Scholar 

  9. Hermann, M. and Privara, I.: On nontermination of Knuth-Bendix algorithm. Proc. ICALP '86, Rennes (1986) 146–156

    Google Scholar 

  10. Kapur, D. and Narendran, P.: The Knuth-Bendix completion procedure and Thue systems. SIAM J. Comput., Vol. 14, No 4 (1985) 1052–1071

    Article  Google Scholar 

  11. Kirchner, H.: Schematization of infinite sets of rewrite rules. Application to the divergence of completion processes. Proc. RTA '87, Bordeaux (1987) 180–191

    Google Scholar 

  12. Kirchner, H. and Hermann, M.: Computing meta-rules from crossed rewrite systems. Preprint, Extended abstract in: Proc. CTRS '90, Montreal (1990) 60

    Google Scholar 

  13. Lange, S.: Towards a set of inference rules for solving divergence in Knuth-Bendix completion. Proc. All '89, Reinhardsbrunn Castle (1989) 304–316

    Google Scholar 

  14. Lange, S. and Jantke, K.P.: Towards a learning calculus for solving divergence in KnuthBendix completion. Communications of the Algorithmic Learning Group, TH Leipzig (1989)

    Google Scholar 

  15. Mong, C.-T. and Purdom, P.W.: Divergence in the completion of rewriting systems. Technical report, Dept. of Comp. Science, Indiana University (1989)

    Google Scholar 

  16. Sattler-Klein, A.: Divergence phenomena during completion. Proc. RTA '91, Como (1991) 374–385

    Google Scholar 

  17. Sattler-Klein, A.: Infinite, canonical string rewriting systems generated by completion. Internal report, Universität Kaiserslautern (to appear)

    Google Scholar 

  18. Steinbach, J.: Comparing on Strings. Iterated syllable ordering and recursive path orderings. SEKI-Report SR-89-15, Universität Kaiserslautern (1989)

    Google Scholar 

  19. Thomas, M. and Jantke, K.P.: Inductive inference for solving divergence in Knuth-Bendix completion. Proc. All '89, Reinhardsbrunn Castle (1989) 288–303

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Kaiserslautern, Postfach 3049, 6750, Kaiserslautern, FRG

    Andrea Sattler-Klein

Authors
  1. Andrea Sattler-Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sattler-Klein, A. (1992). Infinite, canonical string rewriting systems generated by completion. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013081

Download citation

  • DOI: https://doi.org/10.1007/BFb0013081

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55727-2

  • Online ISBN: 978-3-540-47279-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation