Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Herzlich willkommen! Unser gerade laufendes Thema lautet Unifikation.

Wie schafft es der Prolog Engine, verschiedene Terme aufeinander zu matchen?

Man wird sich erinnern, dass ich am Ende der letzten Sitzung beim Korrektheitsbeweis des Robinson-Algorithmus stecken geblieben bin.

Dass ich stecken geblieben bin, ist wieder mal ein gutes Beispiel dafür, dass man von Verifikation etwas hat.

Die Verifikation scheiterte an dieser Stelle nämlich deswegen, weil der Algorithmus einen Fehler hatte.

Falsche Algorithmen kann man nicht verifizieren, so ist das halt.

So, der Fehler steckte in dem Fall, wo wir auf der einen Seite eine Variable vorfinden,

die wir unifizieren mit einem beliebigen Term auf der anderen Seite.

Den Fall machen wir deswegen jetzt nochmal.

Ja, ich bin sicher, Sie hatten da schlaflose Nächte.

Also, ich fange jetzt einfach mitten im Algorithmus wieder an. Zum Glück war der Fehler ganz am Ende.

Wir haben also vorher einen Fall abgehakt, wo wir auf beiden Seiten Operationen oben liegen hatten.

Was man dann tut, ist eben überprüfen, dass die Operationen gleich sind.

Und wenn das erfolgreich ist, dann die Argumente dieser Operation auf den Stack zu schieben und weiter zu unifizieren.

Und wir sind jetzt in dem anderen Fall, das oben auf eine Variable liegt.

Sagen wir zum Beispiel bei E, das war also der Fall E ist gleich X.

So, und in dem Falle hatten wir jetzt X zu unifizieren mit einem weiteren Term.

Wir haben korrekterweise angemerkt, man muss dann überprüfen, ob dieser weitere Term bereits X enthält.

Wenn er das tut, dann wird er mit X nicht unifizierbar sein, weil egal, welche Substitution ich da ausführe,

immer der vorhandene Term auf der rechten Seite größer bleiben wird.

Dabei hatten wir aber, so wie ich es an die Tafel geschrieben hatte, vergessen, dass wir eine Hintergrundsubstitution bereits mitgeführt haben.

Also eine schon aufgesammelte Substitution, die wir nicht jedes Mal mit in unsere sämtlichen Terme rein substituieren,

sondern die wir on the fly expandieren.

So, und das muss man hier natürlich berücksichtigen.

Hier muss man also letztlich erstens beim Occurrence Check, also bei der Überprüfung, ob X auf der rechten Seite vorkommt,

und zweitens bei der tatsächlichen Substitution, die wir dann ausrechnen, berücksichtigen,

dass wir diese Substitution bereits aufgesammelt haben.

Also, dieser Fall, der sieht dann also so aus.

Jetzt kommt der Occurrence Check, wenn X eine Variable ist, die in nicht D, sondern D Sigma vorkommt.

Sigma ist die bisher zusammengestellte Substitution, die wir noch nicht explizit hier in D mit berücksichtigt haben.

Das heißt also, hier ist der Fehler. Das hat letztes Mal gefehlt.

So, wenn das der Fall ist, dann schlagschlägt die Unifikation fehl. Dann kriegen wir es nicht hin.

Und im anderen Falle machen wir also erfolgreich weiter.

Wir überprüfen zunächst mal, ob wir überhaupt etwas zu tun haben.

Also, else if D Sigma gleich X, then skip. Dann haben wir also nichts weiter zu tun.

Und andernfalls haben wir etwas zu tun, dann müssen wir also,

dann müssen wir diese neue Substitution X wird substituiert durch D Sigma, die müssen wir mit in Sigma aufnehmen.

Das heißt also, else Sigma Doppelpunkt gleich Sigma erweitert und X geht auf D Sigma.

Hier ist der zweite Fehler, nicht da hat das Sigma auch gefehlt.

Gut, ja, nicht? Und dann der Rest geht weiter wie bisher. Also, das kann ich jetzt noch eben ausschreiben.

Also, der Fall, dass D eine Variable X ist, der ist analog. Und das letzte Statement ist dann return Sigma.

Ach so, das gehört hier vor. Die beiden Abfragen sind vertauscht.

Kann man das einfach durch vertauschende Zeilen? Das muss ich nochmal schreiben.

Die beiden Abfragen sind andersrum. Ich frage erst nach, ob das gleich X ist und sonst hier.

Moment, denn am besten geht es so. Okay.

Also, wenn es in D Sigma vorkommt, dann, wenn es X selber ist, ist es okay. Else fail.

So, und dann muss ich also, ja, glücklicherweise ist das Else jetzt schon weiter nach links eingerückt als die Zeile drüber.

Also, ist dieses Else jetzt ein Else zu diesem Zen hier? Das heißt also, wenn X da nicht vorkommt, dann subsidiere ich ihn.

So.