| Autor(es) | John C. Reynolds (1935–2013); Peter O’Hearn; David Pym; Samin Ishtiaq |
| Fecha / periodo | 1999–2002 · Siglo XX-XXI · Estados Unidos y Reino Unido |
| Tipo | Formal |
| Deriva de | Lógica relevante · Lógicas subestructurales y cálculo de Lambek · Lógica de Hoare y lógica dinámica · Lógica lineal |
| Derivan de ella | — |
| Tres leyes | Identidad: ✓ (\(P \to P\) y \(P \vdash P\); pero \(P \nvdash P \ast P\)) · No contradicción: ✓ (conectivas aditivas booleanas en el modelo de memoria) · Tercio excluso: matizado (✓ en la lógica BI booleana de la separación; ✗ en BI intuicionista) |
La lógica de Hoare funciona bien para programas que manipulan variables, pero se vuelve inmanejable con punteros: dos nombres pueden designar la misma celda de memoria, y cualquier asignación puede alterar en silencio una estructura que se razonaba por separado. La lógica de la separación resuelve este problema con una conectiva nueva, la conjunción separadora \(P \ast Q\): la memoria se divide en dos porciones disjuntas, una satisface \(P\) y la otra \(Q\). Con ella se enuncia la regla de marco, que permite razonar localmente: si un fragmento de programa solo usa una parte de la memoria, lo que vale en el resto sigue valiendo. El gesto distintivo es tratar las aserciones como descripciones de recursos, no de estados globales. Esa lectura coincide con la de la lógica de las implicaciones agrupadas (BI) de O’Hearn y Pym, de la que la lógica de la separación resultó ser un modelo.
BI (O’Hearn y Pym, 1999). Combina dos familias de conectivas:
Los contextos del cálculo de secuentes son «manojos» (bunches) con dos modos de combinación: \(\Gamma, \Delta\) (multiplicativo) y \(\Gamma ; \Delta\) (aditivo). Debilitamiento y contracción valen para «;» y no para «,». Las reglas de introducción de las dos implicaciones son:
Semántica de recursos. Un monoide parcial conmutativo \((M, \cdot, e)\) con un preorden. \(m \models P \ast Q\) si \(m = m_1 \cdot m_2\) con \(m_1 \models P\) y \(m_2 \models Q\); \(m \models P -\!\ast\, Q\) si para todo \(n\) compatible con \(n \models P\) se cumple \(m \cdot n \models Q\). BI es correcta y completa respecto de ciertas clases de estos modelos (Pym, 2002).
Modelo de la memoria (Reynolds, 2002). Un estado es un par (pila \(s\), montículo \(h\)), donde \(h\) es una función parcial finita de direcciones a valores. Aserciones básicas:
Por ejemplo, \(x \mapsto 3 \ast y \mapsto 3\) implica que \(x \ne y\), mientras que \(x \mapsto 3 \land y \mapsto 3\) implica que \(x = y\).
Ternas y axiomas pequeños. Una terna \(\{P\}\, C\, \{Q\}\) de corrección parcial afirma, además, que \(C\) no provoca fallos de memoria cuando parte de un estado que satisface \(P\). Axiomas locales para las órdenes de memoria:
Regla de marco. De \(\{P\}\, C\, \{Q\}\) se infiere \(\{P \ast R\}\, C\, \{Q \ast R\}\), siempre que \(C\) no modifique variables libres de \(R\). Es correcta gracias a la propiedad de evitar fallos: si \(C\) no falla con solo la porción \(P\), no puede tocar la porción \(R\).
Predicados inductivos. Las estructuras se describen recursivamente. Una lista enlazada que representa la sucesión \(\alpha\) desde \(x\) hasta \(\mathsf{nil}\): \(\mathsf{list}(\epsilon, x) \leftrightarrow x = \mathsf{nil} \land \mathsf{emp}\) y \(\mathsf{list}(a \cdot \alpha, x) \leftrightarrow \exists y\, (x \mapsto a, y \ast \mathsf{list}(\alpha, y))\). La separación garantiza que la lista no tiene ciclos ni comparte celdas.
Qué se pierde y qué se gana. \(\ast\) no es idempotente: \(P \nvdash P \ast P\), porque un recurso no se puede duplicar. Tampoco vale en general \(P \ast Q \vdash P\) sin información adicional sobre el resto de la memoria. La lógica de primer orden de la separación con cuantificadores y varita mágica es indecidible (Calcagno, Yang y O’Hearn, 2001), pero fragmentos como el de las listas son decidibles y se usan en herramientas automáticas.
La lógica de la separación es una extensión de la lógica de Hoare: conserva las ternas, las reglas estructurales de composición, condicional y bucle, y añade las aserciones sobre la memoria y la regla de marco. Su componente lógica, BI, procede de la teoría de la prueba subestructural. De la lógica relevante toma la idea de contextos con dos modos de combinación, los manojos, que Dunn, Belnap y Read habían usado para distinguir combinación extensional e intensional de premisas. De la lógica lineal toma la conjunción multiplicativa \(\ast\), análoga a \(\otimes\), aunque BI no tiene exponenciales y combina las conectivas multiplicativas con las aditivas intuicionistas en lugar de derivar unas de otras. Como lógica de recursos, BI es una lógica subestructural más, y comparte con ellas el método de restringir el debilitamiento y la contracción.
La convergencia fue histórica. Reynolds esbozó las ideas hacia 1999–2000 con un lenguaje de aserciones propio; Ishtiaq y O’Hearn (2001) mostraron que era una instancia de BI y añadieron la varita mágica; el artículo de Reynolds en LICS 2002 fijó el nombre. O’Hearn y Brookes extendieron el marco a la concurrencia en 2004–2007, trabajo que recibió el premio Gödel en 2016.
Es uno de los casos más claros en que una lógica no clásica, diseñada con motivos teóricos, pasa a la industria. Smallfoot (2005) fue el primer verificador automático; Infer, desarrollado por Monoidics y adquirido por Facebook en 2013, analiza a gran escala código de aplicaciones reales. Iris y VST son marcos de lógica de la separación de orden superior usados en asistentes de prueba. Para la pregunta «¿una lógica o muchas?» ofrece un argumento práctico: cuando las proposiciones describen recursos, la contracción deja de ser inocua, y la lógica que conviene no es la clásica, sino una que combina la clásica con una capa subestructural. Las dos conviven en el mismo cálculo, cada una con su propia conjunción y su propia implicación.