Algorithme de Robinson pour PGCU

Fermé
Leunamme - Modifié le 6 juil. 2023 à 16:01
mamiemando Messages postés 33539 Date d'inscription jeudi 12 mai 2005 Statut Modérateur Dernière intervention 19 février 2025 - 6 juil. 2023 à 19:13

Bonjour,

Je cherche à réaliser un TP sur l'algorithme de Robinson où il s'agit de trouver le plus grand commun unificateur entre 2 termes. Mais j'ai du mal à démarrer ????. 

J'ai besoin d'aide, s'il vous plaît...

Si vous avez besoin de plus d'indications, posez les et je vous les fournirai. 

2 réponses

yg_be Messages postés 23476 Date d'inscription lundi 9 juin 2008 Statut Contributeur Dernière intervention 20 février 2025 Ambassadeur 1 568
2 juil. 2023 à 10:04

bonjour,

le point de départ, c'est de comprendre ce que fait l'algorithme.

quel est le contexte du TP?

0
mamiemando Messages postés 33539 Date d'inscription jeudi 12 mai 2005 Statut Modérateur Dernière intervention 19 février 2025 7 828
Modifié le 6 juil. 2023 à 20:40

Bonjour,

J'ai regardé en diagonal cet article wikipedia pour tenter de comprendre l'algorithme de Robinson.

En particulier cet exemple, on tente d'unifier les termes t1 = f(x, g(x, x)) et t2 = f(h(y), g(z, h(1))). En posons x = h(1), y = 1 et z = h(1) on obtient bien t1 = t2 = g(h(1), g(h(1), h(1)))

Par contre, je n'ai pas compris la description wikipedia de l'algorithme (ni Robinson, ni Cordin & Bidoit) donc si tu peux nous en dire un peu plus ce serait pas mal.

Il faudrait également nous indiquer quel langage de programmation tu comptes utiliser. Par exemple, Prolog étant conçu pour faire de la programmation logique, il est sans doute plus indiqué (n'en ayant jamais fait, je ne peux pas être catégorique). Si tu pars sur du python, le module prolog est sans doute bienvenu pour les même raisons.

Voici une compréhension plus personnelle et qui n'engage que moi.

Dans le cas général, je pense que tu auras besoin d'une classe de DAG.

Toute variable (dans mon exemple : x, y, z) et tout terme (dans mon exemple : t1, t2) est représenté par un DAG. Chaque nœud impliqué dans un DAG est étiqueté soit par

  • une valeur (dans mon exemple : 1),
  • une fonction (dans mon exemple : g, h) 
  • une variable (dans mon exemple : x, y, z).

L'expression d'une valeur ou d'une fonction est elle-même. Par contre l'expression d'une variable dépend, selon qu'on ait ou non décidé d'attribuer une expression ou non à une variable (les flèches bleues dans l'exemple wikipedia).

Quoi qu'il en soit, on peut à tout moment reconstruire l'expression d'un DAG : il suffit de faire un parcours en largeur d'abord dudit DAG en partant de sa racine et en traitant les enfants d'un nœuds de gauche à droite (cela s'écrit très facilement avec une fonction récursive).

Si au cours du parcours, le nœud en cours de traitement est une variable, soit on lui a assigné une valeur (flèche bleue) et son expression est celle du DAG pointé par cette assignation, soit on ne lui a rien assigné et sa valeur est son propre nom.

Maintenant que l'on sait convertir n'importe quel DAG/variable/terme sous forme d'expression, on peut facilement vérifier si deux termes sont unifiés ou non (étant donné un ensemble -éventuellement vide- d'assignations).

Soit dit en passant, on ne veut pas forcément faire une assignation (et je suspecte que c'est ce que tu sous-entend par "plus grand unificateur"). Prenons l'exemple t1 = f(x, y, 1) et t2 = f(x, z, 1) : on pourrait très bien choisir :

  • y = z = 1 : terme unifié : f(1, 1, 1)
  • y =  1 : terme unifié : f(x, 1, 1)
  • x = y : terme unifié : f(x, x, 1)

De cet exemple en jouet, on voit que pas d'assignation (y = y) est mieux qu'assigner une variable à une autre variable (y = x), qui est mieux qu'assigner une valeur à une variable (y = 1).

Ensuite, regardons quelles assignations sont possibles dans les faits. Une variable y assignée ne doit pas dépendre d'elle-même (y compris si y dépend d'une variable x qui dépend à terme de y). Ainsi les seuls cas autorisés sont y = y (pas d'assignation) ou y = x (substitution). Cela limite de facto l'ensemble des assignations possibles. De part ces dépendances, je suspecte qu'on a intérêt à commencer par les variables qui ont le moins de dépendances possible et remonter progressivement dans les DAG des termes à unifier. À chaque fois qu'on assigne une valeur, il faut corriger l'ensemble des assignations possibles, puis recalculer l'expression des deux termes à unifier pour voir s'ils le sont ou non. Je suppose que c'est ce qui est évoqué dans cette section.

Voici une implémentation simpliste en python pour démarrer.

class Node:
    def __init__(self, label: str):
        self.label = label
    def __str__(self) -> str:
        return str(self.label)

class NodeValue(Node):
    pass

class NodeVariable(Node):
    def __init__(self, label: str, assignment: Node = None):
        super().__init__(label)
        self.assignment = assignment
    def assign(self, node: Node) -> bool:
        self.assignment = node
        return True
    def __str__(self) -> str:
        return (
            str(self.assignment) if self.assignment
            else super().__str__()
        )

class NodeFunction(NodeVariable):
    def __init__(self, label: str):
        super().__init__(label)
        self.children = list()
    def append_child(self, node: Node):
        self.children.append(node)
    def assign(self, node: Node) -> bool:
        if self.label == node.label:
            self.assignment = node
            return True
        return False
    def __str__(self) -> str:
        return (
            str(self.assignment) if self.assignment
            else (
                super().__str__()
                + "("
                + ", ".join(str(child) for child in self.children)
                + ")"
            )
        )

class Dag:
    def __init__(self):
        self.root = None
        self.nodes = list()
        self.map_variable_node = dict()
    def add_vertex(self, node) -> Node:
        self.nodes.append(node)
        return node
    def add_function(self, name) -> Node:
        node = NodeFunction(name)
        return self.add_vertex(node)
    def add_value(self, value) -> Node:
        node = NodeValue(value)
        return self.add_vertex(node)
    def add_variable(self, name) -> Node:
        node = self.map_variable_node.get(name)
        if node is not None:
            return node
        node = NodeVariable(name)
        return self.add_vertex(node)
    def set_root(self, node: Node):
        self.root = node
    def assign(self, name, assignment: Node) -> bool:
        node = self.map_variable_node.get(name)
        if node is not None:
            node.assign(assignment)
            return True
        return False
    def add_edge(self, node1: Node, node2: Node) -> bool:
        try:
            node1.append_child(node)
            return True
        except:
            return False
    def __str__(self) -> str:
        return str(self.root)

# Exemple https://fr.wikipedia.org/wiki/Unification#/media/Fichier:Unification_dag_exemple.svg

def make_t1() -> Dag:
    # f(x, g(x, x))
    t1 = Dag()
    f1 = t1.add_function("f")
    g1 = t1.add_function("g")
    x1 = t1.add_variable("x")
    t1.set_root(f1)
    f1.append_child(x1)
    f1.append_child(g1)
    g1.append_child(x1)
    g1.append_child(x1)
    return t1

def make_t2() -> Dag:
    # f(h(y), g(z, h(1)))
    t2 = Dag()
    f2 = t2.add_function("f")
    g2 = t2.add_function("g")
    h2 = t2.add_function("h")
    y2 = t2.add_variable("y")
    z2 = t2.add_variable("z")
    t2.set_root(f2)
    f2.append_child(h2)
    f2.append_child(g2)
    h2.append_child(y2)
    g2.append_child(z2)
    h2_ = t2.add_function("h")
    one2 = t2.add_value(1)
    g2.append_child(h2_)
    h2_.append_child(one2)
    return t2

t1 = make_t1()
t2 = make_t2()
print("t1 =", t1)
print("t2 =", t2)
[f2, g2, h2, y2, z2, h2_, one2] = t2.nodes
[f1, g1, x1] = t1.nodes
assert f1.assign(f2)
assert g1.assign(g2)
assert x1.assign(h2)
assert y2.assign(one2)
assert z2.assign(h2)
assert h2_.assign(h2)
print("t1 =", t1)
print("t2 =", t2)

Dans ce code, je rejoue cet exemple :

  • t1 désigne le premier terme (graphe de gauche)
    • je note f1 le nœud étiqueté par f
    • je note g1 le nœud étiqueté par g
    • je note x1 le nœud étiqueté par x
  • t2 désigne le second terme (graphe de droite)
    • je note f2 le nœud étiqueté par f
    • je note g2 le nœud étiqueté par g
    • je note h2 le nœud étiqueté par h le plus à gauche
    • je note h2_ le nœud étiqueté par h le plus à droite
    • je note y2 le nœud étiqueté par y
    • je note z2 le nœud étiqueté par z

Au début j'affiche les expressions de t1 et de t2 sans assignation :

print("t1 =", t1)
print("t2 =", t2)

... ce qui donne :

t1 = f(x, g(x, x))
t2 = f(h(y), g(z, h(1)))

Puis je fais l'assignation et les ré-affiche:

[f2, g2, h2, y2, z2, h2_, one2] = t2.nodes
[f1, g1, x1] = t1.nodes
assert f1.assign(f2)
assert g1.assign(g2)
assert x1.assign(h2)
assert y2.assign(one2)
assert z2.assign(h2)
assert h2_.assign(h2)

... ce qui donne :

t1 = f(h(1), g(h(1), h(1)))
t2 = f(h(1), g(h(1), h(1)))

Une manière naïve (et un peu sale) de vérifier si deux termes sont unifiés consiste donc à comparer ces deux chaînes de caractères. C'est un peu sale car il ne faut pas qu'il y ait de collisions sur les noms de labels, mais si jamais ça arrive il suffirait d'adapter les méthodes __str__ (par exemple en utilisant les adresses mémoire des nœuds, en python cela se fait avec la fonction id).

Pour cela, c'est très simple, on adapte simplement la méthode Node.__str__ comme suit :

class Node:
    def __init__(self, label: str):
        self.label = label
    def __str__(self) -> str:
        return hex(id(self)) #str(self.label)

... et à l'exécution on aura bien deux chaînes ne comportant aucun risque d'ambiguïté.

Ce faisant

t1 = f(h(1), g(h(1), h(1)))
t2 = f(h(1), g(h(1), h(1)))

... devient : 

t1 = 0x7fc8f65fb110(0x7fc8f65fb350(0x7fc8f65fb510), 0x7fc8f65fb2d0(0x7fc8f65fb350(0x7fc8f65fb510), 0x7fc8f65fb350(0x7fc8f65fb510)))
t2 = 0x7fc8f65fb110(0x7fc8f65fb350(0x7fc8f65fb510), 0x7fc8f65fb2d0(0x7fc8f65fb350(0x7fc8f65fb510), 0x7fc8f65fb350(0x7fc8f65fb510)))

... et l'égalité de ces deux chaînes suffit à montrer que les deux termes t1 et t2 sont unifiées.

La seule difficulté revient alors à trouver la bonne assignation. Dans le cas général les nœuds variable et fonction doivent d'un terme être assignés à un nœud compatible du même DAG ou de l'autre DAG (ce qu'on peut vérifier avec la valeur retournée par la méthode assign). Dans mon exemple toutes les assignations étaient valides et donc les assertions se sont passées sans problèmes.

Reste cependant à implémenter l'algorithme de Robinson (ou de Corbin et Bidoit), mais pour que je t'en dise plus, il faudrait que je comprenne lesdits algorithmes...

Bonne chance

0