Und zwar willkommen in der Übung zur Theorie der Programmierung. Um das noch mal sicher zu stellen,

erstmal so ein paar organisatorische Sachen. Ihr seid in der Übung und das bedeutet, was machen wir

hier? Wir besprechen vor allem die Blätter. Das schreibe ich nicht alles auf. Wir besprechen

die meisten Aufgaben auf den Blättern. Im Moment hat jeder ein Übungsblatt vor sich ausgedruckt.

Einer hat eins. Ihr seht es auch da an der Tafel. An manchen dieser Aufgaben steht keine

Punktezahl wie bei dieser hier. Und bei anderen steht hier so eine schöne Punktezahl. Das heißt,

wir besprechen jetzt in dieser und den nächsten zwei Wochen nacheinander in irgendeiner Reihenfolge

die unbepunkteten Aufgaben. Und in drei Wochen gebt ihr dann in Einzelabgaben die Lösungen

für die letzten zwei Aufgaben auf diesem Blatt ab. Die sind jeweils zehn Punkte. Und letztendlich

dient das die Übung dafür, dass ihr so ein bisschen in die Standardaufgaben reinkommt und das was ihr

dann lernt adaptieren könnt um die Aufgaben zu lösen. Also die sind jetzt nicht unglaublich

unterschiedlich zu dem was wir hier jetzt schon besprechen, aber eben auch nicht komplett gleich.

Dann von den Punkten gibt es Bonuspunkte am Ende. Insgesamt könnt ihr bis zu 15 Prozent an

Bonuspunkten in der Klausur erzielen. Genau. Das ist so der Inhalt der Übung. Und wenn ihr

irgendwelche Fragen habt zu vorlesen, könnt ihr die natürlich auch stellen. Dann gibt es so weit

Fragen zum organisatorischen. Wunderbar. Dann hatte ich vor jetzt so noch eine kurze Wiederholung

von dem Klausurstoff zu machen, der jetzt relevant ist für die heutige Übung. Also ich mache das

jetzt nicht in in allem Detail, aber so die grundlegenden Begriffe wiederhole ich kurz. Und

zwar was haben wir gemacht? Termersetzungssysteme. Das heißt wir haben uns eine Signatur angeschaut

von irgendwelchen Symbolen. Ja. Irgendeine Signatur. Und in dieser Signatur ist eine Menge

von Funktionssymbolen und jedes Funktionssymbol hat eine Arität. Das ist irgendeine natürliche

Zahl, die mit Arität 0 sind, die Konstanten. Also eigentlich ungefähr genauso wie in Clolop.

Und auf diesen Funktionssymbolen, daraus können wir Terme bauen und mit diesen Termen können wir

Regeln erstellen. Also wie sieht so ein Term aus? So ein Term über Sigma mit irgendwelchen Variablen

aus V. Das ist so. Ein Term ist entweder irgendeine Variable V aus V oder X aus V oder eben wenn T1

bis Tn bereits Terme über Sigma sind und f genau die Arität n hat und das n Sigma ist, dann können

wir die n Terme in die n Parameter von f stecken und erhalten einen neuen Term. Dann ist f T1 bis Tn so ein Term.

Man könnte jetzt noch extra dazu sagen, so der Basisfall ist entweder eine Variable oder eine

Konstante, aber dieser Basisfall, ein Term besteht nur aus einer Konstante, steckt eigentlich schon

hier drin für wenn ich irgendeine Konstante habe, dann ist die, hat die Arität 0. Das heißt, ich

brauche keine Terme, keine weiteren Terme zum zusammenbauen und dann folgt einfach daraus,

dass dieses C so ein Sigma-Term ist. Und mit zwei solchen Termen können wir eine Regel bauen und

dabei müssen wir so ganz natürliche Sachen beachten, wie auf der rechten Seite der Regel

dürfen nur Variablen vorkommen, die auch auf der linken Seite erwähnt werden. Also das Beispiel

in der Vorlesung, f von x ist x und g von x ist 1, also sind f und g haben Arität 2 und 1 ist eine

Konstante, die hat Arität. Das ist jetzt so die Signatur. Und damit können wir mal was ausprobieren,

die Regelanwendungen sind eigentlich relativ intuitiv, die kann man jetzt natürlich formal

definieren, wenn man die formale Definition sehen möchte, schaut man sich die Vorlesungsaufzeichnung

an. Wir machen das jetzt einfach mal nach der Notation in der Vorlesung mit Übung 1. Und was

ich noch gar nicht gesagt hatte, und zwar, ich hatte jetzt eigentlich nicht die Idee oder wir hatten

nicht die Idee, so 90 Minuten Frontalunterricht für euch zu machen, sondern es wäre eigentlich am

besten, wenn ihr so nacheinander die Übungen löst, denn am meisten lernt man eigentlich,

wenn man die Übung an der Tafel macht. Dabei geht es auch nicht darum, die Lösung hinzukritzeln und

dem Tutor zu zeigen, dass man es verstanden hat, sondern es den anderen Kommilitonen zu erklären.

Also fühlt euch berufen, die Übungen an der Tafel zu machen. Ich werde dann am Ende der

Übung auch sagen, welche Aufgaben wir beim nächsten Mal machen, und dann könnt ihr die euch schon mal

angucken und das auf Papier vorbereiten und dann an der Tafel präsentieren. Es geht los mit der

ersten Aufgabe. Wir haben ein paar Regeln, die man einfach immer nebenher Anzeigen angezeigt haben

muss, weil sie jetzt nicht so super intuitiv sind. Und was wir zeigen sollen ist, dass das System

nicht normalisierend ist. Also wir suchen irgendeine unendliche Kette von Termen und die Relation ist