Dieser Begriff wird eingefangen in der folgenden Definition.

Wir nehmen uns hier ein Time-Ersetzungssystem T mit Signatur Sigma und Reduktionsregeln Pfeil 0.

Zwei Sigma-Terme S und T heißen zusammenführbar, kurz ZF.

Wenn es einen dritten Term U gibt, zudem sowohl S als auch T in beliebig vielen Schritten reduzieren.

Als zweites kommt jetzt schon der oben genannte Begriff der Konfluenz.

Das ist eine Eigenschaft des Term-Ersetzungssystems als Ganzes.

Also wir sagen T sei Konfluent, wenn Folgendes gilt,

beziehungsweise Confluent bzw. Cr für Church und Rossa.

Es ist blöd mit den Bindestrichen, weil man nicht weiß, ob das eine oder zwei Personen sind.

Wir definieren diesen Begriff der Konfluenz.

Wenn eine bestimmte Eigenschaft wieder für alle Terme S und T gilt,

ist es, dass beide Redukte ein und desselben Term sind.

Das ist dieses Bild hier oben in eine Formale Definition gegossen.

Die Ausgangssituation ist diese hier oben.

Dann Reduktion in eventuell mehreren Schritten zu S einerseits und T andererseits.

Dann reduziert hier unten ein Term V, sodass sowohl T als auch V in eventuell mehreren Schritten zu V reduziert.

Das ist das mit der Konfluenz.

Das ist ein schönes Kriterium, von dem man auch viel hat.

Wenn man sich jetzt vorstellt, man müsste vom Terme-Ersetzungssystem zeigen, dass es Konfluent ist,

dann sieht diese Aufgabe erstmal ein bisschen unangenehm aus,

wegen dieses Quantors hier über S und T, die jeweils Redukte in beliebig vielen Schritten von dem U aus sind.

Ich muss also praktisch für jedes U in den Griff bekommen, sämtliche Terme zu denen das reduziert.

Und mir für jeweils zwei Terme, die ich mir aus dieser eventuell riesigen Menge herausgreife, zeigen,

dass die wieder zusammenführbar sind. Das könnte im Zweifelsfalle anstrengend werden.

Deswegen kommt jetzt ein einfacherer Begriff.

Wir sagen, T sei lokalkonfluent oder mit Abkürzung WCR wie weekly Charles Rossa.

Das liest sich jetzt fast genauso wie die Definition von Vollerkonfluenz.

Ich mache also insbesondere wieder eine Aussage über alle Paare von Termen S, T mit,

und jetzt kommt der subtile Unterschied. S und T sind Redukte eines gemeinsamen Ausgangsterms in genau einem Schritt,

also ohne Stern. Und von solchen Termen verlange ich dann wieder, dass sie zusammenführbar sind.

Das können wir wieder mit Diagrammen malen. Ich habe hier also wieder Reduktionen ausgehend von einem gemeinsamen Ausgangsterm U,

einmal zu S, einmal zu T, ohne Stern hier, also in einem Schritt.

Und dann soll wieder ein V existieren, zu dem sowohl S auch T jeweils reduzierbar sind, jetzt wieder in beliebig vielen Schritten.

Wir wissen noch nicht, was wir von dieser Aussage haben, und es wird ein bisschen anstrengender zu zeigen,

dass wir von dieser Aussage was haben, aber man sieht auf jeden Fall schon die Aufgabe, die wir hier haben,

und das ist jetzt zunächst mal deutlich angenehmer. Was wir dazu geworfen kriegen, sind also von einem fixen Term U ausgehend

nur die Dinge, die ich durch Anwendung einer einzelnen Umformungsregel bekomme. Da habe ich noch Hoffnung,

dass ich das vielleicht irgendwie in den Griff bekomme. Ich gucke mir halt den Term an, welche Gleichungen kann ich anwenden, welche nicht.

Man hat irgendwie das Gefühl, das würde man hinkriegen können. Und in der Tat können wir es noch ein bisschen weiter vereinfachen,

wie wir später sehen werden. Das heißt also, das hier ist ein handhabbares Kriterium, wir müssen dann nur sehen, in welchem Verhältnis die zueinander stehen.

So, wir halten noch mal ein kurzes, also Lemma verdient das Ding nicht als Namen, sondern

ein kurzes Faktum über Zusammenführbarkeit fest, nämlich wenn S zu T reduziert,

und dann halten wir noch mal ausdrücklich fest, zum Beispiel, dann wenn S und T tatsächlich gleich sind, also syntaktisch gleiche Terme,

dann reduziert nämlich S in gar keinem Schritt zu T, Stern heißt ja beliebig viele Schritte, inklusive eventuell keiner.

Dann sind S und T zusammenführbar, nämlich zu welchem Term?

Ja, T, danke, sind zusammenführbar zu T. Man muss dann eben schon auch mal frech sein und die Diagramme malen.

Also hier haben wir nach Voraussetzung das S zu T reduziert und hier haben wir aber auch das T zu T reduziert, halt in keinem Schritt.

Gut.

So, ich schreibe jetzt gleich mal als Satz hin das Verhältnis zwischen diesen beiden Begriffen, Church Russell und Weekly Church Russell,

oder eben Confluent und Lokal Confluent. Ich werde den heute wahrscheinlich nicht mehr beweisen, sondern erst in der nächsten Sitzung.