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 compositivo de computadoras y otros sistemas. Tiene semántica de teoría de categorías y de función de la verdad, que se puede entender 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 de tipo árbol (agrupaciones) en lugar de listas o ( multi ) conjuntos 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 visto más aplicaciones en la verificación de programas , donde es la base del lenguaje de aserció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]}

El teorema de deducción de la lógica clásica relaciona conjunción e implicación:

${\displaystyle A\cuña B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Flecha derecha C}$

La lógica agrupada tiene dos versiones del teorema de deducción:

${\displaystyle A*B\vdash C\quad {\mbox{iff}}\quad A\vdash B{-\!\!*}C\qquad {\mbox{y también}}\qquad A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow C}$

$Estilo de visualización A*B$y son formas de conjunción e implicación que tienen en cuenta los recursos (explicado más adelante). Además de estos conectivos, la lógica agrupada tiene una fórmula, a veces escrita 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 no depende de ellos en modo alguno. ${\displaystyle B{-\!\!*}C}$${\displaystyle \cuña}$${\displaystyle \Flecha derecha}$${\displaystyle \cuña}$${\displaystyle \Flecha derecha}$${\estilo de visualización \neg}$

La forma más sencilla de entender estas fórmulas es en términos de su semántica veritativo-funcional. En esta semántica, una fórmula es verdadera o falsa con respecto a los recursos dados. afirma que el recurso disponible puede descomponerse en recursos que satisfacen y . dice que si componemos el recurso disponible 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}$${\estilo de visualización B}$${\displaystyle B{-\!\!*}C}$${\estilo de visualización B}$${\estilo de visualización C}$${\displaystyle \cuña}$${\displaystyle \Flecha derecha}$

La base para esta lectura de fórmulas fue proporcionada por una semántica de forzamiento propuesta por Pym, donde la relación de forzamiento significa ' A contiene el recurso r ' . La semántica es análoga a la semántica de Kripke de la lógica intuicionista o modal , pero donde los elementos del modelo son considerados como recursos que pueden ser compuestos y descompuestos, en lugar de mundos posibles que son accesibles entre sí. Por ejemplo, la semántica de forzamiento para la conjunción es de la forma ${\displaystyle r\modelos A}$

${\displaystyle r\modelos A*B\quad {\mbox{sí y sólo si}}\quad \existe r_{A}r_{B}.\,r_{A}\modelos A,\,r_{B}\modelos B,\,{\mbox{y}}\,r_{A}\bullet r_{B}\leq r}$

donde es una forma de combinar recursos y es una relación de aproximación. ${\displaystyle r_{A}\bullet r_{B}}$${\estilo de visualización \leq}$

Esta semántica de la lógica agrupada se basa en trabajos previos en lógica de relevancia (especialmente la semántica operacional de Routley-Meyer), pero difiere de ella al no requerir y aceptar la semántica de las versiones intuicionistas o clásicas estándar de y . La propiedad está justificada cuando se piensa en la relevancia, pero se niega por consideraciones de recursos; tener dos copias de un recurso no es lo mismo que tener uno, y en algunos modelos (por ejemplo, los modelos de montón ) podría incluso no estar definida. La semántica estándar de (o de negación) es a menudo rechazada por los relevantesistas en su intento de escapar de las "paradojas de la implicación material", que no son un problema desde la perspectiva de modelar recursos y, por lo tanto, no son rechazadas por la lógica agrupada. La semántica también está relacionada con la "semántica de fase" de la lógica lineal , pero nuevamente se diferencia al aceptar la semántica estándar (incluso booleana) de y , que en la lógica lineal se rechaza en un intento de ser constructiva. Estas consideraciones se analizan en detalle en un artículo sobre semántica de recursos de Pym, O'Hearn y Yang. ^[7]${\displaystyle r\bullet r\leq r}$${\displaystyle \cuña}$${\displaystyle \Flecha derecha}$${\displaystyle r\bullet r\leq r}$${\displaystyle r\bullet r}$${\displaystyle \Flecha derecha}$${\displaystyle \cuña}$${\displaystyle \Flecha derecha}$

La versión doble del teorema de deducción de la lógica agrupada tiene una estructura de teoría de categorías correspondiente. Las demostraciones en lógica intuicionista pueden interpretarse en categorías cerradas cartesianas , es decir, categorías con productos finitos que satisfacen la correspondencia de adjunción ( natural en A y C ) que relaciona conjuntos hom:

${\displaystyle Hom(A\wedge B,C)\quad {\mbox{es isomorfo a}}\quad Hom(A,B\Rightarrow C)}$

La lógica agrupada se puede interpretar en categorías que poseen dos estructuras de este tipo.

Un modelo categórico de lógica agrupada es una categoría única que posee dos estructuras cerradas, una monoidal simétrica cerrada y la otra cartesiana cerrada.

Se puede dar una gran cantidad de modelos categóricos utilizando la construcción del producto tensorial de Day . ^[8] Además, al fragmento implicacional de la lógica agrupada se le ha dado una semántica de juego . ^[9]

La semántica algebraica de la lógica agrupada es un caso especial de su semántica categórica, pero es simple de enunciar y puede ser más accesible.

Un modelo algebraico de lógica agrupada es un conjunto parcial que es un álgebra de Heyting y que lleva una estructura reticular residual conmutativa adicional (para la misma red que el álgebra de Heyting): es decir, un monoide conmutativo ordenado con una implicación asociada que satisface .${\displaystyle A*B\leq C\quad {\mbox{iff}}\quad A\leq B{-\!\!*}C}$

La versión booleana de la lógica agrupada tiene modelos como los siguientes.

Un modelo algebraico de lógica agrupada booleana es un conjunto parcial que es un álgebra booleana y que lleva una estructura monoide conmutativa residual adicional.

El cálculo de demostración de la lógica agrupada difiere de los cálculos secuenciales habituales en que tiene un contexto de hipótesis en forma de árbol en lugar de una estructura plana en forma de lista. En sus teorías de demostración basadas en secuencias, el contexto en un juicio de implicación es un árbol finito con raíz cuyas hojas son proposiciones y cuyos nodos internos están etiquetados con modos de composición correspondientes a las dos conjunciones. Los dos operadores de combinación, coma y punto y coma, se utilizan (por ejemplo) en las reglas de introducción para las dos implicaciones. ${\estilo de visualización \Delta}$${\displaystyle \Delta \vdash A}$

${\displaystyle {\frac {\Gamma ,A\vdash B}{\Gamma \vdash A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;A\vdash B}{\Gamma \vdash A{\Rightarrow }B}}}$

La diferencia entre las dos reglas de composición proviene de reglas adicionales que se les aplican.

• La composición multiplicativa niega las reglas estructurales del debilitamiento y la contracción.${\displaystyle \Delta,\Gamma}$
• La composición aditiva permite el debilitamiento y la contracción de racimos enteros.${\displaystyle \Delta;\Gamma}$

Las reglas estructurales y otras operaciones sobre racimos se aplican a menudo en lo profundo de un contexto de árbol, y no sólo en el nivel superior: se trata, en cierto sentido, de un cálculo de inferencia profunda .

La lógica agrupada corresponde a una teoría de tipos que tiene dos tipos de funciones. Siguiendo la correspondencia de Curry-Howard , las reglas de introducción para las implicaciones corresponden a las reglas de introducción para los tipos de funciones.

${\displaystyle {\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda xM:A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;x:A\vdash M:B}{\Gamma \vdash \alpha xM:A{\Rightarrow }B}}}$

Aquí, hay dos enlazadores distintos, y , uno para cada tipo de función. ${\estilo de visualización \lambda}$${\estilo de visualización \alpha}$

La teoría de la prueba de la lógica agrupada tiene una deuda histórica con el uso de racimos en la lógica de relevancia. ^[10] Pero la estructura agrupada puede en cierto sentido derivarse de la semántica categórica y algebraica: para formular una regla de introducción para debemos imitar a la izquierda en los consecuentes, y para introducir debemos imitar . Esta consideración conduce al uso de dos operadores de combinación. ${\estilo de visualización {-\!\!*}}$${\estilo de visualización *}$${\displaystyle \Flecha derecha}$${\displaystyle \cuña}$

James Brotherston ha realizado un trabajo significativo adicional sobre una teoría de prueba unificada para la lógica agrupada y sus variantes, ^[11] empleando la noción de lógica de visualización de Belnap . ^[12]

Galmiche, Méry y Pym han proporcionado un tratamiento exhaustivo de la lógica agrupada, incluida la completitud y otras metateorías, basadas en tablas etiquetadas . ^[13]

En lo que quizás sea el primer uso de la teoría de tipos subestructurales para controlar recursos, John C. Reynolds mostró cómo usar una teoría de tipos afines para controlar el aliasing y otras formas de interferencia en lenguajes de programación similares a Algol . ^[14] O'Hearn usó la teoría de tipos agrupados para extender el sistema de Reynolds al permitir que la interferencia y la no interferencia se mezclaran de manera más flexible. ^[2] Esto resolvió problemas abiertos relacionados con la recursión y los saltos en el sistema de Reynolds.

La lógica de separación es una extensión de la lógica de Hoare que facilita el razonamiento sobre estructuras de datos mutables que utilizan punteros . Siguiendo la lógica de Hoare, las fórmulas de la lógica de separación tienen la forma , pero las condiciones previas y posteriores son fórmulas interpretadas en un modelo de lógica agrupada. La versión original de la lógica se basaba en los siguientes modelos: ${\displaystyle \{Pre\}programa\{Publicar\}}$

• ${\displaystyle Montones=L\rightharpoonup _{f}V\qquad }$( funciones parciales finitas de posiciones a valores)
• ${\displaystyle h_{0}\bullet h_{1}=}$unión de montones con dominios disjuntos, indefinido cuando los dominios se superponen.

La idea de separación se modela por la falta de definición de la composición en montones superpuestos. Este es un modelo de la variante booleana de la lógica agrupada.

La lógica de separación se utilizó originalmente para demostrar propiedades de programas secuenciales, pero luego se extendió a la concurrencia utilizando una regla de prueba.

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}} {\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

que divide el almacenamiento al que acceden los subprocesos paralelos. ^[15]

Más tarde, se utilizó la mayor generalidad de la semántica de recursos: una versión abstracta de la lógica de separación funciona para los triples de Hoare donde las precondiciones y las poscondiciones son fórmulas interpretadas sobre un monoide conmutativo parcial arbitrario en lugar de un modelo de montón particular. ^[16] Mediante la elección adecuada del monoide conmutativo, se descubrió sorprendentemente que las reglas de prueba de las versiones abstractas de la lógica de separación concurrente se podían usar para razonar sobre procesos concurrentes que interfieren, por ejemplo, codificando el razonamiento basado en confianza-garantía y en trazas. ^{[17] [18]}

La lógica de separación es la base de una serie de herramientas para el razonamiento automático y semiautomático sobre programas, y se utiliza en el analizador de programas Infer actualmente implementado en Facebook. ^[19]

La lógica agrupada se ha utilizado en conexión con el cálculo de recursos-procesos (sincrónico) SCRP ^{[4] [5] [6]} para dar una lógica (modal) que caracteriza, en el sentido de Hennessy - Milner , la estructura compositiva de sistemas concurrentes.

SCRP se destaca por interpretar en términos tanto de composición paralela de sistemas como de composición de sus recursos asociados. La cláusula semántica de la lógica de proceso de SCRP que corresponde a la regla de lógica de separación para concurrencia afirma que una fórmula es verdadera en el estado recurso-proceso , solo en caso de que haya descomposiciones del recurso y el proceso ~ , donde ~ denota bisimulación , de modo que es verdadera en el estado recurso-proceso , y es verdadera en el estado recurso-proceso , ; es decir, si y solo si y . $Estilo de visualización A*B$$Estilo de visualización A*B$${\estilo de visualización R}$${\estilo de visualización E}$${\displaystyle R=S\bullet T}$${\estilo de visualización E}$${\displaystyle F\times G}$${\estilo de visualización A}$${\estilo de visualización S}$${\estilo de visualización F}$${\estilo de visualización B}$${\estilo de visualización T}$${\estilo de visualización G}$${\displaystyle R,E\modelos A}$${\displaystyle S,F\models A}$${\displaystyle T,G\models B}$

El sistema SCRP ^{[4] [5] [6]} se basa directamente en la semántica de recursos de la lógica agrupada; es decir, en monoides ordenados de elementos de recursos. Si bien esta elección es directa e intuitivamente atractiva, conduce a un problema técnico específico: el teorema de completitud de Hennessy-Milner se cumple solo para fragmentos de la lógica modal que excluyen la implicación multiplicativa y las modalidades multiplicativas. Este problema se resuelve basando el cálculo de procesos de recursos en una semántica de recursos en la que los elementos de recursos se combinan utilizando dos combinadores, uno correspondiente a la composición concurrente y otro correspondiente a la elección. ^[20]

Cardelli, Caires, Gordon y otros han investigado una serie de lógicas de cálculos de procesos, donde una conjunción se interpreta en términos de composición paralela. ^{[ cita requerida ]} A diferencia del trabajo de Pym et al. en SCRP, no distinguen entre la composición paralela de los sistemas y la composición de los recursos a los que acceden los sistemas.

Sus lógicas se basan en instancias de la semántica de recursos que dan lugar a modelos de la variante booleana de la lógica agrupada. Aunque estas lógicas dan lugar a instancias de lógica agrupada booleana, parecen haberse elaborado de forma independiente y, en cualquier caso, tienen una estructura adicional significativa en forma de modalidades y vinculantes. También se han propuesto lógicas relacionadas para modelar datos XML .

• Lógica de separación
• Lógica de relevancia
• Lógica lineal