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

Herzlich willkommen!

Wir hatten uns in der letzten Sitzung befasst mit Terminierungen in Terminersetzungssystemen.

Wir haben uns den Begriff der Reduktionsordnung angesehen und festgestellt,

wir müssen nur eine Reduktionsordnung finden, unter der dann immer die linke Seite jeder Reduktionsregel größer ist als die rechte Seite.

Sobald wir das haben, haben wir sogar starke Normalisierung des Systems gezeigt.

Wir haben uns dann zwei sehr naive Ideen angeguckt, da ging es insbesondere um zwei Aspekte.

Eine Reduktionsordnung sollte genau wie die Einschrittreduktion selbst kontextabgeschlossen und stabil sein.

Das heißt also, man sollte sowohl bei Verkleinerungen innen in einem komplizierten Term auch wirklich den gesamten großen Term verkleinern,

als auch dann, wenn man Terme verkleinert, in die statt der variablen komplizierten Terme eingesetzt sind.

Also die Reduktionsordnung sollte kontextabgeschlossen und stabil sein.

Wir haben zwei Beispiele gesehen, bei denen einmal das mit der Stabilität nicht immer hinhaute und einmal das mit der Kontextabgeschlossenheit.

Das Beispiel, wo die Stabilität nicht immer geklappt hat, das war das, wo wir schlicht und einfach als Reduktionsordnung die Termgröße ansetzen.

Gut, das lässt sich in manchen Fällen retten.

Dagegen der andere Ansatz, wo wir also die Subtermrelation verwendet haben, der ist mehr oder weniger unrettbar und diente mehr als Beispiel dafür,

wo mal die Stabilität klappt und die Kontextabgeschlossenheit aber nicht.

Wir lernen jetzt eine relativ allgemeine Methode kennen, mit der wir in relativ vielen Fällen durchkommen.

Einer der Fälle, der wird in den Übungen abgehandelt, ist eben ausmultiplizieren.

Das mache ich jetzt nicht hier in der Vorlesung, auch wenn es ein schönes Beispiel wäre,

um mal zu sehen, wie man diese Polynormordnung verwendet, weil es eben auf dem Zettel ist.

Das illustriert so ein bisschen aber jetzt vorweg als motivierendes Beispiel, was man vielleicht im Kopf behält.

Sie können sich auch gerne schon mal die Polynormordnung ansehen, die dann ja auf dem Zettel steht.

Ich nehme an, der ist schon raus.

Ja, schon da.

Man denkt ja seit der Mittelstufe, dass das selbstverständlich terminiert.

Ich nehme einen Term, der besteht nur aus Plus und Mal und ich fange an, den auszumultiplizieren.

Ich bin mir völlig sicher, wenn ich das anfange, dass ich damit mal fertig werde.

Aber so völlig klar ist eben nicht, warum das funktioniert.

Das mit der Termgröße, das geht schon mal gleich schief.

Beim Ausmultiplizieren wird ein Term eher größer als kleiner.

Ich kann nicht darauf zurückziehen, dass ich sage, ich reduziere die Term von der Größe her

und irgendwann werden sie nicht mehr kleiner.

Ganz im Gegenteil. Ich blase so einen Term einen Zweifelsfall schon ganz schön auf.

Probieren Sie mal, ein Produkt von lauter Summen auszumultiplizieren.

Da werden Sie sehen, dass das ganz schön explodiert.

Man kann dann anfangen zu sagen, wenn ich eine Multiplikation oberhalb einer Summe habe, dann ist das eine Fehlstellung.

Diese Reduktion hier reduziert die Anzahl Fehlstellungen.

Das stimmt zunächst mal bei dieser naiven Form der Gleichung.

Hier habe ich eine Fehlstelle. Das x ist oberhalb von diesem Plus.

Diese eine Fehlstelle ist rechts völlig verschwunden.

Hier habe ich zwar zwei Multiplikationen, aber die sind beide unterhalb von dem Plus.

Stabilität geht aber sofort flöten.

Wenn ich einfach nur Fehlstellen zähle, dann falle ich sofort deswegen auf die Nase, weil das x ja dann für einen komplizierten Term stehen könnte, mit 300.000 Fehlstellen.

Aus diesen 300.000 Fehlstellen werden auf der rechten Seite 600.000 Fehlstellen.

Mit naiven Methoden kommt man da nicht durch. Mit Polynomordnungen aber sogar relativ flott.

Das heißt, das soll uns jetzt beschäftigen.

Jetzt kommt erst mal der Teil, wo wir uns dumm stellen und fragen, was eine Dampfmaschine eigentlich ist.

Was ist ein Polynom? Das sollte hoffentlich aus den Ingenieur-Matte-Vorlesungen bekannt sein.

Hier machen wir einen eingeschränkten Fall, der so wahrscheinlich noch nicht dran war.

Und zwar nehmen wir ein Polynome über N, also über den natürlichen Zahlen und heißt zweierlei.