Una coinstitución para la lógica de comportamiento abstracto
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 componente...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | Spanish |
| Published: |
Universidad Industrial de Santander
2014-12-01
|
| Series: | Revista Integración |
| Subjects: | |
| Online Access: | http://revistas.uis.edu.co/index.php/revistaintegracion/article/view/4383/4669 |
| Summary: | 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.
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. |
|---|---|
| ISSN: | 0120-419X 2145-8472 |