MaudeTypedLog: A Typed Interpreter for Prolog in Maude

Imaginez que vous construisez un château de cartes. Dans le monde de l'informatique, il existe un langage très populaire appelé Prolog qui agit comme un maître bâtisseur, mais il possède un carnet de règles très décontracté : il ne se soucie pas si vous essayez de poser une brique lourde sur une tente de papier délicate. Il essaie simplement de les faire s'emboîter. Si la brique est trop lourde, toute la structure pourrait s'effondrer plus tard, ou le bâtisseur pourrait simplement dire : « Eh bien, ça n'a pas marché », sans vous dire pourquoi cela a échoué. C'est parce que Prolog est traditionnellement « non typé », ce qui signifie qu'il ne vérifie pas si les pièces que vous essayez de connecter sont réellement de la bonne forme ou du bon matériau avant de commencer à construire.

Cependant, parfois, le bâtisseur sait mieux. Si vous lui demandez de mélanger une liste de nombres avec un nombre unique d'une manière spécifique, il pourrait lever les mains et dire : « Erreur ! ». Mais cela n'arrive que lorsque la construction a déjà commencé à vaciller. Pendant des années, les informaticiens ont essayé de donner un meilleur carnet de règles à Prolog — un « système de types » — qui vérifie les matériaux avant que la construction ne commence. Le problème est que la plupart de ces tentatives sont soit trop compliquées pour être utilisées par les humains, soit si vagues qu'elles ratent les erreurs évidentes. C'est comme avoir un inspecteur de sécurité qui ne vérifie le toit que si vous le lui demandez spécifiquement, ou un inspecteur qui dit « peut-être que les briques sont correctes » alors qu'elles sont manifestement faites de gelée.

C'est ici qu'un nouvel outil intervient, conçu par les chercheurs Enrique Gallifa-Tronch, João Barbosa et Santiago Escobar. Ils ont décidé d'arrêter d'essayer de réparer directement Prolog et ont plutôt construit un tout nouvel interprète super strict appelé MaudeTypedLog. Considérez cela comme le fait de prendre les plans de Prolog et de les faire passer par un nouveau moteur de simulation magique et ultra-rapide appelé Maude. Ce moteur ne se contente pas d'essayer de faire s'emboîter les pièces ; il vérifie si les pièces sont même autorisées à se toucher en premier lieu. Si vous essayez de coller un « nombre » à un « mot », la machine s'arrête immédiatement et crie : « Erreur de type ! » avant que le moindre dommage ne soit causé.

L'article présente cet interprète, le premier du genre à utiliser un système de logique spécifique à trois voies. Au lieu de simplement dire « Oui » (cela fonctionne) ou « Non » (cela ne fonctionne pas), ce système peut dire « Faux » (c'est une erreur de type). Les auteurs n'ont pas seulement deviné que cela fonctionnerait ; ils ont écrit le code, construit l'interprète et testé l'outil avec plusieurs programmes logiques. Ils ont montré que leur outil peut identifier avec succès des erreurs tant dans les instructions (le programme) que dans les questions (les requêtes) que d'autres outils pourraient manquer. Ils ont également démontré qu'ils peuvent pointer précisément la ligne de code spécifique qui cause le problème, agissant comme un détective qui ne se contente pas de dire « un crime a eu lieu », mais qui désigne le suspect exact. Bien qu'ils admettent que leur outil n'est pas encore parfait et nécessite plus de tests avec des fonctions mathématiques complexes, leurs simulations prouvent que cette nouvelle façon stricole de vérifier les programmes Prolog est une méthode viable et puissante pour détecter les erreurs précocement.

L'histoire de MaudeTypedLog

Le Problème : La « Colle » qui ne vérifie rien
Prolog est un langage utilisé pour résoudre des énigmes et des problèmes de logique. Il fonctionne en prenant une liste de faits et de règles et en essayant de les coller ensemble pour répondre à une question. Traditionnellement, Prolog est « non typé ». Imaginez que vous jouez à un jeu où vous devez assortir des chaussettes. Dans Prolog, vous pouvez essayer d'associer une chaussette rouge avec une chaussure bleue, et le jeu continue d'essayer jusqu'à ce qu'il abandonne. Il ne hurle pas : « Hé, ce ne sont même pas les mêmes sortes d'objets ! » avant la fin, et même à ce moment-là, il peut simplement dire « Pas de correspondance » sans expliquer que la chaussure était le problème.

Les auteurs soutiennent que cela est dangereux. Parfois, un programme peut dire « Non » parce que la réponse est véritablement « Non » (comme 2 n'est pas dans la liste [1, 3]), mais d'autres fois, il dit « Non » parce que vous avez tenté de faire quelque chose d'impossible (comme mettre un nombre à l'intérieur d'une liste de mots). Prolog traite les deux « Non » de la même manière, ce qui est déroutant.

La Solution : Un feu de signalisation à trois voies
Les chercheurs ont construit MaudeTypedLog, un interprète qui exécute des programmes Prolog mais ajoute une « Vérification de Type » stricte à chaque étape. Au lieu d'un simple feu de signalisation avec seulement Vert (Circulez) et Rouge (Arrêt), ce système possède un troisième feu : Jaune (Faux/Erreur).

• Vert (Vrai) : Les pièces s'ajustent, les types correspondent et la logique fonctionne.
• Rouge (Faux) : Les pièces correspondent aux types, mais la logique ne fonctionne pas (ex: 2 n'est pas dans la liste).
• Jaune (Faux/Erreur) : Les pièces ne peuvent pas s'ajuster car elles sont du mauvais type (ex: essayer d'ajouter un mot à un nombre).

Ce feu « Jaune » est l'innovation clé. Il permet au système de s'arrêter immédiatement lorsqu'il voit une erreur de type, plutôt que de laisser le programme planter plus tard ou de donner une réponse confuse.

Comment ils l'ont construit
Pour réaliser cela, les auteurs ont utilisé un outil puissant appelé Maude. Maude est comme un moteur de simulation surpuissant capable de réécrire des règles très rapidement. Les auteurs ont pris les règles de Prolog et les ont réécrites à l'intérieur de Maude.

1. L'algorithme d'Unification Typée : C'est le moteur central. Dans le Prolog normal, l'« unification » est le processus consistant à faire en sorte que deux choses se ressemblent. Dans MaudeTypedLog, ils ont créé un algorithme d'« Unification Typée ». Avant d'essayer de coller deux choses ensemble, il vérifie leurs « types ». Si les types ne correspondent pas, il ne se contente pas d'échouer ; il renvoie un signal spécifique de « Faux/Erreur ».
2. La Résolution TSLD : C'est le nom sophistiqué de la méthode qu'ils utilisent pour résoudre les énigmes. C'est une version améliorée de la méthode de résolution standard de Prolog (résolution SLD). Le « T » signifie « Typée ». Elle construit un arbre de toutes les manières possibles de résoudre un problème. Si une branche de l'arbre rencontre un signal « Faux/Erreur », cette branche est coupée immédiatement, et le système sait exactement quelle règle a causé l'erreur.

Ce qu'ils ont trouvé
Les auteurs ont testé leur nouvel interprète avec plusieurs exemples.

• Exemple 1 : Ils ont créé un programme où une règle appelée r tente de trouver un nombre qui est à la fois dans une liste de nombres et dans une liste de lettres. Le système a correctement identifié que si certains chemins fonctionnaient (trouver le nombre 1), d'autres chemins heurtaient un signal « Faux/Erreur » car ils tentaient de mélanger des nombres et des lettres.
• Exemple 2 : Ils ont créé un programme avec une erreur de type cachée. Une règle tentait de mettre une lettre dans un emplacement destiné à un nombre. Lorsqu'ils ont exécuté la commande « check », MaudeTypedLog ne s'est pas contenté de dire que le programme avait échoué ; il a pointé directement la règle spécifique (clause 3) qui était la coupable.

Les résultats ont montré que l'outil fonctionne exactement comme la théorie le prédisait. Il peut détecter des erreurs de type tant dans le programme lui-même que dans les questions posées au programme.

Ce qu'il ne peut pas encore faire
Les auteurs sont honnêtes quant aux limites de leur travail actuel. Leur outil est un prototype. Il ne gère pas encore toutes les fonctions mathématiques complexes que possède habituellement Prolog (comme calculer des racines carrées ou ajouter des nombres dynamiquement). Ils n'ont pas non plus testé l'outil sur les vastes bibliothèques de règles utilisées par les programmes Prolog professionnels. Ils suggèrent qu'à l'avenir, ils devront apprendre à l'outil comment gérer ces fonctionnalités mathématiques avancées et des structures de données plus complexes comme les arbres.

Pourquoi cela importe
Cet article ne prétend pas avoir résolu tous les problèmes de l'informatique. Au lieu de cela, il offre une nouvelle façon plus claire d'aborder la programmation logique. En utilisant Maude pour créer un interprète typé strict, les auteurs ont démontré qu'il est possible de détecter les erreurs tôt et de localiser précisément où elles se produisent. C'est comme donner à un bâtisseur un niveau laser qui non seulement lui indique qu'un mur est de travers, mais lui indique aussi exactement quelle brique est de la mauvaise forme, afin qu'il puisse la corriger avant que la maison ne s'effondre.