Institución (informática)

El concepto de institución fue creado por Joseph Goguen y Rod Burstall a finales de los años 1970 para hacer frente a la "explosión demográfica de los sistemas lógicos utilizados en informática ". El concepto intenta "formalizar el concepto informal" de sistema lógico. ^[1]

El uso de instituciones permite desarrollar conceptos de lenguajes de especificación (como estructuración de especificaciones, parametrización, implementación, refinamiento y desarrollo), cálculos de demostración e incluso herramientas de una manera completamente independiente del sistema lógico subyacente. También existen morfismos que permiten relacionar y traducir sistemas lógicos. Aplicaciones importantes de esto son la reutilización de la estructura lógica (también llamada préstamo) y la especificación heterogénea y la combinación de lógicas.

La difusión de la teoría de modelos institucionales ha generalizado diversas nociones y resultados de la teoría de modelos , y las propias instituciones han influido en el progreso de la lógica universal . ^{[2] [3]}

La teoría de las instituciones no presupone nada sobre la naturaleza del sistema lógico. Es decir, los modelos y las oraciones pueden ser objetos arbitrarios; el único supuesto es que existe una relación de satisfacción entre los modelos y las oraciones, que indica si una oración se cumple en un modelo o no. La satisfacción se inspira en la definición de verdad de Tarski , pero de hecho puede ser cualquier relación binaria. Una característica crucial de las instituciones es que siempre se considera que los modelos, las oraciones y su satisfacción viven en algún vocabulario o contexto (llamado firma ) que define los símbolos (no lógicos) que se pueden usar en las oraciones y que deben interpretarse en los modelos. Además, los morfismos de firma permiten extender firmas, cambiar la notación, etc. No se presupone nada sobre las firmas y los morfismos de firma excepto que los morfismos de firma pueden ser compuestos; esto equivale a tener una categoría de firmas y morfismos. Finalmente, se supone que los morfismos de firma conducen a traducciones de oraciones y modelos de una manera que se preserva la satisfacción. Mientras que las oraciones se traducen junto con los morfismos de la firma (pensemos en los símbolos que se reemplazan a lo largo del morfismo), los modelos se traducen (o mejor: se reducen) en función de los morfismos de la firma. Por ejemplo, en el caso de una extensión de la firma, un modelo de la firma de destino (más grande) se puede reducir a un modelo de la firma de origen (más pequeña) simplemente olvidando algunos componentes del modelo.

Sea lo opuesto a la categoría de categorías pequeñas . Una institución consta formalmente de ${\displaystyle \mathbf {Gato} ^{\mathrm {op} }}$

• una categoría de firmas ,${\displaystyle \mathbf {Signo} }$
• un funtor que da, para cada firma , el conjunto de oraciones , y para cada morfismo de firma , el mapa de traducción de oraciones , donde a menudo se escribe como ,${\displaystyle {\mathit {Sen}}\colon \mathbf {Signo} \to }$ ${\displaystyle \mathbf {Conjunto}}$${\estilo de visualización \Sigma}$ ${\displaystyle {\mathit {Sen}}(\Sigma)}$${\displaystyle \sigma \colon \Sigma \to \Sigma '}$ ${\displaystyle {\mathit {Sen}}(\sigma )\colon {\mathit {Sen}}(\Sigma )\to {\mathit {Sen}}(\Sigma ')}$${\displaystyle {\mathit {Sen}}(\sigma)(\varphi)}$${\displaystyle \sigma (\varphi )}$
• un funtor que da, para cada firma , la categoría de modelos , y para cada morfismo de firma , el funtor reduct , donde a menudo se escribe como ,${\displaystyle \mathbf {Mod} \colon \mathbf {Sign} \to \mathbf {Cat} ^{\mathrm {op} }}$${\displaystyle \Sigma }$ ${\displaystyle \mathbf {Mod} (\Sigma )}$${\displaystyle \sigma \colon \Sigma \to \Sigma '}$ ${\displaystyle \mathbf {Mod} (\sigma )\colon \mathbf {Mod} (\Sigma ')\to \mathbf {Mod} (\Sigma )}$${\displaystyle \mathbf {Mod} (\sigma )(M')}$${\displaystyle M'|_{\sigma }}$
• una relación de satisfacción para cada uno ,${\displaystyle {\models _{\Sigma }}\subseteq |{\mathbf {Mod} (\Sigma )|\times {\mathit {Sen}}(\Sigma )}}$${\displaystyle \Sigma \in \mathbf {Sign} }$

de modo que para cada uno en , se cumple la siguiente condición de satisfacción : ${\displaystyle \sigma \colon \Sigma \to \Sigma '}$${\displaystyle \mathbf {Sign} }$

$${\displaystyle M'\models _{\Sigma '}\sigma (\varphi )\quad {\text{if and only if}}\quad M'|_{\sigma }\models _{\Sigma }\varphi }$$

para cada uno y . ${\displaystyle M'\in \mathbf {Mod} (\Sigma ')}$${\displaystyle \varphi \in {\mathit {Sen}}(\Sigma )}$

La condición de satisfacción expresa que la verdad es invariante bajo el cambio de notación (y también bajo la ampliación o cociente del contexto).

Estrictamente hablando, el functor modelo termina en la "categoría" de todas las categorías grandes.

• Lógica común
• Lenguaje común de especificación algebraica (CASL)
• Lógica de primer orden
• Lógica de orden superior
• Lógica intuicionista
• Lógica modal
• Lógica proposicional
• Lógica temporal
• Lenguaje de ontología web (OWL)

• Teoría de modelos abstractos
• Teoría del modelo institucional
• Lógica universal

• JA Goguen; RM Burstall (1984), "Introducción a las instituciones", en E. Clarke; D. Kozen (eds.), Lógica de programas: Actas del Taller de lógica de programación de 1983 , Lecture Notes in Computer Science, vol. 164, Springer, Berlín, Alemania, págs. 221–256, doi :10.1007/3-540-12896-4_366, ISBN 978-3-540-12896-0Esta fue la primera publicación sobre la teoría de las instituciones y la versión preliminar de Goguen y Burstall (1992).
• J. Meseguer (1989), "Lógica general", en H.-D. Ebbinghaus; J. Fernández-Prida; M. Garrido; D. Lascar; M. Rodríguez Artalejo (eds.), Coloquio de lógica '87: Actas del coloquio celebrado en Granada, España , vol. 129, Elservier, pp. 274–307
• JA Goguen; G. Rosu (2002), "Morfismos institucionales", Aspectos formales de la informática , 13 (3–5): 274–307, doi : 10.1007/s001650200013 , S2CID  5687318
• D. Sannella; A. Tarlecki (1988), "Especificaciones en una institución arbitraria", Información y Computación , 76 (2–3): 165–210, doi : 10.1016/0890-5401(88)90008-9
• R. Diaconescu (2008), Teoría de modelos independientes de las instituciones, Birkhäuser, Basilea

• Răzvan Diaconescu, "Teoría de la institución", Internet Encyclopedia of Philosophy , consultado el 31 de enero de 2021
• Joseph Goguen (2006), Instituciones, Universidad de California, San Diego , consultado el 31 de enero de 2021
• Formalismo, lógica, institución: relación, traducción y estructuración. Incluye amplia bibliografía.
• Răzvan Diaconescu, Publicaciones seleccionadas, Instituto de Matemáticas Simion Stoilow de la Academia Rumana , consultado el 31 de enero de 2021. Contiene trabajos recientes sobre la teoría de modelos institucionales.