A Classical Linear $λ$-Calculus based on Contraposition

Resumen Técnico: Un $\lambda$-Cálculo Lineal Clásico basado en la Contraposición

Planteamiento del Problema
El artículo aborda el desafío de armonizar las simetrías clásicas de la Lógica Lineal (LL) con el formalismo computacional del $\lambda$-cálculo. La Lógica Lineal exhibe simetrías fuertes (por ejemplo, la dualidad entre las reglas de la izquierda y de la derecha, y la negación involutiva donde $\neg\neg A = A$), pero las presentaciones estándar de deducción natural suelen fallar al intentar preservar estas simetrías manteniendo buenas propiedades computacionales como la confluencia y la normalización fuerte. Los sistemas existentes suelen caer en dos categorías:

1. Fragmentos intuicionistas: Sistemas como ILL o DILL restringen la lógica a sequentes de una sola conclusión, perdiendo las simetrías clásicas y la capacidad de modelar ciertos razonamientos.
2. Sistemas basados en sequentes: Sistemas derivados del cálculo de sequentes (por ejemplo, redes de pruebas o cálculo de procesos) preservan las simetrías, pero a menudo tratan las pruebas como procesos paralelos en lugar de programas funcionales, lo que los hace menos adecuados para los paradigios de programación funcional.

Específicamente, los autores señalan que en la lógica clásica, afirmar una proposición $A$ como tesis es equivalente a negar $A$ como hipótesis. En el contexto de la Lógica Lineal, esto implica que $A \multimap B$ y $B^\perp \multimap A^\perp$ deben compartir las mismas pruebas. Sin embargo, los $\lambda$-cálculos clásicos estándar (como el $\lambda\mu$ de Parigot) son confluentes pero no simétricos (la negación no es involutiva), mientras que los sistemas simétricos (como los de Barbanera y Berardi) a menudo carecen de confluencia. El artículo busca un sistema de deducción natural de una sola conclusión para la Lógica Lineal Lineal Exponencial Multiplicativa (MELL) que retenga las simetrías clásicas y disfrute de las propiedades estándar de los lenguajes de programación tipados.

Metodología
Los autores proponen una nueva asignación de términos para MELL, denominada el cálculo $\lambda$MELL, fundamentada en el paradigma de "proposiciones como tipos". La metodología central consiste en:

1. Fundamento Lógico: Partiendo del fragmento intuicionista de la L lógica Lineal Multiplicativa (MLL), los autores introducen una regla de modus tollens lineal. Mientras que la eliminación de la implicación lineal estándar (modus ponens) permite derivar $B$ a partir de $A \multimap B$ y $A$, la nueva regla permite derivar $A^\perp$ a partir de $A \multimap B$ y $B^\perp$. Esta adición recupera la MLL clásica.
2. Operación Novedosa: Contra-sustitución: Para proporcionar una interpretación computacional para la regla del modus tollens, los autores definen una nueva operación llamada contra-sustitución, denotada como $t\{a \backslash s\}$.
   • Intuición: Si la sustitución estándar $t\{a := s\}$ reemplaza una ocurrencia única de la variable $a$ en $t$ con $s$, la contra-sustitución "atrapa" la ocurrencia única de $a$ en $t$ y "tira" de ella, efectivamente volteando el término $t$ "del revés" (como un calcetín) antes de reemplazar $a$ con $s$.
   • Mecanismo: Esta operación se define por inducción estructural en términos lineales. Por ejemplo, si $t = \langle u, a \rangle$ y $s : A \multimap B^\perp$, entonces $\langle u, a \rangle\{a \backslash s\}$ resulta en $s \bullet u : B^\perp$.
3. Construcción del Cálculo: El cálculo incluye los constructos lineales estándar (tensor, implicación lineal, abstracción lambda) junto con la nueva contra-aplicación ($t \blacktriangledown s$), que corresponde a la eliminación del modus tollens. Para MELL, el cálculo se extiende para incluir las modalidades exponenciales ($!$ y $?$) y las unidades, requiriendo una definición refinada de linealidad y una relación de equivalencia estructural.
4. Equivalencia Estructural: Para asegurar la confluencia en presencia de exponenciales y rutas de reducción complejas, los autores definen una equivalencia estructural ($\equiv$) que actúa como una bisimulación fuerte con respecto a la pre-reducción. Esta equivalencia incluye axiomas para la propagación de eliminadores y el manejo de unidades (por ejemplo, $t[\star := s] \equiv s[\star := t]$ para términos de tipo 1).

Contribuciones Clave

1. El Cálculo $\lambda$MELL: Una presentación de deducción natural de un solo lado para MELL donde las pruebas se modelan como expresiones funcionales. Introduce el constructo de contra-aplicación y la operación de contra-sustitución.
2. Corrección y Completitud: Los autores demuestran que el cálculo es correcto y completo con respecto a MELL. Específicamente, cualquier sequent válido de MELL puede leerse como un juicio de tipado en $\lambda$MELL seleccionando cualquier fórmula como tesis y las negaciones de las demás como hipótesis.
3. Propiedades Metateóricas: El cálculo satisface las propiedades estándar de un lenguaje de programación tipado:
   • Reducción de Sujeto: La reducción preserva el tipado.
   • Confluencia: La relación de reducción es confluente (modulo la equivalencia estructural).
   • Normalización Fuerte: Toda secuencia de reducción termina.
4. Codificación de Sistemas Clásicos: El artículo demuestra que varias asignaciones de términos bien conocidas para la lógica clásica pueden codificarse en $\lambda$MELL, incluyendo:
   • El $\lambda\mu$-cálculo de Parigot (vía traducciones T y Q).
   • El $\lambda\mu\tilde{\mu}$-cálculo de Curien y Herbelin.
   • El $\mu$DCLL de Hasegawa.

Resultados
Los resultados primarios son las demostraciones de las propiedades metateóricas. Los autores establecen la normalización fuerte utilizando la técnica de candidatos de reducibilidad, definiendo conjuntos de términos asociados con cada tipo. La confluencia se demuestra mediante el Lema de Newman al establecer la confluencia local, lo cual depende de que la equivalencia estructural actúe como una bisimulación fuerte para la pre-reducción. El artículo también proporciona demostraciones constructivas para la completitud del cálculo, mostrando cómo recuperar términos de derivaciones libres de cortes de MLL.

Significancia
El artículo afirma su importancia al ofrecer una interpretación "funcional" de la lógica lineal clásica que preserva sus simetrías inherentes sin recurrir a cálculos de procesos o a la deducción natural de múltiples conclusiones. Al introducir la contra-sustitución, los autores proporcionan un mecanismo para manejar computacionalmente el principio clásico de la contraposición dentro de un marco de una sola conclusión. Este trabajo sugiere una base para lenguajes de programación funcional lineales y asistentes de prueba que puedan soportar nativamente el razonamiento clásico y la sensibilidad a los recursos. Los autores señalan que extender el enfoque a los conectivos aditivos es no trivial debido a la dependencia de la linealidad para la contra-sustitución, pero el sistema actual maneja con éxito los fragmentos multiplicativos y exponenciales. El trabajo cierra la brecha entre la simetría del cálculo de sequentes y la naturaleza funcional de los $\lambda$-cálculos.