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

Also ein GLOLOB betraf das typischerweise beweisbare Formeln.

Also wenn ich irgendwelche Formeln hingeschrieben hatte, durfte ich dann andere Formeln hinschreiben.

Und ich habe das gelesen als Beweisbarkeit im Sinne von, wenn ich eine Formel beweisen kann, dann ist sie gültig.

Das gibt es auch anders. Das gibt es zum Beispiel für Erfüllbarkeit.

Typische Tablokalküle haben dann hier Prämissen, das sind Formeln deren Erfüllbarkeit, nicht etwa Gültigkeit,

die ich schon gezeigt habe und wenn ich was hier unten hinschreibe, dann zeige ich praktisch davon Gültigkeit.

Oder muss es noch zeigen, das kann sogar eine Weitbeweisverpflichtung bedeuten.

Und in unserem Falle, wie wir es hier im einfach getübten Lambda-Kalkül gesehen haben, waren das halt solche Typisierungsaussagen.

Etwas von dieser Form, was also besagte, in einem gegebenen Kontext hat ein gegebener Term einen gegebenen Typ.

Das heißt, ich habe immer so ein Kalkülformat, also ich habe eine bestimmte Form für die Aussagen, die ich hier oberhalb, unterhalb des Strichs hinschreiben darf.

Es kommen eben eventuell dazu die Seitenbedingungen, die man deswegen an die Seite schreibt, weil sie nicht in den Kalkül passen.

Da stehen zum Beispiel Bedingungen an freier Variablen drin oder so etwas oder nähere Beschreibungen des syntaktischen Materials.

In ganz schlimmerhaftigen Fällen wie Separation Logic oder so stehen da semantische Seitenbedingungen, dann wird es ganz böse.

Jedenfalls, in den Seitenbedingungen steht also alles, was nicht im Kalkül ausgedrückt ist.

Ja, und das ist einfach nur das Grundwesen einer Regel.

Also eine Regel sagt mir praktisch, wenn ich das hingeschrieben habe, was oberhalb der Regel steht, kann ich das hinschreiben, was unterhalb der Regel steht.

Und das ist letztlich nur eine syntaktische Disziplin, die mir sagt, welche Strings darf ich hinschreiben.

Gut. Ja, wenn Unklarheiten entstehen dieser Art, immer gerne nachfragen.

So, wir haben heute, wenn ich damit den Aufarbeitungsteil abschließe und also jetzt wieder zum Fortlauf des Materials zurückkehre,

ein recht klar gestecktes Ziel. Wenn wir das fertig haben, gehen wir nach Hause.

Und zwar ist das der Beweis des Satzes von Church Russell.

Wir haben ja den Ausdruck Church Russell schon gehört im ersten Kapitel über Thermersetzungssysteme.

Ich erinnere nochmal, wie sah das aus? Church Russell war diese Bedingung hier.

Wenn ich zwei in zwei Richtungen auseinander laufende Reduktionssequenzen habe, die vom selben Therm ausgehen,

dann kann ich die wieder zusammenführen. Mit anderen Worten, es existiert ein vierter Term,

zu dem diese beiden Redukte ihrerseits gemeinsam reduzieren.

Wir hatten das auch genannt Konfluenz, und dieses Diagramm illustriert sehr schön, was das heißt.

Es ist egal, ob ich links oder rechts an der Flussinsel vorbeifahre, am Ende komme ich am anderen Ende der Flussinsel an, egal was ich mache.

Und davon gab es dann eine Version, die nannte sich Schwache-Church-Wasser-Eigenschaft oder lokale Konfluenz.

Das ist genau dasselbe Diagramm, aber jetzt habe ich hier in jeder Richtung nur genau einen Reduktionsschritt.

Hier der Stern bedeutet, es sind beliebig viele.

So, ich habe ein paar

Also beliebig viele heißt insbesondere meinetwegen einer, aber natürlich nicht umgekehrt.

Das ist genau das selbe Diagramm, aber jetzt habe ich hier in jeder Richtung nur genau einen Reduktionsschritt.

Hier der Stern bedeutet, es sind beliebig viele.

So, ich habe also eine einfache Aufgabe. Ich habe hier eine speziellere Situation als da.

Also beliebig viele heißt insbesondere meinetwegen einer, aber natürlich nicht umgekehrt.

So, und diese beiden einzelnen Schritte, die soll ich dann wieder in beliebig vielen Schritten zusammenführen können.

Das ist lokale Konfluenz.

Und unser entscheidendes Werkzeug, auch in den Übungen, wo wir also Konfluenz von Systemen gezeigt haben, war Newman's Lemma.

Das besagt, wenn ich stark normalisierend bin und weak Church-Rossa habe, dann habe ich auch Church-Rossa.

So, das ist ja alles so ganz töfte, aber der Lambda-Kalkül, der ist ja nun mal nicht stark normalisierend.

Also mit mal eben Newman's Lemma anwenden ist also nichts. Da muss man sich was anderes ausdenken.

So, und was man also stattdessen tut, ist,

man beweist stattdessen das sogenannte Streifen-Lemma.

Das ist jetzt meine freie deutsche Übersetzung des englischen Wortes Strip-Lemma.

Das ist so eine Art Mittelding zwischen Church-Rossa und Newman's Lemma.

Das ist so eine Art Mittelding zwischen Church-Rossa und schwachen Church-Rossa, also zwischen Konfluenz und lokaler Konfluenz, nämlich,

ich mal es mal extra so ein bisschen asymmetrisch, erstens, damit man den Unterschied sieht und zweitens, damit man das Wort Streifen-Lemma versteht.