 |
|||
| HSG |
|
Definition
Unter Unifikation zweier Terme versteht man die Ersetzung der in ihnen vorkommenden (freien) Variablen durch Terme derart, dass die verbleibenden Terme als Zeichenketten gleich werden.
Beispiele
Die Terme T1=p(X) und T2=p(f(Y)) kann man durch die Ersetzung X=f(Y) unifizieren. Es gilt dann T1'=p(f(Y) und T2'=p(f(Y), also T1'=T2'. Ersetzt man X=f(a) und Y=a, so erhält man T1''=p(f(a)) und T2''=p(f(a)), also ebenfalls T1''=T2''. Die erste Ersetzung ist dabei die allgemeinere in dem Sinn, dass man sich nicht unnötig festgelegt hat.
Ersetzt man X=f(Z), so erhält man T1'''=p(f(Z)) und T2'''=p(f(Y)). T1''' ist nun als Zeichenkette nicht gleich zu T2''', was sich aber leicht durch eine weitere Ersetzung Z = Y 'flicken' lässt.
Freie und gebundene Variablen
20 ?- var(X). Yes 21 ?- X=a,var(X). No 22 ?- var(X),X=a. X = a ; No
Versuche mit Termen
fehlt noch!
Ein Unifikationsalgorithmus
Der folgende Algorithmus stammt aus Sterlin,L.: PROLOG, Fortgeschrittene Programmiertechniken. Bonn: Addison-Wesley, 1988 und wird nach Röhner,G.:Informatik mit Prolog, 3.Auflage 2007,S.53 zitiert.
Eingabe: Zwei zu unifizierende Terme S und T
Ausgabe: Die allgemeinste Substitution U von S und T, oder Scheitern
Initialisiere die Substitution U zu leer, den Keller mit der Gleichung S=T, und Scheitern mit falsch.
solange (Keller nicht leer und Scheitern=falsch)
hole X=Y vom Keller
falls
1. X eine Variable ist, die nicht in Y
vorkommt
ersetze X im Keller und in U durch Y
füge X=Y zu U hinzu
2. Y eine Variable ist, die nicht in X
vorkommt
ersetze Y im Keller und in U durch X
füge Y=X zu U hinzu
3. X und Y identische Konstanten oder Variablen sind
fahre fort
4. X = f(X1,...,Xn) und Y = f(Y1,...,Yn) für einen Funktor f und n>0 ist
schreibe Xi=Yi, i=1,...,n auf den Keller
5. ansonsten
Scheitern := wahr
wenn Scheitern
dann gebe Scheitern aus
ansonsten gebe U aus
Realisierung in Prolog
wird noch näher erläutert ...
subst(Alt,Neu,Alt,Neu) :- !.
subst(Alt,_,T,T) :- atomic(T),T \== Alt,!.
subst(Alt,Neu,AT,NT) :- AT =.. [F|Arg],subst_liste(Alt,Neu,Arg,Arg1),NT =.. [F|Arg1].
subst_liste(Alt,Neu,[K|R],[Kn|Rn]) :- subst(Alt,Neu,K,Kn),subst_liste(Alt,Neu,R,Rn),!.
subst_liste(_,_,[],[]).
:- dynamic k/1.
k([]).
pushK(X) :- retract(k(L)),assert(k([X|L])).
popK(X) :- k([X|R]),retract(k(_)),assert(k(R)).
:- dynamic u/1.
u([]).
pushU(X) :- retract(u(L)),assert(u([X|L])).
popU(X) :- u([X|R]),retract(u(_)),assert(u(R)).
:- dynamic scheitern/1.
scheitern(falsch).
init :- retractall(k(_)),assert(k([])),retractall(u(_)),assert(u([])),
retractall(scheitern(_)),assert(scheitern(falsch)),
listing(k),listing(u),listing(scheitern).
substK(Alt,Neu) :- retract(k(L)),subst_liste(Alt,Neu,L,L1),assert(k(L1)).
substU(Alt,Neu) :- retract(u(L)),subst_liste(Alt,Neu,L,L1),assert(u(L1)).
variable(K) :- atom(K),atom_prefix(K,v).
in(A,T) :- atomic(T),A == T,!.
in(A,T) :- T =.. [_|Arg],inListe(A,Arg),!.
inListe(A,Arg) :- Arg = [T|_],in(A,T).
inListe(A,Arg) :- Arg = [_|R],inListe(A,R).
fall1(X,Y) :- variable(X),not(in(X,Y)),substK(X,Y),substU(X,Y),
Gl =.. [=|[X,Y]],pushU(Gl).
fall2(X,Y) :- variable(Y),not(in(Y,X)),substK(Y,X),substU(Y,X),
Gl =.. [=|[Y,X]],pushU(Gl).
fall3(X,Y) :- (atomic(X),not(variable(X)),atomic(Y),not(variable(Y)),X == Y);
(atomic(X),variable(X),atomic(Y),variable(Y),X == Y).
fall4(X,Y) :- X =.. [F|Rx],Y =.. [F|Ry],length(Rx,N),length(Ry,N),N > 0,
pushKListe(Rx,Ry).
pushKListe(L,R) :- L = [Kl|Rl],R = [Kr|Rr],Gl =.. [=|[Kl,Kr]],pushK(Gl),
pushKListe(Rl,Rr).
pushKListe([],[]).
schritt :- popK(Gl),Gl =.. [=|[X,Y]],
( ( fall1(X,Y);fall2(X,Y);fall3(X,Y);fall4(X,Y) )
-> (retractall(scheitern(_)),assert(scheitern(falsch)))
; (retractall(scheitern(_)),assert(scheitern(wahr))) ),
listing(k),listing(u),listing(scheitern).
unify(T1,T2,U) :- init,Gl =.. [=|[T1,T2]],pushK(Gl),schritte,
scheitern(falsch),u(U).
schritte :- k([]),!.
schritte :- not(k([])),scheitern(falsch),schritt,schritte.
test1 :- unify(vX,a,[vX=a]).
test2 :- unify(b,vY,[vY=b]).
test3 :- unify(a,a,[]).
test4 :- unify(vX,vX,[]).
test5 :- unify(lehrer(meier,vX,vY),lehrer(vZ,mathe,10),[vZ=meier, vX=mathe, vY=10]).
test6 :- not(unify(jagt(vU,katze),jagt(katze,maus),_)).
test7 :- unify(append([a,b],[c,d],vLs),append([vX|vXs],vYs,[vX|vZs]),[vX=a, vXs=[b], vYs=[c, d], vLs=[a|vZs]]).
test8 :- unify(p(vX),p(f(vY)),[vX=f(vY)]).
test :- test1,test2,test3,test4,test5,test6,test7,test8.
Substitution
Das Prädikat subst(+Alt,+Neu,+AlterTerm,-NeuerTerm) ersetzt in AlterTerm alle Vorkommen von Alt durch Neu. Dabei dürfen Alt, Neu und AlterTerm keine Variablen enthalten.
subst(Alt,Neu,Alt,Neu) :- !. subst(Alt,_,T,T) :- atomic(T),T \== Alt,!. subst(Alt,Neu,AT,NT) :- AT =.. [F|Arg],subst_liste(Alt,Neu,Arg,Arg1),NT =.. [F|Arg1]. subst_liste(Alt,Neu,[K|R],[Kn|Rn]) :- subst(Alt,Neu,K,Kn),subst_liste(Alt,Neu,R,Rn),!. subst_liste(_, _, [],[]).
Um auf Alt zu stoßen, muss AlterTerm möglicherweise mehrfach zerlegt werden. Diese Zerlegung wird mit dem univ-Operator durchgeführt. Jedes Argument der Argument-Liste muss nun möglicherweise weiterzerlegt werden. Beim Zerlegen stößt man möglicherweise auf den zu ersetzenden Teilterm Alt. Er kann dann durch Neu ersetzt werden. Da dann nicht weiter zu tun ist, verhindert ein Cut den Rest. Das Zerlegen geht natürlich nur soweit, bis AlterTerm atomar ist. Ist nun AlterTerm ungleich Alt, so ist nichts zu tun, NeuerTerm wird einfach gleich AlterTerm gewählt. Wieder verhindert ein Cut weitere Aktivitäten. Das Bearbeiten der Argumentliste wird rekursiv mit der Kopf-Rest-Methode durchgeführt. Die Rekursion endet, wenn die Liste leer ist
Stack
:- dynamic k/1. k([]). push(X) :- retract(k(L)),assert(k([X|L])). pop(X) :- k([X|R]),retract(k(_)),assert(k(R)).
Unifikator
Prolog kann mit dem Prädikat unifiable den Unifikator zweier Terme angeben. Dabei muss den Termen das Zeichen @ vorangestellt werden.
16 ?- unifiable(@append([a,b],[c,d],Ls),@append([X|Xs],Ys,[X|Zs]),U). U = [Ls=[X|Zs], Ys=[c, d], Xs=[b], X=a] ;
Links
- Unifikation - wikipedia
- Unification - engl. wikipedia
- Unifikation und Resolution - Prof. Peter H. Starke, HU Berlin
