Herzlich willkommen zur zweiten Sitzung zum Thema Konfluenz. Wir hatten letztes Mal uns den Begriff

des kritischen Paares angesehen, schon mal das sogenannte Critical Pairedemma als Behauptung

hingeschrieben, allerdings noch nicht bewiesen und wir haben uns Beispiele angesehen. So wir

werden heute noch ein paar Beispiele nachschieben, dann die fehlenden Beweise führen, erstens des

Critical Pairedemmas und zweitens des Newton-Lemmas und damit dann hoffentlich, wenn alles gut geht,

das Kapitel Thermenersetzung abschließen, dann geht es also ab der nächsten Sitzung weiter mit dem

Wir fangen noch mal an mit einer Erinnerung ans letzte Mal und zwar

an den Begriff des kritischen Paares. Also das war folgendermaßen definiert, wir stellen uns

vor wir hätten zwei Umformungsregeln, L1 formt um in R1, L2 formt um in R2. L1 hat irgendwie ein

Unterterm T, das drücke ich dadurch aus, dass L1 sich zerlegen lässt in einen Kontext, in dem ich

in dem Freilatz den Term T einsetze und L2, also die linke Seite der zweiten Umformungsregel,

unifiziert mit diesem Teilterm. Wenn ich diese Daten alle habe, mal gucken, dass ich nichts

vergessen habe. Dann bekomme ich ein kritisches Paar und zwar durch die beiden konkurrierenden

Umformungen, die ich jetzt auf L1 sigma bekomme. Ich kann L1 sigma eben umformen, zum einen natürlich

in R1 sigma, weil L1 nach R1 eine Umformungsregel ist und zweitens kann ich hier durch das sigma das

T als eine Instanz von oder mit der Substitution drin dann als eine Instanz von L2 identifizieren

und das dann in entsprechenden R2 Umlauf formen, das heißt also C von R2 sigma ist die andere

Hälfte des kritischen Paares. Gut, es war noch ein kleiner Twist dabei.

Wir verlangen, dass die beiden linken Seiten unserer Umformungsregeln sich keine Variablen

teilen, das stellen wir im Zweifel und das werden wir auch gleich im Beispiel nochmal

sehen, einfach dadurch sicher, dass wir die Variablen bei Bedarf umbenennen.

So, wir haben letztes Mal uns ein Beispiel nochmal angeguckt, was wir schon mal gesehen

hatten, wo wir also einen Term aus der Gruppentheorie auf zwei verschiedenen Wegen umformen und wir

haben gesehen, dass das in dieser jetzt entwickelten Sprache einfach heißt, dass wir da ein kritisches

Paar vor uns haben und dieses kritische Paar zusammenführbar ist.

So, jetzt machen wir mal ein Beispiel, wo es nicht klappt.

Und zwar sehen wir uns mal diesen Term hier an.

So, der entsteht, indem ich ja praktisch mir das Assoziativgesetz angucke und mir überlege,

wo finde ich Teilterne im Assoziativgesetz, die vielleicht so aussehen oder die nach

Weiterem substituieren so aussehen wie die linke Seite einer weiteren Regel.

So, man kommt dann auf diesen hier zum Beispiel, ja das Assoziativgesetz sagt ja zunächst

mal, ich kann also ein solches Produkt hier nach links umklammern.

So, ich finde hier insbesondere auf der rechten Seite ein Teilterm, der ist ein Produkt.

Das hier ist, also das hier ist praktisch Cl1 Sigma.

Das Sigma erläutern wir gleich noch.

Das entsteht hier aus x mal y mal z, indem ich mir hier diesen Teilterm als t ausgucke,

das heißt der Kontext ist dementsprechend hier x mal Freistelle.

Und diesen Teilterm hier, das t, unifiziere mit der linken Seite einer anderen Regel,

das ist in diesem Falle die Inversenregel.

Also, so, das ist mit dem Unifizieren ist in diesem Falle langweilig und wie gesagt

wir machen die Beispiele sowieso so, dass es also größtenteils langweilig ist.

Wir haben zu unifizieren dieses t hier mit in diesem Fall der linken Seite der Inversenregel,

die wir vorher umbenannt haben.

Gut, es ist in diesem Falle egal, wir machen es einfach defaultmäßig immer.

Wenn man es einmal sieht, die Variablen waren vorher auch schon disjunkt, also ich hätte

hier bei dem x bleiben können, aber ich illustriere einfach mal, dass ich einfach immer mit Gewalt

alle Variablen in der zweiten Regel per Strich umbenenne.

So, ich muss also y mal z unifizieren mit x Strich mal x Strich hoch minus eins.

Gut, das heißt, warum würde ich es machen?

Ich ersetze y durch x Strich und ich ersetze z durch x Strich hoch minus eins.