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

Ja, also wie gesagt, wir hatten letztes Jahr angefangen mit dem Unifikationsalgorithmus,

hatten den Algorithmus auch schon in Gänze gesehen,

und uns überlegt, dass er richtige Antworten liefert, sofern er terminiert.

Und der Beweis dieser Terminierung, der steht aber noch aus.

Erinnere ich mich richtig, man protestiere, wenn ich jetzt zu viel unterstelle.

Stimmt so, gut, danke.

So, um die Terminierungsanalyse durchzuführen, hilft es zunächst mal nichts, wir müssen den Algorithmus nochmal anschreiben.

Sie kennen das jetzt schon, also ich pinse das einfach nochmal hier hin.

Ich sage ausnahmsweise mal nichts dazu, weil Sie es ja wie gesagt schon kennen.

Ja oder nein, ich erkläre es Ihnen nochmal, dann werden Sie es zwar mal erklärt.

Also die erste Regel war eine Regel, die offensichtlich triviale Gleichung der Form X gleich X wegwirft,

die wir dann an der Stelle also erledigt haben.

So, die zweite Regel war die, die ein zu oberst liegendes Funktionssymbol, das auf beiden Seiten gleich ist,

praktisch wegwirft und dann versucht, die jeweiligen Argumente gleich zu machen.

So, die entsprechende Regel für den Fall, dass auf beiden Seiten Funktionssymbole oben liegen, die aber verschieden sind,

ich mache mir gar nicht die Mühe, Ihre Argumente noch hinzuschreiben, weil die nicht interessieren,

die Regel transformiert also diesen Fall in einen Clash, das heißt in diesem Falle sind die beiden Seiten nicht unifizierbar.

So, dann kommt eine rein bürokratische Regel, die Orientierungsregel, die einem sagt,

wenn wir im Prinzip die Gleichung schon gelöst haben, gewissermaßen nur das Ergebnis auf der falschen Seite stehen haben,

links statt rechts, dann vertauschen wir die Gleichung, sodass also jetzt die Gleichung links steht.

Und zwar in dem Fall, dass E keine Variable ist, wenn wir das auch dann machen würden, wenn E selbst eine Variable ist,

dann würden wir hier auf alle Ewigkeiten hin und her drehen, das wollen wir nicht.

Der letzte Fall, der dann in zwei Regeln praktisch zerfällt, weil er eine Fallunterscheidung hat,

weil wir jetzt praktisch erfolgreich gewesen sind und also das Gleichungssystem so transformiert haben,

wenn hier eine Variable links steht und irgendein Term rechts, dann gibt es zwei Fälle.

Und zwar einmal einen erneuten Clash, also Ausgabe nicht unifizierbar, wenn x auf der rechten Seite wieder frei vorkommt.

Wir haben uns überlegt, dass in dem Falle die Gleichung eben nicht lösbar, nicht unifizierbar ist.

Ich schreibe hier in Klammern dazu, das machen wir nur dann, wenn x nicht gleich E ist, denn sonst ist es harmlos,

also x gleich x ist natürlich lösbar. Ich schreibe das deswegen in Klammern, weil gemeint ist,

dass die Regeln von oben nach unten priorisiert sind, also zu dem Fall kommen wir hier nie,

weil dann oben schon die Leadzug überschlagen hat.

Im anderen Falle, das ist also der gute Fall, wo das System lösbar ist,

dann nehmen wir jetzt diese Lösung und substituieren sie im Rest für x, sodass also x im Rest nicht mehr vorkommt.

Das machen wir nur dann, wenn der erste Fall nicht zugeschlagen hat, das ist diese Bedingung hier,

und das machen wir außerdem nur dann, wenn x im Rest tatsächlich noch vorkommt, damit wir es nicht mehrmals machen.

So, das war der Algorithmus.

Die Frage ist jetzt, warum terminiert das Ding? Die Schwierigkeit dabei ist der letzte Fall, die allerletzte Zeit,

in der wir eine Lösung, die wir gefunden haben, in den Rest rein substituieren.

Alles andere, da sehen wir so ein paar offensichtliche Maße, die immer kleiner werden,

also die meiste Zeit wird das Gleichungssystem kleiner, bis auf diesen Orientierungsfall da,

und dann, gut, wir sehen, dass man diese Orientierungsregel offensichtlich auch nur endlich oft anwenden kann.

Das ist alles unproblematisch, aber hier unten, da kommt also ein Schritt, der womöglich alles, was wir erreicht haben, wieder kaputt macht.

Also erstens, wir substituieren hier ja was Größeres für was Kleineres.

Das e ist ja größer als das x, das heißt, wir machen den Term größer, das x kann sogar mehrfach vorkommen,

wir machen ihn eventuell viel größer, und wir machen sogar das mit der Orientierung wieder kaputt,

wenn wir also mühsam was zurechtgetauscht haben, jetzt die Variable auf der linken Seite steht von der Gleichung,

dann wird ja womöglich jetzt wieder was nicht triviales dafür substituiert.

Also das passiert, andersrum, das passiert nicht, nachdem wir die Orientierungsregel angewendet haben,

weil wir die ja nur dann anwenden, wenn das Ding rechts keine Variable ist,