Towards an HRS Category in TermCOMP

Résumé Technique : Vers une catégorie HRS dans TermCOMP

Énoncé du Problème
La compétition annuelle de terminaison (TermCOMP) inclut une catégorie pour la réécriture d'ordre supérieur. Historiquement, cette catégorie a utilisé la sémantique des Systèmes Algébriques Fonctionnels (SAF), qui reposent sur l'appariement simple et des règles de $\beta$-réduction explicites. Bien que les systèmes de réécriture d'ordre supérieur (HRS) de Nipkow, qui effectuent une réécriture modulo $\beta\eta$ et utilisent généralement les motifs de Miller (PRS) ou le plus récent système de réécriture de motifs déterministes d'ordre supérieur (DPRS), soient des formalismes bien établis, ils n'ont pas été pleinement intégrés dans le cadre compétitif de TermCOMP. Le défi consiste à réconcilier la sémantique des HRS (réécriture modulo $\beta\eta$) avec le cadre existant de TermCOMP (basé sur les SAF et les méta-substitutions) afin de permettre aux outils ciblant les HRS de rivaliser directement avec ceux ciblant les SAF.

Méthodologie
Les auteurs proposent un pont formel entre les HRS et la sémantique d'ordre supérieur actuelle de TermCOMP, définie comme des Systèmes de Réécriture par Méta-Substitution Simplement Typés (STMRS). La méthodologie comprend trois étapes principales :

1. Généralisation des Motifs : Les auteurs introduisent les Systèmes de Réécriture de Motifs Étendus (EPRS), une sous-classe des HRS qui généralise à la fois les PRS et les DPRS. Les EPRS utilisent des « Motifs Étendus » (EPATs), qui relâchent les contraintes d'appariement déterministes des DPRS tout en maintenant une structure où les variables libres sont appliquées à des arguments non-abstraits. Cette classe est définie principalement pour faciliter la preuve théorique plutôt que comme un outil pratique autonome.
2. Extension de la Sémantique STMRS : Les auteurs étendent la définition des règles STMRS (le standard actuel de TermCOMP) pour permettre aux membres gauches d'être des EPATs plutôt que de simples motifs standards. Ils introduisent le concept de termes bien élevés (well-behaved) et quasi-bien élevés (quasi-well-behaved). Ces restrictions syntaxiques garantissent que lorsque les méta-substitutions sont appliquées, les termes résultants restent en forme normale $\beta$ (spécifiquement en forme normale longue $\beta\eta$) sans générer de nouveaux $\beta$-redex qui nécessiteraient des étapes de réduction supplémentaires.
3. Implémentation via la Réécriture Normalisée : La contribution technique centrale est d'établir que la réécriture dans un STMRS bien élevé, suivie de la $\beta$-normalisation, simule la réécriture dans l'EPRS correspondant. Les auteurs définissent une traduction entre les substitutions ordinaires (utilisées dans les EPRS) et les méta-substitutions (utilisées dans les STMRS) pour prouver que les deux systèmes sont équivalents concernant la terminaison.

Contributions Clés

• Définition des EPRS : Une nouvelle sous-classe syntaxique des HRS qui généralise les DPRS, permettant une gamme plus large de benchmarks tout en conservant des propriétés d'appariement gérables.
• Restrictions Syntaxiques pour l'Équivalence : L'introduction de règles STMRS « bien élevées ». Ces règles restreignent les membres gauches pour qu'ils soient bien élevés et les membres droits pour qu'ils soient quasi-bien élevés. Cela garantit que l'application de méta-substitutions ne crée pas de $\beta$-redex, préservant ainsi la forme normale $\beta$ des termes.
• Théorème d'Équivalence Formelle : Les auteurs prouvent que pour un STMRS bien élevé $R$ et un terme $s$ en forme normale longue $\beta\eta$, une étape de réécriture dans la sémantique EPRS ($s \to_R t$) se produit si et seulement si une étape de réécriture dans la sémantique STMRS suivie d'une $\beta$-normalisation se produit ($s \Rightarrow_R \cdot \Rightarrow!_\beta t$).

Résultats
Le résultat principal est le Théorème 15, qui établit la correspondance entre les relations de réécriture des STMRS bien élevés et leurs EPRS correspondants. Plus précisément :

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ si et seulement si $s \to_R t$ (en considérant $R$ comme un EPRS).
• Cela mène au Corollaire 20, qui stipule que la terminaison de la stratégie « réécrire puis $\beta$-normaliser » dans un STMRS bien élevé coïncide avec la terminaison universelle de l'EPRS correspondant.

Les auteurs démontrent que cette équivalence tient pour les termes en forme normale longue $\beta\eta$. Ils notent que pour les STMRS de second ordre, la correspondance est encore plus forte, offrant une correspondance un pour un entre les étapes car les méta-substitutions ne peuvent pas créer de $\beta$-redexes dans ce contexte spécifique.

Signification
L'article affirme poser la fondation formelle pour une (sous-)catégorie HRS dans TermCOMP. En définissant un sous-ensemble de benchmarks syntaxiquement vérifiables (STMRS bien élevés) au sein du format TPDB existant, les auteurs permettent :

1. Une Compétition Directe : Les outils conçus pour les HRS (utilisant la réécriture $\beta\eta$) peuvent désormais rivaliser avec les outils conçus pour les SAF au sein de la même catégorie, car leurs propriétés de terminaison sont prouvées comme coïncidant sous les sémantiques proposées.
2. Un Support d'Outils Plus Large : Le résultat d'implémentation permet la comparaison de propriétés au-delà de la simple terminaison, car la simulation est basée sur une correspondance étape par étape plutôt que sur une simple propriété de terminaison globale.
3. Un Raffinement des Travaux Existants : Le résultat renforce les implémentations précédentes des PRS dans les AFSM (Kop) et les systèmes combinatoires (van Oostrom et van Raamsdonk) en les étendant à une classe plus générale de HRS (EPRS) et en fournissant une preuve rigoureuse de l'équivalence entre la réécriture normalisée et la réécriture d'ordre supérieur.

Les auteurs restent modestes quant à la portée de leur travail, reconnaissant que le résultat ne couvre pas tous les HRS car la méta-substitution est strictement moins puissante que la pleine substitution d'ordre supérieur. Cependant, ils soutiennent que la sous-classe définie est suffisante pour accommoder une partie significative des benchmarks existants et les DPRS spécifiques introduits dans leurs travaux antérieurs.