Ordered Adjoint Logic (Extended Version)

Resumen Técnico de "Lógica Adyacente Ordenada"

Enunciado del Problema
Las lógicas ordenadas y los sistemas de tipos son esenciales para aplicaciones que van desde la lingüística computacional hasta la aplicación de protocolos de seguridad, donde el orden de uso de los recursos es significativo. En la mayoría de las formulaciones, los tipos ordenados también son lineales, lo que requiere que los recursos se utilicen exactamente una vez. Aunque trabajos anteriores de Kanovich et al. investigaron cálculos que relajan esta restricción mediante subexponenciales dentro de una lógica ordenada lineal, este enfoque depende de un "modo base" donde ocurren todas las inferencias. Para las lógicas ordenadas, este modo base debe prohibir todas las reglas estructurales (debilitamiento, contracción, intercambio), obligando a las aplicaciones a cambiar frecuentemente dentro y fuera de este modo restrictivo. Además, los sistemas de subexponenciales existentes no exploran completamente la posibilidad de propiedades estructurales unilaterales (por ejemplo, movilidad izquierda sin movilidad derecha). Los autores tienen como objetivo generalizar estos marcos para soportar un preorden de modos con propiedades estructurales variables y de grano fino, incluido el control independiente sobre el debilitamiento, la contracción izquierda/derecha y la movilidad izquierda/derecha, sin depender de un único modo base restrictivo.

Metodología
Los autores introducen la Lógica Adyacente Ordenada, un sistema que combina la flexibilidad estructural de las modalidades adyacentes con las restricciones de ordenamiento de las lógicas ordenadas. La metodología procede en dos etapas principales:

1. Formulación del Cálculo de Secuentes:
   Los autores definen un cálculo de secuente donde los antecedentes son secuencias ordenadas de hipótesis etiquetadas. Las reglas estructurales no son globales, sino que están gobernadas por un preorden de modos ($k \geq m$). Cada modo $m$ está asociado a un conjunto de propiedades estructurales $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$ (Debilitamiento, Contracción, Movilidad Izquierda, Movilidad Derecha).

   • Modalidades de Desplazamiento: En lugar de un modo base, el sistema utiliza modalidades de desplazamiento ($\downarrow^k_m$ y $\uparrow^m_l$) para cambiar entre razonamientos en diferentes modos. Estos desplazamientos se derivan de la lógica adyacente de Benton, pero se generalizan para manejar contextos ordenados.
   • Reglas Estructurales: Los autores descomponen la movilidad y la contracción en variantes unilaterales. Las reglas de movilidad permiten que una única proposición se mueva arbitrariamente hacia la izquierda o hacia la derecha dentro de la secuencia de antecedentes, siempre que el modo de la proposición admita la movilidad direccional correspondiente. La contracción se permite de forma no local (fusionando duplicados no adyacentes) para garantizar la eliminación de cortes, distinta de la contracción local en la lógica lineal estándar.
   • Conectivos Lógicos: El lenguaje incluye implicaciones ordenadas ($\multimap$ y $\multimap$), conjunciones fusionadas y retorcidas, y desplazamientos. Las reglas son paramétricas en sus modos, con condiciones específicas que aseguran la preservación de la independencia de modos (por ejemplo, $k \geq m \geq r$) al leer las reglas de la conclusión a las premisas.

2. Deducción Natural y Decidibilidad:
   Los autores transitan a una formulación de deducción natural donde las reglas estructurales son implícitas, buscando una base adecuada para lenguajes de programación.

   • Explícito vs. Implícito: Inicialmente, presentan un sistema con reglas estructurales explícitas para cerrar la brecha con el cálculo de secuente. Luego definen un sistema donde las reglas estructurales (debilitamiento, contracción, movilidad) son implícitas.
   • Algoritmo para la Verificación de Pruebas: Para abordar la no determinismo introducido por las reglas estructurales implícitas (específicamente la aplicación ilimitada del debilitamiento y la colocación de variables en las reglas de eliminación), los autores definen un juicio de "forma normal" ($\Omega \gg_{\Gamma, r} \Omega_{nf}$). Este algoritmo calcula el conjunto de todas las formas normales posibles (contextos sin variables repetidas) para un contexto dado $\Omega$, un conjunto de hipótesis $\Gamma$ y un modo $r$.
   • Juicios Basados en Conjuntos: Las reglas de deducción natural se elevan para operar sobre conjuntos de contextos de forma normal ($\Xi$). Por ejemplo, la introducción de conjunción calcula el producto cartesiano de conjuntos de contextos, mientras que la intersección se utiliza para reglas que requieren acuerdo de contexto (como la conjunción aditiva).

Contribuciones Clave

• Lógica Adyacente Generalizada: El artículo generaliza la lógica adyacente a entornos ordenados, introduciendo un preorden de modos donde cada modo controla independientemente el debilitamiento, la contracción y la movilidad unilateral.
• Propiedades Estructurales Unilaterales: El sistema modela y demuestra explícitamente propiedades para la movilidad y la contracción izquierda y derecha como propiedades estructurales separadas e independientes, una característica anticipada pero no explorada en trabajos anteriores sobre subexponenciales.
• Eliminación de Cortes: Los autores demuestran que el cálculo de secuente adyacente ordenado admite eliminación de cortes (mediante multicorte) y eliminación de identidad, estableciendo el sistema como un marco lógico bien comportado.
• Decidibilidad de la Verificación de Pruebas: El artículo proporciona un sistema de deducción natural con reglas estructurales implícitas y demuestra que la verificación de pruebas para este sistema es decidible. Esto se logra construyendo un algoritmo terminante que calcula el conjunto de contextos de forma normal.

Resultados

• Solidez Teórica: Se muestra que el cálculo de secuente satisface la eliminación de cortes e identidad. Se demuestra que el sistema de deducción natural es sólido y completo con respecto al cálculo de secuente.
• Decidibilidad: Se demuestra que el algoritmo para calcular formas normales ($NF_{\Gamma, r}(\Omega)$) termina. En consecuencia, el problema de verificar pruebas en el sistema de deducción natural implícito es decidible.
• Subsumción Subestructural: Los resultados implican la decidibilidad de la subsumción subestructural, un componente central de los algoritmos de verificación de tipos para lenguajes como QRTT (que utiliza semántica de Kripke con mundos explícitos).

Significado y Afirmaciones
Los autores afirman que la Lógica Adyacente Ordenada proporciona una base adecuada para un lenguaje de programación adyacente expresivo o un marco lógico. Al desacoplar las propiedades estructurales de un único modo base y utilizar desplazamientos adyacentes, el sistema permite un razonamiento nativo en diversas disciplinas (lineal, ordenada, ilimitada) con un cambio fluido. La decidibilidad de la verificación de pruebas con reglas estructurales implícitas se destaca como un paso crítico hacia la implementación de verificadores de tipos bidireccionales para lenguajes de programación funcional que puedan manejar propiedades estructurales de grano fino del código. El artículo señala que, aunque se ha establecido el procedimiento de decisión, la eficiencia práctica (por ejemplo, evitar la complejidad exponencial de debilitamientos innecesarios) sigue siendo un tema para futuras optimizaciones. El trabajo se posiciona como una generalización directa de la lógica ordenada subexponencial de Kanovich et al. y una extensión de los tipos adyacentes de Jang et al. para incluir el orden.