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

Ja, zusammenfassend kann man zur letzten Sitzung vielleicht noch sagen, es wird natürlich

nie jemand darum bitten, diesen Beweis des Normalisierungsatzes für Reduktionen zu

reproduzieren. Was Sie für Zwecke des Bestehens der Klausur und dergleichen mitnehmen sollten,

ist die Definition und ein Verständnis dieser Reduktionsstrategien. Also wie funktionieren

diese Strategien? Das geht auch hoffentlich jetzt nachdem wir Sie gegenüber letzten Semester

korrigiert haben. Sie stehen also das ist nämlich zum Beispiel etwas, was leider das ist nicht die

Schuld der Leute, die das aufgeschrieben haben, sondern meine eigene. Das stand also letztes

Semester nicht so ganz korrekt da. Also es war also korrekt an Beispielen vorgeführt und

korrekt erklärt, aber nicht ganz korrekt von der rekursiven Definition her. Das finden Sie also

dann in der neuen Version des Skripts dann auch korrekt, nur die ist noch nicht online.

So, ja nun mehr. Ja wir wenden uns nunmehr also zu dem sogenannten Einfach-Geprägsverfahren

am getypten Lambda-Kalkül. Kurz Lambda-Pfeil, weil ein Pfeil der Funktionentyp-Konstruktor

der einzige Typ-Konstruktor ist, der da vorkommt. Ja die Idee am getypten Lambda-Kalkül ist jetzt

von dieser wilden aufregenden Welt des ungetypten Lambda-Kalküls, wo ich revolutionäre Terme wie

Lambda x Punkt x x hinschreiben kann und so wieder wegzukommen. Das ist dann weniger

genialisch, aber funktioniert vielleicht besser. Das heißt, wir führen eben ein sogenannte Typen

für Terme. So und wir wollen die Terme einschränken, das setze ich jetzt mal so ein bisschen in

Anführungsstriche, was ich damit genau meine, wird im Laufe der Veranstaltung klar werden.

Und wir wollen eben die Terme einschränken auf sogenannte typisierbare Terme. Gut, um

ein bisschen jetzt ein Beispiel zu machen, muss ich einmal jetzt informell einführen, eben unseren

einzigen Typ-Konstruktor. Allgemein schreibe ich für Typen Meta-Buchstaben, also Meta-Variabeln

wie Alpha Beta und so weiter, also Anfang des griechischen Alphabets. Und aus zwei solchen Typen konstruiere

ich dann den Typ Alpha Pfeil Beta. Das ist der sogenannte Funktionstyp. Ja, was soll

das heißen? Das soll also sein der Typ der Funktionen von Alpha nach Beta.

Und dann wollen wir den Termen solche Typen zuweisen und wir wollen einen Term nur dann

als vernünftig in diesem Kalkül ansehen, wenn er eben in unserem System einen Typ bekommt.

Hier ist ein positives Beispiel. Lambda x Punkt x, also die einfachste sinnvolle Funktion,

die ich mir ausdenken kann, die sollte hoffentlich typisierbar sein, wenn ich nicht mal mehr das

darf, ja also einfach mein Argument wieder zurückgeben, dann habe ich offensichtlich

irgendwas falsch gemacht. Und in der Tat, das bekommt einen Typ der Form A nach A. Ja,

warum A und nicht natürliche Zahlen? Nun, das hier, das funktioniert natürlich ohne

Rücksicht darauf, was x jetzt ist. Also x könnte eine natürliche Zahl oder ein Buhlcher

Wert oder eine Funktion sein. Ja, also diese einfache Operation, mein Argument einfach

wieder zurückgeben, das kann ich natürlich mit allem machen. Welchen Java würde das

heißen? Das ist eine Funktion auf dem Typ Object, nicht? Oder auf der Klasse Object.

So, dieses Ding hier, das ist eine Typvariable. Das heißt, wir haben in unserem Typsystem

Variablen für Typen, für die wir später andere Typen einsetzen können.

Ja, und mal vielleicht ein negatives Beispiel. Dieser etwas komische Term hier, der sich

sein Argument nimmt und das Argument auf sich selbst anwendet. Der hat, wie sich zeigen

wird, keinen Typ. Das ist aber so ein bisschen subtil. Sie werden, wenn Sie ein bisschen

vorgeblättert haben, auf dem Übungszettel gebeten, einen Typ für dieses Ding herzuleiten

und das ist nicht, weil wir Sie ärgern wollen und daneben stehen uns die Hände reiben,

wenn Sie es nicht hinkriegen, sondern das findet statt in einem stärkeren Typsystem

als in diesem einfach getypten Lambda-Kalkül und in diesem stärkeren Typsystem kann man

das Ding typen. Ich schreibe also mal dazu in Lambda-Pfeil. Ja, nicht? Und dann wird

da eben ein noch schlimmerer Term angegeben. Das hier, erinnere ich, war ja Omega. Und

dann wird da nochmal dieser nicht terminierende Term hergenommen, Omega, angewendet auf Omega

und der hat noch nicht mal in dem stärkeren System einen Typ. Also kurz, welche Terme

einen Typ haben und welche nicht, hängt ab von der Stärke des Typsystems. Und das hier