Guten Morgen allerseits. Mein Name ist Christoph Rauch und ich werde in den nächsten zwei Wochen

den Herrn Professor Schröder vertreten in dieser Vorlesung Theorie der Programmierung. Bevor wir

aber jetzt wieder in unser Thema der Thermersetzungssysteme einsteigen, würde ich

gerne noch in Erfahrung bringen, ob mit der Übungsanmeldung denn jetzt alles geklappt hat

oder ob es da noch irgendwie Probleme gibt. Leute, die sich nicht anmelden konnten, die

nicht den richtigen Termin gefunden haben. Wie Sie sicherlich feststellen konnten,

wurde die Freitagsübung ja jetzt gekippt, weil zu wenig Interesse bestand. Deswegen gibt es

allerdings eine zusätzliche Montagsübung, um die Tutoren etwas zu entlasten. Es wird deswegen

wahrscheinlich jemand, entweder ich oder ihr Übungsleiter, auf Sie zukommen am Montag und

Sie fragen, ob Sie vielleicht wechseln wollen in die neu erstellte Gruppe, damit das sich ein

bisschen besser verteilt, nur um schon mal Sie darauf vorzubereiten. Also wir haben uns in der

letzten Woche beschäftigt mit Thermersetzungssystemen, allerdings sind wir noch nicht so weit gekommen,

dass wir besprochen haben, was denn ein Thermersetzungssystem überhaupt ist. Also

wir haben uns beschäftigt mit Relationen und Eigenschaften von Relationen, wir haben uns

beschäftigt mit Termen und mit Substitutionen und jetzt fehlt uns aber noch ein bisschen was von dem

Handwerkszeug, um zu definieren, was eigentlich ein Thermersetzungssystem ist. Und zwar müssen wir

noch sagen, was ein Kontext ist und das kann man sich wieder einfach vorstellen an diesem Beispiel,

dass ich hier jetzt rechts mal aufziehen werde, wenn wir eine Signatur haben, zum Beispiel nur

dieses zweistellige Plus und ich bilde daraus einen Term, also über irgendeine Variablenmenge mit x,

y, z und so weiter und ich möchte da jetzt einen Term bilden, a plus b plus c, ja was auch immer plus e.

Ja und sagen wir, wir haben irgendein Assoziativgesetz, das uns Klammern vertauscht,

dann würde ja jeder von ihnen schon einfach intuitiv feststellen können, dass man dieses

Assoziativgesetz nicht nur auf den ganzen Term anwenden kann, sondern auch innerhalb von diesem

Term und das ist, was uns ein Kontext aussagen soll, dass wir den Term isoliert, also einen Subterm

isoliert betrachten können in einem Kontext, zum Beispiel dieses plus e hier als Kontext und eine

Regel innerhalb dieses Subterms anzuwenden. Deswegen hier jetzt Definition. Also ein Kontext

soll sein, einfach ein, also intuitiv ein Term mit genau einem Loch. Ja und formal kann man das auch

wieder mit einer Grammatik ausdrücken. Also wir nennen solche Kontexte, wir nennen wir mit einem c und so einem

Fehlzeichen und die Grammatik dafür ist einfach, entweder ist ein Kontext einfach nur ein Loch oder

es ist eben ein Term mit einem Loch, also ein Funktionssymbol mit irgendwelchen Termen t1 bis t

i minus eins, dann einem Loch, einen Kontext, Entschuldigung, Rekursiv und weiteren Termen t i plus eins bis tn.

Ja und dabei müssen wir natürlich jetzt beachten, dass f, das habe ich jetzt vergessen hier oben

hinzuschreiben, sei Sigma eine Signatur. Da müssen wir jetzt beachten, dass dieses f natürlich aus

unserer Signatur sein soll und zwar endstellig, das heißt hier f n ist unsere Signatur und diese t i

sollen Terme sein, also die t i sind Terme über Sigma und eine Variablemenge, die wir jetzt hier

nicht näher spezifizieren. Also das ist irgendwie ein erster Teil von dieser Definition, jetzt wollen

wir natürlich noch wissen, was wir mit diesen Kontexten machen können und was da eben noch fehlt

ist die sogenannte Einsetzung oder das Resultat, das bezeichnen wir mit c von t, jetzt ist hier

jetzt t einfach ein Term, der in dieses Loch, das in dem Kontext drin ist, eingesetzt wird.

Resultat der Einsetzung eines Terms t in Kontext c von Leerstelle und das ist auch wieder,

ich kann es nicht einfach hochschieben, auch wieder rekursiv definiert.

Ja und bei einem einfachen Loch hier ist es natürlich einfach, also ein Loch angewendet auf t,

ist einfach dieser Term t, wenn ich einen t in ein Loch einsetz, dann kommt dieser Term t wieder

raus und jetzt kriege ich Platzprobleme, naja ich glaube ich kriege es in eine Zeile, also wenn

ich jetzt hier einen solchen Term habe mit einem Loch f von t1 bis t i-1 Kontext t i plus 1 und so

weiter und setze da mein t ein, naja dann lasse ich das einfach rekursiv in diese in diesen Kontext

reinrutschen, also das ist dann einfach f von t1 t i-1 c von t t i plus 1 cn.

So und mit dieser Definition haben wir jetzt wirklich alles Handwerkszeug um mal zu sagen,

was so ein Thermersetzungssystem überhaupt ist und zwar ist ein Thermersetzungssystem nichts anderes,

als eine Relation zwischen solchen Termen. Also ein Thermersetzungssystem