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

Ja heute ist so ein wunderschöner Tag. Wir machen

wir den Beweis der Church-Rosser Eigenschaft für den ungetypten Lambda Kalkül. Und wenn wir damit

fertig sind gehen wir nach Hause. Nein jetzt noch nicht. Ich beginne mit einer kurzen Erinnerung

negativer Natur. Wir machen das Ganze für den ungetypten Lambda Kalkül. Das macht man sich

fragen. Jetzt haben wir also mühsam diese Typen eingeführt. Warum machen wir das nicht im getypten

Lambda Kalkül? Es ist eine rein syntaktische Eigenschaft von Betareduktion. Das heißt, wenn

wir es für den ungetypten Kalkül zeigen, dann erben das alle getypten Kalküle, sofern sie

Subject Reduction haben, wie wir es ja für den einfach getypten Lambda Kalkül schon gezeigt haben.

Subject Reduction bedeutet insbesondere, dass ich jede Reduktion eines getypten Terms, die ich im

ungetypten Kalkül hinkriege, auch im getypten Kalkül machen kann, weil ich die Typen unterwegs

beim Reduzieren nicht verliere. Dank Subject Reduction überträgt sich das also hier auf den

getypten Lambda Kalkül. Der ungetypte Lambda Kalkül hat nun aus Sicht von Konfluenzbeweisen oder

eben Beweisen der Church-Russer-Eigenschaft einen entscheidenden Nachteil. Der ist nicht stark

normalisierend, wie wir gesehen haben. Er ist noch nicht mal schwach normalisierend. Also es gibt

Terme, die haben überhaupt keine Normalfunktion. Mit anderen Worten, wir haben New Man's Lemma nicht

zur Verfügung. Es wird uns relativ leicht fallen, lokale Konfluenz zu zeigen, das wäre nicht weiter

schwer, aber das hilft uns nichts, weil der Kalkül nicht stark normalisieren ist. So und nochmal das

explizit von eben. Also dank Subject Reduction erbt der einfach getypte Lambda Kalkül diese

Church-Russer-Eigenschaft, wenn wir sie denn gezeigt haben, vom Ungetypten. Im einfach getypten

Lambda Kalkül hätte man andersrum allerdings das Leben auch deutlich einfacher. Nur so weit sind

wir noch nicht. Wir werden ja vom einfach getypten Lambda Kalkül werden wir noch zeigen, der ist stark

normalisieren. Wir werden sogar von einem noch viel stärkeren System zeigen, dass es stark

normalisierend ist. Und dann haben wir den New Man natürlich wieder und dann reicht es uns lokale

Konfluenz zu zeigen, was viel einfacher ist. Aber beweist dann, wenn man kann, gerne starke

Resultate und das stärkste Resultat ist jetzt eben der ungetypte Lambda Kalkül, der nicht stark

normalisierend ist. Es ist trotzdem immerhin noch Church-Russer. Also wir formulieren es einmal,

Missverständnis zu vermeiden, ausdrücklich und klar als Satz. Der ungetypte Lambda Kalkül ist

Church-Russer, natürlich bezüglich Better-Reduktion. Es war uns schon mal aufgefallen, dass die

Konfluenz eigentlich zu stark formalisiert war. Wir hatten ja so verschiedene Diamantenförmige

Diagramme, das war das für Konfluenz. Wenn wir in beiden Richtungen mehrere Reduktionsschritte

machen, dann können wir die später wieder zusammenführen. Das war CR. Dann gab es dasselbe mit

jeweils nur einen Reduktionsschritt in jeder Richtung. Das ist lokale Konfluenz oder eben

WCR wie Weak Church-Russer. Es war uns schon mal aufgefallen, dass wir für die Zieleigenschaft,

nämlich Eindeutigkeit der Normalform, eigentlich nur die Variante brauchen, wo der Stern nur auf

einer Seite steht. Wo wir also nur einmal beliebig viele Reduktionen haben, auf der anderen Seite

genau eine. Das kommt jetzt. Es kommt jetzt das sogenannte Streifenlämmer. Das Streifenlämmer

ist das eigentlich zentrale Resultat, was wir jetzt bezeigen, aus dem unser Hauptsatz

dann sofort folgt. Das ist genau von dieser Form. Wenn ich hier beliebig viele Better-Reduktionen

habe eines Terms und hier nur eine, dann kann ich die wieder zusammenführen. Deshalb gibt

es einen gemeinsamen Redukt der beiden Seiten. Machen wir uns erstmal klar, warum uns das reicht.

An Beweis davon, warum uns das reicht, sieht man auch, warum das Streifenlämmer heißt.

Die Zusammenführungen sind bei allen diesen Varianten immer in beliebig vielen. Zusammenführen

darf ich immer in beliebig vielen Schritten, inklusive immer auch eventuell gar keinen.

Ich mal die Situation hin, die ich dann im Allgemeinen Fall für die Konfluenz, also

Fossil Search Wasser habe. Ich habe hier eine Reduktion in eine Richtung, die male ich mal

einfach mit dem Stern. Die andere male ich mal so ein bisschen expliziter. Da finden

dann mehrere Schritte statt. Jetzt habe ich mal vier gemalt. Wie hilft mir das Streifenlämmer

dabei? Nun, hier habe ich einen Schritt und hier beliebig viele. Die kann ich zusammenführen.

Ich sage hier dasselbe. Beliebe ich viele Schritte und ein. Und so weiter. Ich reduziere es mal