Ja, herzlich willkommen. Heute kann es zumindest die Kreide nicht zerbröseln.

Ja, wir machen jetzt noch einen von eigentlich zwei Nachträgen aus dem ungetübten Lambda-Kalkül,

die ich also jetzt zurückgestellt hatte, damit Herr Rauch seine Zettel bearbeitungsfertig rausbringen

kann. Das wäre gewesen erstens der Standardisierungssatz und zweitens der

Satz von Church-Rosser. Wenn ich es im Moment richtig abschätze, werden wir den

Standardisierungssatz zu beweisen wahrscheinlich nicht mehr schaffen.

Wir beweisen stattdessen den Satz von Church und Rosser. Ich habe deswegen den

Satz von Church-Rosser ausgewählt, weil der Beweis schon doch auch irgendwie in

dem Falle ein bisschen informative ist. Der Beweis des Standardisierungssatzes ist

da... Also erstens kann man hier nur mit Lücken präsentieren, weil da für eine

zweistündige Sitzung für vollständige Präsentation halt zu lang ist. Man muss

dann gewisse Lämmer da zwischendurch glauben und da wird es insgesamt auch

einfach irgendwie uninformativ. Man zuckt so am Ende mit den Schultern. Der Beweis

des Church-Rosser-Satzes ist dagegen eine vergleichsreiseangenehme Sache. Ja, worauf

will ich hinaus mit dem Satz von Church-Rosser?

Wir haben ja die Church-Rosser Eigenschaft schon eingeführt, als wir

über Termersetzung gesprochen haben. Und im Kapitel über Termersetzung haben wir

die Church-Rosser Eigenschaft. Das ist im Wesentlichen dieser Diamant hier.

Wenn ich beliebig viele Schritte in eine Richtung reduzieren kann und beliebig

viele Schritte in eine andere Richtung reduzieren kann, dann kriege ich das

wieder zusammengeführt. Das ist die Church-Rosser Eigenschaft. Die hatten wir

hergeleitet aus einer schwächeren Eigenschaft, wo das hier nur verlangt wird

für den Fall, wo ich hier ausgehend von meinem Ursprungspunkt in irgendeine

Richtung einen Schritt reduziere, in irgendeine andere Richtung ebenfalls

genau einen Schritt reduziere. Das muss sich zusammenführen können.

Diese Eigenschaft heißt

Weekly Church-Rosser oder Lokalkonfluent hatten wir gesagt. Das hier

hieß Konfluent, das hier hieß Lokalkonfluent. Und um jetzt aber aus der

schwachen Konfluenz oder lokalen Konfluenz die Konfluenz folgern zu können,

musste man starke Normalisierung reinstecken. Das war Newman's Lemma.

Starke Normalisierung plus lokale Konfluenz impliziert Konfluenz. Wenn wir

das jetzt auf den Lambda-Kalkül anwenden wollen, dann bekommen wir das Problem,

dass nun eben genau diese starke Normalisierung eben im Allgemeinen nicht

gilt. Wir haben Terme, die keine Normalform haben und die noch nicht mal

schwach normalisierend sind, wo ich beliebig lange in welche Richtung auch

immer vor mich hin reduzieren kann und nie eine Normalform erreichen.

So, das heißt dieser Satz von Church-Rosser, der hat schon so ein

bisschen mehr Gehalt. Der Satz von Church-Rosser, der sagt, besagt eben genau

diese Eigenschaft hier, die volle Konfluenz, die gilt, obwohl starke

Normalisierung nicht gilt, im Lambda-Kalkül eben doch. Also ich kann das

im Lambda-Kalkül zeigen. Ich kann es natürlich nicht mittels

Newman's Lemma zeigen. Ich muss mir irgendwas anderes ausdenken.

So, jetzt malen wir also einmal noch einmal den Zielsatz hin.

Also wir schreiben hin, der Lambda-Kalkül ist Church-Rosser. Also das ist der Satz

von Church-Rosser. So haben Church und Rosser das natürlich nicht formuliert.

Also mit anderen Worten im Lambda-Kalkül gilt diese Eigenschaft hier. Und wir

reduzieren das Ganze, indem wir scheinbar so einen Kompromiss zwischen diesen

beiden Eigenschaften hier finden. Also ganz naiv gesagt sehe ich hier in der

Church-Rosser-Eigenschaft zwei Sterne oben. Ich sehe insgesamt vier, aber im

entscheidenden Teil sehe ich also zwei. Und in der schwachen Church-Rosser-Eigenschaft