Substitution und Unifikation
Aus Infostudium Wiki
Inhaltsverzeichnis |
Definition Substitution
Eine Substitution σ ist eine Abbildung, die jeder Individuenvariablen einen Term zuordnet. Ist T ein Term, so bezeichne T[σ] den Term, der entsteht, wenn simultan für jede Variable xi der Term σ(xi) eingesetzt wird und H[σ] bezeichnet den Ausdruck, der aus H in diesem Fall entsteht.
Definition Unifikator
Eine Substitution σ heißt Unifikator für Ausdrücke H1, H2, wenn ![H_1[\sigma]\equiv H_2[\sigma]](/images/math/c/c/2/cc2cabba4d890ac99270463be3895e6b.png)
ist.
Beispiel
Beispiel 1
Wir betrachten die Ausdrücke 
und 
und wollen beide unifizieren.
| x | y | z | v | |
| σ1 | f(a) | a | a | g(a) |
![H_1[\sigma_1]\equiv Aaf(a)f(g(a))\equiv H_2[\sigma_1]](/images/math/3/3/d/33d929d0c9088d21e60b306c8dd1672e.png)
also σ1 ist ein Unifikator für H1, H2.
| x | y | z | v | |
| σ2 | f(a) | y | a | g(y) |
![H_1[\sigma_2]\equiv Aaf(a)f(g(y))\equiv H_2[\sigma_2]](/images/math/7/a/1/7a1d7986984ff576f4ec584f8e3db082.png)
Auch σ2 ist ein Unifikator für H1, H2, aber σ2 ist allgemeiner als σ1, weil eine Substitution σ3 so existiert, daß σ3(σ2(.)) = σ1(.) ist.
Beispiel 2
Geben Sie den allgemeinsten Unifikator für die folgenden Term-Paare an, oder begründen Sie warum dieser nicht existiert.
- f(g(a), X, Y) und f(Y, g(b), X)
- g(a) = Y = X = g(b) stellt einen Widerspruch zu a
b dar.
- f(X, Y, Z) und f(g(Y, Y), g(Z,Z), a)
- σ = { Z/a; Y/g(a,a); X/g(g(a,a), g(a,a)) }
Definition allgemeinster Unifikator (MGU)
σ heißt allgemeinster Unifikator für H1,H2, wenn
- σ ein Unifikator für H1,H2 ist
- Zu jedem Unifikator σ' für H1,H2 eine Substitution σ'' mit σ'(.) = σ''(σ(.)) existiert.
Unifikator μ ist MGU wenn alle anderen Unifikatoren σ aus μ entstehen, indem man Terme für seine Variablen einsetzt.
Clash Failure
- f(g(X),a,Y,h(Z)) und f(Y,X,g(Z),h(b))
Die Terme sind nicht unifizierbar. Aufgrund der ersten drei Argumente von f muss Z mit a instantiiert werden, aber für das vierte Argument müssen dann a und b unifiziert werden, was zu einem Clash Failure führt.
Occur Failure
- k(Y,Z,g(Z),Y) und k(h(X),f(U),X,U)
Die Terme sind nicht unifizierbar. Aufgrund der ersten drei Argumente von k muss Y mit h(g(f(U))) instantiiert werden, aber für das vierte Argument müssen dann h(g(f(U))) und U unifiziert werden, was zu einem Occur Failure führt.
Die Variable taucht also im Gegensatz zum Clash Failure zweimal auf.
Weblinks
http://www.informatik.hu-berlin.de/lehrstuehle/automaten/logik/node34.html
