Sie können sich sicher erinnern, dass wir uns letzte Woche mit der Terminierung von

Thermersetzungssystemen beschäftigt haben. Das heißt insbesondere, wir haben uns eine

wichtige Frage gestellt, wenn ich bei so einem Thermersetzungssystem irgendwo an einem Punkt

anfange und einfach mal so wild drauf los reduziere, komme ich dann irgendwann an einem Punkt an,

wo ich aufhören kann, also wo ich sogar aufhören muss. Und wir haben aber in unserem Eingangsbeispiel

letzten Montag auch schon festgestellt, dass man sich noch eine zweite wichtige Frage stellen kann,

nämlich wenn ich einen anderen Weg gehe, komme ich dann auch wieder am selben Punkt heraus,

also komme ich auf diese selbe Normalform, was natürlich wichtig ist bei Dingen wie,

wenn wir Arithmetik betreiben, wenn ich erst umklammere und dann addiere, dann sollte natürlich

das gleiche herauskommen, wie wenn ich sofort addiere und dann erst die Klammern auswerte.

Und das lässt sich alles zusammenfassen unter dem Begriff der Konfluenz.

Das habe ich jetzt vielleicht ungünstig gemacht, naja, egal.

Also die Überschrift für diese Woche lautet Konfluenz und Eindeutigkeit von Normalformen.

Und

die Begriffe der Konfluenz und eines etwas schwächeren Begriffs sind relativ knapp zu

fassen und auch leicht zu verstehen. Das heißt, die können wir uns auch sofort mal aufschreiben

und uns dann damit beschäftigen, wie wir von einem System nachweisen können,

dass es diese Eigenschaft auch hat. Also wir geben uns wieder ein Thermesetzungssystem vor.

Das besteht aus, wie schon wie immer aus einer Signatur und einer Schrittreduktion,

Fall Null. Und in so einem System heißen zwei Terme zusammenführbar, also zwei Terme S und T.

Und das kürzen wir oft mit ZF ab, damit wir nicht dauernd das lange Wort schreiben müssen.

Wenn folgendes gilt.

Wenn ein U existiert, also ein weiterer Term, zudem sowohl S als auch T reduzieren,

in beliebigen vielen Schritten.

Und das kann man jetzt, diesen Begriff der Zusammenführbarkeit kann man jetzt ganz einfach

auf das ganze System übertragen. Deshalb zweitens, unser System T heißt Konfluent.

Und das wird üblicherweise abgekürzt mit CR, was die Abkürzung für den Namen der Erfinder

dieses Begriffs ist, nämlich Charge und Rosser.

Wenn alle Terme S und T, die von einem gemeinsamen Term U aus abgeleitet werden können, zusammenführbar sind.

Das heißt, ich starte von irgendeinem U, das ist auch allquantifiziert hier implizit.

Ich starte von diesem U, erreiche zwei verschiedene Terme, das habe ich hier oben ja auch im Prinzip aufgemalt.

Also wenn man an irgendwelchen Punkten hier in diesen Ketten anhält, und dann verlange ich,

dass diese Terme, bei denen ich angelange, auch wieder zusammenführbar sind.

Das heißt, dass ich wieder auf einen gemeinsamen Punkt komme.

Ja?

Nein, auf einem beliebigen anderen Term, richtig.

Also das ist nur Zufall, dass das hier der gleiche Buchstabe ist.

Also die Definition ist relativ simpel, aber wenn man sich anschaut, wie viele Quantoren wir hier haben,

also wir haben irgendwie ein Quantor über diese, also für jedes U, also für jeden Term in unserem System,

müssen wir uns alle Terme anschauen, die davon abgeleitet werden können und unterschiedlich sind,

und müssen davon dann beweisen, dass die zusammenführbar sind.

Also wieder ein Quantor, dass ein U existiert, sodass wir da hinkommen.

Also das sieht es relativ schlecht aus, wenn wir direkt versuchen, ein System uns herzunehmen und das einfach zu beweisen.

Ja, da werden wir ziemlich lange beschäftigt sein.

Deswegen führen wir jetzt sofort einen schwächeren Begriff ein, und zwar den der lokalen Konfluenz.

Und das wird dann eben abgekürzt mit BCR für weekly charge roster.

Genau dann wenn, und jetzt sieht das erstmal so ähnlich aus wie hier.

Also auch über alle Terme S und T quantifizieren, und jetzt kommt der kleine Unterschied.

Wir verlangen nicht, dass hier in beliebig vielen Schritten von einem U zu S und zu T übergegangen werden darf,

sondern wir sagen, das muss genau ein Schritt sein.