Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-25T04:03:21.456Z Has data issue: false hasContentIssue false
  • English
  • Français

Diagrammatic logic applied to a parameterisation process

Published online by Cambridge University Press:  24 June 2010

CÉSAR DOMÍNGUEZ  and
DOMINIQUE DUVAL
CÉSAR DOMÍNGUEZ
Affiliation:
Departamento de Matemáticas y Computación, Universidad de La Rioja, Edificio Vives, Luis de Ulloa s/n, E-26004 Logroño, La Rioja, Spain Email: [email protected]
DOMINIQUE DUVAL
Affiliation:
Laboratoire Jean Kuntzmann, Université de Grenoble, 51 rue des mathématiques, BP 53, F-38041 Grenoble Cédex 9, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper provides an abstract definition of a class of logics, called diagrammatic logics, together with a definition of morphisms and 2-morphisms between them. The definition of the 2-category of diagrammatic logics relies on category theory, mainly on adjunction, categories of fractions and limit sketches. This framework is applied to the formalisation of a parameterisation process. This process, which consists of adding a formal parameter to some operations in a given specification, is presented as a morphism of logics. Then the parameter passing process for recovering a model of the given specification from a model of the parameterised specification and an actual parameter is shown to be a 2-morphism of logics.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 20 , Issue 4 , August 2010 , pp. 639 - 654
Copyright
Copyright © Cambridge University Press 2010

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

Barr, M. and Wells, C. (1999) Category Theory for Computing Science, 3rd Edition, Centre de Recherches Mathématiques (CRM) Publications.Google Scholar
Coppey, L. and Lair, C. (1984) Leçons de Théorie des Esquisses. Diagrammes 12.Google Scholar
Domínguez, C. and Duval, D. (2009) A parameterization process as a categorical construction. Available at arXiv:0908.3634.Google Scholar
Domínguez, C., Duval, D., Lambán, L. and Rubio, J. (2005) Towards diagrammatic specifications of symbolic computation systems. In: Coquand, T., Lombardi, H. and Roy, M. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar 05021. (Available at http://drops.dagstuhl.de/portals/index.php?semnr=05021.)Google Scholar
Domínguez, C., Lambán, L. and Rubio, J. (2007) Object-oriented institutions to specify symbolic computation systems. Rairo – Theoretical Informatics and Applications 41 191–214.CrossRefGoogle Scholar
Domínguez, C., Rubio, J. and Sergeraert, F. (2006) Modeling inheritance as coercion in the Kenzo system. Journal of Universal Computer Science 12 (12)1701–1730.Google Scholar
Dousson, X., Sergeraert, F. and Siret, Y. (1999) The Kenzo program. Institut Fourier, Grenoble. (Available at http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo.)Google Scholar
Dumas, J. G., Duval, D. and Reynaud, J. C. (2009) Cartesian effect categories are Freyd-categories. (Available at arXiv:0903.3311.)Google Scholar
Duval, D. (2003) Diagrammatic specifications. Mathematical Structures in Computer Science 13 857–890.Google Scholar
Duval, D. (2007) Diagrammatic inference. (Available at arXiv:0710.1208.)Google Scholar
Ehresmann, C. (1968) Esquisses et types de structures algébriques. Bull. Instit. Polit. Iaşi XIV.Google Scholar
Gabriel, P. and Ulmer, F. (1971) Lokal präsentierbare Kategorien. Springer-Verlag Lecture Notes in Computer Science 221.Google Scholar
Gabriel, P. and Zisman, M. (1967) Calculus of Fractions and Homotopy Theory, Springer-Verlag.CrossRefGoogle Scholar
Goguen, J. A. and Burstall, R. M. (1984) Introducing Institutions. Springer-Verlag Lecture Notes in Computer Science 164 221–256.CrossRefGoogle Scholar
Goguen, J. and Malcolm, G. (2000) A hidden agenda. Theoretical Computer Science 245 (1)55–101.Google Scholar
Goguen, J. A. and Roşu, G. (2002) Institution morphisms. Formal Aspects of Computing 13 274–307.CrossRefGoogle Scholar
Hensel, U. and Reichel, H. (1995) Defining equations in terminal coalgebras. In: Recent Trends in Data Type Specifications. Springer-Verlag Lecture Notes in Computer Science 906 307–318.Google Scholar
Kan, D. M. (1958) Adjoint Functors. Transactions of the American Mathematical Society 87 294–329.Google Scholar
Lambán, L., Pascual, V. and Rubio, J. (2003) An object-oriented interpretation of the EAT system. Applicable Algebra in Engineering, Communication and Computing 14 (3)187–215.Google Scholar
Lellahi, S. K. (1989) Categorical abstract data type (CADT). Diagrammes 21 SKL1–SKL23.Google Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd EditionSpringer-Verlag.Google Scholar
Makkai, M. (1997) Generalized sketches as a framework for completeness theorems (I). Journal of Pure and Applied Algebra 115 49–79.Google Scholar
Pitts, A. M. (2000) Categorical Logic. In: Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds.) Algebraic and Logical Structures. Handbook of Logic in Computer Science 5 Chapter 2, Oxford University Press.Google Scholar
Rubio, J., Sergeraert, F. and Siret, Y. (2007) EAT: Symbolic Software for Effective Homology Computation. Institut Fourier, Grenoble. (Available at http://www-fourier.ujf-grenoble.fr/~sergerar/Kenzo/#Eat.)Google Scholar
Rutten, J. J. M. M. (2000) Universal coalgebra: a theory of systems. Theoretical Computer Science 249 (1)3–80.CrossRefGoogle Scholar
Tarlecki, A. (2000) Towards heterogeneous specifications. In: Gabbay, D. M. and de Rijke, M. (eds.) Frontiers of Combining Systems (FroCos'98), Studies in Logic and Computation 7Research Studies Press/Wiley 337–360.Google Scholar
Wells, C. (1993) Sketches: Outline with References. (Available at http://www.cwru.edu/artsci/math/wells/pub/papers.html.)Google Scholar