Lógica agrupada

La forma más sencilla de entender estas fórmulas es mediante su semántica veritativo-funcional. En esta semántica, una fórmula es verdadera o falsa con respecto a determinados recursos. ${\displaystyle A*B}$afirma que el recurso en cuestión puede descomponerse en recursos que satisfacen${\displaystyle A}$y${\displaystyle B}$. ${\displaystyle B{-\!\!*}C}$dice que si componemos el recurso disponible con un recurso adicional que satisfaga${\displaystyle B}$, entonces el recurso combinado satisface${\displaystyle C}$.${\displaystyle \wedge }$y${\displaystyle \Rightarrow }$tienen sus significados familiares.

La base para esta lectura de fórmulas fue proporcionada por una semántica forzante.${\displaystyle r\models A}$propuesto por Pym, donde la relación de forzamiento significa ' A posee 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 se consideran recursos que pueden componerse y descomponerse, 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\models A*B\quad {\mbox{si y solo si}}\quad \exists r_{A}r_{B}.\,r_{A}\models A,\,r_{B}\models B,\,{\mbox{y}}\,r_{A}\bullet r_{B}\leq r}$

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

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 ${\displaystyle r\bullet r\leq r}$y aceptando la semántica de las versiones intuicionistas o clásicas estándar de${\displaystyle \wedge }$y${\displaystyle \Rightarrow }$La propiedad${\displaystyle r\bullet r\leq r}$ se justifica al pensar en la relevancia pero se niega por consideraciones de recursos; tener dos copias de un recurso no es lo mismo que tener una, y en algunos modelos (por ejemplo, modelos de montón )${\displaystyle r\bullet r}$Puede que ni siquiera esté definido. La semántica estándar de ${\displaystyle \Rightarrow }$(o de negación) suele ser rechazada por los relevanteistas en su intento de escapar de las "paradojas de la implicación material", que no son un problema desde la perspectiva de los recursos de modelado 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${\displaystyle \wedge }$y${\displaystyle \Rightarrow }$, que en lógica lineal se rechaza en un intento de ser constructivo. Estas consideraciones se discuten en detalle en un artículo sobre semántica de recursos de Pym, O'Hearn y Yang. ^{[ 7 ]}

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

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

La lógica agrupada puede interpretarse en categorías que poseen dos de dichas estructuras.

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

Se pueden dar numerosos modelos categóricos utilizando la construcción de 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 sencilla de enunciar y puede ser más accesible.

Un modelo algebraico de lógica agrupada es un poset que es un álgebra de Heyting y que lleva una estructura de retículo residuado conmutativo adicional (para el mismo retículo 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{si y solo si}}\quad A\leq B{-\!\!*}C}$.

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

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

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

${\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 radica en las reglas adicionales que se les aplican.

• Composición multiplicativa${\displaystyle \Delta,\Gamma}$Niega las reglas estructurales de debilitamiento y contracción.
• Composición aditiva${\displaystyle \Delta$ ;\Gamma } admite el debilitamiento y la contracción de grupos enteros.

Las reglas estructurales y otras operaciones sobre grupos se aplican a menudo en lo profundo de un contexto de árbol, y no solo en el nivel superior: es, por lo tanto, en cierto sentido, un cálculo de inferencia profunda .

La lógica agrupada se corresponde con una teoría de tipos que posee dos tipos de funciones . Siguiendo la correspondencia de Curry-Howard , las reglas de introducción para las implicaciones se corresponden con 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 carpetas distintas,${\displaystyle \lambda }$y${\displaystyle \alpha }$, uno para cada tipo de función.

La teoría de la demostración de la lógica agrupada tiene una deuda histórica con el uso de grupos en la lógica de relevancia. ^{[ 10 ]} Pero la estructura agrupada puede, en cierto sentido, derivarse de la semántica categórica y algebraica: formular una regla de introducción para${\displaystyle {-\!\!*}}$deberíamos imitar${\displaystyle *}$a la izquierda en secuencias, y para introducir${\displaystyle \Rightarrow }$deberíamos imitar${\displaystyle \wedge }$Esta consideración lleva al uso de dos operadores de combinación.

James Brotherston has done further significant work on a unified proof theory for bunched logic and variants,^[11] employing Belnap's notion of display logic.^[12]

Galmiche, Méry, and Pym have provided a comprehensive treatment of bunched logic, including completeness and other meta-theory, based on labelled tableaux.^[13]

In perhaps the first use of substructural type theory to control resources, John C. Reynolds showed how to use an affine type theory to control aliasing and other forms of interference in ALGOL-like programming languages.^[14] O'Hearn used bunched type theory to extend Reynolds' system by allowing interference and non-interference to be more flexibly mixed.^[2] This resolved open problems concerning recursion and jumps in Reynolds' system.

Separation logic is an extension of Hoare logic that facilitates reasoning about mutable data structures that use pointers. Following Hoare logic the formulae of separation logic are of the form ${\displaystyle \{Pre\}programa\{Publicar\}}$, but the preconditions and postconditions are formulae interpreted in a model of bunched logic. The original version of the logic was based on models as follows:

• ${\displaystyle Montones=L\rightharpoonup _{f}V\qquad }$ (finite partial functions from locations to values)
• ${\displaystyle h_{0}\bullet h_{1}=}$ union of heaps with disjoint domains, undefined when domains overlap.

It is the undefinedness of the composition on overlapping heaps that models the separation idea. This is a model of the boolean variant of bunched logic.

Separation logic was used originally to prove properties of sequential programs, but then was extended to concurrency using a proof rule

${\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}\}}}}$

that divides the storage accessed by parallel threads.^[15]

Later, the greater generality of the resource semantics was utilized: an abstract version of separation logic works for Hoare triples where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.^[16] By suitable choice of commutative monoid, it was surprisingly found that the proofs rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding rely-guarantee and trace-based reasoning.^[17][18]

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

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

SCRP es notable por interpretar${\displaystyle A*B}$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 procesos de SCRP que corresponde a la regla de la lógica de separación para la concurrencia afirma que una fórmula${\displaystyle A*B}$es cierto en el estado de proceso de recursos${\displaystyle R}$,${\displaystyle E}$por si acaso se producen descomposiciones del recurso${\displaystyle R=S\bullet T}$y proceso ${\displaystyle E}$~${\displaystyle F\times G}$, donde ~ denota bisimulación , tal que${\displaystyle A}$es cierto en el estado de proceso de recursos${\displaystyle S}$,${\displaystyle F}$y${\displaystyle B}$es cierto en el estado de proceso de recursos${\displaystyle T}$,${\displaystyle G}$; eso es${\displaystyle R,E\models A}$si y solo si${\displaystyle S,F\models A}$y${\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, conlleva un problema técnico específico: el teorema de completitud de Hennessy-Milner solo se cumple 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 mediante 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álculo de procesos, donde una conjunción se interpreta en términos de composición paralela. A diferencia del trabajo de Pym et al. en SCRP, no distinguen entre la composición paralela de sistemas y la composición de 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. Si bien estas lógicas generan instancias de lógica agrupada booleana, parecen haberse desarrollado de forma independiente y, en cualquier caso, presentan una estructura adicional significativa en cuanto a modalidades y conectores. También se han propuesto lógicas similares para el modelado de datos XML .