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

Wir folgen mit der Organisation des Materials jetzt gewissen Zwängen des Übungsblattes.

Das heißt, wir haben jetzt noch eine zunächst mal letzte Sitzung zum Thema System F und

machen ab Montag reguläre Ausdrücke, kehren dann aber in den letzten Sitzungen des Semesters

wieder zu System F zurück. So, wir machen jetzt also noch diejenigen Anteile über System F,

die man also unbedingt braucht, um den Zettel lösen zu können.

Eingangsfrage, hat jemand sich angeguckt diesen Typen hier und mal versucht einen

Term zu konstruieren? Es geht nicht, man kann keinen Term von diesem Typ konstruieren.

Gut, um das jetzt tatsächlich zu zeigen, müsste man also schwereres Geschütz auffahren.

Die Tatsache alleine, dass man irgendwie eine halbe Stunde irgendwie Herleitungen

hin und her schiebt und dann nichts dabei rauskommt, die sagt ja noch nichts.

Vom logischen Standpunkt aus ist das klar.

Wie gesagt, man kann im Rahmen dieses Curry-Howard-Isomorphismus, darf man solche Typen

durchaus als Formeln lesen. Gut, diesen Alquantur hier, den sehen wir als Alquantur über Propositionen.

Also über Wahrheitswerte, wenn man so will. Als solcher sagt er an dieser Stelle,

alle Wahrheitswerte sind wahr. Das ist natürlich Unsinn, denn es gibt ja auch im einfachsten

Falle zum Beispiel falsch, das ist nun mal nicht wahr. Das heißt, diese Formel ist schlicht

und einfach eine Abkürzung für falsch. Insofern ist es ganz gut, dass man keinen Term dafür

konstruieren kann, denn dieser Term wäre ja gemäß Curry-Howard-Isomorphismus ein Beweis

der absurden Aussage.

So, okay. Mit anderen Worten, diese parametrische Polymorphie, die schränkt die Terme, die man

schreiben kann, sehr ein. Und das wird auch wichtig sein für diese Datentyp-Konstruktion,

die wir letztes Mal schon angefangen haben. Ich werde jetzt hier die Konstruktion nicht

im Einzelnen durchixen, weil sie größtenteils auf einem Zettel stehen. Ich werde hier jetzt

nur exemplarisch noch mal erinnern an die natürlichen Zahlen und an Summen und für

die natürlichen Zahlen dann tatsächlich mal so eine Typherleitung vorführen, wie sie

auch auf dem Übungsblatt vorkommt.

Also, nicht nochmal Wiederholung der letzten Überschrift Datentypen in System F. Nicht

mehr. Das hier war der Typ der natürlichen Zahlen, der eben genau gerade die Initialitätseigenschaft

einfängt, wie letztes Mal diskutiert.

Zero schreibe ich nicht nochmal hin, ich schreibe nochmal hin den Successor, den brauchen

wir gleich noch.

Das ist eine Funktion von N nach N und wir definieren sie als, zunächst mal nimmt das

Ding natürlich eine natürliche Zahl und es spuckt dann wieder eine natürliche Zahl aus,

sprich so ein Ding hier, eine Polymorphenfunktion mit zwei Argumenten, von denen eins funktional

ist. Das heißt, da kommt jetzt wieder ein Lambda für diese beiden Funktionsargumente,

f hier das Funktionale und x das aus a und es kommt raus f von Nf a. Und wenn wir uns

entsinnen, dass wir also, nicht a, x, das hier lesen als N mal nacheinander f auf x angewandt,

dann ist klar, dass man das so definieren muss. Hier wenden wir es halt erst N mal an

und dann noch einmal mehr und das ist unsere Interpretation von N plus 1, denn genau das

soll der Successor hier definieren.

So, ja dann gab es eine Fold-Funktion und die Fold-Funktion tut eben mehr oder weniger

genau das, was hier suggeriert wird. Vielleicht reiben wir sie nochmal hin, bevor ich es jetzt

lange erkläre. Fold ist wieder eine Polymorphenfunktion, die also für jeden Typ a funktioniert und

zwar dann eine Algebra-Struktur auf diesen Typ entgegen nimmt und eine Abbildung produziert

von den natürlichen Zahlen in den Typ rein. Das also spricht den eindeutigen Homomorphismus

liefert und das ist definiert wie folgt. Ja, was nimmt das Ding entgegen? Das nimmt also

hier wieder unsere Algebra-Struktur entgegen, also das f und das x hier oben und dann eine

natürliche Zahl. Und was gibt es zurück? Nun das einzige, was man machen kann, es wendet

halt N an auf diese Algebra, also fx, damit landet dann auf der Spezifikation von N wie