Advertisement

Modular algebraic specifications and the orientation of equations into rewrite rules

  • Frédéric Voisin
  • Michel Bidoit
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)

Abstract

We consider the problem of orienting equations into rewrite rules in the framework of a modular algebraic specification language. When a specification is built from “modules”, the orientation should neither be done globally for all modules, nor independently for each module. The termination ordering we define respects the modules boundaries. Equations of a module are partitioned into two sets: the ones that can be “statically” oriented, in a reusable way, and the ones with potential inter-modules conflicts which are handled in a “dynamic” phase.

Keywords

Generic Module Parameter Module Modular Structure Abstract Syntax Parameter Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137–159, 1987.Google Scholar
  2. 2.
    M. Bidoit. Pluss, un langage pour le développement de spécifications algébriques modulaires. Thèse d'Etat, Université de Paris Sud, 1989.Google Scholar
  3. 3.
    N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.Google Scholar
  4. 4.
    N. Dershowitz. Hierarchical termination. In Workshop on C. T. R. S., pages 89–105, Jerusalem, Israel, 1994. LNCS 968, Springer Verlag.Google Scholar
  5. 5.
    N. Dershowitz and J.-P. Jouannaud. Rewrite Systems, chapter 6, pages 243–320. Elsevier, Amsterdam, 1990.Google Scholar
  6. 6.
    M. Fernandez. Modèles de calcul multi-paradigmes fondés sur la réécriture. Thèse de doctorat, Université de Paris Sud, 1993.Google Scholar
  7. 7.
    M. Fernandez and J.-P. Jouannaud. Modular termination of term rewriting systems revisited. In Recent Trend in Data Type Specification, 10th Workshop on Specification of Abstract Data Types, joint with the 5th Compass Workshop, pages 255–272, S. Margherita, Italy, 1995. LNCS 906, Springer Verlag.Google Scholar
  8. 8.
    S. Garland and J. V. Guttag. A Guide to LP, The Larch Prover. Technical Report 82, DEC-SRC, 1991.Google Scholar
  9. 9.
    J. V. Guttag and J. J. Horning. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993. ISBN 0-387-94006-5/ISBN 3-540-94006-5.Google Scholar
  10. 10.
    M.R.K. Krishna Rao. Simple termination of hierarchical combinations of term rewriting systems. In 11th Symposium on Theoretical Aspects of Computer Science, pages 203–223. LNCS 789, Springer Verlag, 1994.Google Scholar
  11. 11.
    R. Nakajima, M. Honda, and Nakahara, R., Hierarchical program specification and verification — a many-sorted logical approach. Acta Informatica, 14:135–155, 1980.Google Scholar
  12. 12.
    E. Ohlebusch. Modular Properties of Composable Term Rewriting Systems. PhD thesis, Universität Bielefeld, Germany, 1994.Google Scholar
  13. 13.
    C. Roques. Modularité dans les spécifications algébriques: Théorie et Applications. Thèse de doctorat, Université de Paris Sud, 1994.Google Scholar
  14. 14.
    A. Rubio. Extension orderings. In Proc. of the 22th ICALP, Szeged, Hungary, 1995.Google Scholar
  15. 15.
    D.T. Sannella and R. M. Burstall. Structured theories in l.c.f. In C.A.A.P., pages 377–391, 1983.Google Scholar
  16. 16.
    Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett., 25:141–143, 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Frédéric Voisin
    • 1
  • Michel Bidoit
    • 2
  1. 1.C.N.R.S. U.R.A. 410 and Université de Paris-SudOrsay CedexFrance
  2. 2.C.N.R.S. U.R.A. 1327 and Ecole Normale Supérieure, L.I.E.N.S.Paris Cedex 05France

Personalised recommendations