Wir haben heute eine Sitzung, wo wir genau wissen, was wir vorhaben.

Das ist mal was Schönes, wenn man einen Klumpen hat, der genau in eine Sitzung passt.

Wir erinnern uns, es geht um die Church-Rossa Eigenschaft im Lambda-Kalkül.

Das besagt, wann immer ich divergierende Reduktionen habe, laufen da die anderen.

Ich kann die verschiedenen Ergebnisse trotzdem immer wieder zu einem Redukt zusammenführen.

Das impliziert, wenn wir uns entsinnen, Eindeutigkeit der Normalform.

Church-Rossa impliziert generell in jedem Term Ersetzungssystem Eindeutigkeit der Normalform.

Wenn das hier schon Normalformen wären, dann reduzieren die ja nicht mehr echt.

Das heißt, müssen beide schon gleich diesem gemeinsamen Reduktier sein.

Die Church-Rossa Eigenschaft ist hier Determinismus.

Wir haben Programme, die wir eventuell auf verschiedene Arten ausführen können,

indem sich der Compiler womöglich an verschiedenen Stellen entscheidet, die Bettaredukte zu reduzieren.

Aber was rauskommt, wenn es normalisiert, ist in jedem Fall das Cell.

Es ist jetzt, was ich hier dazu sage, ein bisschen Cumbranosales zu nehmen,

weil echte Programmiersprachen nicht ganz genau per Bettareduktion auf Normalform reduzieren,

sondern ein bisschen was subtil anderes tun, aber so in etwa heißt es das.

Wir hatten uns schon in Erinnerung gerufen, dass wir zwar unser schönes Newman's Lemma haben,

was uns sagt, dass wir Church-Rossa auf die schwache Church-Rossa Eigenschaft oder in dieser anderen Begrifflichkeit

Konfluenz auf lokale Konfluenz reduzieren können, aber dazu brauchen wir starke Normalisierung,

und die haben wir hier nicht. Es ist also ein bisschen schwieriger.

Wir haben uns aber klar gemacht, dass man zumindest auf einer Seite hier den Stern weglassen kann,

das heißt nochmal, es reicht das sogenannte Streifenlemma, wo die Situation also die ist.

Ich habe hier an einer Einrichtung beliebig viele Bettareduktionen, aber in der anderen Richtung genau eine,

und die kann ich dann mit links und rechts jeweils beliebig vielen Bettareduktionen wieder zusammenführen.

Womit wir uns also den Rest der Sitzung befassen, ist der Beweis dieses Streifenlemmas.

Wenn wir das geschafft haben, gehen wir nach Hause.

Also, was ist die Situation, die wir da haben? Ich habe das da oben so sehr bezeichnungsfrei skizziert,

also ein Pfeil nach links, ein paar Pfeile nach rechts. Gut, geben wir uns für diese Situation mal Bezeichner.

Also, was haben wir? Wir haben hier auf der linken Seite einen Bettareduktionsschritt.

Was heißt das nun? Der findet in irgendeinem Kontext statt, C, und da haben wir also einen Bettaredex T,

der auf T-Strich reduziert, und wie gesagt, das Ganze in einem Kontext C.

Wir haben dafür ja im Rahmen des Beweises des Standardisierungssatzes uns Notationen noch verschafft,

also wir können das jetzt so schreiben, T reduziert ganz außen in einem Schritt zu T-Strich,

das U hier stand für outermost, das heißt, diese Notation steht für Wettareduktionsschritte, die ganz oben im Term stattfinden.

So, und dann haben wir hier rechts eine gewisse Anzahl Reduktionsschritte, die zu irgendeinem Term führen,

von denen geben wir mal einen Namen, S. Ne, aus irgendeinem Grunde S-Strich. Naja, gut, S wird wahrscheinlich noch gebraucht.

So, eigentlich hört sich jetzt ja die Aufgabe leicht an. Generell ist das ein Beweis, der ist relativ leicht zu verfolgen,

eigentlich er hat keine wirklich schwierigen Schritte, er startet ein paar Definitionen gleich aufeinander,

aber wie man sich dann merken muss während des Beweises, er hat nirgendwo echte Hürden vom Verständnis her.

Die Globalstruktur, was da eigentlich passiert in diesem Beweis zu verstehen, das ist mir persönlich auch noch nicht gelungen.

Man denkt eigentlich, das müsste ganz leicht sein, also wir haben hier einen Better Redux, den können wir reduzieren.

Oder wir machen erstmal was anderes. Dieser Better Redux stirbt dabei ja nicht, sondern der wird nur irgendwie so ein bisschen rumgereicht.

Der wird vielleicht dann, wenn er selber irgendwo in anderen Better Reduxen drin sitzt, mal verdoppelt oder verfünffacht.

Macht uns alles nichts, das kennen wir ja nur mittlerweile, dann reduzieren wir eben, wenn er sich verfünffacht hat, am Ende fünfmal.

Und vielleicht verändert sich in ihm noch der ein oder andere Teilterm, also zum Beispiel das Argument oder der Funktionskörper, die können ja better reduziert werden,

aber das kratzt mich ja nicht, dabei bleibt da ja ein Better Redux und ich kann ihn immer noch reduzieren.

Irgendwie so richtig sieht man nicht, warum das schwierig sein soll. Aber man muss eben ein bisschen Maschinerie auffahren, um das tatsächlich durchzudrücken.

Wir merken uns jedenfalls aus meiner dahinspekulierten Diskussion, was müssen wir machen?

Wir müssen irgendwie sehen, dass wir den Better Redux, den wir ursprünglich hatten, hier mitverfolgen.

Wir müssen sehen, was mit dem hier in dem S-Strich passiert ist, um dann passend hier ihn nach reduzieren zu können.