💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Cet article de travail introduit une tactique de correspondance de motifs automatique pour Autosubst qui répond à ses limitations actuelles dans la gestion des règles de typage, des relations de réduction et des solutions non uniques, comme le démontrent les évaluations sur les défis POPLMark et POPLMark Reloaded.

Auteurs originaux : Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

Publié 2026-07-15

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de résoudre un puzzle magique géant où chaque pièce possède une étiquette cachée. Dans le monde de l'informatique, ces étiquettes sont appelées « indices de De Bruijn ». C'est une façon astucieuse de garder une trace des variables dans le code, mais elles sont notoirement difficiles. Voyez cela comme un jeu de chaises musicales (où les chaises, les variables, changent de nom à chaque fois que quelqu'un s'assoit). Si vous essayez de faire correspondre une pièce de puzzle (une règle) à un trou (un objectif), les pièces peuvent paraître différentes même si elles sont en réalité les mêmes, simplement en portant des chapeaux différents.

Pendant longtemps, un outil appelé Autosubst a été le héros de cette histoire. C'est comme un robot super intelligent qui peut instantanément vous dire si deux pièces de puzzle sont identiques, même si leurs étiquettes ont été mélangées. Il y parvient en utilisant un ensemble de règles magiques (appelées $\sigma$ -calcul) pour normaliser les pièces jusqu'à ce qu'elles soient identiques. Si vous voulez simplement vérifier si deux choses sont égales, ce robot est parfait.

Le Problème : Le Piège de l'« Apply »
Cependant, il y a un piège. Lorsque vous essayez d'utiliser ces pièces de puzzle pour résoudre un problème en appliquant une règle (comme utiliser un bouton « Appliquer » dans un jeu vidéo), le robot reste bloqué. Il est excellent pour dire « Oui, ces deux éléments sont égaux », mais il est très mauvais pour dire « Voici comment vous insérez cette règle dans ce trou spécifique ».

Pourquoi ? Parce que parfois, une règle peut s'insérer dans un trou de plusieurs manières, et le robot ne sait pas laquelle est la « bonne » sans aide. Par le passé, les programmeurs humains devaient faire tout le gros du travail. Ils devaient réécrire leurs règles de manière étrange et indirecte ou deviner manuellement les étiquettes manquantes juste pour faire fonctionner le robot. C'était comme essayer de forcer une cheville carrée dans un trou rond en ponçant la cheville soi-même, plutôt que de simplement trouver le bon outil.

La Nouvelle Idée : Une Tactique de Devinette Intelligente
Ce papier présente un nouvel outil appelé as_apply. Voyez cela comme un nouveau bras de robot, légèrement plus aventureux, conçu pour saisir ces pièces de puzzle et essayer de les enfoncer dans les trous, même lorsque les étiquettes ne correspondent pas parfaitement au premier abord.

Au lieu d'abandonner ou de demander à l'humain de tout réécrire, cette nouvelle tactique utilise un ensemble d'heuristiques (qui sont essentiellement des devinettes éduquées basées sur des modèles déjà observés). Elle regarde le trou, regarde la règle et se dit : « Je parie que si je décale ces étiquettes juste un tout petit peu, elles conviendront ! »

Comment ça marche (Le Tour de Magie)
Le processus se déroule en deux étapes :

Préparation : Le robot nettoie d'abord les pièces du puzzle en utilisant les anciennes règles fiables d'Autosubst pour les rendre aussi propres que possible.
Le Jeu de Devinettes : Il tente ensuite de faire correspondre les pièces. Si les pièces ne correspondent pas parfaitement, il ne panique pas. Au lieu de cela, il essaie quelques astuces spécifiques :
- Il vérifie si le décalage est un simple « décalage » (comme déplacer une variable d'un cran vers le haut).
- Il vérifie si la pièce manquante est juste une « identité » (ne rien faire).
- Il recherche des motifs courants qui arrivent habituellement dans ces puzzles.

Si l'une de ces devinettes fonctionne, il remplit les étiquettes manquantes et continue. Si elle échoue, il revient en arrière (backtrack) et essaie une autre devinette.

Ce que le Papier Dit (et Ne Dit Pas)
Les auteurs font très attention à ne pas trop survendre leur travail. Ils admettent que ce n'est pas une baguette magique qui résout tous les problèmes possibles.

Ce n'est pas parfait : Le papier stipule explicitement que parfois, un puzzle peut avoir plusieurs solutions, et ce robot pourrait choisir la mauvaise. Il est possible de construire un exemple complexe où le robot se trompe, même si une bonne réponse existe.
C'est un « Travail en Cours » : Les auteurs décrivent cela comme une méthode « en cours de développement ». Ils ne prétendent pas avoir résolu toute la théorie de la correspondance pour toujours.
Les Résultats : Ils ont testé cette nouvelle tactique sur deux défis célèbres et difficiles appelés POPLMark et POPLMark Reloaded. Ce sont comme les « Jeux Olympiques » pour prouver des choses sur les langages de programmation.
- Dans le défi POPLMark (642 lignes de code), ils ont utilisé la nouvelle tactique 15 fois.
- Dans le défi POPLMark Reloaded (683 lignes de code), ils l'ont utilisée 10 fois.
- Dans chacun de ces cas, la tactique a résolu l'objectif avec succès.

Le Verdict
Le papier suggère que, bien que cette nouvelle tactique ait des limites théoriques (elle peut être confuse par des puzzles très bizarres ou adverses), elle fonctionne étonnamment bien dans le monde réel. Elle permet aux programmeurs d'arrêter de réécrire leurs règles de manière étrange et indirecte pour simplement les écrire naturellement.

Les auteurs sont optimistes mais prudents. Ils suggèrent que cette approche pourrait remplacer l'ancienne méthode lourde et maladroite dans de nombreux cas pratiques, mais ils savent qu'il reste du travail pour s'assurer que le robot ne choisisse jamais la mauvaise solution. Ils travaillent actuellement à déterminer exactement quels types de puzzles ce robot peut résoudre avec une certitude de 100 %, et lesquels pourraient encore nécessiter qu'un humain vérifie le travail.

En bref, c'est un nouvel outil ingénieux et utile qui rend la tâche désordonnée de l'appariement des pièces de puzzle beaucoup plus facile, même s'il n'est pas encore prêt à être le seul outil de la boîte.

Résumé Technique : Une tactique pour l'appariement de motifs dans Autosubst

Énoncé du Problème
Le papier traite d'une limitation spécifique du framework Autosubst, un générateur de code pour l'assistant de preuve Rocq (anciennement Coq) qui automatise le raisonnement sur les termes de de Bruijn et la substitution via le $\sigma$ -calcul. Bien qu'Autosubst automatise avec succès la vérification d'égalité pour les buts sans hypothèses via la tactique asimpl, il échoue lorsque les utilisateurs tentent d'appliquer des hypothèses (par exemple, des règles de typage ou des lemmes) à un but via des tactiques standards comme apply ou eapply.

Dans ces scénarios, l'utilisateur doit unifier un but avec une hypothèse modulo l'équivalence $\sigma$ . Cependant, l'automatisation d'Autosubst n'est pas conçue pour l'appariement avec des hypothèses. Par conséquent, les utilisateurs sont contraints d'employer des contournements laborieux, tels que :

La formulation de règles sous des formes indirectes (en utilisant des méta-variables fraîches au lieu de termes de substitution directs).
L'introduction de lemmes auxiliaires pour combler le fossé entre le but et l'hypothèse.
La transformation manuelle des buts ou l'instanciation explicite de variables existentielles lors des preuves.

La difficulté fondamentale réside dans le fait que l'appariement $\sigma$ (l'appariement modulo l'équivalence $\sigma$ ) n'est pas unique ; un problème d'appariement peut admettre plusieurs solutions, dont certaines ne satisfont pas les prémisses du contexte. De plus, l'appariement de second ordre pour le $\lambda\sigma$ -calcul complet est indécidable, et même sans la réduction $\beta$ , les solutions ne sont pas nécessairement uniques.

Méthodologie
Les auteurs proposent une tactique heuristique de type "travail en cours" nommée as_apply, implémentée dans le langage Ltac de Rocq, pour automatiser l'appariement de motifs modulo l'équivalence $\sigma$ . La tactique opère en deux phases principales :

Prétraitement :
- Le but et la conclusion de l'hypothèse cible sont tous deux normalisés par rapport au $\sigma$ -calcul en utilisant la tactique asimpl existante.
- Les variables quantifiées dans l'hypothèse sont remplacées par des variables existentielles (evars).
- Les prémisses de l'hypothèse sont converties en sous-buts à résoudre après la phase d'appariement.
- La tactique gère les conversions entre les opérations de renommage explicites (ex: $s\langle\xi\rangle$ ) et les opérations d'instanciation ( $s[\xi]$ ) en utilisant substify et renamify.
Phase d'Appariement :
- La tactique construit un ensemble d'équations d'appariement $M = \{s_i =_\sigma t_i\}$ entre les termes du but et les termes de l'hypothèse instanciés.
- Elle traite les équations de gauche à droite en utilisant une procédure partielle, $\sigma_{min}$ , qui tente de faire correspondre les termes modulo le fragment $\sigma_{min}$ (un sous-ensemble de règles $\sigma$ caractérisant l'instanciation et la compositionnalité).
- Heuristiques : Si $\sigma_{min}$ $σ_{min}$ échoue à trouver un appariement, la tactique applique un ensemble d'heuristiques capturant des motifs courants dans les développements formels. Celles-ci incluent :
  - La gestion d'équations de la forme $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ en instanciant l'inconnu par une substitution levée ( $?s \mapsto s[\Uparrow\sigma]$ ).
  - La gestion de cas impliquant des substitutions d'identité ou des structures de variables spécifiques.
- Après l'application des substitutions, la tactique re-normalise l'hypothèse. Le succès est déterminé si le but et l'hypothèse deviennent syntaxiquement égaux.

La tactique a été généralisée pour supporter l'intégralité du langage d'entrée du compilateur Autosubst, incluant de multiples sortes mutuellement inductives, des substitutions de vecteurs et des renommages de premier ordre.

Contributions Clés

Introduction de as_apply : Une tactique heuristique conçue pour remplacer apply/eapply dans les développements basés sur Autosubst, permettant l'appariement modulo l'équivalence $\sigma$ en présence d'hypothèses.
Généralisation : Extension de la logique d'appariement pour couvrir toute la syntaxe supportée par Autosubst, y compris les lieurs complexes et les opérations de renommage.
Évaluation Empirique : Application de la tactique à des benchmarks standards, spécifiquement les défis POPLMark et POPLMark Reloaded.

Résultats
Les auteurs ont évalué as_apply sur les solutions des défis POPLMark (642 lignes) et POPLMark Reloaded (683 lignes).

Fréquence d'utilisation : La tactique a été utilisée 15 fois dans la solution POPLMark B et 10 fois dans la solution POPLMark Reloaded.
Efficacité : Dans tous les cas testés, as_apply a résolu avec succès les buts visés.
Simplification : L'utilisation de la tactique a éliminé le besoin de formulations de règles indirectes, de lemmes auxiliaires et de transformations manuelles de buts qui caractérisaient les solutions précédentes.
Limitations : Les auteurs reconnaissent que as_apply n'est pas $\sigma$ -complète et n'est pas un décideur. Comme l'appariement $\sigma$ peut avoir plusieurs solutions, la nature heuristique de la tactique signifie qu'elle pourrait théoriquement sélectionner une solution incorrecte lorsqu'une solution correcte existe, bien qu'aucun échec de ce type n'ait été observé dans les études de cas.

Signification et Revendications
Le papier affirme que bien que le problème théorique de l'appariement $\sigma$ soit intrinsèquement difficile (solutions non uniques, indécidabilité dans le $\lambda\sigma$ complet), une approche pragmatique et heuristique peut récupérer un haut niveau d'automatisation en pratique. La signification réside dans la réduction de la charge manuelle imposée aux utilisateurs travaillant avec la syntaxe de de Bruijn, leur permettant d'énoncer des règles de typage et des lemmes dans leurs formes directes et naturelles plutôt que dans des formes indirectes adaptées aux limitations du moteur d'unification de l'assistant de preuve.

Les auteurs restent modestes quant à l'état actuel du travail, le qualifiant de "Travail en cours". Ils notent que la tactique actuelle repose sur des heuristiques en raison du potentiel de solutions infinies ou multiples. Les travaux futurs visent à identifier le plus grand fragment $\sigma'$ pour lequel un critère d'unicité tient, menant potentiellement à une tactique d'appariement avec des garanties prouvées.

Articles similaires