Modular aspects of rewrite-based specifications | SpringerLink
Skip to main content
Springer Nature Link
Log in

Modular aspects of rewrite-based specifications

  • Contributed Papers
  • Conference paper
  • First Online:
Recent Trends in Algebraic Development Techniques (WADT 1997)

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

Included in the following conference series:

  • 125 Accesses

Abstract

We investigate modular properties of term rewriting systems, the basic operational formalism for equational specifications. First we study sufficient conditions for the preservation of the termination property under disjoint (and more general) combinations of term rewriting systems. By means of a refined analysis of existing approaches we show how to prove several new asymmetric preservation results. For this purpose we introduce two interesting new properties of term rewriting systems related to collapsing reductions: uniquely collapsing and collapsing confluent. We discuss these properties w.r.t. well-known confluence, and normal form properties, and show that they are modular consistency for left-linear systems, but not in general.

This work was supported by a Marie Curie Research Fellowship of the European Community under contract No ERBFMBICT961235.

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. L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In J. Siekmann, ed., Proc. 8th CADE, LNCS 230, pp. 5–20. Springer, 1986.

    Google Scholar 

  2. N. Dershowitz. Hierarchical termination. In N. Dershowitz and N. Lindenstrauss, eds., Proc. 4th CTRS (1994), LNCS 968, pp. 89–105. Springer, 1995.

    Google Scholar 

  3. N. Dershowitz. Innocuous constructor-sharing combinations. In H. Comon, ed., Proc. 8th RTA, LNCS 1232, pp. 202–216. Springer, 1997.

    Google Scholar 

  4. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, ed., Formal models and semantics, Handbook of Theoretical Computer Science, volume, B, chapter 6, pp. 243–320. Elsevier-The MIT Press, 1990.

    Google Scholar 

  5. K. Drosten. Termersetzungssysteme. Informatik-Fachberichte 210. Springer, 1989.

    Google Scholar 

  6. M. Fernández and J.-P. Jouannaud. Modular termination of term rewriting systems revisited. In Recent Trends in Data Type Specification, LNCS 906, pp. 255–272, Springer, 1995.

    Google Scholar 

  7. B. Gramlich. Generalized sufficient conditions for modular termination of rewriting. Applicable Algebra in Engineering, Communication and Computing, 5:131–158, 1994.

    Google Scholar 

  8. B. Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 24:3–23, 1995.

    Google Scholar 

  9. B. Gramlich. Termination and Confluence Properties of Structured Rewrite Systems. PhD thesis, Fachbereich Informatik, Universität Kaiserslautern, Jan. 1996.

    Google Scholar 

  10. J. W. Klop. Term rewriting systems.In S. Abramsky, D. Gabbay, and T. Maibaum, eds., Handbook of Logic in Computer Science, volume 2, chapter 1, pp. 2–117. Clarendon Press, Oxford, 1992.

    Google Scholar 

  11. J. W. Klop, A. Middeldorp, Y. Toyama, and R. Vrijer. Modularity of confluence: A simplified proof. Information Processing Letters, 49:101–109, 1994.

    Article  Google Scholar 

  12. M.R.K. Krishna Rao. Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science, 151(2):487–512, Nov. 1995.

    Google Scholar 

  13. M. Marchiori. Modularity of UN→ for left-linear term rewriting systems. Technical Report CS-119433, CWI, Amsterdam, May 1994.

    Google Scholar 

  14. M. Marchiori. Modularity of Completeness Revisited. In J. Hsiang, ed., Proc. 6th RTA, LNCS 914, pp. 2–10. Springer, 1995.

    Google Scholar 

  15. A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Free University, Amsterdam, 1990.

    Google Scholar 

  16. A. Middeldorp, H.Ohsaki and H. Zantema. Transforming termination by self-labelling. In Proc. 13th CADE, LNAI 1104, pp. 373–387. Springer, 1996.

    Google Scholar 

  17. A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. Journal of Symbolic Computation, 15:331–348, Sept. 1993.

    Google Scholar 

  18. E. Ohlebusch. Modular Properties of Composable Term Rewriting Systems. PhD thesis, Universität Bielefeld, 1994. Report 94-01.

    Google Scholar 

  19. E. Ohlebusch. On the modularity of termination of term rewriting systems. Theoretical Computer Science, 136:333–360, 1994.

    Article  Google Scholar 

  20. E. Ohlebusch. Modular properties of composable term rewriting systems. Journal of Symbolic Computation, 20(1):1–42, 1995.

    Article  Google Scholar 

  21. M. Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. Journal of Symbolic Computation, 8(1):51–99, 1989.

    Google Scholar 

  22. M. Schmidt-Schauß, M. Marchiori, and S. Panitz. Modular termination of rconsistent and left-linear term rewriting systems. Theoretical Computer Science, 149(2):361–374, 1995.

    Google Scholar 

  23. Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, 1987.

    Google Scholar 

  24. Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128–143, 1987.

    Article  Google Scholar 

  25. Y. Toyama, J. Klop, and H. Barendregt. Termination for direct sums of left-linear complete term rewriting systems. Journal of the ACM, 42(6):1275–1304, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Lorraine & CRIN, BP 101, 54602, Villers-lés-Nancy, France

    Bernhard Gramlich

Authors
  1. Bernhard Gramlich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Francesco Parisi Presicce

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gramlich, B. (1998). Modular aspects of rewrite-based specifications. In: Presicce, F.P. (eds) Recent Trends in Algebraic Development Techniques. WADT 1997. Lecture Notes in Computer Science, vol 1376. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-64299-4_38

Download citation

  • DOI: https://doi.org/10.1007/3-540-64299-4_38

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-69719-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation