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

Ja, herzlich willkommen. Wir hatten letztes Mal uns die Definition angesehen,

davon was ein Term-Ersetzungssystem eigentlich ist und von den Anfängen seiner operationalen

Semantik, das heißt davon was es letztlich mit einem Term tut. Das wiederholen wir kurz noch mal.

Ich hatte letztes Mal noch keinen allgemeinen Buchstaben dafür eingeführt, was wir typischerweise

so fünf Buchstaben verwenden, um ein Termersetzungssystem zu definieren. Formal besteht ein Termersetzungssystem

aus einer Signatur Sigma und einer Ersetzungsrelation über Termen in dieser Signatur. Meistens geben wir

es einfach an, indem wir diese Termersetzungsrelation angeben. Die Signatur kann man dann typischerweise

ablesen an den Symbolen, die in den Gleichungen nun mal vorkommen. Dabei ist eben diese Termersetzungsrelation,

die wir Pfeil 0 schreiben, einfach eine beliebige Teilmenge, eine beliebige Relation auf T Sigma v Kreuz T Sigma v.

Also es setzt immer zwei Terme in Beziehung. Und die grundlegende Definition, die wir uns dann angesehen hatten,

war die, die uns sagt, wie kann ich denn nun tatsächlich einen Term umformen gemäß einer solchen grundlegenden

definierten Relation. Dazu muss man zwei Dinge tun. Erstens, man muss diese Grundumformung hier an Pfeil 0 einbetten

in einen Kontext. Ich kann also tief intern drin umformen und man muss reinhängen eine Substitution.

Das heißt, ich kann auch dann diese Umformung durchführen, wenn nicht, wie ursprünglich angegeben,

die irgendwelche Variablen dastehen, sondern wenn für diese Variablen irgendwas eingesetzt ist.

Also genau das, was man erwartet eigentlich. Formal hieß das die Einschrittreduktion.

Die schreiben wir jetzt einfach als Pfeil. Und die definieren wir als, ja. Wir hatten sie auf zwei Arten definiert.

Wir haben gesagt, die Einschrittreduktion ist die kleinste Kontext abgeschlossene und stabile Relation,

die unser Pfeil 0 enthält. Und das kann man expliziter sagen und diese Definition wiederhole ich jetzt.

So, und zwar sind das eben alle Paare dieser Form hier, wobei T und S aus der ursprünglich angegebenen

Ersetzungsrelation stammen und das schließe ich eben jetzt ab, wie eben angedeutet.

Das heißt, ich packe einen beliebigen Kontext draußen rum.

Noch mal ausdrücklich. Sieh jetzt mal.

Also, dass die Ersetzung darf in einem beliebigen Kontext, also tief innen im Term stattfinden und

Siegmeister Substitution. Das heißt, in meine Gleichung, die ich da anwende, kann ich auch beliebige Dinge einsetzen.

So, ich mache jetzt noch ein bisschen weiter mit Definitionen, die wir dann brauchen und steige dann wieder ein in das Beispiel,

das wir letztes Mal angefangen haben, um dann auch diese erweiterten Begriffe daran zu illustrieren.

Also, erstens.

Wir reden als nächstes von der Reduktionsrelation des Systems.

Nicht mehr ein Schritt Reduktion, sondern Reduktion schlechthin.

Und ich deute hier durch die Klammern an, dass ich meistens nur Reduktion und nicht Reduktionsrelation sage und schreibe.

Nun, die beschreiben wir Pfeilstern.

Und das heißt genau das, was es eben nach der Eingangs der letzten Sitzung eingeführten Maschinerie nun mal heißt.

Ja, in dieser Maschinerie für binäre Relationen hieß Stern einfach reflexiv transitiver Abschluss.

Und genau das ist das hier.

Also, die Reduktionsrelation Pfeilstern ist der reflexiv transitive Abschluss von Pfeil, also von der Einschritt Reduktion.

So, das heißt, das ist jetzt Reduktion nicht mehr in einem Schritt, sondern in beliebig vielen Schritten.

Also, ich kann gar nicht reduzieren oder ich kann 20 mal reduzieren.

So, dann haben wir Konvertierbarkeit.

Das ist jetzt so was Ähnliches, aber unter Aufgabe der Maßgabe, dass wir nur in einer Richtung vorgehen könnten.

Das ist also Umformung womöglich in verschiedenen Richtungen längs dieser ursprünglich gegebenen Umformungsrelation.

So, das Symbol dafür ist, ja wie lese ich es denn vor, hin und her Pfeilstern, ja, Doppelpfeilstern.

So, das ist jetzt also nicht mehr der reflexiv transitive Abschluss von dieser Einschritt Reduktion,

sondern das ist der reflexiv transitiv symmetrische Abschluss, also die erzeugte Rekvivalenzrelation.

Mit anderen Worten, ich kann wieder endlich viele Schritte machen, aber ich darf dabei auch falsch rumlaufen.

Also, was ausschreiben ist also diese Konvertierbarkeitsrelation.

Ist also vom symmetrischen Abschluss von Pfeil, also von der Einschritt Reduktion, noch mal der reflexiv transitive Abschluss.

Wir hatten uns letztes Mal überlegt, dass das tatsächlich wieder symmetrisch also der Äquivalenzabschluss ist.

Das hier schreiben wir eben auch als Pfeil in die andere Richtung, natürlicherweise ja, die Umkehrung von Pfeil nach rechts ist eben Pfeil nach links.