Algebraic and operational semantics of positive/negative conditional algebraic specifications

  • Stéphane Kaplan
Session 11 Logic Prog. And Theorem Proving
Part of the Lecture Notes in Computer Science book series (LNCS, volume 338)


This paper introduces positive/negative conditional term rewriting systems, with rules of the generic form : u = v Λ u' ≠ v' ⇒ λ → ρ, as they often appear in algebraic specifications. We consider the algebraic semantics of such systems (viewed as sets of axioms). They do not in general have initial models ; however, we show that they admit quasi-initial models, that are in some sense extremal within the class of all models. We then introduce the subclass of reducing rewrite systems, constrained by the condition : λ > ρ, u, v, u', v' (for some reduction ordering >). For such systems, we show that an optimal rewrite relation → may be defined, and constructed as a "limit". We prove the total validity of an interpreter that computes the normal forms of terms for →. It is then shown that when → is confluent, the algebra of normal forms is a quasi-initial model. We state a general result about the converse. Lastly, we present a complete critical-pair criterion à la Knuth-Bendix to check for the confluence of reducing systems.


Normal Form Operational Semantic Ground Term Algebraic Semantic Ground Instance 
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. [ABW 87]
    K. Apt, H. Blair, A. Walker, Towards a theory of declarative knowledge, I.B.M. T.J. Watson Research Center Report, submitted for publication (1987)Google Scholar
  2. [ADJ 78]
    J.A. Goguen, J.W. Thatcher, E.G. Wagner,An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types, Current Trends in Programming Methodology, Vol. 4, Ed. Yeh R., Prentice-Hall, pp. 80–149 (1978)Google Scholar
  3. [BBK 87]
    J. Baeten, J. Bergstra, J.W. Klop,Term rewriting systems with priority, Proc. of the RTA'87 Conf., LNCS 256, Springer Verlag (1987)Google Scholar
  4. [BBWT 81]
    J. Bergstra, M. Broy, M. Wirsing, J. Tucker,On the power of algebraic specifications, Proc. of the MFCS'81 Conference, LNCS 118 (1981)Google Scholar
  5. [BH 86]
    N. Bidoit, R. Hull,Positivism vs. Minimalism in Deductive Data Bases, Proc. of the ACM SIGACT-SIGMOD Symposium on Principle of Data Base Systems, Cambridge (1986)Google Scholar
  6. [Dershowitz 85]
    N. Dershowitz,Termination, Proc. of the 1st Conf. on Rewriting Techniques and Applications, LNCS 202, Dijon — France (1985)Google Scholar
  7. [EM 85]
    H. Ehrig, B. Mahr,Fundamentals of algebraic specifications. I: Equations and initial semantics, EATCS monographs on Theoretical Computer Science, Springer Verlag (1985)Google Scholar
  8. [Ganziger 86]
    H. Ganziger,Ground term confluence in parametric conditional equational specifications, Proc. of the STACS'87 Conf., LNCS 252, Springer Verlag (1987)Google Scholar
  9. [Huet 77]
    G. Huet,Confluent reductions: abstract properties and applications to term rewriting systems, Proc. of the 18th FOCS Conf., Providence (1978)Google Scholar
  10. [HO 80]
    G. Huet, D.C. Oppen,Equations and rewrite rules: a survey, Formal languages: Perspective and open problems, R. Book Ed., Academic Press (1980)Google Scholar
  11. [JK 84]
    J.-P. Jouannaud, C. Kirchner,Completion of a set of rules modulo a set of equations, Proc. of the 11th POPL Conf. (1984)Google Scholar
  12. [JW 86]
    J.-P. Jouannaud, B. Waldmann, Reductive conditional term rewriting systems, Proc. of the 3rd TC2 Working Conf. on the formal Description of Programming Concepts, North-Holland Pub. Company (1986)Google Scholar
  13. [Kaplan 82]
    S. Kaplan,Specifications of abstract data types: the power of several classes of axioms with semi-decidable congruence, Proc. of the AFCET Mathematics for Computer Science Conf., Paris (1982)Google Scholar
  14. [Kaplan 84a]
    S. Kaplan,Conditional rewrite rules, TC 33 (1984)Google Scholar
  15. [Kaplan 84b]
    S. Kaplan,Fair conditional term rewrite systems, Report 194, University of Paris-South (1984)Google Scholar
  16. [Kaplan 87]
    S. Kaplan,Simplifying conditional term rewriting systems, to appear in the Journal of Symbolic Computation (1987)Google Scholar
  17. [Klop 87]
    J.W. Klop,Term rewriting systems: a tutorial, Bulletin of the EATCS, 32, pp. 143–183 (1987)Google Scholar
  18. [Lifschitz 86]
    V. Lifschitz,On the declarative semantics of logic programs with negation, Workshop on the Foundations of Deductive Data Bases and Logic Programming, Washington D.C. (1986)Google Scholar
  19. [Przymusinski 86]
    T.C. Przymusinski,On the semantics of stratified deductive databases, Workshop on the Foundations of Deductive Data Bases and Logic Programming, Washington D.C. (1986)Google Scholar
  20. [RZ 84]
    J.L. Rémy, H. Zhang,REVEUR4: a system for validating conditional algebraic specifications of abstract data types, Proc. of the 6th ECAI Conf. (1984)Google Scholar
  21. [RZ 85]
    J.L. Rémy, H. Zhang,Contextual rewriting, Proc. of the 1st RTA Conf., LNCS 202, Springer Verlag (1985)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Stéphane Kaplan
    • 1
    • 2
    • 3
  1. 1.Computer Science DepartmentHebrew University, Givat RamJerusalemIsrael
  2. 2.L.R.I., Bât. 490Université des SciencesOrsay CedexFrance
  3. 3.Computer Science DepartmentBar-Ilan UniversityRamat-GanIsrael

Personalised recommendations