Lógica agrupada

---

La lógica agrupada ^[1] es una variedad de lógica subestructural propuesta por Peter O'Hearn y David Pym . La lógica agrupada proporciona primitivas para razonar sobre la composición de recursos , que ayudan en el análisis de composición de la computadora y otros sistemas. Tiene una semántica de teoría de categorías y función de verdad, que puede entenderse en términos de un concepto abstracto de recurso, y una teoría de prueba en la que los contextos Γ en un juicio de implicación Γ ⊢ A son estructuras en forma de árbol (racimos) en lugar de listas o conjuntos ( múltiples ) como en la mayoría de los cálculos de prueba. La lógica agrupada tiene una teoría de tipos asociada , y su primera aplicación fue proporcionar una forma de controlar el aliasing y otras formas de interferencia en programas imperativos . ^[2] La lógica ha tenido más aplicaciones en la verificación de programas , donde es la base del lenguaje de afirmación de la lógica de separación , ^[3] y en el modelado de sistemas , donde proporciona una forma de descomponer los recursos utilizados por los componentes de un sistema. ^{[4] [5] [6]}

${\ estilo de visualización A * B}$y son formas de conjunción e implicación que toman en cuenta los recursos (explicadas a continuación). Además de estos conectores, la lógica agrupada tiene una fórmula, a veces escrita como I o emp, que es la unidad de *. En la versión original de la lógica agrupada y eran los conectivos de la lógica intuicionista , mientras que una variante booleana toma y (y ) como de la lógica booleana tradicional . Por lo tanto, la lógica agrupada es compatible con los principios constructivos, pero de ninguna manera depende de ellos.${\displaystyle B{-\!\!*}C}$${\ Displaystyle \ wedge}$${\ estilo de visualización \ flecha derecha}$${\ Displaystyle \ wedge}$${\ estilo de visualización \ flecha derecha}$${\ Displaystyle \ neg}$

La forma más fácil de entender estas fórmulas es en términos de su semántica funcional de verdad. En esta semántica una fórmula es verdadera o falsa con respecto a recursos dados. afirma que el recurso disponible se puede descomponer en recursos que satisfacen y . dice que si componemos el recurso en cuestión con un recurso adicional que satisface , entonces el recurso combinado satisface . y tienen sus significados familiares.${\ estilo de visualización A * B}$${\ estilo de visualización A}$${\ Displaystyle B}$${\displaystyle B{-\!\!*}C}$${\ Displaystyle B}$${\ Displaystyle C}$${\ Displaystyle \ wedge}$${\ estilo de visualización \ flecha derecha}$

La base para esta lectura de fórmulas fue proporcionada por una semántica de forzamiento avanzada por Pym, donde la relación de forzamiento significa ' Retención del recurso r ' . La semántica es análoga a la semántica de la lógica intuicionista o modal de Kripke , pero donde los elementos del modelo se consideran recursos que se pueden componer y descomponer, en lugar de mundos posibles que son accesibles entre sí. Por ejemplo, la semántica forzada para la conjunción es de la forma${\ estilo de visualización r \ modelos A}$

---