Cette page ne fonctionne pas sur votre navigateur. Utilisez FireFox, Opéra, Chrome, Safari...
Options de l'unificateur
Options des graphes
Le bouton fige les dessins en images svg pour pouvoir les télécharger.
Entrez une clause et évaluez
Une clause est :
- une expression gauche, le signe « = », une expression droite.
Une expression est soit :
- un terme
- une variable
Un terme est soit :
- un prédicat
- une constante
Une constante est un identificateur commençant par une minuscule.
Les identificateurs commencent par une lettre et sont éventuellement suivis par des lettres et chiffres ou le blanc souligné « _ ».
Une variable est un identificateur commençant par une majuscule a la Prolog.
Un prédicat est un identificateur formé comme une constante, et suivi par une liste non vide d’arguments entre parenthèses et séparés par des virgules.
Pour créer des termes partagés et/ou cycliques, on peut étiqueter un prédicat
en le faisant précéder par un entier suivit de ":".
Pour réutiliser les prédicats étiquetés ailleurs dans la clause, il faut
le caractère "@" suivit par l'entier correspondant.
L'utilisation d'une étiquette peut précéder sa définition, mais il doit exister une définition.
Par exemple :
- un partage :
2:f(@1, Y) = f(1:f(@2, a), a)
- un graphe d'unification cyclique en résultat :
1:f(@2) = 2:f(@1)
- une boucle
1:f(X) = f(f(f(f(f(@1)))))
- à comparer avec :
1:f(@1) = f(f(f(f(f(X)))))
- simple :
2:f(@2, X) = f(X, @2)
- Exemple de Daniel Goossens
1:f(@1,f(X, f(X,X)))=2:f(f(Y, Y),@2)
Les arguments sont des expressions.
Les éléments peuvent être séparés par des espaces et des retours à la ligne.
Par Vincent Lesbros - 2020/05/03
Pour unifier les deux expressions données par une clause, on construit un graphe d’unification dont les nœuds sont les paires (ou les couples) {gauche, droite} formés par l’assemblage des nœuds rencontrés à gauche et à droite dans un parcours simultané des deux expressions.
Au cours de la construction de ce graphe, les variables du contexte sont affectées si elle sont libres et confrontées à une valeur différente d’elle-même.
Lors de la création d’un nœud {g , d} les côtés gauche et droite sont déréférencés :
si g, (resp d), est une variable liée, on calcule g1, (resp d1), comme étant la dernière valeur n’étant pas une variable liée. Un terme reste un terme, une variable libre reste elle-même, une variable liée est remplacée par sa valeur, et récursivement. Dans cette page, des nœuds de déréférencement sont créés explicitement pour le visualiser.
On analyse alors la paire {g1 , d1} pour trouver ses fils dans le graphe d’unification.
Note : les exemples de Wikipédia comme f(g(X),X) = f(Y,a) peuvent être copier-collés directement.
Le parseur est écrit avec la bibliothèque PEG.js Parser Generator for JavaScript acessible à l'adresse : https://pegjs.org