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

System F ist stark normalisierend. Wir haben das schon ein paar mal angekündigt und ich habe auch

schon hinreichend betont, dass das eine relativ erstaunliche Tatsache ist, wenn man sich anschaut,

wie viele Funktionen man in System F typisieren kann. Nämlich im Wesentlichen alle diejenigen,

von denen man in Second Order Arithmetic beweisen kann, dass sie terminieren.

So der Beweis ist nicht fürchterlich schwer. Er basiert auf einer originellen Idee und zwar

einer praktisch induktiven Invariante von Typen, die man durchdrückt.

Und zwar genauer gesagt nicht der Typen selbst, sondern einer Semantik, die man für diese Typen

definiert. Wir haben jetzt nicht fürchterlich viel Semantik gemacht, aber wir erinnern uns

alle an die Semantik von Logik erster Stufe. Wie war das? Gut, wir haben also irgendwie

einen Grundbereich und alles lebt auf diesem Grundbereich. Und genau so funktioniert das hier

auch. Und zwar ist der Grundbereich auf dem alles lebt die Menge Sn soll heißen die Menge aller

stark normalisierenden Lambda-Termen. Definieren können wir ja vieles. Wir wissen zwar nicht,

ob so ein Termin stark normalisierend ist, wenn wir ihn sehen, aber wir können mal definieren,

die Menge aller Terme, für die das halt der Fall ist. Stark normalisierend heißt jede

Reduktionssequenz beginnend mit diesem Terminiert. So und wir interpretieren jetzt die Typen als

Teilmengen dieses Universums. Die schreiben wir wieder so und nicht mit unseren Semantikklammern,

wie wir das immer tun bei Semantik. Die sollen einfach dann Teilmengen davon sein.

Ja und wir erwarten schon, dass das vielleicht noch nicht alles ist, also dass wir einem Typen

eine Semantik so direkt zuweisen. Ja, denn in dem Typen kommen ja Variablen vor, Typvariablen.

Und man müsste schon so konditioniert sein, dass man jetzt erwartet, ja das ganze wird

wohl abhängen von einer Interpretation der freien Typvariablen. So das heißt das Ding hier kriege

ich noch mal ein Index, Index Xi. Das habe ich hier doch nicht genug Platz freigelassen.

So also gegeben ein Typ und gegeben eine Valuation für die in ihm vorkommenden Typvariablen,

was das genau heißt, das kommt jetzt später. Also gleich, wenn wir genau gesagt haben,

was die Werte sind, die wir den Typvariablen zuweisen. Also abhängig jedenfalls von einer

vorhandenen Interpretation der Typvariablen interpretieren wir die Typen als Mengen,

die eben in diesem Gesamtuniversum der stark normalisierenden Terme leben.

Und die Schlüsselidee ist dann die, dass wir bezüglich dieser Semantik Korrektheit des

Typsystems zeigen. Das heißt, das heißt, wann immer wir so ein herleitbares Typisierungsstatement

haben in Kontext Gamma hat T Typ Alpha, dann soll dasselbe semantisch gelten. Das deute ich eben

wie üblich jetzt durch einen Doppelquerstrich an. Das haben wir noch nicht definiert, was das heißt,

das kommt noch. Und das hier lesen wir so ungefähr, ein genaueres kommt gleich, so ungefähr als T ist

dann tatsächlich ein Element der Interpretation von Alpha. Und dann in dem Moment haben wir offenbar

gewonnen, denn Alpha oder die Interpretation von Alpha ist eine Teilmenge der Menge der stark

normalisierenden Terme. Das hier impliziert dann also insbesondere, dass T stark normalisierend ist.

Ja, also diese Korrektheit wird dann besagen, jeder typisierbare Term ist stark normalisierend,

einfach aufgrund Korrektheit der Typregeln bezüglich dieser Semantik. So, das ist so die

grobe Outline, so soll das funktionieren. So, hier endet die Outline, also das war jetzt die

grobe Beweisskizze, wie das Ganze ablaufen soll und jetzt fangen wir tatsächlich damit an.

So, und zwar kommt jetzt als nächstes die induktive Invariante, die wir brauchen,

um das alles tatsächlich durchzudrücken. Und zwar sagt sie uns, dass diese, also sie behauptet

es zunächst einmal und wir zeigen es dann, dass diese Teilmengen von Sn, durch die wir die Typen

interpretieren, dass das nicht irgendwelche Teilmengen, sondern Teilmengen mit bestimmten

angenehmen Eigenschaften sind. Und die definieren wir jetzt. Und zwar sind das sogenannte saturierte

Mengen. Wir definieren jetzt, was es heißt, saturiert zu sein. Das sind zwei Eigenschaften.

Erstens, ja, es sind beides Abschlusseigenschaften. Die erste ist sehr leicht. Ich verlange, dass im

Wesentlichen alle Anwendungen von Variablen auf irgendwas, also eine Anzahl Argumente in A sind,

mit einer Maßgabe, nämlich, dass diese Argumente, die ich da reinstecke, alles stark normalisierend

sind. Offensichtlich muss ich diese Einschränkung machen. Ja, ich kann nicht verlangen, dass x