Abstract
Birkhoff (quasi-)variety categorical axiomatizability results have fascinated many scientists by their elegance, simplicity and generality. The key factor leading to their generality is that equations, conditional or not, can be regarded as special morphisms or arrows in a special category, where their satisfaction becomes injectivity, a simple and abstract categorical concept. A natural and challenging next step is to investigate complete deduction within the same general and elegant framework. We present a categorical deduction system for equations as arrows and show that, under appropriate finiteness requirements, it is complete for satisfaction as injectivity. A straightforward instantiation of our results yields complete deduction for several equational logics, in which conditional equations can be derived as well at no additional cost, as opposed to the typical method using the theorems of constants and of deduction. At our knowledge, this is a new result in equational logics.
Keywords
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Adámek, J., Rosický, J.: Locally Presentable and Accessible Categories. Cambridge University Press, Cambridge (1994), London Math. Society. Lecture Note Series 189
Andréka, H., Németi, I.: A general axiomatizability theorem formulated in terms of cone-injective subcategories. In: Csakany, B., Fried, E., Schmidt, E. (eds.) Universal Algebra. Colloquia Mathematics Societas János Bolyai, vol. 29, pp. 13–35. North-Holland, Amsterdam (1981)
Andréka, H., Németi, I.: Generalization of the concept of variety and quasivariety to partial algebras through category theory. In: ISSAC 1985 and EUROCAL 1985, vol. 204, Polish Scientific Publishers, Warsaw (1983)
Banaschewski, B., Herrlich, H.: Subcategories defined by implications. Houston Journal Mathematics 2, 149–171 (1976)
Bergstra, J., Tucker, J.: Characterization of computable data types by means of a finite equational specification method. In: de Bakker, J., van Leeuwen, J. (eds.) Data Base Techniques for Pictorial Application. LNCS, vol. 81, pp. 76–90. Springer, Heidelberg (1980)
Bergstra, J., Tucker, J.V.: Equational specifications, complete term rewriting systems, and computable and semicomputable algebras. Journal of the Associationfor Computing Machinery 42(6), 1194–1230 (1995)
Birkhoff, G.: On the structure of abstract algebras. In: Proceedings of the Cambridge Philosophical Society, vol. 31, pp. 433–454 (1935)
Birkhoff, G., Lipson, J.: Heterogenous algebras. Journal of Combinatorial Theory 8, 115–133 (1970)
Borovanský, P., Cîrstea, H., Dubois, H., Kirchner, C., Kirchner, H., Moreau, P.-E., Ringeissen, C., Vittek, M.: Elan. User manual, http://www.loria.fr/equipes/protheo/SOFTWARES/ELAN
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)
Broy, M., Wirsing, M., Pepper, P.: On the algebraic definition of programming languages. ACM Trans. on Prog. Lang. and Systems 9(1), 54–99 (1987)
Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings, First International Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier Science, Amsterdam (1996)
Căzănescu, V.: Local equational logic. In: Ésik, Z. (ed.) FCT 1993. LNCS, vol. 710, pp. 162–170. Springer, Heidelberg (1993)
Diaconescu, R.: Category-based Semantics for Equational and Constraint Logic Programming. PhD thesis, University of Oxford (1994)
Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)
Freyd, P., Kelly, G.: Categories of continuous functors. Journal of Pure and Applied Algebra 2, 169–191 (1972)
Goguen, J., Malcolm, G.: Alg. Semantics of Imperative Programs. MIT Press, Cambridge (1996)
Goguen, J., Malcolm, G.: A hidden agenda. Theoretical Computer Science 245(1), 55–101 (2000)
Goguen, J., Meseguer, J.: Completeness of many-sorted equational logic. Houston Journal of Mathematics 11(3), 307–334 (1985), Preliminary versions have appeared in: SIGPLAN Notices, July 1981, Vol. 16(7), pp. 24–37; SRI Report CSL-135, May 1982; and Report CSLI-84-15, Stanford (September 1985)
Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105(2), 217–273 (1992)
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: algebraic specification in action, pp. 3–167. Kluwer, Dordrecht (2000)
Grothendieck, A.: Sur quelques points d’algébre homologique. Tôhoku Mathematical Journal 2, 119–221 (1957)
Herrlich, H., Strecker, G.: Category Theory. Allyn and Bacon (1973)
Isbell, J.R.: Subobjects, adequacy, completeness and categories of algebras. Rozprawy Matematyczne 36, 1–33 (1964)
Lambek, J.: Completions of Categories. Lecture Notes in Mathematics, vol. 24. Springer, Heidelberg (1966)
Lane, S.M.: Categories for the Working Mathematician. Springer, Heidelberg (1971)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, Springer, Heidelberg (1998)
Mitchell, B.: Theory of categories. Academic Press, New York (1965)
Németi, I.: On notions of factorization systems and their applications to coneinjective subcategories. Periodica Mathematica Hungarica 13(3), 229–335 (1982)
Németi, I., Sain, I.: Cone-implicational subcategories and some Birkhoff-type theorems. In: Csakany, B., Fried, E., Schmidt, E. (eds.) Universal Algebra. Colloquia Mathematics Societas János Bolyai, pp. 535–578. North-Holland, Amsterdam (1981)
Padawitz, P., Wirsing, M.: Completeness of many-sorted equational logic revisited. Bulletin of the European Association for Theoretical Computer Science 24, 88–94 (1984)
Reichel, H.: Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press, Oxford (1987)
Roşu, G.: A Birkhoff-like axiomatizability result for hidden algebra and coalgebra. In: Jacobs, B., Moss, L., Reichel, H., Rutten, J. (eds.) Proceedings of the First Workshop on Coalgebraic Methods in Computer Science (CMCS 1998). Electronic Notes in Theoretical Computer Science, vol. 11, pp. 179–196. Elsevier Science, Amsterdam (1998)
Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000), http://ase.arc.nasa.gov/grosu/phd-thesis.ps
Roşu, G.: Complete categorical equational deduction. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 528–538. Springer, Heidelberg (2001)
Roşu, G.: Equational axiomatizability for coalgebra. Theoretical Computer Science 260(1-2), 229–247 (2001)
Roşu, G.: Axiomatizability in inclusive equational logics. Mathematical Structures in Computer Science, http://ase.arc.nasa.gov/grosu/iel.ps (to appear)
Roşu, G., Goguen, J.: On equational Craig interpolation. Journal of Universal Computer Science 6(1), 194–200 (2000)
Rodenburg, P.H.: A simple algebraic proof of the equational interpolation theorem. Algebra Universalis 28, 48–51 (1991)
Smolka, G., Nutt, W., Goguen, J., Meseguer, J.: Order-sorted equational computation. In: Nivat, M., Aït-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures Rewriting Techniques, vol. 2, pp. 299–367. Academic, New York (1989)
Wand, M.: First-order identities as a defining language. Acta Informatica 14, 337–357 (1980)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Roşu, G. (2006). Complete Categorical Deduction for Satisfaction as Injectivity. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_9
Download citation
DOI: https://doi.org/10.1007/11780274_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35462-8
Online ISBN: 978-3-540-35464-2
eBook Packages: Computer ScienceComputer Science (R0)