Begriff
Unification
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Du hast zwei Puzzleteile mit Lücken (Variablen).
A: f(X, a) (Funktion f mit Variable X und Konstante a).
B: f(b, Y) (Funktion f mit Konstante b und Variable Y).
Passen sie zusammen?
Ja, wenn wir X = b und Y = a setzen.
Dann werden beide zu f(b, a).
Das ist Unifikation: Das Finden einer Ersetzung (Substitution), die zwei Terme identisch macht.
Es ist viel mächtiger als einfaches String.equals().
Es ist das Herz von Prolog und Type Inference (in Haskell/Rust).
Merksatz: Ein algorithmisches Verfahren zur Lösung von Gleichungen zwischen symbolischen Ausdrücken, indem Variablen durch Terme ersetzt werden, sodass die Ausdrücke syntaktisch identisch werden.
In Java Generics oder TypeScript.
Du rufst List.of("Hallo") auf.
Die Methode ist List<T> of(T t).
Der Compiler unifiziert T mit String.
Ergebnis: List<String>.
Der Compiler löst Gleichungen im Hintergrund.
1. Most General Unifier (MGU)
Es gibt oft viele Lösungen.
f(X) und f(Y).
Lösung 1: X = a, Y = a -> f(a). (Zu speziell).
Lösung 2: X = Y. -> f(Y). (Allgemein).
Der MGU ist die allgemeinste Lösung, die alle anderen Lösungen impliziert.
Robinson zeigte: Wenn es einen Unifikator gibt, gibt es einen eindeutigen MGU (bis auf Umbenennung).
2. Occur Check
Die Falle.
X unifizieren mit f(X).
Geht das?
X = f(X).
Ersetzen: f(f(X)).
Ersetzen: f(f(f(X))).
Endless Loop!
Prolog schaltet den "Occur Check" standardmäßig aus (Speed > Correctness). Das führt manchmal zu zyklischen Termen. Logisch korrekt wäre: "Fail".
1. Robinson vs. Martelli-Montanari
Der originale Robinson-Algorithmus war exponentiell in Zeit und Speicher (wegen Term-Kopien). In der Produktion (Compilern) nutzt man den Algorithmus von Martelli & Montanari. Er nutzt Union-Find Datenstrukturen. Variablen werden nicht durch Terme ersetzt, sondern zeigen via Pointer auf sie. Das macht Unifikation nahezu linear $O(n \cdot \alpha(n))$. Ohne diese Optimierung würde ein Rust-Compiler bei komplexen Typ-Verschachtelungen Stunden statt Sekunden brauchen.
2. AC-Unification (Associative-Commutative)
In der echten Welt gilt oft: $x + y = y + x$ (Kommutativität). Standard-Unifikation scheitert hier ($x+y$ unifiziert nicht mit $b+a$). AC-Unifikation erlaubt es dem Algorithmus, Terme umzuordnen, um eine Lösung zu finden. Das ist mathematisch viel schwerer (NP-Complete oder sogar unentscheidbar in manchen Theorien). Man braucht es in Theorem Provern (wie ACL2) oder bei der Optimierung von Hardware-Schaltkreisen, wo die Reihenfolge von Gattern oft egal ist.
3. Higher-Order Unification (HOU)
Was, wenn wir Funktionen unifizieren wollen?
f(a) unifizieren mit g. Lösung: g = \lambda x . f(x).
Das ist das Feld von Gerard Huet.
HOU ist im allgemeinen Fall unentscheidbar. Aber für spezielle Fälle (Pattern Unification) funktioniert es. Es ist die Basis für Sprachen wie Lambda Prolog oder Frameworks wie Isabelle/HOL, wo man Beweisschritte über Funktionen hinweg automatisieren muss.
Quick-Check
Pattern Matching?
Ja. Aber Pattern Matching (in Scala/Rust) ist meist "One-Way" (Daten gegen Muster). Unifikation ist "Two-Way" (Muster gegen Muster, beide haben Variablen).Zeitkomplexität?
Fast linear (mit Union-Find Datenstruktur). Martelli-Montanari Algorithmus.Wichtigkeit?
Ohne Unifikation keine Logik-Programmierung und keine moderne Typ-Inferenz (Hindley-Milner).