The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

Resumen Técnico: El Orden de Camino de Computabilidad para la Reescritura de Orden Superior Beta-Eta-Normal

Planteamiento del Problema
La reescritura de orden superior abarca varios formalismos, notablemente la reescritura de orden superior "simple" (usando coincidencia sintáctica y tratando la reducción $\beta$ como una regla de reescritura) y la reescritura de orden superior "normal" (usando coincidencia módulo $\beta\eta$ y considerando términos en sus formas normales $\beta\eta$). Si bien existen métodos de terminación potentes para la reescritura simple, como el Orden de Camino de Computabilidad (CPO), adaptar estos a la reescritura de orden superior normal (específicamente Sistemas de Reescritura de Orden Superior o HRS al estilo de Nipkow) presenta desafíos significativos.

Los métodos existentes para los HRS, tales como el NHORPO (Orden de Camino Recursivo de Orden Superior Normal), a menudo dependen de una técnica de transformación llamada "neutralización" para manejar sistemas donde el orden central falla. Sin embargo, la neutralización complica la automatización. Además, los órdenes de camino estándar tienen dificultades con la reescritura normal porque los órdenes bien fundados compatibles con $\beta\eta$ generalmente no son monotónicos (cerrados bajo contextos) ni estables (cerrados bajo sustituciones) en el sentido tradicional. Por ejemplo, si un orden es compatible con $\beta\eta$ y cerrado bajo contextos, puede conducir a contradicciones como $c > c$, violando la bien fundamentación.

Metodología
Los autores proponen elevar el Computability Path Order (CPO), definido originalmente para la reescritura de orden superior simple, al entorno de la reescritura de orden superior $\beta\eta$-normal. El orden resultante se denomina $\beta\eta$-normal Computability Path Order (NCPO).

La metodología se basa en los siguientes componentes centrales:

1. Par de Orden de Reducción: Siguiendo el enfoque de Jouannaud y Rubio, los autores definen un orden de reducción como un par $(>, \sqsupset)$, donde $>$ es el orden primario (NCPO) y $\sqsupset$ es una variante "simple" (CPO). El par satisface la estabilidad $\beta\eta$-normal: si $s > t$, entonces $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ para todas las sustituciones $\sigma$, donde $\downarrow$ denota la normalización $\beta\eta$. Esto permite que la prueba de terminación dependa de la bien fundamentación y la monotonicidad del componente CPO simple.
2. Términos No Versátiles: Una innovación técnica crítica es la restricción de la aplicación del orden a térmos no versátiles. Un término es no versátil si la sustitución y la subsecuente normalización $\beta\eta$ solo afectan a sus subtérminos propios. Los autores proporcionan una condición suficiente mejorada para la no versatilidad (Lema 1) en comparación con el trabajo previo, lo cual es esencial para probar la estabilidad del orden.
3. Extensiones desde CPO: El NCPO incorpora dos extensiones clave del CPO original:
   • Subtérmos Accesibles: Estos permiten que las comparaciones recursivas omitan descensos estrictos de tipo en casos específicos determinados por posiciones de tipos (posiciones de tipo base positiva/negativa).
   • Símbolos Pequeños: Esta característica permite que ciertos símbolos de función sean tratados como "pequeños", permitiendo pruebas de terminación para sistemas donde los órdenes de camino recursivos estándar fallan (por ejemplo, funciones de procesamiento de listas).
4. Conjunto de Reglas: El orden se define inductivamente mediante un conjunto de reglas (Figura 1) que manejan símbolos de función (grandes y pequeños), aplicaciones y abstracciones. Notablemente, las reglas para orientar las reducciones $\beta$ y $\eta$ se eliminan, ya que el orden opera directamente sobre las formas normales. Se introduce una nueva regla, $\langle \lambda\triangleright\eta \rangle$, para manejar casos específicos que involucran la expansión $\eta$ en el contexto de los subtérminos accesibles.

Contribuciones Clave

• Definición de NCPO: El artículo define formalmente el NCPO, el primer orden de camino de computabilidad diseñado específicamente para la reescritura de orden superior $\beta\eta$-normal que integra subtérmos accesibles y símbolos pequeños.
• Prueba de Corrección: Los autores demuestran que el par $(>_\tau, \sqsupset_\tau)$ constituye un orden de reducción de orden superior $\beta\eta$-normal válido (Teorema 2), garantizando así la terminación para cualquier HRS compatible con él.
• Condición de No Versatilidad Mejorada: El documento ofrece una condición suficiente refinada para la no versatilidad, la cual es más fuerte que la proporcionada en el trabajo fundacional sobre NHORPO.
• Automatización vía SAT/SMT: Los autores argumentan que el NCPO es más apto para la automatización que el NHORPO con neutralización. Mientras que la neutralización requiere un análisis sintáctico complejo de términos transformados que dependen de parámetros simbólicos (lo que dificulta la codificación SMT), los parámetros del NCPO (precedencia, órdenes de tipo, estatus) pueden codificarse de manera más directa.

Resultados
Los autores implementaron un prototipo de NCPO en Haskell, utilizando el paquete Hasmtlib para codificar problemas de terminación en formato SMT-LIB 2 y resolverlos usando el solver Z3. Los resultados experimentales (Tabla 1) comparan el NCPO contra el NHORPO (con y sin neutralización), así como implementaciones de HORPO en WANDA y CSI$^{ho}$.

• Superioridad sobre NHORPO: El NCPO logra probar la terminación de varios sistemas donde el NHORPO (incluso con neutralización) falla. Específicamente:
  • Ejemplo 8 (Incremento de listas): El NCPO prueba la terminación usando símbolos pequeños, una característica ausente en NHORPO.
  • Ejemplo 7 (Formas Normales Negativas): El NCPO prueba la terminación usando subtérmos accesibles, mientras que el NHORPO con neutralización falla al intentar orientar las reglas debido a la incapacidad de manejar términos versátiles en la comparación.
• Poder Incomparable: El estudio identifica casos (por ejemplo, neutr.p) donde el NHORPO con neutralización tiene éxito pero el NCPO falla, demostrando que ambos enfoques tienen un poder incomparable.
• Eficiencia: Se muestra que la búsqueda de parámetros para el NCPO es computacionalmente eficiente, tomando a menudo un tiempo comparable a las búsquedas de NHORPO, mientras que la búsqueda de parámetros de neutralización puede explotar en complejidad.

Significancia y Reivindicaciones
El artículo afirma que el NCPO proporciona una alternativa poderosa y ligera a la combinación de NHORPO y neutralización. Los autores enfatizan que, si bien el NHORPO con neutralización es un competidor fuerte, la complejidad de automatizar la técnica de neutralización hace que el NCPO sea una opción más práctica para la prueba automática de terminación en la reescritura de orden superior normal.

Los autores señalan modestamente que la transitividad del NCPO sigue siendo una cuestión abierta, ya que la inclusión de la reducción $\beta$ en el orden simple subyacente justifica la no transitividad para CPO y NHORPO, pero las propiedades específicas del NCPO requieren mayor investigación. Además, sugieren que integrar el NCPO en las técnicas de pares de dependencia para la reescritura de orden superior normal es un siguiente paso lógico. El documento concluye resaltando la necesidad de formalizar los métodos de terminación de orden superior para evitar errores encontrados en la literatura previa, como afirmaciones incorrectas sobre la capacidad de resolución de ciertos ejemplos por parte de NHORPO.