Unifikation

Unifikation bezeichnet in der Logik und Informatik den Prozess, durch den zwei Terme durch eine Substitution gleich gemacht werden können. Ein Term besteht aus Variablen, Konstanten und Funktionssymbolen. Eine Substitution sigma ordnet jeder Variablen eine Term zu und wird auf Terme angewandt, dabei werden Variablen durch ihre Zuordnungen ersetzt. Ziel ist es, eine Substitution sigma zu finden, so dass sigma(T1) = sigma(T2). Eine solche Substitution heißt Unifikator.

Ein Unifikator wird als allgemein bezeichnet, wenn jeder andere Unifikator durch weitere Substitutionen aus ihm gewonnen werden kann; der allgemeinste Unifikator (MGU) ist ein zentrales Konzept. In der Praxis bedeutet dies, dass alle anderen Unifikatoren durch die Kombination der MGUn mit zusätzlichen Substitutionen entstehen.

Der bekannteste Algorithmus zur Unifikation erster Ordnung ist der Robinson-Algorithmus. Er arbeitet schrittweise an Gleichungen, eliminiert Variablen durch geeignete Substitutionen und vergleicht Funktionssymbole. Ein wichtiger Zusatz ist der Occurs-Check, der verhindert, dass man sich selbst mittels einer Substitution unendlich wiederholt (etwa X = f(X)). In vielen Implementierungen wird dieser Check weggelassen, was zu inkorrekten Ergebnissen führen kann.

Anwendungen finden sich u. a. in der logischen Programmierung (Prolog), in der automatisierten Beweistheorie und in Typinferenzsystemen wie dem Hindley-Milner-Typensystem (Algorithmus W), wo Unifikation Typgleichungen löst und allgemeinste Typen bestimmt.

Beispiele: Aus S = f(x, g(y)) und T = f(a, g(b)) ergibt sich sigma = {x -> a, y -> b} als Unifikation; beide Terme werden durch sigma gleich. Höhere Ordnung Unifikation ist komplexer und in der Regel schwieriger zu handhaben; dort kommen spezialisierte, eingeschränkte Vorgehen zum Einsatz.