Una coinstitución para la lógica de
comportamiento abstracto

JAIME ANDRÉS CASTAÑO PEREA^*, GUILLERMO ORTIZ RICO,

Universidad del Valle, Departamento de Matemáticas, Cali, Colombia.

Resumen. Recientemente, la especificación de un problema en ciencias de la computación -un paso intermedio entre el problema dado y su aplicación como un sistema de software que garantiza su solución- utiliza el álgebra universal y la teoría de coálgebras para su descripción. Esta etapa incluye componentes sintácticas y semánticas, que tienen como resultado un sistema lógico. En [3], se propone la lógica ecuacional multitipada para la especificación de problemas. Dualmente, en [9] se estudia una lógica de comportamiento abstracto, la cual modela procesos y comportamiento de sistemas coalgebraicos. En ambas lógicas los componentes sintáctico y semántico son conectados por medio de una relación de satisfacción, caracterizada por el siguiente principio: la verdad se preserva bajo transformaciones del lenguaje. En un marco general y moderno, hoy contamos con las instituciones en la especificación algebraica y coinstituciones en la especificación coalgebraica. El propósito del presente artículo es estudiar un caso particular de la lógica de comportamiento abstracto presentada en [9], en donde las coálgebras las restringimos a funtores polinomiales. Identificamos la respectiva coinstitución coalgebraica, detallando sus componentes y explícitamente presentaremos la relación de satisfacción como un resultado final.

Palabras Claves: Especificación, categoría, álgebra, coálgebra, relación de satisfacción, institución, coinstitución.
MSC2010: 18A05, 18C10, 03B70, 68Q65.

A coinstitution for abstract behavioral logic

Abstract. Recently, the specification of a problem in computer sciences -an intermediate step between the given problem and its implementation as a software system that guarantees its solution- uses universal algebra and coalgebra theories for its description. This stage includes a syntactic and a semantic component, having a logic system as result. In [3], the case of many-sorted equational logic is studied for the purpose of specification problems. Dually, in [9] an abstract behavioral logic, which models processes and coalgebraic systems behavior is studied. In both logics, the syntactic and semantic components are connected via a satisfaction relation, characterized by the following principle: the truth of formulas is invariant under language translations. In a general and modern framework, we use the institutions in algebraic specification and coinstitutions in coalgebraic specification. We research a particular case of behavioral abstract logic presented in [9], in which coalgebras are restricted to polinomial functors. We identify the respective algebraic coinstitution, detail all its components, and explicitly present the satisfaction relation as the final result.

Keywords: Specification, categories, algebra, coalgebra, satisfaction relation, institution, coinstitution.

Texto Completo disponible en PDF

Referencias

[1] Awodey S., Category Theory, Oxford Logic Guides, 49. The Clarendon Press, Oxford University Press, New York, 2006.

[2] Burris S. and Sankappanavar H., A Course In Universal Algebra, Graduate Texts in Mathematics, 78. Springer-Verlag, New York-Berlin, 1981.

[3] Burstall R. and Goguen J., "The Semantics of Clear, A Specification Languaje", in Proc. Copenagen Winter School on Abstract Software Specifications, (ed. Dines Bjorner), Springer, Vol. 86 (1979), 292-332.

[4] Castaño Perea J.A., "Especificación coalgebraica ecuacional y coecuacional", Tesis (M.Sc.), Universidad del Valle, Cali, Colombia, 2011, 36 p.

[5] Domínguez C., "Especificación orientada a objetos de sistemas de cálculo simbólico", Tesis (Ph.D), Universidad de la Rioja, España, Logroño, 2003, 70 p.

[6] Goguen J. and Burstall R., "A study in the foundations of programming methodology: specifications, institutions, charters and parchments", Category theory and computer programming (Guildford, 1985), 313-333, Lecture Notes in Comput. Sci., 240, Springer, Berlin, 1986.

[7] Goguen J. and Burstall R., "Institutions: abstract model theory for specification and programming", J. Assoc. Comput. Mach. 39 (1992), no. 1, 95-146.

[8] Kurz A., "A co-variety-theorem for modal logic. Advances in modal logic", Vol. 2 (Uppsala, 1998), 367-380, CSLI Lecture Notes, 119, CSLI Publ., Stanford, CA, 2001

[9] Pattinson D., "Translating Logics for Coalgebras", in Lecture Notes in Computer Science, Recent Trends in Algebraic Development Techniques, Springer, Vol. 2755 (2003), 393-408.

[10] Pierce B., Basic Category Theory for Computer Scientist, Londres, Inglaterra, The MIT Press 1991.

[11] Rutten J.J.M.M., "Universal coalgebra: a theory of systems. Modern algebra and its applications", (Nashville, TN, 1996), Theoret. Comput. Sci. 249 (2000), no. 1, 3-80.

[12] MacLane S., Categories for the working mathematician, Graduate Texts in Mathematics, Vol. 5. Springer-Verlag, New York-Berlin, 1971.

^*E-mail: jaime.castano@correounivalle.edu.co
Recibido: 11 de diciembre de 2013, Aceptado: 23 de agosto de 2014.
Para citar este artículo: J.A. Castaño Perea, G. Ortiz Rico, Una coinstitución para la lógica de
comportamiento abstracto, Rev. Integr. Temas Mat. 32 (2014), no. 2, 199-210.