Quel est l'algorithme "unificateur le plus général" optimal?

Question

La question

Quel est l'algorithme MGU le plus efficace? Quelle est sa complexité temporelle? Est-il assez simple de décrire comme une réponse de dépassement de pile?

J'ai essayé de trouver la réponse sur Google, mais continuez à trouver des fichiers .PDF privés auxquels je ne peux accéder que via un abonnement ACM.

J'ai trouvé une discussion SICP: here

Explication de ce qu'est un « algorithme d'unification la plus générale » est: Prenez deux arbres d'expression contenant « variables libres » et « constantes » ... par exemple Ensuite, l'algorithme Most Unifier général renvoie l'ensemble le plus général de liaisons qui rend les deux expressions équivalentes.

à savoir

 
mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5 

Par "plus général", vous pouvez lier au lieu (x = 1) et (z = 1) et cela également e1 et e2 équivalent, mais il serait plus spécifique.

L'article SICP semble impliquer qu'il est raisonnablement coûteux.

Pour info, la raison pour laquelle je demande est parce que je sais que l'inférence de type implique également cet algorithme "d'unification" et je voudrais le comprendre.

Answer 1

L'algorithme simple qui est utilisé en pratique (par exemple dans Prolog) est exponentiel pour les cas pathologiques. Il existe un algorithme théoriquement plus efficace par Martelli et Montanari (IIRC il est linéaire), mais il est beaucoup plus lent pour les cas simples qui se produisent dans la pratique, donc il n'est pas beaucoup utilisé.

Answer 2

Baader and Snyder publié plusieurs algorithmes d'unification, à la fois pour l'unification syntaxique et l'unification équationnelle. Ils déclarent que leur troisième algorithme d'unification syntaxique (section 2.3) s'exécute dans O (n alpha (n)) où alpha (n) est la fonction inverse d'Ackermann - dans la pratique, elle équivaut à une petite constante.