Ja, herzlich willkommen. Wir haben im Lambda-Kalkül eigentlich noch ein Thema über, das ist die

starke Normalisierung des einfach getypten Lambda-Kalküls. Dieser starke Normalisierungsbeweis,

den werden Sie im Skript finden in zwei Versionen. Also einmal in der Version für den einfach getypten

Lambda-Kalkül und einmal für eine viel stärkere Sprache für das sogenannte System F. Das kommt

also jetzt ein Kapitel nach dem nächsten. Das kann man auch zwei Arten aufziehen. Man kann also

entweder erst diesen spezielleren Beweis für das schwächere System machen und ihn dann aufbohren

und für das stärkere System nochmal präsentieren oder man kann, was ein bisschen Zeit spart, ihn

jetzt weglassen und später einfach den gesamten Beweis für das starke System führen, aus dem dann

ohne Weiteres die Aussage für den einfach getübten Lambda-Kalkül folgt. Ich habe mich mit Herrn Rauch

kurz geschlossen und Herr Rauch sagt, so wir haben nur noch so und so viele Termine, machen wir lieber

schneller. So, also das heißt wir lassen das mit der starken Normalisierung des einfach getübten

Lambda-Kalküls jetzt vorläufig weg, das wird also später folgen aus der starken Normalisierung

von System F und gehen direkt zum Thema

Induktiver Datentyp. Ja, da die meisten hier ja eine funktionale Programmiersprache beherrschen,

wissen die meisten auch, was ein Induktiver Datentyp ist. Ja, ich schreibe mal, Scherz ist halber,

aber einen in, naja so halbwegs Haskell-Syntax, man vergebe mir den einen oder anderen Syntax-Fehler

hin. Ja, in Haskell führ ich ja so einen Datentyp ein mit dem Schlüsselwort data. So, ja in Haskell

würde jetzt ein gleich kommen. Entschuldigung. Und da weichen wir jetzt noch mal bewusst von ab,

also was jetzt kommt ist kein Syntax-Fehler bzw. vielleicht ist es sogar auch legale Haskell-Syntax,

also ich definiere jetzt einen Datentyp natürliche Zahlen. So, und dann mache ich hier mit dem

Schlüsselwort where weiter, das mache ich deswegen, weil ich das dann später in der

Syntax zwanglos verallgemeinern kann auf den dualen Fall der sogenannten Codatentypen,

da haben wir jetzt noch keine Gedanken zu machen, aber das erklärt diese Wahl der Syntax. So, und

hinter diesem where gebe ich einen Stapel Operationen an, mit denen ich den Datentyp,

in diesem Fall soll das also ein Datentyp natürlicher Zahlen werden, wie der Name

andeutet, konstruieren kann, sogenannte Konstruktoren. So, die kann ich auch in

passender Syntax schreiben, also zum Beispiel kann ich den Konstruktor für die Null eben auch

Null nennen. Der kriegt keine Argumente, das heißt, der kriegt hier den Unit-Typ,

den einelementigen Typ als Argumenttyp und liefert dann natürlich eine natürliche Zahl.

Und dann gibt es die Successor Funktion, die schreibe ich mal gemäß Haskell Konvention groß,

die kriegt eine natürliche Zahl als Eingabe und liefert eben auch eine solche zurück. Ja,

in Kurzschreibweise wäre das das hier nicht data not gleich und dann kommt die erste Alternative

ist Null und die zweite ist so knapp, das wäre so die kürzere Syntax dafür, die man in Haskell

wohl normalerweise wählen würde. Wer hat sowas noch nie gesehen?

Zwei. So,

Ja, Gegenstand des nächsten Kapitels ist also die systematische theoretische Behandlung solcher

Datentypen und insbesondere ihrer Semantik, aber auch der Frage, wie ich denn Dinge über

solche Datentypen und Funktionen, die ich darauf definiere, beweise. Ja, fangen wir an mit der

Semantik. Es ist gegeben das, was wir an technischen Methoden schon haben, relativ

straight forward. Was passiert dann? Ich habe es extra jetzt eben in dieser abweichenden

Sonntags relativ explizit gemacht. Was da passiert ist, wir deklarieren schlicht und einfach eine

Signatur. Sie steht mehr oder weniger explizit da. Wir wären als Bezeichner für diese Signatur

einfach mal ein Sigma mit dem Index des Datentyp namens. Das ist also in diesem Falle Sigma nat.

So und was kommt da in diesem Falle raus? Gut, ist klar, das ist eine nullstellige Operation 0 und

eine einstellige Operation SUG erinnert alles fürchterlich an Dinge, die wir schon mal gesehen

haben. Und wie gesagt, diese Dinger hier heißen die Konstruktoren des Datentyps.

Ja, und so ein Datentyp, der hat eben auch eine Semantik und da gehen wir zunächst mal

sehr einfach ran. Wie immer schreiben wir die Semantik mit solchen doppelten eckigen

Klammern. Und die Semantik eines Datentyps ist also zunächst mal ändert sich noch schlicht und

einfach eine Menge und zwar eine Menge von Termen über der Signatur, die der Datentyp deklariert,