Ja Gut, dann werden wir heute

zwei Kernaussagen noch Pom benötigen,

über den einfach getubernetesem Landereon-Kalkül beweisen.

Eine langweilige, aber wichtige, die auch so typisch ist für das, was man in solchen Theorien immer sieht.

Deswegen machen wir es mal zur Illustration. Das ist die sogenannte Subjektreduktion.

Das ist gewissermaßen Typsicherheit. Das ist auch eine Frage, die stellt sich in dreckigeren Sprachen, wie zum Beispiel Java oder so.

In Java ist es ganz wichtig sicherzustellen, dass Dinge typsicher sind, dass also Dinge nicht während der Ausführung plötzlich ihren Typ verlieren.

In der Tat einige der wesentlichen Security-Attacken auf Java basierten auf Verletzungen der Typsicherheit.

Also wir zeigen jetzt gleich, dass der Lambda-Kalkül, der einfach getypte Lambda-Kalkül gewissermaßen typsicher ist.

Und das Aufregendere ist, wir zeigen starke Normalisierung, wie eingangs mal versprochen.

Also ich kann zwar im einfach getypten Lambda-Kalkül vergleichsweise wenige, muss man deutlich sagen, Programme nur hinschreiben,

aber die, die ich hinschreiben kann, die terminieren eben alle.

Gut. Ja, das, was ich eben unter dem Stichwort Typsicherheit verkauft habe,

läuft also technisch unter dem wesentlich weniger Aufmerksamkeit heischenden Namen Subjektreduktion.

Dann schon folge ich den Empfehlungen wieder nicht.

Also das etwas motivierendere Stichwort schreiben wir dann schon auch nochmal an die Tafel.

Also irgendwie einmal angeschoben hat, müsste es doch gehen.

Ja, ich schreibe einmal an, was die Aussage dazu eigentlich ist.

Der Satz von der Subjektreduktion, wenn man so will, Subject Reduction Theorem, der lautet, nehmen wir mal an,

wir hätten einen Term, der typisierbar ist mit einem Typ Alpha.

Und nehmen wir mal an, wir fangen an den auszuführen, eben also better zu reduzieren auf einen weiteren Term S.

Dann folgt, S hat ebenfalls diesen Typ Alpha.

So, nicht nochmal zurück auf Java, das heißt also, wenn ich irgendwie ein typkorrektes Java-Programm hätte,

und im Imperativen anfange das auszuführen, dann kommt nicht irgendwann zwischendurch was raus, was diesen Typ nicht mehr hat.

So, wenn man das jetzt so sieht, dann denkt man klar, was denn sonst?

Ja, selbstverständlich, wir verstehen ja schon Better-Reduktion als so eine Art Gleichungsumformung,

deswegen haben wir ja auch vorher Term-Ersetzungen gemacht, die ja auch nur eine Methode praktisch für Gleichungsumformung ist.

Und insofern, wenn T und S mehr oder weniger moralisch derselbe Term sind, dann sollten die ja hoffentlich dieselben Typen haben.

Aber Vorsicht, nach der Argumentation müsste es ja auch in der umgekehrten Richtung gelten.

Wenn ich auf einen Typ reduziere, der einen Term hat, dann müsste ich selbst den auch schon gehabt haben.

Also nach dieser Argumentation T und S sind moralisch derselben Term, also müsste T umgekehrt auch jeden Typen haben, den S hat.

Das ist nicht so. Was nehmen wir mal irgendwie?

Nehmen wir zum Beispiel mal hier so einen Term, der praktisch zweite Projektion ist.

Er nimmt zwei Argumente X und Y und gibt nur Y wieder zurück, X schmeißt er weg.

Und wenn wir den jetzt anwenden auf einen nicht typisierbaren Term, wie zum Beispiel dieses Omega, also lambda X.XX, das Ding haben wir gesehen ist nicht typisierbar,

der Beta reduziert in einem Schritt zu lambda Y.Y, also zur Identität und das Ding hat natürlich einen Typ, da brauche ich keinen Kontext hinzuschreiben,

weil das ein geschlossener Term ist, das Ding hat einfach Typ A nach A.

Wohingegen der Ausgangsterm hier nicht typisierbar ist und zwar deswegen, weil, gut das haben wir nie ausdrücklich als Lemma formuliert,

weil Typisierbarkeit abgeschlossen ist unter Untertermen. Man kann sich also schnell überzeugen, dass die Typregeln so gebaut sind,

dass wenn ein Term nach Typregeln typisierbar ist, dann auch alle seine Teilterme typisierbar sind.

Und dieser Term hier hat einen Teilterm, der nicht typisierbar ist, nämlich diesen hier, also ist er selbst als Ganze auch nicht typisierbar.

Das heißt also ungekehrt funktioniert es nicht, es geht nur vorwärts gewissermaßen.

Bevor wir diesen Satz jetzt beweisen, beweisen wir vorweg ein Lemma, das auch unabhängige Wichtigkeit hat.

Substitution ist ein fürchterliches Wort mit den vielen Ts.

Also das Substitutionslemma für Typisierung, also Substitutionslemma, da gibt es ja für alles mögliche.

Wir haben letztes Semester ein Substitutionslemma gesehen für zum Beispiel Auswertung von Termen und Formeln in Logik 1. Stufe.

Und hier gibt es auch ein Substitutionslemma für Typisierung, das lautet, es gibt es in zwei Formen,

weil ich jetzt zwei Sorten von Variablen habe, für die ich substituieren kann.

Ich habe einmal Typvariablen, für die kann ich Typen substituieren, und ich habe Individuen in Variablen, für die kann ich Terme substituieren.

Und für beide Varianten gibt es also ein Substitutionslemma.