Hostname: page-component-6bf8c574d5-7jkgd Total loading time: 0 Render date: 2025-02-16T01:32:59.387Z Has data issue: false hasContentIssue false
  • English
  • Français

Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras

Published online by Cambridge University Press:  04 March 2009

Hans-Jörg Kreowski  and
Till Mossakowski
Hans-Jörg Kreowski
Affiliation:
Universität Bremen, Fachbereich 3, Postfach 33 04 40, D-28334 Bremen E-mail: kreo@informatik.uni-bremen.de
Till Mossakowski
Affiliation:
Universität Bremen, Fachbereich 3, Postfach 33 04 40, D-28334 Bremen E-mail: till@informatik.uni-bremen.de
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we investigate several logical frameworks whose expressiveness lies between Conditional Equational Logic and Horn Clause Logic. The main result deals with the PART-construction, which interprets total based algebras as partial algebras. This construction can be viewed as a simulation of Horn Clause Theories by means of Conditional Equational Theories. Other constructions in other frameworks are extendable to simulations in a similar way. The notion of categorical retractive simulation captures some essential properties of these, which allows us to measure the equivalence and difference between institutions.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 5 , Issue 2 , June 1995 , pp. 189 - 215
Copyright
Copyright © Cambridge University Press 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Adámek, J., Herrlich, H. and Strecker, G. (1990) Abstract and Concrete Categories, Wiley, New York.Google Scholar
Adámek, J. and Rosický, J. (1994) Locally presentable and accessible categories, Cambridge University Press.CrossRefGoogle Scholar
Antimirov, V. and Degtyarev, A. (1992) Consistency of equational enrichments. In: Voronkov, A. (ed.) Logic Programming and Automated Reasoning 92. Springer-Verlag Lecture Notes in Computer Science 624 313–402.Google Scholar
Antimirov, V. and Degtyarev, A. (1993) Consistency and semantics of equational definitions over predefined algebras. In: Rusinowitch, M. and Rémy, J. L. (eds.) Conditional Term Rewriting Systems 92. Springer-Verlag Lecture Notes in Computer Science 656 67–81.CrossRefGoogle Scholar
Astesiano, E. and Cerioli, M. (1992) Relationships between logical frameworks. In: Bidoit, M. and Choppy, C. (eds.) Proc. 8th ADT workshop. Springer-Verlag Lecture Notes in Computer Science 655 126–143.CrossRefGoogle Scholar
Barr, M. (1989) Models of horn theories. Contemporary Mathematics 92 1–7.CrossRefGoogle Scholar
Baumeister, H. (1991) Unifying initial and loose semantics of parameterized specifications in an arbitrary institution. In: Abramsky, S. and Maibaum, T. S. E. (eds.) TAPSOFT 91 Vol. 1: CAAP 91. Springer-Verlag Lecture Notes in Computer Science 493, 103–120.CrossRefGoogle Scholar
Burstall, R. M. and Goguen, J. A. (1977) Putting theories together to make specifications. In: Proceedings of the 5th International Joint Conference on Artificial Intelligence, Cambridge1045–1058.Google Scholar
Burmeister, P. (1982) Partial algebras - survey of a unifying approach towards a two-valued model theory for partial algebras. Algebra Universalis 15 306–358.CrossRefGoogle Scholar
Burmeister, P. (1986) A model theoretic approach to partial algebras, Akademie Verlag, Berlin.Google Scholar
Broy, M. and Wirsing, M. (1982) Partial abstract types. Acta Informatica 18 47–64.CrossRefGoogle Scholar
Cerioli, M. (1993) Relationships between Logical Formalisms, PhD thesis, TD–4/93, Università di Pisa-Genova-Udine.Google Scholar
Ehrig, H. and Mahr, B. (1985) Fundamentals of Algebraic Specification 1, Springer-Verlag, Heidelberg.CrossRefGoogle Scholar
Ehrig, H. and Mahr, B. (1990) Fundamentals of Algebraic Specification 2, Springer-Verlag, Heidelberg.CrossRefGoogle Scholar
Goguen, J. A. (1978) Order sorted algebras: Exceptions, error sorts, coercion and overloaded operators. Semantics and theory of computation report no. 14, University of California, Los Angeles.Google Scholar
Goguen, J. A. and Burstall, R. M. (1992) Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39 95–146. (Predecessor in: Springer-Verlag Lecture Notes in Computer Science (1984) 164 221–256.)CrossRefGoogle Scholar
Goguen, J. A. and Meseguer, J. (1986) Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D. and Lindstrom, G. (eds.) Logic Programming. Functions, Relations and Equations, Prentice-Hall 295–363.Google Scholar
Gogolla, M. (1986) Über partiell geordnete Sortenmengen und deren Anwendung zur Fehlerbehandlung in abstrakten Datentypen, PhD thesis, Braunschweig.Google Scholar
Kreowski, H.-J. (1987) Partial algebras flow from algebraic specifications. In: Proc. ICALP 87. Springer-Verlag Lecture Notes in Computer Science 267 521–530.CrossRefGoogle Scholar
Meseguer, J. (1989) General logics. Logic Colloquium 87, North-Holland275–329.Google Scholar
Mosses, P. (1989) Unified algebras and institutions. Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science 304–312.Google Scholar
Mossakowski, T. (1993a) Parameterized recursion theory - a tool for the systematic classification of specification methods. In: Nivat, M., Rattray, C., Rus, T. and Scollo, G. (eds.) Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, 1993, Workshops in Computing, Springer-Verlag 139–146. (Submitted to Theoretical Computer Science.)Google Scholar
Mossakowski, T. (1995) A hierarchy of institutions separated by properties of parameterized abstract data types. In: Astesiano, E., Reggio, G. and Tarlecki, A. (eds.) Recent Trends in Data Type Specification (Proceedings) Springer-Verlag Lecture Notes in Computer Science 906.CrossRefGoogle Scholar
Manca, V., Salibra, A. and Scollo, G. (1990) Equational type logic. Theoretical Computer Science 77 131–159.CrossRefGoogle Scholar
Manca, V., Salibra, A. and Scollo, G. (1991) On the expressiveness of equational type logic. In: Rattray, C. and Clark, R. (eds.) The Unified Computation Laboratory, Oxford University Press 85–100.Google Scholar
Padawitz, P. (1988) Computing in Horn Clause Theories, Springer-Verlag, Heidelberg.CrossRefGoogle Scholar
Reichel, H. (1987) Initial Computability, Algebraic Specifications and Partial Algebras, Oxford Science Publications.CrossRefGoogle Scholar
Salibra, A. and Scollo, G. (1992) A soft stairway to institutions. In: Bidoit, M. and Choppy, C. (eds.) Proc. 8th ADT workshop. Springer-Verlag Lecture Notes in Computer Science 655 310–329.CrossRefGoogle Scholar
Sannella, D. and Tarlecki, A. (1988) Specifications in an arbitrary institution. Information and Computation 76 165–210.CrossRefGoogle Scholar
Tarlecki, A. (1985) On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37 269–304.CrossRefGoogle Scholar
Wolter, U. (1994) Institutional Frames. Technical report, Technical University of Berlin.Google Scholar