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

Résumé Technique : L'Ordre de Chemin de Computabilité pour le Réécriture de Ordre Supérieur $\beta\eta$-Normal

Énoncé du Problème
La réécriture d'ordre supérieur englobe diverses formalismes, notamment la réécriture d'ordre supérieur « simple » (utilisant l'appariement syntaxique et traitant la réduction $\beta$ comme une règle de réécriture) et la réécriture d'ordre supérieur « normale » (utilisant l'appariement modulo $\beta\eta$ et considérant les termes dans leurs formes normales $\beta\eta$). Bien que des méthodes de terminaison puissantes existent pour la réécriture simple, telles que l'Ordre de Chemin de Computabilité (CPO), l'adaptation de celles-ci à la réécriture d'ordre supérieur normale (spécifiquement les Systèmes de Réécriture d'Ordre Supérieur ou HRS à la manière de Nipkow) présente des défis importants.

Les méthodes existantes pour les HRS, telles que le NHORPO (Normal Higher-Order Recursive Path Order), reposent souvent sur une technique de transformation appelée « neutralisation » pour gérer les systèmes où l'ordre central échoue. Cependant, la neutralisation complique l'automatisation. De plus, les ordres de chemin standards peinent avec la réécriture normale car les ordres bien fondés compatibles avec $\beta\eta$ ne sont généralement pas monotones (clos sous les contextes) ou stables (clos sous les substitutions) au sens traditionnel. Par exemple, si un ordre est compatible avec $\beta\eta$ et clos sous les contextes, il peut mener à des contradictions comme $c > c$, violant ainsi la bien-fondation.

Méthodologie
Les auteurs proposent de porter l'Ordre de Chemin de Computabilité (CPO), défini à l'origine pour la réécriture d'ordre supérieur simple, vers le cadre de la réécriture d'ordre supérieur $\beta\eta$-normale. L'ordre résultant est nommé l'Ordre de Chemin de Computabilité $\beta\eta$-normal (NCPO).

La méthodologie repose sur les composants clés suivants :

1. Paire d'Ordre de Réduction : Suivant l'approche de Jouannaud et Rubio, les auteurs définissent un ordre de réduction comme une paire $(>, \sqsupset)$, où $>$ est l'ordre primaire (NCPO) et $\sqsupset$ est une variante « simple » (CPO). La paire satisfait la stabilité $\beta\eta$-normale : si $s > t$, alors $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ pour toutes les substitutions $\sigma$, où $\downarrow$ désigne la normalisation $\beta\eta$. Cela permet de faire reposer la preuve de terminaison sur la bien-fondation et la monotonie de la composante CPO simple.
2. Termes Non-Versatiles : Une innovation technique cruciale est la restriction de l'application de l'ordre aux termes non-versatiles. Un terme est non-versatile si la substitution et la normalisation $\beta\eta$ subséquentes n'affectent que ses sous-termes propres. Les auteurs fournissent une condition suffisante améliorée pour la non-versatilité (Lemme 1) par rapport aux travaux précédents, ce qui est essentiel pour prouver la stabilité de l'ordre.
3. Extensions à partir du CPO : Le NCPO incorpore deux extensions clés du CPO original :
   • Sous-termes Accessibles : Ceux-ci permettent aux comparaisons récursives de contourner les diminutions de type strict dans des cas spécifiques déterminés par les positions de type (positions de types de base positives/négatives).
   • Symboles Petits : Cette caractéristique permet à certains symboles de fonction d'être traités comme « petits », permettant des preuves de terminaison pour des systèmes où les ordres de chemin récursifs standards échouent (ex: fonctions de traitement de listes).
4. Ensemble de Règles : L'ordre est défini de manière inductive via un ensemble de règles (Figure 1) gérant les symboles de fonction (grands et petits), les applications et les abstractions. Notamment, les règles pour orienter les réductions $\beta$ et $\eta$ sont supprimées, car l'ordre opère directement sur les formes normales. Une nouvelle règle, $\langle \lambda\triangleright\eta \rangle$, est introduite pour gérer les cas spécifiques impliquant l'expansion $\eta$ dans le contexte des sous-termes accessibles.

Contributions Clés

• Définition du NCPO : Le papier définit formellement le NCPO, le premier ordre de chemin de computabilité spécifiquement conçu pour la réécriture d'ordre supérieur $\beta\eta$-normale qui intègre les sous-termes accessibles et les symboles petits.
• Preuve de Correction : Les auteurs prouvent que la paire $(>_\tau, \sqsupset_\tau)$ constitue un ordre de réduction d'ordre supérieur $\beta\eta$-normal valide (Théorème 2), garantissant ainsi la terminaison de tout HRS compatible avec lui.
• Condition de Non-Versatilité Améliorée : Le papier offre une condition suffisante raffinée pour la non-versatilité, qui est plus forte que celle fournie par le travail fondateur sur le NHORPO.
• Automatisation via SAT/SMT : Les auteurs soutiennent que le NCPO est plus apte à l'automatisation que le NHORPO avec neutralisation. Alors que la neutralisation nécessite une analyse syntaxique complexe de termes transformés dépendant de paramètres symboliques (rendant l'encodage SMT difficile), les paramètres du NCPO (précédence, ordres de types, statut) peuvent être encodés plus directement.

Résultats
Les auteurs ont implémenté un prototype de NCPO en Haskell, utilisant le package Hasmtlib pour encoder les problèmes de terminaison au format SMT-LIB 2 et les résoudre avec le solveur Z3. Les résultats expérimentaux (Tableau 1) comparent le NCPO au NHORPO (avec et sans neutralisation), ainsi qu'aux implémentations de HORPO dans WANDA et CSI$^{ho}$.

• Supériorité sur le NHORPO : Le NCPO prouve avec succès la terminaison de plusieurs systèmes là où le NHORPO (même avec neutralisation) échoue. Spécifiquement :
  • Exemple 8 (Incrément de liste) : Le NCPO prouve la terminaison en utilisant des symboles petits, une caractéristique absente du NHORPO.
  • Exemple 7 (Formes Normales de Négation) : Le NCPO prouve la terminaison en utilisant des sous-termes accessibles, tandis que le NHORPO avec neutralisation échoue à orienter les règles en raison de l'incapacité à gérer les termes versatiles lors de la comparaison.
• Puissance Incomparable : L'étude identifie des cas (ex: neutr.p) où le NHORPO avec neutralisation réussit mais le NCPO échoue, démontant que les deux approches ont une puissance incomparable.
• Efficacité : La recherche de paramètres pour le NCPO est montrée comme étant informatiquement efficace, prenant souvent un temps comparable à la recherche de paramètres NHORPO, alors que la recherche de paramètres de neutralisation peut voir sa complexité exploser.

Signification et Revendications
Le papier affirme que le NCPO fournit une alternative puissante et légère à la combinaison du NHORPO et de la neutralisation. Les auteurs soulignent que bien que le NHORPO avec neutralisation soit un compétiteur fort, la complexité de l'automatisation de la technique de neutralisation fait du NCPO un choix plus pratique pour la preuve automatique de terminaison en réécriture d'ordre supérieur normale.

Les auteurs notent modestement que la transitivité du NCPO reste une question ouverte, car l'inclusion de la réduction $\beta$ dans l'ordre simple sous-jacent justifie la non-transitivité pour le CPO et le NHORPO, mais les propriétés spécifiques du NCPO nécessitent des investigations supplémentaires. De plus, ils suggèrent que l'intégration du NCPO dans les techniques de paires de dépendance pour la réécriture d'ordre supérieur normale est une étape logique suivante. Le papier conclut en soulignant la nécessité de formaliser les méthodes de terminaison d'ordre supérieur pour éviter les erreurs trouvées dans la littérature précédente, telles que des affirmations incorrectes concernant la résolution de certains exemples par le NHORPO.