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 el razonamiento sobre la composición de recursos , que ayudan en el análisis compositivo de computadoras y otros sistemas. Tiene una semántica de teoría de categorías y de 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 vinculación Γ ⊢ A son estructuras en forma de árbol (grupos) 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 manera 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 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]}

Cimientos

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

${\displaystyle A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow 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{and also}}\qquad A\wedge B\vdash C\quad {\mbox{iff}}\quad A\vdash B\Rightarrow C}$

${\displaystyle A*B}$y son formas de conjunción e implicación que tienen en cuenta los recursos (se explican a continuación). 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 ) a partir de la lógica booleana tradicional . Por tanto, la lógica agrupada es compatible con los principios constructivos, pero no depende en modo alguno de ellos. ${\displaystyle B{-\!\!*}C}$ ${\displaystyle \wedge }$ ${\displaystyle \Rightarrow }$ ${\displaystyle \wedge }$ ${\displaystyle \Rightarrow }$ ${\displaystyle \neg }$

Semántica funcional de verdad (semántica de recursos)

La forma más sencilla 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. ${\displaystyle A*B}$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle B{-\!\!*}C}$ ${\displaystyle B}$ ${\displaystyle C}$ ${\displaystyle \wedge }$ ${\displaystyle \Rightarrow }$

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 ' A tiene del recurso r ' . La semántica es análoga a la semántica de lógica intuicionista o modal de Kripke , pero donde los elementos del modelo se consideran recursos que pueden componerse y descomponerse, en lugar de mundos posibles accesibles entre sí. Por ejemplo, la semántica forzada para la conjunción es de la forma ${\displaystyle r\models A}$

${\displaystyle r\models A*B\quad {\mbox{iff}}\quad \exists r_{A}r_{B}.\,r_{A}\models A,\,r_{B}\models B,\,{\mbox{and}}\,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}}$ ${\displaystyle \leq }$

Esta semántica de lógica agrupada se basa en trabajos anteriores en lógica de relevancia (especialmente la semántica operativa de Routley-Meyer), pero difiere de ella al no requerir y aceptar la semántica de las versiones clásicas o intuicionistas estándar de y . La propiedad se justifica pensando en la relevancia pero se niega por consideraciones de recurso; tener dos copias de un recurso no es lo mismo que tener una, y en algunos modelos (por ejemplo, modelos de montón ) es posible que ni siquiera esté definido. La semántica estándar de (o de la negación) es a menudo rechazada por los relevantesistas en su intento por 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 y , que en lógica lineal se rechaza en un intento por 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 \wedge }$ ${\displaystyle \Rightarrow }$ ${\displaystyle r\bullet r\leq r}$ ${\displaystyle r\bullet r}$ ${\displaystyle \Rightarrow }$ ${\displaystyle \wedge }$ ${\displaystyle \Rightarrow }$

Semántica categórica (categorías doblemente cerradas)

La versión doble del teorema de deducción de la lógica agrupada tiene una estructura teórica de categorías correspondiente. Las pruebas en lógica intuicionista se pueden interpretar 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 de homs:

${\displaystyle Hom(A\wedge B,C)\quad {\mbox{is isomorphic to}}\quad Hom(A,B\Rightarrow C)}$

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

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 pueden proporcionar una gran cantidad de modelos categoriales utilizando la construcción de productos tensoriales de Day . ^[8] Además, al fragmento implicacional de la lógica agrupada se le ha dado una semántica de juego . ^[9]

Semántica algebraica

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 poset 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 los siguientes modelos.

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

Teoría de la prueba y teoría de tipos (grupos)

El cálculo de prueba de la lógica agrupada se diferencia de los cálculos secuenciales habituales en que tiene un contexto de hipótesis en forma de árbol en lugar de una estructura en forma de lista plana. En sus teorías de prueba basadas en secuencias, el contexto en un juicio de vinculación es un árbol de raíces finitas 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. ${\displaystyle \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 de debilitamiento y contracción. ${\displaystyle \Delta ,\Gamma }$
• La composición del aditivo admite debilitamiento y contracción de racimos enteros. ${\displaystyle \Delta ;\Gamma }$

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

A la lógica agrupada corresponde una teoría de tipos que tiene dos tipos de funciones. Siguiendo la correspondencia 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 x.M:A{-\!\!*}B}}\qquad \qquad {\frac {\Gamma ;x:A\vdash M:B}{\Gamma \vdash \alpha x.M:A{\Rightarrow }B}}}$

Aquí, hay dos carpetas distintas, una para cada tipo de función. ${\displaystyle \lambda }$ ${\displaystyle \alpha }$

La teoría de la prueba de la lógica agrupada tiene una deuda histórica con el uso de agrupaciones 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 debemos imitar a la izquierda en los secuentes, y para introducir debemos imitar . Esta consideración lleva al uso de dos operadores de combinación. ${\displaystyle {-\!\!*}}$ ${\displaystyle *}$ ${\displaystyle \Rightarrow }$ ${\displaystyle \wedge }$

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

Galmiche, Méry y Pym han brindado un tratamiento integral de la lógica agrupada, incluida la completitud y otras metateorías, basado en cuadros etiquetados . ^[13]

Aplicaciones

Control de interferencias

Quizás en el primer uso de la teoría de tipos subestructurales para controlar recursos, John C. Reynolds mostró cómo utilizar 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 utilizó la teoría de tipos agrupados para ampliar el sistema de Reynolds al permitir que la interferencia y la no interferencia se mezclen de manera más flexible. ^[2] Esto resolvió problemas abiertos relacionados con la recursividad y los saltos en el sistema de Reynolds.

Lógica de separación

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 basó en los siguientes modelos: ${\displaystyle \{Pre\}program\{Post\}}$

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

Es la indefinición de la composición sobre montones superpuestos lo que modela la idea de separación. Este es un modelo de la variante booleana de lógica agrupada.

La lógica de separación se usó originalmente para probar propiedades de programas secuenciales, pero luego se extendió a la concurrencia usando 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 triples de Hoare donde las condiciones previas y posteriores 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 podrían usarse para razonar sobre la interferencia de procesos concurrentes, por ejemplo codificando el razonamiento basado en trazas y garantía de confianza. ^{[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]

Recursos y procesos

La lógica agrupada se ha utilizado en conexión con el cálculo (síncrono) de recursos-proceso SCRP ^{[4] [5] [6]} para dar una lógica (modal) que caracterice, 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 concurrencia de la lógica de separación afirma que una fórmula es verdadera en el estado recurso-proceso , en caso de que haya descomposiciones del recurso y el proceso ~ , donde ~ denota bisimulación , tal que es verdadera en el estado de proceso de recursos , y es verdadero en el estado de proceso de recursos ,; eso es si y . ${\displaystyle A*B}$ ${\displaystyle A*B}$ ${\displaystyle R}$ ${\displaystyle E}$ ${\displaystyle R=S\bullet T}$ ${\displaystyle E}$ ${\displaystyle F\times G}$ ${\displaystyle A}$ ${\displaystyle S}$ ${\displaystyle F}$ ${\displaystyle B}$ ${\displaystyle T}$ ${\displaystyle G}$ ${\displaystyle R,E\models 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 es directa e intuitivamente atractiva, esta elección conduce a un problema técnico específico: el teorema de completitud de Hennessy-Milner es válido sólo 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 proceso de recursos en una semántica de recursos en la que los elementos de los recursos se combinan usando dos combinadores, uno correspondiente a la composición concurrente y otro correspondiente a la elección. ^[20]

Lógicas espaciales

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. ^{[ cita necesaria ]} A diferencia del trabajo de Pym et al. en SCRP, no distinguen entre composición paralela de sistemas y composición de recursos a los que acceden los sistemas.

Su lógica se basa 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 casos de lógica booleana agrupada, parece que se llegó a ellas de forma independiente y, en cualquier caso, tienen una estructura adicional significativa en cuanto a modalidades y aglutinantes. También se han propuesto lógicas relacionadas para modelar datos XML .

Ver también

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

Referencias

1. O'Hearn, Peter; Pym, David (1999). "La lógica de las implicaciones agrupadas" (PDF) . Boletín de Lógica Simbólica . 5 (2): 215–244. CiteSeerX  10.1.1.27.4742 . doi :10.2307/421090. JSTOR  421090. S2CID  2948552.
2. O'Hearn, Peter (2003). "Sobre la escritura agrupada" (PDF) . Revista de programación funcional . 13 (4): 747–796. doi :10.1017/S0956796802004495.
3. Ishtiaq, Samin; O'Hearn, Peter (2001). "BI como lenguaje de aserción para estructuras de datos mutables" (PDF) . POPL . 28 (3): 14-26. CiteSeerX 10.1.1.11.4925 . doi :10.1145/373243.375719. 
4. Pym, David; Tofts, Chris (2006). «Un Cálculo y lógica de recursos y procesos» (PDF) . Aspectos formales de la informática . 8 (4): 495–517. doi :10.1007/s00165-006-0018-z. S2CID  16623194.
5. Collinson, Mateo; Pym, David (2009). "Álgebra y lógica para el modelado de sistemas basados ​​en recursos". Estructuras matemáticas en informática . 19 (5): 959–1027. CiteSeerX 10.1.1.153.3899 . doi :10.1017/S0960129509990077. S2CID  14228156. 
6. Collinson, Mateo; Monahan, Brian; Pym, David (2012). Una disciplina de modelado de sistemas matemáticos . Londres: Publicaciones universitarias. ISBN 978-1-904987-50-5.
7. Pym, David; O'Hearn, Peter; Yang, Hongseok (2004). "Mundos y recursos posibles: la semántica de BI". Informática Teórica . 315 (1): 257–305. doi : 10.1016/j.tcs.2003.11.020 .
8. Día, Brian (1970). "Sobre categorías cerradas de functores" (PDF) . Informes del Seminario Categoría Medio Oeste IV . Apuntes de conferencias de matemáticas. vol. 137. Saltador. págs. 1–38.
9. McCusker, chico; Pym, David (2007). "Un modelo de juego con implicaciones agrupadas" (PDF) . Lógica informática . Apuntes de conferencias sobre informática. vol. 4646. Saltador.
10. Leer, Stephen (1989). Lógica relevante: un examen filosófico de la inferencia . Wiley-Blackwell.
11. Hermanoston, James (2012). "Se muestran lógicas agrupadas" (PDF) . Estudios Lógica . 100 (6): 1223-1254. CiteSeerX 10.1.1.174.8777 . doi :10.1007/s11225-012-9449-0. S2CID  13634990. 
12. Belnap, Nuel (1982). "Lógica de visualización". Revista de Lógica Filosófica . 11 (4): 375–417. doi :10.1007/BF00284976. S2CID  41451176.
13. Galmiche, Didier; Méry, Daniel; Pym, David (2005). "La semántica de BI y cuadros de recursos". Estructuras matemáticas en informática . 15 (6): 1033–1088. CiteSeerX 10.1.1.144.1421 . doi :10.1017/S0960129505004858. S2CID  1700033. 
14. Reynolds, John (1978). "Control sintáctico de interferencias". Actas del quinto simposio ACM SIGACT-SIGPLAN sobre principios de lenguajes de programación - POPL '78 . págs. 39–46. doi : 10.1145/512760.512766 . ISBN 9781450373487. S2CID  18716926.
15. O'Hearn, Peter (2007). «Recursos, Concurrencia y Razonamiento Local» (PDF) . Informática Teórica . 375 (1–3): 271–307. doi : 10.1016/j.tcs.2006.12.035 .
16. Calcagno, Cristiano; O'Hearn, Peter W.; Yang, Hongseok (2007). «Acción local y lógica de separación abstracta» (PDF) . 22º Simposio anual del IEEE sobre lógica en informática (LICS 2007) . págs. 366–378. CiteSeerX 10.1.1.66.6337 . doi :10.1109/LICS.2007.30. ISBN  978-0-7695-2908-0. S2CID  1044254.
17. Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Mateo; Yang, Hongseok (2013). "Vistas: razonamiento compositivo para programas concurrentes" (PDF) . Actas del 40º Simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . 48 : 287–300. doi :10.1145/2480359.2429104.
18. Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015). "Especificar y verificar algoritmos concurrentes con historias y subjetividad" (PDF) . 24º Simposio Europeo de Programación . arXiv : 1410.0306 . Código Bib : 2014arXiv1410.0306S.
19. Calcagno, Cristiano; Distéfano, Dino; O'Hearn, Peter (11 de junio de 2015). "Facebook Infer de código abierto: identifique errores antes de realizar el envío".
20. Anderson, Gabrielle; Pym, David (2015). "Un cálculo y una lógica de procesos y recursos agrupados". Informática Teórica . 614 : 63–96. doi : 10.1016/j.tcs.2015.11.035 .