Towards Weak Stratification for Logics of Definitions

Resumen Técnico: Hacia la estratificación débil para lógicas de definiciones

Planteamiento del problema
La lógica de definiciones es una familia de lógicas utilizadas para codificar y razonar sobre juicios especificados por reglas de inferencia, donde los predicados atómicos se asocian con fórmulas lógicas que pueden depender del propio predicado. Para resolver la circularidad aparente inherente a tales definiciones, los enfoques estándar imponen una condición de estratificación, asegurando que un predicado no aparezca negativamente (a la izquierda de una implicación) en el cuerpo de su propia definición. Esta condición trata efectivamente las definiciones como operadores de punto fijo monótonos.

Sin embargo, muchas especificaciones útiles, particularmente aquellas que involucran relaciones lógicas para probar propiedades de lenguajes de programación, requieren definiciones donde el predicado aparece negativamente. En la lógica $\mathcal{G}$, que subyace al asistente de pruebas Abella, tales definiciones están prohibidas. Tiu [19] introdujo previamente una lógica llamada $\mathcal{LD}$ que relaja la condición de estratificación hacia una estratificación débil (permitiendo ocurrencias negativas siempre que el nivel de la cabecera sea estrictamente mayor que el nivel de la ocurrencia negativa), pero $\mathcal{LD}$ estaba limitada a un fragmento central. Carecía de soporte para el cuantificador nabla ($\nabla$), esencial para razonar sobre nombres y frescura mediante constantes nominales, y para definiciones inductivas generales más allá de la inducción sobre números naturales. El desafío abordado en este trabajo es extender la lógica de definiciones para incluir la estratificación débil manteniendo la consistencia en presencia de $\nabla$ y definiciones inductivas generales.

Metodología
El artículo define una nueva lógica, $\mathcal{LD}\mu\nabla$, que extiende la $\mathcal{LD}$ de Tiu con cuantificación nabla y definiciones inductivas generales. La metodología procede en tres etapas principales:

1. Sintaxis y semántica de $\mathcal{LD}\mu\nabla$:
   La lógica se formula como una extensión del cálculo de secuentes de primer orden con un conjunto de definiciones $\mathcal{D}$ y un conjunto de definiciones inductivas $\mathcal{I}$.

   • Estratificación débil: Un conjunto de definiciones $\mathcal{D}$ es débilmente estratificado si para cada cláusula $H \triangleq_X B$ y sustitución de enraizamiento $\rho$, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Crucialmente, esto permite ocurrencias negativas del predicado definido si el nivel de la cabecera es estrictamente mayor que el nivel de la ocurrencia negativa.
   • Estratificación estricta para la inducción: El artículo impone una condición más estricta en las definiciones inductivas $\mathcal{I}$: estas deben ser estrictamente estratificadas (el nivel de un predicado atómico enraizado debe ser independiente de sus argumentos). Esta restricción es necesaria para prevenir la inconsistencia al combinar la inducción con la estratificación débil.
   • Cuantificador Nabla: La lógica incorpora el cuantificador $\nabla$ para manejar constantes nominales y la frescura, distinguiendo entre instancias genéricas y específicas de nombres.

2. Lógica de enraizamiento e interpretación:
   Para probar la consistencia, los autores construyen una versión de enraizamiento de la lógica, $\mathcal{LD}\mu\nabla_\infty$, donde todas las fórmulas son de enraizamiento (sin variables propias).

   • Lema de enraizamiento: Un paso técnico clave es probar que cualquier derivación en $\mathcal{LD}\mu\nabla$ puede interpretarse como una derivación en $\mathcal{LD}\mu\nabla_\infty$ mediante una sustitución de enraizamiento. Esto reduce el problema de consistencia de la lógica completa a la consistencia de la lógica de enraizamiento.
   • Reglas infinitarias: En $\mathcal{LD}\mu\nabla_\infty$, las reglas estándar $\forall R$ y $\exists L$ son reemplazadas por reglas infinitarias que cuantifican sobre todos los términos de enraizamiento, y la regla $\mu L$ para la inducción es similarmente expandida para cubrir todas las instancias de enraizamiento.

3. Eliminación de cortes:
   El núcleo de la prueba de consistencia es la eliminación de la regla de corte (específicamente, la regla de multicut) en $\mathcal{LD}\mu\nabla_\infty$.

   • Relación de reducción: Se define una relación de reducción sobre las derivaciones, especificando cómo los cortes pueden ser empujados hacia arriba o eliminados.
   • Reducibilidad: Siguiendo la técnica de Tait-Martin-Löf adaptada por McDowell y Miller, los autores definen una noción de reducibilidad (y normalizabilidad) para las derivaciones. Prueban que toda derivación en $\mathcal{LD}\mu\nabla_\infty$ es reducible.
   • Manejo de casos inductivos: Un aspecto crítico de la prueba es el manejo de la interacción entre la estratificación débil y la inducción. Los autores muestran que, mientras la estratificación débil es suficiente para las definiciones generales, las definiciones inductivas deben permanecer estrictamente estratificadas. Proporcionan un contraejemplo (Sección 3.3) demostrando que permitir definiciones inductivas débilmente estratificadas conduce a la inconsistencia lógica.

Contribuciones clave

• Definición de $\mathcal{LD}\mu\nabla$: El artículo define formalmente una lógica que combina la estratificación débil, la cuantificación nabla y las definiciones inductivas generales.
• Prueba de consistencia: La contribución principal es la prueba de que $\mathcal{LD}\mu\nabla$ es consistente. Esto se logra probando la eliminación de cortes para la lógica de enraizamiento $\mathcal{LD}\mu\nabla_\infty$ y estableciendo una interpretación de enraizamiento.
• Restricciones de estratificación: El trabajo clarifica el límite entre las definiciones permisibles e impermisibles. Demuestra que, si bien la estratificación débil es suficiente para las definiciones generales (permitiendo las relaciones lógicas), las definiciones inductivas requieren una estratificación estricta para preservar la consistencia.
• Contraejemplo: El artículo proporciona un contraejemplo específico que muestra cómo relajar la condición de estratificación para las definiciones inductivas conduce a la inconsistencia lógica, justificando la restricción impuesta sobre $\mathcal{I}$.

Resultos

• Consistencia: Se demuestra que la lógica $\mathcal{LD}\mu\nabla$ es consistente. En consecuencia, la lógica $\mathcal{LD}\mu\nabla_\infty$ admite derivaciones libres de cortes para todos los secuentes demostrables.
• Propiedades de inversión: El artículo establece propiedades metateóricas para $\mathcal{LD}\mu\nabla_\infty$, incluyendo la invertibilidad de varias reglas de introducción (p. ej., $\wedge R$, $\vee L$, $\nabla R$) y la invertibilidad parcial específica para $\vee R$, $\exists R$ y las reglas de definición ($\Delta R$) cuando el contexto está vacío. Estas propiedades son crucialas para los procedimientos de búsqueda de pruebas.
• Limitaciones: El teorema de eliminación de cortes se establece únicamente para la lógica de enraizamiento $\mathcal{LD}\mu\nabla_\infty$. El artículo señala que extender este resultado a la lógica completa $\mathcal{LD}\mu\nabla$ (con variables propias) sigue siendo un desafío abierto.

Significado
El significado de este trabajo radica en su potencial para extender las capacidades del asistente de pruebas Abella. Abella se basa en la lógica $\mathcal{G}$, que actualmente restringe las definiciones a ser estrictamente estratificadas. Al justificar la inclusión de definiciones débilmente estratificadas, esta investigación allana el camino para que Abella soporte nativamente las relaciones lógicas, una técnica fundamental para probar propiedades semánticas de lenguajes de programación (como la seguridad de tipos y la corrección de compiladores).

El artículo posiciona este trabajo como un paso fundacional hacia una extensión más amplia de $\mathcal{G}$. Mientras que el resultado actual maneja la estratificación débil con $\nabla$ e inducción, los autores señalan que una justificación completa para Abella requeriría extensiones adicionales para incluir la coinducción y la abstracción nominal. El trabajo también destaca la necesidad de mantener la estratificación estricta para las definiciones inductivas, una restricción que evita las inconsistencias que de otro modo surgirían al mezclar la estratificación débil con la inducción.