Anwendungen der Vereinigung?

Question

Was sind die (praktisch) Anwendungen von Unification ? Wo es tatsächlich in der realen Welt verwendet?

Ich kann nicht die ganze Idee verstehen, was es wirklich ist und warum es als Teil der Künstlichen Intelligenz betrachtet.

Answer 1

Unification ist im wesentlichen ein Prozeß von Substitution . Ich habe es gesehen „Zwei-Wege-Matching“ genannt.

In Prolog, in anderen logischen Programmiersprachen und in Sprachen direkt auf Logik basiert Umschreiben ( Maude Elan , etc ...) ist der Mechanismus, durch den freien (logische) Variablen sind, binden an Begriffe / Werte. In Concurrent Prolog werden diese Variablen als Kommunikationskanäle interpretiert.

IMO, der bessere Weg zu verstehen, ist es mit einigen Beispielen aus der Mathematik ist (Vereinigung war / ist ein Basisschlüsselmechanismus, zum Beispiel im Rahmen von automatisierten Theorembeweisern Forschung, ein Teilgebiet der KI, eine andere Verwendung in in Typ Inferenzalgorithmen ). Die Beispiele, die aus dem Kontext der Computeralgebra-Systeme (CAS) :

Erstes Beispiel:

Gegeben sei eine Menge Q und zwei binäre Operationen * und + auf sie, dann * ist links distributive über +, wenn:

X * (Y + Z)   =   (X * Y) + (X * Z)   |1|

Dies ist ein Rewrite-Regel (ein Satz von Regeln für das Umschreiben ist ein Umschreiben System ).

Wenn wir diese Rewrite-Regel auf einen konkreten Fall anwenden möchten, sagen:

a * (1 + b)   |2|

wir Unify (über einen Unifikationsalgorithmus) diesen Begriff, | 2 |, mit der linken Seite ( LHS ) von | 1 | und wir haben diese (trivial absichtlich) Substitution (die allgemeinste Einige MGU ):

{X/a, Y/1, Z/b}   |3|

Nun Anwendung | 3 | auf die rechte Seite ( rhs ) von | 1 |, haben wir schließlich:

(a * 1) + (a * b)

Das war einfach und zu schätzen, was Vereinigung tun kann ich ein wenig komplexes Beispiel zeigen werde.

Zweites Beispiel:

In Anbetracht dieser Rewrite-Regel:

log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4|

wir es auf diese Gleichung:

log(e,(x+1)) + log(e,(x-1)) = k   |5|

( LHS von | 5 | vereinigen zu LHS von | 4 |), so haben wir dieses MGU :

{X/e, Y/(x+1), Z/(x-1)}   |6|

Beachten Sie, dass X und x sind zwei verschiedene Variablen. Hier haben wir zwei Variablen, X und Y, die zwei passen zusammengesetzte Begriffe , (x + 1) und (x-1), nicht einfache Werte oder Variablen.

Wir wenden diese MGU , | 6 |, zu rhs von | 4 | dann und wir diese stellen in | 5 |; so haben wir:

log(e,(x+1)*(x-1)) = k   |7|

und so weiter.

(die Hoffnung, ich habe keinen Fehler oder dies kann Neophyten noch mehr verwirren.)

Answer 2

Vereinheitlichung ist ein Schlüsselmechanismus in Typinferenz . Praktisch gesprochen Vereinigung in diesem Zusammenhang reduzieren stark Verschleiß an den Fingern.

Answer 3

Prolog zum Beispiel verwendet Einigungs Werte für die Variablen zu finden, die die Regeln erfüllen - siehe diese Erklärung für ein Beispiel. Ich erwarte, dass es ist eine typische Technik in logische Programmiersprachen im Allgemeinen, obwohl ich keine Erfahrung mit irgendwelchen anderen haben.

Answer 4

Vereinheitlichung ist wie Pattern-Matching, wo Sie zwei Strukturen miteinander reiben, wo Variablen in einem erlaubt sind in den anderen Werten entsprechen.

Die einfachste Form der Vereinigung geschieht, wenn Sie eine Funktion in einer normalen Sprache nennen. Der Anrufer hat Argumente und die Angerufene hat Parameter. Die Parameter „gebunden“ die Argumente sind, und das erzeugt eine Ausprägung der Funktion.

Eine weitere einfache Form der Vereinigung ist, wenn Sie einen regulären Ausdruck für den Abgleich verwenden, beispielsweise an einer Eingabeaufforderung Sie könnten dir x*y*.z* sagen, welche einige übereinstimmen, aber nicht alle Dateinamen.

Künstliche Intelligenz mag Verwendung von Inferenzmaschinen zu machen, um zu versuchen Argumentation aus einem Korpus des Wissens zu simulieren, in der Regel in Form von Anweisungen in einer Logik. Um ein dummes Beispiel zu wählen, könnten Sie „wissen“, dass „alle Menschen sind sterblich“, wie in forall(x)(man(x) implies mortal(x)). Dann, wenn Sie eine Frage stellen „ist Sam sterblich“ als mortal(Sam)?, Sie, dass mit der Regel vereinigen könnte eine neue Frage zu bekommen „ist Sam ein Mann“ man(Sam)?

Ich hoffe, das hilft.