Beyond conditional equations
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.
KeywordsMinimal Covering Forgetful Functor Initial Covering Conditional Equation Consistent Extension
Unable to display preview. Download preview PDF.
- [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
- [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
- [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
- [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
- [EM8S]H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1. Monographs in Computer Science, Springer, Berlin, 1985.Google Scholar
- [EM90]H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 2. Monographs in Computer Science, Springer, Berlin, 1990.Google Scholar
- [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
- [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
- [Gut75]J. V. Guttag. The specification and application to programming of abstract data types. PhD thesis, University of Toronto, 1975.Google Scholar
- [HK89]D. Hofbauer and R. Kutsche. Grundlagen des machinellen Beweisens. Vieweg, Braunschweig/Wiesbaden, 1989.Google Scholar
- [HS73]H. Herrlich and G. Strecker. Category Theory. Allyn and Bacon, Rockleigh, New Jersey, 1973.Google Scholar
- [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
- [Mac71]S. MacLane. Categories for the Working Mathematician. Springer, Berlin, 1971.Google Scholar
- [Mal73]A. I. Mal'cev. Algebraic Systems. Springer, Berlin, 1973. translated from the original edition 1970.Google Scholar
- [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
- [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
- [Rei87]H. Reichel. Initial Compulability, Algebraic Specifications, and Partial Algebras. Akademie-Verlag, Berlin, 1987.Google Scholar
- [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
- [Wir86]M. Wirsing. Structured algebraic apecification: a kernel language. Theoretical Computer Science, 43:123–250, 1986.Google Scholar
- [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
- [Wol91]U. Wolter. Deduction in partial equational Horn theories. Journal of Information Processing and Cybernetics (EIK), 27(2):85–128, 1991.Google Scholar
- [Zil74]S. N. Zilles. Algebraic specification of data types. Technical Report, MIT, Project MAC Progress Report 11, pages 28–52, 1974.Google Scholar