Beyond conditional equations

Quasi-initial semantics for parametric algebraic specifications
  • Uwe Wolter
  • Michael Löwe
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


Inspired by the work of S. Kaplan about positive/negative conditional rewriting, we investigate initial semantics for algebraic specifications with Gentzen-formulas. Since the standard initial approach is limited to conditional equations (i.e. positive Horn-formulas), the notion of semi-initial and quasi-initial algebras is introduced and it is shown that all specifications with (positive) Gentzen-formulas admit quasi-initial models.

The whole approach is generalized to the parametric case where quasi-initiality generalizes to quasi-freeness. Since quasi-free objects need not be isomorphic, the persistency requirement is added to obtain a unique semantics for many interesting practical examples. Unique persistent quasi-free semantics can be described as a free construction when the parameter category is restricted to injective homomorphisms.

An example which does not admit a correct initial semantics but a correct unique persistent quasi-initial semantics demonstrates that the concepts introduced in this paper might be of some importance w.r.t. practical applications.


Minimal Covering Forgetful Functor Initial Covering Conditional Equation Consistent Extension 
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. [ABW87]
    K. Apt, H. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, Los Altos, 1987.Google Scholar
  2. [BDP*79]
    M. Broy, W. Dosch, H. Partsch, P. Pepper, and M. Wirsing. Existential quantifiers in abstract data types. In H. A. Maurer, editor, Sixth International Colloquium on Automata, Languages, and Programming, pages 73–87, Springer Lecture Notes on Computer Science 71, Berlin, 1979.Google Scholar
  3. [BF89]
    S. Bratella and G. File. A completeness result for SLDNF resolution. Technical Report Rapporto Interno Dip 9, Dipartimento di Mathematica, Universita di Padova, 1989.Google Scholar
  4. [ECB*89]
    H. Ehrig, I. Claßen, P. Boehm, W. Fey, M. Korff, and M. Löwe. Algebraic concepts for software development in ACT ONE, ACT TWO, and LOTOS. In GI Tagung Softwareentwicklung, pages 201–224, Springer Informatik Fachberichte 212, Berlin, 1989.Google Scholar
  5. [EM8S]
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1. Monographs in Computer Science, Springer, Berlin, 1985.Google Scholar
  6. [EM90]
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 2. Monographs in Computer Science, Springer, Berlin, 1990.Google Scholar
  7. [Gog88]
    J. A. Goguen. What is unification? A categorical view of substitution, equation, and solution. Technical Report CSLI-88-124, Center for the Study of Languages and Information, 1988.Google Scholar
  8. [GTW76]
    J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types. Research Report RC 6487, IBM T. J. Watson Research Center, Yorktown Heights, 1976. Also in: Current Trends in Programming IV: Data Structuring (ed. R.Yeh), Prentice Hall, 80–149 (1978).Google Scholar
  9. [Gut75]
    J. V. Guttag. The specification and application to programming of abstract data types. PhD thesis, University of Toronto, 1975.Google Scholar
  10. [HK89]
    D. Hofbauer and R. Kutsche. Grundlagen des machinellen Beweisens. Vieweg, Braunschweig/Wiesbaden, 1989.Google Scholar
  11. [HS73]
    H. Herrlich and G. Strecker. Category Theory. Allyn and Bacon, Rockleigh, New Jersey, 1973.Google Scholar
  12. [Kap88]
    S. Kaplan. Positive/negative conditional rewriting. In S. Kaplan and J. P. Jouannaud, editors, Conditional Term Rewriting Systems, pages 129–143, Springer Lecture Notes in Computer Science 308, Berlin, 1988.Google Scholar
  13. [Mac71]
    S. MacLane. Categories for the Working Mathematician. Springer, Berlin, 1971.Google Scholar
  14. [Mal73]
    A. I. Mal'cev. Algebraic Systems. Springer, Berlin, 1973. translated from the original edition 1970.Google Scholar
  15. [MM82]
    B. Mahr and J.A. Makowski. Characterizing specification languages which admit initial semantics. Technical Report 232, Technion Haifa, 1982. Also in Theoretical Computer Science, 31:49–59, 1984.Google Scholar
  16. [Rei81]
    H. Reichet. Behavioural equivalence — a unifying concept for initial and final specification methods. In Third Hungarian Computer Science Conference, pages 27–39, 1981.Google Scholar
  17. [Rei87]
    H. Reichel. Initial Compulability, Algebraic Specifications, and Partial Algebras. Akademie-Verlag, Berlin, 1987.Google Scholar
  18. [Wec88]
    W. Wechler. Universal algebra for computer scientists. Technical Report, Technische Universität Dresden, Sektion Mathematik, 1988. To be published as a book by Springer.Google Scholar
  19. [Wir86]
    M. Wirsing. Structured algebraic apecification: a kernel language. Theoretical Computer Science, 43:123–250, 1986.Google Scholar
  20. [Wir89]
    M. Wirsing. Algebraic Specification. Research Report MIP-8914, University of Passau, 1989. Updated version also in “Handbook of Theor. Comp. Sci. Vol. B, Elsevier, Amsterdam, 1990.Google Scholar
  21. [Wol91]
    U. Wolter. Deduction in partial equational Horn theories. Journal of Information Processing and Cybernetics (EIK), 27(2):85–128, 1991.Google Scholar
  22. [Zil74]
    S. N. Zilles. Algebraic specification of data types. Technical Report, MIT, Project MAC Progress Report 11, pages 28–52, 1974.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Uwe Wolter
    • 1
  • Michael Löwe
    • 1
  1. 1.FB InformatikTechnische Universität BerlinBerlin 10

Personalised recommendations