💻 computer science

Non-Termination of Logic Programs Using Patterns

Ce document adapte une approche de réécriture de termes pour la détection de la non-terminaison sans boucle à la programmation logique en introduisant une nouvelle technique de déploiement qui génère des motifs représentant des ensembles infinis de séquences de réécriture finies, laquelle est évaluée expérimentalement à l'aide de l'outil NTI.

Auteurs originaux : Etienne Payet

Publié 2026-08-10

📖 3 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Etienne Payet

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 regardez un robot essayer de résoudre un puzzle. Parfois, le robot s'enferme dans une boucle : il fait l'étape A, puis l'étape B, puis l'étape A à nouveau, encore et encore, pour toujours. C'est comme un hamster qui court dans une roue ; il bouge, mais il n'avance nulle part. Dans le monde de l'informatique, plus précisément dans un domaine appelé la programmation logique, ces robots sont des programmes qui tentent de répondre à des questions en suivant un ensemble de règles. Si un programme s'enferme dans une boucle, il ne termine jamais son travail, ce qui est un bogue que les programmeurs veulent détecter.

Mais il existe un type de problème plus complexe. Parfois, un programme ne s'enferme pas dans un cercle répétitif et net. Au lieu de cela, il fait un pas, puis un pas légèrement différent, puis un pas qui ressemble presque au précédent mais qui ne l'est pas tout à fait, et continue ainsi indéfiniment sans jamais répéter exactement le même motif. C'est comme un danseur qui ne répète jamais un mouvement mais qui ne s'arrête jamais de danser. C'est ce qu'on appelle la non-terminaison non-bouclante. Il est incroyablement difficile de la repérer car il n'y a pas de « boucle » évidente à pointer du doigt. Détecter ces séquences infinies et non répétitives est un défi majeur pour les informaticiens qui veulent prouver qu'un programme finira par s'arrêter ou trouver le point de départ spécifique qui le fait tourner indéfiniment.

Cet article introduit une nouvelle façon astucieuse de capturer ces boucles infinies et insaisissables qui ne se répètent pas. L'auteur, Etienne Payet, a construit un outil appelé NTI qui agit comme un détective surpuissant pour les programmes logiques. Au lieu d'essayer de regarder le programme s'exécuter étape par étape (ce qui prendrait une éternité), l'outil utilise une technique appelée dépliage (unfolding). Pensez au dépliage comme si vous aplatissiez une grue en origami complexe pour voir le motif des plis en dessous. En aplatissant les règles du programme, l'outil crée des « motifs » — des schémas abstraits qui décrivent non pas un seul chemin spécifique, mais une famille infinie de chemins possibles que le programme pourrait emprunter.

La découverte principale de cet article est qu'en utilisant ces schémas, plus précisément une version simplifiée appelée « motifs simples », l'outil peut prouver mathématiquement qu'un programme tournera indéfiniment sans jamais s'enfermer dans une boucle simple. L'auteur a testé cela sur 41 programmes logiques différents qui étaient connus pour être difficiles. Leur outil a réussi à identifier les chemins infinis et non répétitifs dans beaucoup d'entre eux, y compris quatre programmes qu'aucun autre outil existant n'avait été capable de prouver comme étant non-terminants auparavant. Cependant, l'article est honnête sur ses limites : l'outil n'a pas résolu tous les cas, et pour certains programmes, il s'est bloqué ou a expiré après 10 secondes de fonctionnement. L'auteur suggère que, bien que leur méthode soit un nouvel ajout puissant à la panoplie du détective, elle n'est pas encore une baguette magique qui résout tous les mystères. Ils prévoient de rendre l'outil plus intelligent à l'avenir, avec l'espoir de capturer encore plus de ces boucles infinies et non répétitives si complexes.

Résumé Technique : Non-terminaison des programmes logiques à l'aide de motifs (Patterns)

Énoncé du Problème
Cet article traite de la détection automatique de la non-terminaison dans les programmes logiques (LP). Alors que la recherche existante se concentre largement sur la détection de boucles (des séquences de réécriture finies qui peuvent être répétées indéfiniment), ce travail cible la non-terminaison sans boucle. Il s'agit de séquences de réécriture infinies qui ne contiennent aucune boucle, ce qui les rend intrinsèquement non périodiques et difficiles à détecter. L'auteur note que de telles séquences peuvent provenir de programmes logiques simples, pourtant les méthodes standards de détection de boucles échouent souvent à les identifier. La motivation est double : théorique (étudier des formes remarquables de séquences infinies) et pratique (aider les programmeurs à identifier les requêtes qui tournent indéfiniment).

Méthodologie
L'auteur adapte une approche initialement introduite pour la réécriture de termes par Emmes et al. (2012) au domaine de la programmation logique. La méthodologie centrale consiste à définir une nouvelle technique de déploiement (unfolding) qui génère des « motifs » décrivant des ensembles potentiellement infinis de séquences de réécriture finies.

Définitions des Motifs (Patterns) :
- Substitutions de Motifs : Définies comme des paires $\theta = (\sigma, \mu)$ , notées $\sigma \star \mu$ , décrivant un ensemble de substitutions $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$ .
- Termes de Motifs : Des paires $(s, \theta)$ décrivant l'ensemble $\{s\theta(n) \mid n \in \mathbb{N}\}$ .
- Règles de Motifs : Des paires de termes de motifs $(p, q)$ décrivant un ensemble de règles binaires $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$ .
Correction et Déploiement :
- Une règle de motif est jugée correcte par rapport à un programme $P$ si l'ensemble de règles qu'elle décrit est un sous-ensemble du déploiement binaire de $P$ ($binunf(P)$).
- L'auteur introduit un nouvel opérateur de déploiement $T^\pi_{P,B}$ qui calcule des règles de motifs à partir d'un programme $P$ et d'un ensemble de base de règles de motifs correctes $B$ . Cet opérateur utilise un algorithme d'unification pour les termes de motifs afin de combiner les règles, effectuant ainsi un déploiement du programme plus rapidement que le déploiement binaire traditionnel en capturant des sous-ensembles infinis de $binunf(P)$ via des représentations finies.
Motifs Simples et Unification :
- Pour rendre l'approche automatisable, l'auteur restreint le domaine aux termes de motifs simples, où les substitutions suivent une structure spécifique impliquant des contextes unaires.
- Un algorithme d'unification est fourni pour ces termes simples. Il projette les termes de motifs simples vers des termes sur une signature spécialisée $\Upsilon$ (utilisant des symboles unaires $c_{a,b}$ pour représenter les plongements répétés) et applique des algorithmes d'unification classiques (par exemple, Robinson, Martelli-Montanari).
- L'algorithme est prouvé partiellement correct : s'il se termine avec succès, il produit un unificateur le plus général (mgu) pour les séquences de motifs d'entrée.
Critères de Non-Terminaison :
- Critère Général (Théorème 3) : Adapté d'Emmes et al., il stipule que si le déploiement de motifs contient une règle de la forme $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ où $\sigma'$ commute avec $\sigma$ et $\mu$ , alors une chaîne infinie existe.
- Critère Spécial (Théorème 5) : Une condition plus facilement vérifiable pour les règles de motifs spéciales (un sous-ensemble des règles simples). Si une telle règle existe dans le déploiement, l'article prouve l'existence d'une chaîne infinie partant d'instances spécifiques du côté gauche de la règle.

Contributions Clés
L'article présente quatre contributions principales :

Nouvelle Technique de Déploiement : Une méthode pour produire des règles de motifs correctes pour la programmation logique, offrant une présentation plus compacte que les neuf règles d'inférence utilisées en réécriture de termes et éliminant le besoin de stratégies d'application complexes.
Termes de Motifs Simples et Unification : La définition d'une forme restreinte de termes de motifs (« simples ») et d'un algorithme d'unification correspondant dont la correction est prouvée.
Condition de Suffisance Automatisable : Une condition facilement vérifiable (Théorème 5) pour détecter la non-terminaison sans boucle des motifs simples.
Implémentation (NTI) : L'implémentation de cette approche dans un outil nommé NTI.

Résultats Expérimentaux
L'auteur a évalué NTI sur 41 programmes logiques dérivés de Systèmes de Réécriture de Termes (TRS) non-terminants sans boucle issus de la base de données de problèmes de terminaison (TPDB).

Succès : L'outil a prouvé avec succès la non-terminaison pour 36 des 41 programmes. Notamment, il a réussi sur 4 programmes (marqués par un † dans les tableaux) qui n'avaient été prouvés non-terminants par aucun autre analyseur de TRS de la Compétition Internationale de Terminaison jusqu'en 2024.
Échec : L'approche a échoué sur 5 programmes, principalement en raison de l'incomplétude de l'algorithme d'unification lors de l'utilisation du « choix naturel » pour les représentants de termes (comme discuté dans l'Exemple 12) ou de la restriction aux motifs simples (Exemple 9).
Performance : Les temps d'exécution étaient généralement faibles (moins de 300 ms pour les cas réussis), bien que certains cas complexes aient entraîné des dépassements de délai (timeouts).

Signification et Revendications
L'auteur affirme que leur approche est le seul outil participant à la Compétition Internationale de Terminaison capable de prouver la non-terminaison de programmes logiques. Il note que bien qu'une autre approche par Payet (2024) existe pour prouver la non-terminaison sans boucle, celle-ci traite d'une classe différente de non-bouclage et est incapable de prouver la non-terminaison des programmes spécifiques testés dans cet article (Tableaux 1 et 2). Inversement, l'approche de Payet (2024) peut prouver la non-terminaison de programmes là où cette méthode échoue. Ainsi, les deux approches sont présentées comme complémentaires.

L'article conclut avec modestie, reconnaissant que l'algorithme d'unification est actuellement incomplet et que la restriction aux motifs simples limite la portée (par exemple, l'échec sur des programmes nécessitant des contextes à 1-variable). Des travaux futurs sont prévus pour traiter la complétude, étendre le déploiement initial (Prop. 2) et adapter l'approche aux TRS pour une comparaison directe avec Emmes et al. (2012).

Articles similaires