Abstract
We examine a variety of liberal logical frameworks of partial algebras. Therefore we use simple, conjunctive and weak embeddings of institutions which preserve model categories and may map sentences to sentences, finite sets of sentences, or theory extensions using unique-existential quantifiers, respectively. They faithfully represent theories, model categories, theory morphisms, colimit of theories, reducts etc. Moreover, along simple and conjunctive embeddings, theorem provers can be re-used in a way that soundness and completeness is preserved. Our main result states the equivalence of all the logical frameworks with respect to weak embeddability. This gives us compilers between all frameworks. Thus it is a chance to unify the different branches of specification using liberal partial logics.
This is important for reaching the goal of formal interoperability of different specification languages for software development. With formal interoperability, a specification can contain parts written in different logical frameworks using a multiparadigm specification language, and one can re-use tools which are available for one framework also for other frameworks.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Adámek, J. Rosický. Locally Presentable and Accessible Categories. Cambridge University Press, 1994.
E. Astesiano, M. Cerioli. Multiparadigm specification languages: a first attempt at foundations. In J.F. Groote C.M.D.J. Andrews, ed., Semantics of Specification Languages (SoSl 93), Workshops in Computing, 168–185. Springer Verlag, 1994.
M. Barr, C. Wells. Toposes, Triples and Theories, Grundlehren der mathematischen Wissenschaften 278. Springer Verlag, 1985.
P. Burmeister. Partial algebras — survey of a unifying approach towards a two-valued model theory for partial algebras. Algebra Universalis 15, 306–358, 1982.
P. Burmeister. A model theoretic approach to partial algebras. Akademie Verlag, Berlin, 1986.
R. M. Burstall, J. A. Goguen. Putting theories together to make specifications. In Proceedings of the 5th International Joint Conference on Artificial Intelligence, 1045–1058. Cambridge, 1977.
M. Cerioli. Relationships between Logical Formalisms. PhD thesis, TD-4/93, Università di Pisa-Genova-Udine, 1993.
M. Cerioli, J. Meseguer. May I borrow your logic? In A.M. Borzyszkowski, S. Sokolowski, eds., Proc. MFCS'93 (Mathematical Foundations of Computer Science), LNCS 711, 342–351. Springer Verlag, Berlin, 1993. To appear in Theoretical Computer Science.
M. Coste. Localisation, spectra and sheaf representation. In M.P. Fourman, C.J. Mulvey, D.S. Scott, eds., Application of Sheaves, Lecture Notes in Mathematics 753, 212–238. Springer Verlag, 1979.
H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification 1. Springer Verlag, Heidelberg, 1985.
H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification 2. Springer Verlag, Heidelberg, 1990.
H. Ehrig, P. Pepper, F. Orejas. On recent trends in algebraic specification. In Proc. ICALP'89, LNCS 372, 263–288. Springer Verlag, 1989.
W. A. Farmer. A partial functions version of Church's simple type theory. Journal of Symbolic Logic 55, 1269–1291, 1991.
P. Freyd. Aspects of topoi. Bull. Austral. Math. Soc. 7, 1–76, 1972.
P. Gabriel, F. Ulmer. Lokal präsentierbare Kategorien, Lecture Notes in Mathematics 221. Springer Verlag, Heidelberg, 1971.
J. A. Goguen, R. M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39, 95–146, 1992. Predecessor in: LNCS 164(1984):221–256.
J. A. Goguen, J. Meseguer. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105, 217–273, 1992.
Joseph Goguen, Jean-Pierre Jouannaud, José Meseguer. Operational semantics of order-sorted algebra. In Wilfried Brauer, ed., Proceedings, 1985 International Conference on Automata, Languages and Programming. Springer, 1985. Lecture Notes in Computer Science, Volume 194.
J. W. Gray. Categorical aspects of data type constructors. Theoretical Computer Science 50, 103–135, 1987.
H.-J. Hoehnke. On partial algebras. In Universal Algebra (Proc. Coll. Esztergom 1977), Colloq. Math. Soc. J. Bolyai 29, 373–412. North Holland, Amsterdam, 1981.
G. Jarzembski. Weak varieties of partial algebras. Algebra Universalis 25, 247–262, 1988.
G. Jarzembski. Programs in partial algebras. Theoretical Computer Science 115, 131–149, 1993.
S.C. Kleene. Introduction to Metamathematics. North Holland, 1952.
H.-J. Kreowski, T. Mossakowski. Equivalence and difference of institutions: Simulating horn clause logic with based algebras. Mathematical Structures in Computer Science 5, 189–215, 1995.
J. Meseguer. General logics. In Logic Colloquium 87, 275–329. North Holland, 1989.
J. Meseguer, J. Goguen. Order-sorted algebra solves the constructor, selector, multiple representation and coercion problems. Information and Computation 103(1), 114–158, March 1993.
T. Mossakowski. Simulations between various institutions of partial and total algebras. Talk at the Workshop of the ESPRIT Basic Research Working Group COMPASS, Dresden, September 1993.
T. Mossakowski. Parameterized recursion theory — a tool for the systematic classification of specification methods. In M. Nivat, C. Rattray, T. Rus, G. Scollo, eds., Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, 1993, Workshops in Computing, 139–146. Springer-Verlag, London, 1993. Also to appear in Theoretical Computer Science.
T. Mossakowski. A hierarchy of institutions separated by properties of parameterized abstract data types. In Recent Trends in Data Type Specification. Proceedings, Lecture Notes in Computer Science 906, 389–405. Springer Verlag, London, 1995.
T. Mossakowski. Different types of arrow between logical frameworks. In ICALP 96, LNCS. To appear. Springer Verlag, 1996.
J. Slominski. Peano-algebras and quasi-algebras, Dissertationes Mathematicae (Rozprawy Mat.) 62. 1968.
A. Poigné. Algebra categorically. In D. Pitt et al., ed., Category Theory and Computer Programming, Lecture Notes in Computer Science 240, 76–102. Springer Verlag, 1986.
H. Reichel. Initial Computability, Algebraic Specifications and Partial Algebras, Oxford Science Publications, 1987.
D. Sannella, A. Tarlecki. Specifications in an arbitrary institution. Information and Computation 76, 165–210, 1988.
J.R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, Massachusetts, 1967.
A. Tarlecki. Working with multiple logical systems. Unpublished manuscript.
A. Tarlecki. On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37, 269–304, 1985.
M. Wirsing. Structured algebraic specifications: A kernel language. Theoretical Computer Science 42, 123–249, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mossakowski, T. (1996). Equivalences among various logical frameworks of partial algebras. In: Kleine Büning, H. (eds) Computer Science Logic. CSL 1995. Lecture Notes in Computer Science, vol 1092. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61377-3_51
Download citation
DOI: https://doi.org/10.1007/3-540-61377-3_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61377-0
Online ISBN: 978-3-540-68507-4
eBook Packages: Springer Book Archive