2009-05-13 7 views
10

Die FrageWas ist der optimale "allgemeinste Unifier" -Algorithmus?

Was ist der effizienteste MGU-Algorithmus? Was ist seine zeitliche Komplexität? Ist es einfach genug, um eine Stapelüberlaufantwort zu beschreiben?

Ich habe versucht, die Antwort auf Google zu finden, finde aber weiterhin private .PDFs, auf die ich nur über ein ACM-Abonnement zugreifen kann.

fand ich eine Diskussion in SICP: here

Erklärung dessen, was ein „allgemeinste Unifikationsalgorithmus“ ist: zwei Ausdrucksbäume Take „freie Variablen“ und „Konstanten“ enthält ... z.B.

 
e1 = (+ x? (* y? 3) 5) 
e2 = (+ z? q? r?) 

Dann kehrt die allgemeinste Unifier Algorithmus, um die allgemeinste Satz von Bindungen, die die zwei Ausdrücke äquivalent macht.

heißt

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

Mit "allgemeinsten", könnte man stattdessen binden (x = 1) und (z = 1) und das wäre auch e1 und e2 äquivalent machen, aber es wäre genauer sein.

Der SICP-Artikel scheint zu implizieren, dass es ziemlich teuer ist.

Für Informationen, der Grund, den ich frage, ist, weil ich weiß, dass Typschlussfolgerung auch diesen "Vereinigung" -Algorithmus beinhaltet, und ich würde es gerne verstehen.

Antwort

8

Der einfache Algorithmus, der in der Praxis (z. B. in Prolog) verwendet wird, ist für pathologische Fälle exponentiell.

Es gibt einen theoretisch effizienteren Algorithmus von Martelli und Montanari (IIRC ist linear), aber es ist viel langsamer für die einfachen Fälle, die in der Praxis auftreten, so dass es nicht viel verwendet wird.

+0

Kennen Sie ein Dokument, das es beschreibt? Entspricht es im Wesentlichen dem in SICP beschriebenen? –

+0

Ja, der einfache Algorithmus ist im Wesentlichen der gleiche wie in SICP beschrieben. Die übliche Darstellung verwendet Regeln wie Dekomposition, Kollision, Vorkommensprüfung, ..., also sollten Sie danach suchen. – starblue

4

Baader and Snyder veröffentlichten mehrere Vereinheitlichungsalgorithmen, sowohl für syntaktische Vereinheitlichung als auch für Gleichungsvereinheitlichung.

Sie geben an, dass ihr dritter syntaktischer Vereinheitlichungsalgorithmus (in Abschnitt 2.3) in O (n alpha (n)) läuft, wobei alpha (n) die umgekehrte Ackermann-Funktion ist - in praktischen Situationen entspricht sie einer kleinen Konstante.

Verwandte Themen