Templates in Rewriting Induction

1. Énoncé du problème

Le papier aborde un goulot d'étranglement critique dans l'Induction par Réécriture (RI), un système formel utilisé pour prouver l'équivalence de programmes (théorèmes inductifs) dans les Systèmes de Réécriture de Termes (TRS). Bien que la RI soit puissante, son application pratique à des codes réels échoue souvent en raison de la difficulté de la génération automatique de lemmes.

• Le problème de la divergence : Lors de la preuve de l'équivalence de deux programmes (par exemple, différentes implémentations d'une fonction factorielle), le processus de preuve rencontre souvent une séquence d'équations qui ne correspondent pas. Les techniques RI standard (analyse de cas et réécriture) génèrent de nouvelles équations mais ne peuvent pas utiliser les précédentes comme hypothèses d'induction car les termes divergent structurellement.
• Limites des méthodes existantes :
  • Méthodes basées sur les contraintes (par exemple, [9, 12]) : Ces méthodes tentent de découvrir des invariants de boucle (par exemple, $z = a \times j$) pour généraliser les équations. Bien qu'efficaces pour l'arithmétique simple, elles échouent lorsque la relation entre les variables est non polynomiale ou lorsque la structure de la boucle est complexe.
  • Focus de bas niveau : Les méthodes existantes opèrent au niveau de valeurs de variables spécifiques et de contraintes plutôt que de reconnaître des constructions de programmation de haut niveau (comme la récursion terminale par rapport à la récursion générale).
• Contexte : Les auteurs se concentrent sur les Systèmes de Réécriture de Termes Typés Simplement Contraints Logiquement (LCSTRSs), qui modélisent du code de programmation réel avec des types de données primitifs (entiers, booléens) et des contraintes logiques (gardes), les rendant plus adaptés à la vérification de programmes que les TRS standards.

2. Méthodologie

Les auteurs proposent une approche de Génération de Lemmes Basée sur des Modèles qui intègre des motifs de programmation de haut niveau dans le système de preuve RI Borné.

A. Le concept de modèles

Au lieu de rechercher des invariants arithmétiques spécifiques, les auteurs définissent des Modèles : des schémas de réécriture qui capturent des constructions de programmation courantes (par exemple, récursion terminale ascendante/descendante, récursion générale).

• Quatre modèles principaux :
  1. TailUp ($T^+$) : Récursion terminale ascendante (l'indice augmente).
  2. TailDown ($T^-$) : Récursion terminale descendante (l'indice diminue).
  3. RecUp ($R^+$) : Récursion générale ascendante.
  4. RecDown ($R^-$) : Récursion générale descendante.
• Récursors d'ordre supérieur : Ces modèles sont formalisés comme des récursors d'ordre supérieur (par exemple, tailup, recdn). Un programme spécifique est apparié à un modèle en identifiant une fonction de contexte $F$ (l'opération effectuée dans la boucle) et des bornes ($l, u$).

B. La stratégie de preuve

La méthodologie repose sur un processus de preuve en deux étapes au sein de la RI Bornée :

1. Équivalence Modèle-Récursor : Prouver qu'une implémentation concrète de programme est équivalente à son récursor d'ordre supérieur correspondant (par exemple, facTU $\approx$ tailup). Cela se fait par induction structurelle sur l'indice de la boucle.
2. Équivalence des récursors : Prouver les équivalences entre les récursors abstraits eux-mêmes (par exemple, tailup $\approx$ recdn).
   • Appariement unilatéral : Transformer un côté de l'équation cible en un récursor, puis appliquer une équivalence de récursor connue pour simplifier l'autre côté.
   • Appariement bilatéral : Transformer les deux côtés dans leurs récursors respectifs et appliquer directement un théorème d'équivalence général.

C. Équivalences conditionnelles

Pour les cas où une équivalence simple ne tient pas (par exemple, tailup par rapport à taildn), les auteurs introduisent des Théorèmes Inductifs Bornés Conditionnels. Ces preuves reposent sur des axiomes (par exemple, la commutativité et l'associativité de l'opération $F$) et des exigences d'ordre spécifiques pour assurer la terminaison et la correction.

3. Contributions clés

1. Nouvelle heuristique de génération de lemmes : Le papier introduit une méthode qui généralise sur les structures de boucles plutôt que sur des valeurs de variables spécifiques. Cela permet de prouver des équivalences qui étaient auparavant hors de portée pour les générateurs d'invariants basés sur les contraintes.
2. Intégration avec les LCSTRS : L'approche est spécifiquement conçue pour les Systèmes de Réécriture de Termes Typés Simplement Contraints Logiquement, permettant une modélisation directe de l'arithmétique entière et des gardes booléennes sans encodages complexes.
3. Abstraction d'ordre supérieur : En utilisant des récursors d'ordre supérieur, le système peut gérer des opérations arbitraires (comme la multiplication dans la factorielle ou l'application de fonction dans des exemples d'ordre supérieur) en tant que paramètres, rendant les modèles réutilisables dans différents domaines.
4. Système de preuve formel : Les auteurs définissent les règles de déduction spécifiques (Simplifier, Cas, Supprimer, Induire, Hypothèse) et les exigences d'ordre nécessaires pour intégrer ces modèles dans le cadre de la RI Bornée.
5. Démonstration de puissance : Le papier prouve avec succès les équivalences entre diverses implémentations de factorielle (Ascendante vs Descendante, Terminale vs Récursive) et des variantes d'ordre supérieur, y compris des cas où les invariants requis sont non polynomiaux.

4. Résultats

• Succès sur les implémentations de factorielle : Le système a prouvé avec succès l'équivalence de quatre implémentations différentes de factorielle (Itérative Ascendante/Descendante, Récursive Ascendante/Descendante) sous la contrainte $x \ge 1$.
  • Réalisations clés : Prouver facTU $\approx$ facTD (Terminale Ascendante vs Terminale Descendante) était impossible pour les méthodes précédentes ([9, 12]) car les invariants nécessaires n'étaient pas polynomiaux. L'approche par modèles a résolu cela en reconnaissant la similarité structurelle des boucles.
• Extensions d'ordre supérieur : La méthode a été étendue aux fonctions d'ordre supérieur (par exemple, funfacTU), prouvant l'équivalence entre des implémentations qui appliquent une fonction $h$ à l'indice de la boucle avant la multiplication.
• Preuves conditionnelles : Le système a géré des cas nécessitant des axiomes (associativité/commutativité) pour prouver des équivalences entre différentes directions de récursion (par exemple, tailup $\approx$ taildn si l'opération est commutative).

5. Signification

• Combler le fossé : Ce travail comble le fossé entre la preuve de théorèmes automatisée de bas niveau (qui lutte avec les boucles complexes) et la vérification de programmes de haut niveau. Il déplace l'accent de la "recherche du bon invariant" vers la "reconnaissance du bon motif".
• Évolutivité : En abstrayant les valeurs arithmétiques spécifiques, la méthode s'étend à des comportements de calcul plus complexes où les invariants polynomiaux échouent.
• Potentiel d'automatisation : Bien que actuellement implémentée comme un processus manuel/semi-automatique dans l'outil Cora, les auteurs soutiennent que la reconnaissance de modèles est largement syntaxique, suggérant un fort potentiel pour une automatisation complète dans les futurs outils.
• Fondement pour la vérification de programmes : L'approche fournit un cadre robuste pour vérifier les transformations de programmes (par exemple, optimiser une fonction récursive en une fonction récursive terminale) en présence de contraintes logiques, ce qui est essentiel pour la vérification des systèmes logiciels modernes.

En résumé, Hagens et Kop présentent un changement de paradigme dans l'Induction par Réécriture : passer de la découverte d'invariants à la correspondance de motifs structurels, permettant la vérification d'équivalences de programmes qui étaient auparavant impossibles à prouver en raison de la complexité de leurs invariants inductifs.