Towards an HRS Category in TermCOMP

Resumen Técnico: Hacia una categoría de HRS en TermCOMP

Planteamiento del Problema
La competencia anual de terminación (TermCOMP) incluye una categoría para la reescritura de orden superior. Históricamente, esta categoría ha utilizado la semántica de los Sistemas Algebraicos Funcionales (AFS), que se basan en el emparejamiento simple y reglas explícitas de reducción $\beta$. Aunque los Sistemas de Reescritura de Orden Superior (HRS) de Nipkow, que realizan reescritura módulo $\beta\eta$ y típicamente utilizan patrones de Miller (PRS) o los más recientes Sistemas de Reescritura de Patrones Deterministas de Orden Superior (DPRS), son formalismos bien establecidos, no se han integrado plenamente en el marco competitivo de TermCOMP. El desafío radica en reconciliar la semántica de los HRS (reescritura módulo $\beta\eta$) con el marco existente de TermCOMP (basado en AFS y meta-sustituciones) para permitir que las herramientas dirigidas a HRS compitan directamente contra aquellas dirigidas a AFS.

Metodología
Los autores proponen un puente formal entre los HRS y la actual semántica de orden superior de TermCOMP, definida como Sistemas de Reescritura de Meta-Sustitución Simplemente Tipados (STMRS). La metodología implica tres pasos principales:

1. Generalización de Patrones: Los autores introducen los Sistemas de Reescritura de Patrones Extendidos (EPRS), una subclase de los HRS que generaliza tanto a los PRS como a los DPRS. Los EPRS utilizan "Patrones Extendidos" (EPATs), que relajan las restricciones de emparejamiento determinista de los DPRS mientras mantienen una estructura donde las variables libres se aplican a argumentos que no son abstracciones. Esta clase se define principalmente para facilitar la prueba teórica más que como una herramienta práctica independiente.
2. Extensión de la Semántica STMRS: Los autores extienden la definición de las reglas STMRS (el estándar actual de TermCOMP) para permitir que los lados izquierdos sean EPATs en lugar de solo patrones estándar. Introducen el concepto de términos bien comportados (well-behaved) y cuasi-bien comportados (quasi-well-behaved). Estas restricciones sintácticas aseguran que, cuando se aplican las meta-sustituciones, los términos resultantes permanezcan en forma normal $\beta$ (específicamente en forma normal larga $\beta\eta$) sin generar nuevos $\beta$-redexes que requieran pasos de reducción adicionales.
3. Implementación mediante Reescritura Normalizada: La contribución técnica central es establecer que la reescritura en un STMRS bien comportado, seguida de la $\beta$-normalización, simula la reescritura en el correspondiente EPRS. Los autores definen una traducción entre sustituciones ordinarias (usadas en los EPRS) y meta-sustituciones (usadas en los STMRS) para demostrar que los dos sistemas son equivalentes respecto a la terminación.

Contribuciones Clave

• Definición de EPRSs: Una nueva subclase sintáctica de los HRS que generaliza a los DPRSs, permitiendo un rango más amplio de benchmarks mientras mantiene propiedades de emparejamiento manejables.
• Restricciones Sintácticas para la Equivalencia: La introducción de reglas STMRS "bien comportadas". Estas reglas restringen los lados izquierdos para que sean bien comportados y los lados derechos para que sean cuasi-bien comportados. Esto asegura que la aplicación de meta-sustituciones no cree $\beta$-redexes, preservando la forma normal $\beta$ de los términos.
• Teorema de Equivalencia Formal: El artículo demuestra que para un STMRS bien comportado $R$ y un término $s$ en forma normal larga $\beta\eta$, un paso de reescritura en la semántica del EPRS ($s \to_R t$) ocurre si y solo si ocurre un paso de reescritura en la semántica del STMRS seguido de $\beta$-normalización ($s \Rightarrow_R \cdot \Rightarrow!_\beta t$).

Resultados
El resultado principal es el Teorema 15, que establece la correspondencia entre las relaciones de reescritura de los STMRS bien comportados y sus correspondientes EPRS. Específicamente:

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ si y solo si $s \to_R t$ (viendo a $R$ como un EPRS).
• Esto conduce al Corolario 20, que establece que la terminación de la estrategia "reescribir y luego $\beta$-normalizar" en un STMRS bien comportado coincide con la terminación universal del correspondiente EPRS.

Los autores demuestran que esta equivalencia se mantiene para términos en forma normal larga $\beta\eta$. Observan que para los STMRS de segundo orden, la correspondencia es aún más fuerte, ofreciendo un mapeo uno a uno entre pasos porque las meta-sustituciones no pueden crear $\beta$-redexes en ese contexto específico.

Significancia
El artículo afirma sentar las bases formales para una (sub)categoría de HRS en TermCOMP. Al definir un subconjunto de benchmarks sintácticamente comprobable (STMRS bien comportados) dentro del formato TPDB existente, los autores permiten:

1. Competencia Directa: Las herramientas diseñadas para HRS (que usan $\beta\eta$-reescritura) ahora pueden competir contra herramientas diseñadas para AFS dentro de la misma categoría, ya que sus propiedades de terminación se demuestran coincidentes bajo la semántica propuesta.
2. Soporte de Herramientas más Amplio: El resultado de implementación permite la comparación de propiedades más allá de la simple terminación, ya que la simulación se basa en una correspondencia paso a paso en lugar de solo una propiedad de terminación global.
3. Refinamiento del Trabajo Existente: El resultado fortalece las implementaciones previas de los PRS en los AFSM (Kop) y sistemas combinatorios (van Oostrom y van Raamsdonk) al extenderlas a una clase más general de HRS (EPRSs) y proporcionar una prueba rigurosa de la equivalencia entre la reescritura normalizada y la reescritura de orden superior.

Los autores mantienen la modestia respecto al alcance, reconociendo que el resultado no cubre todos los HRS porque la meta-sustitución es estrictamente menos potente que la sustitución de orden superior completa. Sin embargo, argumentan que la subclase definida es suficiente para acomodar una parte significativa de los benchmarks existentes y los DPRS específicos introducidos en su trabajo previo.