Also ich habe jetzt noch zwei so ein bisschen vereinzelte Themen übrig aus dem Bereich des

getypten Lambda-Kalküls. Das erste, was jetzt hier auf dem Programm steht, ist die Subjektreduktion,

die ja im Moment so ein bisschen alleine dasteht, man kann sie auch für sich alleine motivieren.

Sie wird wieder auftauchen, wenn wir in ein paar Sitzungen später nochmal zum getypten

Lambda-Kalkül zurückgehen und für den getypten Lambda-Kalkül starke Normalisierung beweisen,

also jedes typisierbare Programm terminiert. Da werden wir diese Subjektreduktion wieder

brauchen. Und dann anschließend machen wir noch einen kurzen Ausblick auf den sogenannten

Curry-Howard-Isomorphismus, den wir mehrfach schon angedeutet haben, der Proofs are Programs

Isomorphismus. Und dann schwenken wir wieder zurück zum ungetypten Lambda-Kalkül und zeigen

für den praktisch Konfluenz. Das schaffen wir heute nicht mehr in Gänze, da werde ich also nur

einen Hilfsbegriff einführen und kurz illustrieren. So, wie gesagt, also erster Topic heute.

Erstes Thema heute kann man auf Deutsch ruhig sagen. Das erste Thema heute,

die sogenannte Subjektreduktion oder um das mal mehr mit Schlagwort zu sagen,

Typsicherheit. Ja, was heißt Typsicherheit? Typsicherheit heißt, dass ein Term, ein Typ,

den er mal hat im Laufe seines weiteren Lebens, sprich im Laufe seiner weiteren Reduktion nicht

verliert. Die Frage ist, wenn man das zum ersten Mal hört, was das denn mit Sicherheit zu tun hat.

Wenn man genau guckt, ganz viel. Man erinnere sich jetzt mal an Typen zum Beispiel in Java,

also gut so kompliziert wie in Java, also jetzt nicht kompliziert wie in Ausdrucksstärk, sondern

kompliziert wie in kompliziert, geht es hier ja nicht zu. Aber in Java ist in Typen so was

kodiert wie zum Beispiel, welche Felder von bestimmten Datentypen jetzt Publix sind und welche

nicht. Mittlerweile hat man die Typsicherheit von Java, glaube ich, einigermaßen im Griff.

Korrigieren Sie mich, wenn das nicht stimmt, aber die frühen Attacken auf Java, die funktionierten

zum Teil über das Typsystem, in dem genau nämlich Typsicherheit ausgehebelt worden ist und

plötzlich Sachen öffentlich waren, die nicht öffentlich gehören. Das heißt also, man hat ein

Interesse daran, was passiert mit dem Typ eines Ausdrucks, während ich das Programm, das einem

darstellt, tatsächlich ausführe. So, ich formuliere das jetzt nicht formal, das mache ich gleich noch.

Ich beginne stattdessen mit ein paar Lämmer da, die wir dazu brauchen und die auch, ja, die

relativ häufig gebraucht werden und die erstmal auch relativ selbstverständlich aussehen und auch

sind, zum Beispiel dieses hier. Also wir fangen an mit wieder mal einem Substitutionslämmer. Ja,

Sie haben öfter schon solche Substitutionslämmer-Tage gesehen, die also praktisch besagen, ja, wie

verhalten sich syntaktische und semantische Eigenschaften unter Substitution. Substitution

kann ja hier nur zweierlei heißen. Wir haben normale Variablen, für die wir substituieren

können und wir haben Typvariablen, für die wir substituieren können und wir fassen, also für

jedes gibt es ein Substitutionslämmer und wir fassen das hier unter einem Titel zusammen.

Das erste ist also das Substitutionslämmer für Typen. Das besagt, wenn wir einen Typ T in einem

Kontext Gamma mit einem Typ Alpha typisieren können, dann ist das stabil unter Typ Substitution mit

anderen Worten. Wenn wir eine Typ Substitution Sigma haben und die erstens natürlich auf den

Kontext anwenden und zweitens gleichzeitig, gleichzeitig auf den Typ, den unser Thermhalt

bekommt, dann ist das immer noch herleitbar. Und zweitens, das verschliesst, da sehe ich mal

mit dem Schlagwort Individuen, wie Individuenvariablen, also wenn wir eine Substitution haben

auf Individuenvariablen, dann sieht das folgendermaßen aus.

Das ist jetzt ein bisschen komplizierter. Also wir wollen substituieren für eine Variable in

einem Term T, den haben wir irgendwie typisiert. Für diese Variable, also wenn diese Variable hier

in T vorkommt, für die wir substituieren wollen, dann kommt die natürlich im Kontext vor,

sonst könnten wir T nicht typisieren. Und in diesem Kontext hat sie einen Typ Alpha. Wenn wir für T

was substituieren wollen und darunter Typisierbarkeit dann stabil bleiben soll, dann muss das, was wir

substituieren, natürlich den richtigen Typ haben, also Alpha. Das heißt, wir verlangen weiterhin,

dass in dem Kontext jetzt ohne das x, das x wollen wir ja wegsubstituieren, dann ist es nicht mehr da,

in dem Kontext ohne das x ein weiterer Typ S, den wir da jetzt einsetzen wollen, typisierbar ist mit

eben diesem Typ Alpha. Wenn das beides hinhaut, dann können wir gewissermaßen typ korrekt S für x