A Formalization of Abstract Rewriting in Agda

Este artículo presenta una formalización constructiva de los Sistemas de Reescritura Abstracta en Agda, que elimina la lógica clásica en pruebas estándar, refina los criterios de terminación y confluencia y demuestra su aplicabilidad mediante la formalización del cálculo lambda.

Lo esencial

Imagina que el mundo de la informática y las matemáticas es como una inmensa ciudad llena de reglas de tráfico. En esta ciudad, las "reglas de reescritura" (Abstract Rewriting Systems) son como las señales que dicen: "Si ves este coche, puedes transformarlo en ese otro coche".

Los autores de este artículo, Samuel y Andrew, son como dos arquitectos que han decidido construir un manual de instrucciones digital (escrito en un lenguaje llamado Agda) para entender cómo funcionan estas transformaciones de manera perfecta y sin errores.

Aquí te explico los puntos clave de su trabajo usando analogías sencillas:

1. El Objetivo: Construir un "GPS" para la Computación

En lugar de solo decir "esto es verdad" (como hacen los matemáticos clásicos), ellos querían crear un GPS que no solo te diga el camino, sino que también te muestre cómo conducir el coche.

• La analogía: Imagina que tienes un mapa que te dice "llegarás a la meta". Ellos querían un mapa que, además, te diera el volante y los pedales para que tú mismo pudieras llegar. En programación, esto significa que sus pruebas matemáticas son también código que funciona. Si demuestran que dos cosas son iguales, el código puede transformar una en la otra automáticamente.

2. El Problema: Usar "Magia" vs. Construir con Ladrillos

Muchos libros de texto antiguos usan "magia" (lógica clásica) para probar cosas. La magia dice: "O bien pasa esto, o bien pasa lo contrario, así que ya está".

• El problema: En el mundo real de la computación, no puedes usar magia; necesitas ladrillos reales. Si dices "o pasa A o pasa B", la computadora necesita saber cuál de los dos es para poder actuar.
• Su solución: Ellos eliminaron toda la magia. Construyeron todo el sistema usando solo ladrillos que la computadora puede tocar y verificar. Si no pueden decidir algo con certeza, lo dicen claramente en lugar de asumir que sí.

3. Los Dos Grandes Retos: ¿Terminamos o nos perdemos?

En este sistema de reglas, hay dos preguntas vitales:

1. ¿El proceso termina alguna vez? (Normalización): Si sigo transformando el coche, ¿llegará un día en que no pueda transformarlo más y se quede quieto (un "estado final")?
2. ¿El camino importa? (Confluencia): Si tomo dos caminos diferentes para transformar el coche, ¿llegaré al mismo estado final?

La analogía del Laberinto:

• Normalización: Es asegurarse de que el laberinto no tenga pasillos infinitos donde te quedes dando vueltas para siempre.
• Confluencia: Es asegurarse de que, aunque tomes un atajo o un camino largo, ambos te lleven a la misma salida.

4. El Descubrimiento: "El Lemma de Newman" Mejorado

Hay una regla famosa llamada "Lemma de Newman" que dice: "Si el laberinto no tiene bucles infinitos (termina) y tiene una propiedad local de que los caminos se cruzan rápido, entonces todo el sistema funciona perfecto".

• Lo que hicieron ellos: Descubrieron que la regla original era un poco rígida. Encontraron una versión más flexible. Imagina que la regla original exigía que el laberinto fuera "pequeño". Ellos demostraron que funciona incluso si el laberinto es "ordenado" de una manera específica, incluso si es un poco más grande o complejo. Esto permite aplicar la regla a más situaciones reales.

5. La "Caja de Herramientas" para Programadores

Ellos crearon una biblioteca de herramientas (una librería de código) que otros programadores pueden usar.

• El ejemplo del Lambda Cálculo: Imagina que quieres construir un motor de coche (un lenguaje de programación). En lugar de tener que inventar las reglas de cómo se mueven las piezas desde cero, puedes tomar la caja de herramientas de Samuel y Andrew, ponerla en tu motor, y automáticamente sabes que:
  • El motor no se quedará atascado en bucles infinitos.
  • No importa cómo lo enciendas, llegará al mismo estado de funcionamiento.
  • Puedes calcular exactamente cómo se verá el motor al final.

6. ¿Por qué es importante esto?

Antes, si querías probar que un programa era seguro, tenías que escribir una prueba matemática gigante cada vez. Ahora, con su trabajo, tienes un kit de construcción pre-aprobado.

• La metáfora final: Es como si antes, cada vez que querías construir una casa, tuvieras que inventar las leyes de la física para saber si los ladrillos se sostendrían. Ahora, Samuel y Andrew han escrito el "Código de Edificación" universal. Si sigues sus reglas, la casa (o el programa) se mantendrá en pie, y además, tendrás los planos exactos para construirla.

En resumen:
Este artículo es sobre tomar las reglas abstractas de cómo las computadoras transforman datos, limpiarlas de suposiciones mágicas, y convertirlas en un manual práctico, verificable y automático que garantiza que los programas no se atasquen y siempre lleguen a su destino correcto.

Resumen técnico

Aquí presento un resumen técnico detallado del artículo "A Formalization of Abstract Rewriting in Agda" de Samuel Arkle y Andrew Polonsky, estructurado según los puntos solicitados.

1. El Problema

La teoría de sistemas de reescritura abstracta (ARS) es fundamental para el análisis de lenguajes de programación y lógica. Sin embargo, las presentaciones clásicas de esta teoría (como la del libro Terese de Bezem, Klop y De Vrijer) dependen en gran medida de la lógica clásica (por ejemplo, el principio del tercero excluido o pruebas por contradicción).

Esto presenta un desafío para la formalización en asistentes de prueba basados en la teoría de tipos intuicionista, como Agda, que siguen el paradigma de "pruebas como programas" (Curry-Howard). En este contexto:

• Las pruebas deben ser constructivas para ser efectivas (es decir, para que puedan ejecutarse como código).
• El uso de axiomas clásicos o extensionalidad de funciones rompe la capacidad computacional de las pruebas.
• Existe una brecha entre los resultados teóricos estándar y su implementación práctica en sistemas que requieren computación explícita (como la extracción de términos normales o la verificación de convergencia).

El objetivo principal es formalizar la teoría básica de ARS en Agda de manera puramente constructiva, identificando y eliminando el uso innecesario de lógica clásica, y refinando los criterios de terminación y confluencia para que sean aplicables en la práctica.

2. Metodología

Los autores desarrollaron una biblioteca formal en Agda siguiendo principios estrictos de programación funcional y teoría de tipos:

• Paradigma Constructivo: Se evitó el uso de axiomas como la extensiónalidad de funciones, la univalencia, la unicidad de pruebas de identidad (axioma K) o la lógica clásica. Todas las pruebas son programas efectivos.
• Análisis de Decidibilidad: Se identificaron explícitamente las hipótesis de decidibilidad necesarias. Se demostró que para sistemas de reescritura finitamente ramificados y decidibles (como los TRS de primer orden), la mayoría de los resultados clásicos pueden obtenerse constructivamente.
• Revisión de Definiciones: Se redefinieron conceptos clave (como la bien-fundación y la normalización fuerte) para adaptarlos al contexto constructivo, explorando múltiples formulaciones que son lógicamente equivalentes en la lógica clásica pero distintas en la intuicionista.
• Generalización: Se investigaron nuevas propiedades (como la "minimización fuerte" y la "recurrencia") para sustituir o generalizar condiciones clásicas más restrictivas (como la existencia de una función de tamaño).
• Validación Práctica: La teoría se aplicó para formalizar el cálculo lambda no tipado, demostrando la utilidad de la biblioteca en un caso de uso complejo.

3. Contribuciones Clave

El trabajo aporta varias contribuciones significativas a la teoría de la reescritura y la formalización en Agda:

1. Formalización Constructiva de ARS: Una implementación completa de la teoría de ARS basada en Terese, incluyendo un análisis detallado de las relaciones lógicas entre propiedades de terminación y confluencia.
2. Ontología de Propiedades: Se define una jerarquía refinada de propiedades, introduciendo conceptos nuevos como:
   • Formas mínimas (MF): Un concepto de terminación que generaliza las formas normales.
   • Minimización Fuerte (SM) y Débil (WM): Propiedades que permiten analizar la terminación sin asumir la lógica clásica.
   • Propiedad de Recurrencia (RP): Una generalización de la propiedad de "crecimiento" (Inc) que evita la necesidad de funciones de tamaño computacionalmente costosas.
3. Refinamiento del Lema de Newman: Se presenta una generalización del Lema de Newman. Mientras que el clásico requiere Normalización Fuerte (SN) y Confluencia Débil (WCR) para probar Confluencia (CR), los autores demuestran que SM ∧ WCR ⇒ CR. Esto es más fuerte porque SM es una condición más débil que SN en contextos constructivos.
4. Análisis de Bien-Fundación (Well-Foundedness): Se examinan y comparan múltiples definiciones de bien-fundación (accesible, inductiva, coreductiva, por minimalidad, secuencial). Se mapean las implicaciones entre ellas, identificando exactamente qué principios clásicos (como la decidibilidad de subconjuntos o el principio de Markov) son necesarios para pasar de una definición a otra.
5. Eliminación de Lógica Clásica: Se demuestra que para sistemas finitamente ramificados y decidibles, la implicación intuitiva de que "Normalización Fuerte implica Normalización Débil" es válida constructivamente, algo que no es cierto para relaciones arbitrarias.

4. Resultados Principales

• Efectividad de Resultados Estándar: La mayoría de los resultados principales de ARS pueden hacerse completamente efectivos para ejemplos prácticos (TRS de primer orden y cálculo lambda).
• Jerarquía de Implicaciones: Se establecieron tablas de implicaciones locales y globales que muestran cuándo se pueden derivar la confluencia y la normalización fuerte a partir de combinaciones de propiedades. Por ejemplo, se muestra que WN ∧ UN→ ⇒ CR no requiere suposiciones clásicas, a diferencia de SN ∧ UN→.
• Relación entre SN y WN: Se probó que la implicación SN → WN no es demostrable constructivamente en general (su asunción para todas las relaciones implica el principio del tercero excluido). Sin embargo, es válida bajo las hipótesis de decidibilidad y ramificación finita.
• Generalización de Criterios: Se demostró que la propiedad de "recurrencia" (RP) es suficiente para reemplazar la propiedad de "crecimiento" (Inc) en teoremas clave, eliminando la necesidad de funciones de tamaño explícitas.
• Aplicación al Cálculo Lambda: La biblioteca se utilizó exitosamente para formalizar propiedades del cálculo lambda (como la decidibilidad de formas normales y la consistencia ecuacional), demostrando que la teoría general puede aplicarse a estructuras complejas y heterogéneas (tipos anidados) sin interferir con la formalización.

5. Significado e Impacto

Este trabajo es fundamental para el desarrollo de infraestructuras formales en la teoría de lenguajes de programación:

• Cimentación de Bibliotecas Formales: Sirve como un "arranque" (bootstrapping) para un repositorio de teoría de lenguajes de programación formalizados en Appalachian State University, permitiendo que proyectos futuros se basen en resultados de ARS verificados y computables.
• Puente entre Teoría y Práctica: Al eliminar la lógica clásica innecesaria, las pruebas no solo verifican la validez, sino que generan algoritmos. Por ejemplo, una prueba de que un sistema es Church-Rosser se convierte automáticamente en una función que calcula un redúcto común entre dos términos convertibles.
• Claridad Conceptual: Al descomponer definiciones clásicas en sus componentes constructivos, los autores revelan qué suposiciones ocultas (como la decidibilidad de la relación) son realmente necesarias para ciertos teoremas. Esto evita errores de formalización en sistemas donde estas suposiciones no se cumplen.
• Herramienta para Verificación: La capacidad de importar certificados de terminación de herramientas automáticas (como las de la competencia internacional de terminación) y traducirlos a Agda se ve facilitada por esta formalización, permitiendo integrar herramientas de verificación automatizada en flujos de trabajo de desarrollo de lenguajes.

En resumen, el artículo transforma la teoría de reescritura abstracta de un marco teórico clásico en una herramienta computacional robusta y verificada, optimizando las hipótesis necesarias y proporcionando una base sólida para la formalización de sistemas complejos de programación.