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

Wenn wir also noch genug Glück haben, dann mache ich noch einen kurzen Recap über Automatentheorie.

Sonst wäre es vielleicht noch ein Resultat.

Hi, Herr Schäfer.

Wir hören dich.

Ja, aber du hast jetzt ein Video.

Headphones?

Hast du Headphones?

Headphones auf der Kamera?

Signalkamera?

Headphones auf der Kamera.

Nicht wahr?

Immer los mit den Headphones.

Okay.

So, der Beweis für den Einfachen Kreativität ist schon geführt worden.

Wir müssen wissen, dass sich alle noch fragen, wie das funktioniert.

Bei einem Kassentrick.

Also, ich erinnere noch mal daran, wie das funktioniert hat.

Im Einfachen Typen-Landakalkyl hat das Ganze darauf basiert, dass wir eine Interpretation uns ausgedacht haben der Typen.

Die haben wir meistens bei Semantikern so gespielt, also Semantiknamma Alpha.

Alpha ist eine relativ definierte Teilmenge von Sn, normal Sn.

Das waren diejenigen Lambda-Thermetäten, die, das ist ein witzig im Kreis, die Sn sind, die also stark normalisiert sind.

Das sind ganze Worten, die, egal wie sie reduzieren, immer am Ende bei einer Normalform kommen.

So, das wird jetzt, bis zum f-Nur, ein bisschen komplizierter als jetzt.

Die Typen einerseits von Typvariablen abhängen.

Gut, das taten sie jetzt im Einfachgetübten-Landakalkyl im Prinzip auch schon.

Und außerdem aber, sich die Interpretation von Typvariablen im Laufe des induktiven Aufbaus eines Typs ändern kann.

So ähnlich, wie sich in logikerster Stufe der Wert so einer Variablen ändern kann, wenn ich auf einen Quantor stoße, der diese Variable betrifft.

Woraufhin ich also plötzlich den bisherigen Wert der Variable aufgebe und also die Variable stattdessen über alle möglichen Werte, die sie annehmen kann, wandern lasse.

Und das passiert uns hier eben genauso. Wir haben jetzt also hier diese Al-Quantoren über Typvariablen in Alpha-Mutten womöglich drinstecken.

Und müssen deswegen das tun, was wir in der logikerster Stufe auch getan haben.

Wir lassen halt alles abhängen von einer Valuation der Variablen, die sich eventuell unterwegs ändert.

Das heißt, hier kommt jetzt eine moralische Änderung an das Ganze dran.

Also diese Semantik von Typen, die wird abhängen von einer Valuation Xi.

Und dabei wird Xi eine Valuation sein, das heißt eine Abbildung von Variablen auf Werte. So müssen wir einmal gucken, wie ich eigentlich die Menge dieser Typvariablen genannt hatte.

Die hatte ich Vunterstrich genannt. Also naja, an der Tafel nenne ich sie Vunterstrich, im Skript heißt sie V-Dicke-Druck.

So, und diese Valuation, ja die Frage ist jetzt, wohin diese Valuation nun so geht.

Also wenn Typen interpretiert werden als Teilmengen von Sn oder überhaupt zunächst mal als Mengen von Termen, dann wird das sicher auch hier für diese Typumgebung gelten.

Nun ist aber der Clou an dem ganzen Beweis gewesen, dass wir über diese Interpretation von Typen noch was gesondertes gezeigt hatten.

Das war ein gesondertes Lemma, was wir währenddessen gezeigt hatten.

Das war, dass die Interpretation jedes Typs satiiert ist.

Das hat eine entscheidende Rolle nachher gespielt bei dem Korrektheitsbeweis der Semantik. Und insofern ist es vielleicht nicht überraschend, dass wir also auch von den Variablen jederzeit unterstellen,

dass die nicht durch beliebige Mengen von Termen interpretiert werden, sondern nur durch saturierte Mengen.

Das heißt, diese Valuation geht von V-Dicke drückt nach Sat.

Und das sind also, das wollte ich als Buchstaben für die Dinge typischerweise nehmen, das sind also diejenigen Mengen von Lambda-Termen, die diejenigen Mengen A von Lambda-Termen, die saturiert sind.

Das ist also jetzt so im Groben die moralische Änderung. Wir haben jetzt eine Interpretation von Typen, also wir haben sie noch nicht, aber wir werden sie definieren,

die also von so einer Valuation abhängt, so ähnlich wie eben die Interpretation eines Terms in logikerster Stufe von einer Valuation der individuellen Variablen abhängt.

Und nochmal zur Erinnerung, wie es dann so im Groben weitergeht, also wir müssen jetzt verschiedene Dinge nachziehen,

wir müssen also nachziehen überhaupt erstmal die Definition von diesem Tier hier, weil wir ja jetzt eine mächtigere Grammatik für Typen haben,

wo also mindestens ein Fall vorkommt, der bisher gar nicht da war. Dann müssen wir dieses Saturiertheitslämmer nachziehen.