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

Wir haben uns letztes Mal mit Terminierung vom Thermoersetzungssystem befasst.

Das ist eine von zwei großen wichtigen Eigenschaften, für die man sich bei

Thermoersetzungssystem interessiert. Die andere kommt heute.

Ich mache das heute so ein bisschen in Galopp und lasse insbesondere,

was ich normalerweise nicht tue, zwischendurch meinen Beweis raus.

Das holen wir beim nächsten Termin nach. Ich muss das Material heute durchkriegen,

sonst können sie nicht oder zumindest dann nicht, wenn sie ein falsches Taktitorium haben,

den Zettel lösen. Deswegen sehen wir zu, dass wir zumindest die Definition und Resultate kriegen.

Die zweite Eigenschaft ist also etwas weniger eingängig als der Begriff Terminierung.

Ich meine, unter Terminierung können wir uns alle das vorstellen. Confluence ist auch

leicht zu veranschaulichen. Wir haben einen Fluss, wir kommen mit dem Boot angefahren,

können nach links und nach rechts fahren. Und siehe da, ob wir nach links oder nach rechts fahren,

ist egal. Das ist Confluence. Etwas formaler habe ich einen Term T.

Ich kann den umschreiben mittels meines Thermoersetzungssystems.

Einerseits in einen Term S, vielleicht in mehreren Schritten, das deutlicht mit dem Stern an.

Andererseits nehme ich irgendwelche anderen Reduktionen anwende in einen Term S'.

Confluence heißt, es gibt jetzt einen Term Q, so dem ich diese beiden Möglichkeiten S und S'

nicht wiederum reduzieren kann, sodass ich also wieder bei einem und demselben ankommen.

Wiederum, wir gehen in mehreren Schritten.

Das ist also Confluence. Das ist eine Eigenschaft, die ein Term-Ersetzungssystem haben kann,

aber nicht muss. Und wenn es sie hat, ist das sehr vorteilhaft.

Das Ganze jetzt noch mal als formale Definition.

Wir nehmen uns ein kleiner Ersetzungssystem her, T.

Wir definieren zunächst mal, zur kürzeren Formulierung, diesen Teil des Diagramms für zwei Terme S und S'.

Wenn wir so ein Diagramm malen können, über die untere Hälfte, dann nennen wir diese beiden Terme S und S' zusammenführbar.

Dann wird es kurz ZF.

Wenn es nur ein Q existiert wie um, das heißt, sowohl S als auch S' reduzieren zu können.

Und zwei Terme heißen zusammenführbar, wenn ich sie auf einen und demselben Term reduzieren kann.

Jetzt kommen zwei Eigenschaften, die nun das Term-Ersetzungssystem selbst haben kann.

Hier nennen wir Confluent. Das kürzen wir ab mit CR, nach den Herrschaften George und Rossa, die diese Eigenschaft mehr oder weniger erfunden haben.

Eine andere Nadel für Confluent ist sich schlicht und einfach George Rossa.

Wenn für alle T, S und S' wie im Bild der Gestalt das T sowohl zu S als auch zu S' reduziert, eventuell in mehreren Schritten, dann...

...S und S' zusammenführbar sind.

Das ist also einfach nur die Formalisierung von dem Bild.

Die zweite sehr ähnliche Eigenschaft nennen wir Lokal Confluent.

Abgekürzt Weakly George Rossa, WCA.

Dann kommt dieselbe Definition mit einem einzigen Unterschied.

Ich ersetze hier die Mehrschrittreduktion durch die Einschrittreduktion.

Das heißt, ich habe dasselbe Diagramm wie da oben.

Ich verlange dieses Zusammenführen nur für solche Kader S und S' die ich von T aus in genau einem Schritt jeweils erreicht.

Und wenn ich das zusammenführen, darf ich sie dann wieder in mehreren Schritten.

Warum ist das überhaupt eine Eigenschaft für die man sich interessiert?

Nehmen wir uns einmal die eine Anwendung, die wir uns als Motivation für Thermoersetzungen angesehen hatten.

Man kann die Thermoersetzung einfach programmieren.

Dann entspricht diese George Rossa Eigenschaft mehr oder weniger einem Determinismus.

Eine andere Motivation war das Computer-Algebra-System.

Wenn ich dann für Rossa und auch für eine starke Normalisierung habe, kann ich die Gleichheit von Thermen entscheiden, indem ich sie normalisieren.

In dem Moment bekomme ich eine entscheidbare Karte.

Ein Beispiel ist die Theorie der Gruppen.