Hierarchical contextual rewriting with several levels

  • Wadoud Bousdira
  • Jean-Luc Rémy
Contributed Papers Rewriting Systems And Abstract Data Types
Part of the Lecture Notes in Computer Science book series (LNCS, volume 294)


We present our research on conditional hierarchical specifications with several levels and we study hierarchical contextual rewriting. This relation is defined in the conditional rewriting system framework and deals with terms with two levels which support boolean contexts. Our main result is a sufficient condition for confluence on ground terms of hierarchical specifications under some hypotheses. On the other hand, because we manipulate conditional equations whose preconditions are boolean expressions with a specific syntax, we have been led to establish a result of consistency with respect to the boolean sort of hierarchical specification which guarantees the existence of initial algebras which are faithful for the boolean sort. This condition is usually assumed by the researchers working in this area.


Critical Pair Boolean Expression Hierarchy Level Conditional Specification Ground Term 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Der87]
    N. Dershowitz. Termination. Journal of Symbolic Computation, 3(1):69–115, 1987.Google Scholar
  2. [Gan87]
    H. Ganzinger. Ground term confluence in parametric conditional equational specifications. In F.J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, West Germany, Lect. Notes in Comp. Sc. No 247, pages 286–298, Springer, Berlin, 1987.Google Scholar
  3. [Hue81]
    G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Comp. Sys. Sc, 23:11–21, 1981.Google Scholar
  4. [JK86]
    J.P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Computing, 15:1155–1194, 1986.Google Scholar
  5. [JW86]
    J.P. Jouannaud and B. Waldmann. Reductive conditional term rewriting systems. In M. Wirsing, editor, 3rd IFIP Conf. on Formal Description of Programming Concepts, Ebberup, Denmark, Elsevier Science Publishers, Amsterdam, 1986.Google Scholar
  6. [Kap87]
    S. Kaplan. Simplifying conditional term rewriting systems: unification, termination and confluence. Journal of Symbolic Computation (to appear), 1987.Google Scholar
  7. [KB70]
    D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297, Pergamon Press, Elmsford, N.Y., 1970.Google Scholar
  8. [KR87]
    S. Kaplan and J.L. Rémy. Completion algorithms for conditional rewriting systems. In H. AitKaci and M. Nivat, editors, Colloquium on the Resolution of Equations in Algebraic Structures, M.C.C. and I.N.R.I.A., Austin, USA, 1987.Google Scholar
  9. [New42]
    M.H.A. Newman. On theories with a combinatorial definition of equivalence. Annals of Math., 43:223–243, 1942.Google Scholar
  10. [NO84]
    M. Navarro and F. Orejas. On the equivalence of hierarchical and non-hierarchical rewriting on conditional term rewriting systems. In Eurosam Conference, Oxford, 1984.Google Scholar
  11. [REM82]
    J.L. REMY. Etude des systèmes de réécriture conditionnelle et applications aux types abstraits algébriques. Thèse d'Etat de l'Institut National Polytechnique de Lorraine, Nancy, 1982.Google Scholar
  12. [RZ84]
    J.L. Rémy and H. Zhang. Reveur4: a system for validating conditional algebraic specifications of abstract data types. In 6th ECAI Conference, Pisa, Italy, 1984.Google Scholar
  13. [Zha84]
    H. Zhang. REVEUR4: Etude et mise en oeuvre de la réécriture conditionnelle. Thèse de 3ème cycle, Université de Nancy 1, 1984.Google Scholar
  14. [ZR85]
    H. Zhang and J.L. Rémy. Contextual rewriting. In J.P. Jouannaud, editor, 1st Conference on Rewriting Techniques and Applications, Dijon, France, Lect. Notes in Comp. Sc. No 202, pages 46–62, Springer, Berlin, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Wadoud Bousdira
    • 1
  • Jean-Luc Rémy
    • 1
  1. 1.CRIN & INRIA Lorraine Campus ScientifiqueVandœuvre-lès-NancyFrance

Personalised recommendations