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

• Castaño Perea, Jaime Andrés ^[1] ; Ortiz Rico, Guillermo ^[1]
  1. [1] Universidad del Valle
• Localización: Integración: Temas de matemáticas, ISSN 0120-419X, Vol. 32, Nº. 2, 2014 (Ejemplar dedicado a: Revista Integración), págs. 199-210
• Idioma: español
• Títulos paralelos:
  • A coinstitution for abstract behavioral logic
• Enlaces
  • Texto completo (pdf)
• Resumen
  • español

    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.

  • English

    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. 

• Referencias bibliográficas
  • Citas [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,...
  • 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,...
  • [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,...
  • [6] Goguen J. and Burstall R., “A study in the foundations of programming methodology: specifications, institutions, charters and parchments”,...
  • [7] Goguen J. and Burstall R., “Institutions: abstract model theory for specification and programming”,J. Assoc. Comput. Mach. 39 (1992),...
  • [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...
  • [9] Pattinson D., “Translating Logics for Coalgebras”, in Lecture Notes in Computer Science, Recent Trends in Algebraic Development Techniques,...
  • [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....
  • [12] MacLane S., Categories for the working mathematician, Graduate Texts in Mathematics, Vol. 5. Springer-Verlag, New York-Berlin, 1971.