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

Also wohl fundiert. Well founded oder WF. Genau, dann den.

Es ist jetzt eine dieser unglücklichen Definitionen, die sich ausnahmsweise wirklich

mal am besten doch negativ formulieren. Sie ist damit in der Welt eine große Ausnahme.

Also sie heißt dann wohlfundiert, wenn es keine unendlichen Erbfahrt gibt. Also wenn

es keine unendliche Folge gibt, die irgendwo anfängt bei einem x0 weitergeht mit einem x1,

das zu dem ersten Relation R steht und so weiter. Wenn das nicht existiert, denken Sie nicht an

einen Lila-Edefand. Also wenn das nicht existiert, dann heißt die Relation wohlfundiert. Beispiele,

die größere Relation auf den natürlichen Zahlen, die ist wohlfundiert. Das ist so unser wichtigstes

Beispiel einer wohlfundierten Ordnung. Selbstverständlich kriege ich keine unendliche

absteigende Folge von natürlichen Zahlen hin. Irgendwann haue ich mir an der Null den Schädel

ein. Nicht-Beispiele, also Dinge, die dann eben nicht wohlfundiert sind, weil es eben

doch unendliche absteigende Folgen gibt, sind zum Beispiel die ganzen Zahlen und die größere

Relation. Natürlich kann ich eine unendliche absteigende Folge ganzer Zahlen bauen. Ich

ziehe immer eins ab und laufe dagegen minusunendlich, kein Problem. Aber auch zum Beispiel die größere

Relation auf etwas, was zunächst mal aussieht, als wäre es nach unten beschränkt, zum Beispiel

die nicht negativen reellen Zahlen. Also auch auf den positiven Zahlenstrahl oder dem nicht

negativen Zahlenstrahl einschließlich Null kann ich natürlich eine unendliche absteigende

Folge bauen, was weiß ich, nehme ich irgendeine Zahl und halbiere die immer oder sowas. So,

das also wohlfundiertheit. Jetzt Terminierung. Das war etwas, was wir letztes Mal schon diskutiert

hatten. Gegeben irgendein Terminungssystem, erreiche ich von jedem Term aus, wenn ich

also irgendeine nicht weiter eingeschränkte Folge von Umformungsschritten mache, immer

irgendwann ein Term, von dem es aus nicht weitergeht. Gut, wir haben glaube ich noch

nicht so ganz explizit gesagt, was wir mit einem Terminungssystem eigentlich meinen.

Was für Daten ein Terminungssystem besteht. Ein Terminersetzungssystem besteht aus zwei

Teilen. Das ist einmal die Signatur Sigma, die also festlegt, was für Terme ich hinschreiben

kann. Und dann dieses Pfeil Null, also die Grundreduktion, die ich einmal hinschreibe,

typischerweise, endliche Menge. So, das nur mal zur begrifflichen Klarheit. So, jetzt

definieren wir so ein paar Terminationsbegriffe. Und zwar zunächst mal für einen einzelnen

Term. Wir fragen uns, wann terminiert ein Term. Das kann ich beim Programm genauso machen.

Also ich kann mich bei einem Programm fragen, ob das schlechthin für alle Eingaben terminiert

oder ich kann mich fragen, ob ein Programm nun für eine konkrete Eingabe terminiert.

Und hier fangen wir erstmal an mit konkreten Eingaben, also mit konkreten Termen.

So, in Sachen Terminierung, da sind immer Begrifflichkeiten im Wettbewerb, die über

Terminierung reden und andere Begrifflichkeiten, die über Normalisierung reden. Im Bereich

der Termersetzung gewinnen meistens die Begriffe aus dem Bereich Normalisierung. Machen wir

hier auch so. Also wir nennen einen Term schwach normalisierend, wenn er folgende Eigenschaften

hat. Ja, das ist jetzt sehr schnell gesagt mit den Begriffen, die ich am Gegenende der

letzten Sitzung eingeführt habe. Ein Term heißt schwach normalisierend, ein Term t,

wenn er eine Normalform hat. So, und das kann man noch jetzt, indem man diese Definition,

also davon was es heißt, eine Normalform zu haben, noch ein bisschen aufblasen wieder,

also einmal auffalten. Das heißt, wenn ein Term s existiert, zudem t reduziert, in endlich

vielen eventuell keinen Schritt. Und dieser Term ist normal, reduziert also nicht noch

weiter. So, dann sind wir primär interessiert an einem noch stärkeren Begriff, nämlich

der, dass also t stärk normalisierend ist. So, das ist jetzt ein Begriff, der im Prinzip

genauso formuliert ist wie da oben, das mit der Wohlfundiertheit, außer dass ich bei

der Wohlfundiertheit praktisch verlange, dass nirgendwo eine unendliche absteigende Kette

existiert. Hier verlange ich es zunächst mal nur von meinem Term t, den ich gerade in

der Hand habe. Das heißt, ich verlange, es existiert keine unendliche absteigende Kette

bezüglich meiner Einschritt-Reduktionsrelation, die bei t anfängt. Gut. Ja, und jetzt praktisch