Herzlich willkommen humor. Wir hatten letztes Mal begonnen mit der Theorie der Induktivenn

datENSYP und setzen die jetzt fort. Wir wollen das etwas systematisieren. Wir haben über

einerseits die Tatsache, dass Datentypen zu sehen sind als spezielle Algabren für

Signaturen, die zunächst mal eben aus mehreren Operationen verschiedener

Stelligkeit bestehen und dass eine entscheidende Rolle gespielt wird von

strukturerhaltenden Abbildungen zwischen solchen Algabren, sogenannten

Homomorphismen. So wir werden jetzt erstmal den ersten Teil dieser Sitzung

darauf verwenden, dass wir eine etwas monolithischere Sichtweise oder

vereinheitlichte Sichtweise auf diese Algabren gewinnen und zwar

mittels des Begriffs der Mengenkonstruktion. Dieses Wort

Mengenkonstruktion, das ist so ein bisschen Ad Usum del Fini. Diejenigen,

die also jetzt in Alproc schon sitzen oder so was, die werden das wieder

erkennen als den Begriff des Funktors. Damit wollte ich aber hier niemanden

verschrecken und wir geben auch keine allgemeine Definition an dafür, was ein

Funktor ist, sondern wir sehen uns an, wie wir systematisch Beispiele solcher

Konstruktionen generieren. Eigentlich sind es gar nicht so viele

und wir kennen die meisten davon auch schon. Zum Beispiel kennen wir hoffentlich

das kathesische Produkt. Wie viele kennen das kathesische Produkt? Also was

wer weiß, was ich mit x1 Kreuz x2 hier meine. Das sind denn doch die meisten.

Das heißt also das kathesische Produkt x1 x2, das ist ja die Menge der

Paare, x1 x2, wobei x1 aus Groß x1 ist und x2 aus Groß x2.

Wenn man in Begriffen von C-Datentypen zu denken gewohnt ist, dann ist so ein

Ding in etwa ein Struct. Wir wollen uns generell Mengen ja als Typen vorstellen.

Hier habe ich also praktisch so ein Struct mit zwei Feldern, wenn man will.

Da kann ich also eine Sache vom Typ x1 reinschreiben und eine weitere Sache vom

Typ x2. Dann.

Weniger bekannt wahrscheinlich die Summe von Mengen oder die disjunkte

Vereinigung. Um jetzt mal diese Metapher hier fortzusetzen entspricht das in C

einem Union-Typ. Also ein Union von zwei Typen hat nur ein Feld, in das ich

mir aber aussuchen kann, was ich reinschreibe. Entweder eins vom ersten

Typ in der Union oder vom zweiten Typ oder naja gut, die kann natürlich mehr als

nur zwei Felder enthalten, die Union. Das heißt also, das ist jetzt ein Typ, wo ich

mir aussuchen kann, ob ich etwas vom Typ x1 oder vom Typ x2 reinschreibe.

Rein mengen theoretisch gesprochen ist das die disjunkte Vereinigung von Mengen x1

und x2, wobei ich mir aber eben von vornherein nicht sicher sein kann, dass

x1 und x2 tatsächlich disjunkt sind. Wenn sie es nicht sind, dann mache ich sie

disjunkt. Wie mache ich das? Nun, ich schreibe einfach noch ein Label dran, der sagt

von welcher Seite das jetzt kommen soll, was ich da schreibe, wenn ein Element

zufällig auf beiden Seiten auftaucht, dann kriegt es halt verschiedene Label auf

den beiden Seiten. Auf die Weise wird die Geschichte disjunkt.

So, das heißt also,

das wird modelliert als eine tatsächliche Vereinigung, aber eben von

diesen leicht dekorierten Elementen. Das heißt, das sind einmal, wenn ich es wirklich

zu schreiben, ja will ich. Das sind also Einerseits-Elemente der Form 1, sagen wir

x1 mit x aus x1 oder eben 2,x, wobei x aus x2 ist und diese Zeile, die kann ich

natürlich in einem Rutsch schreiben, als die Menge aller Paare i,x, wobei

i entweder 1 oder 2 ist und x aus Groß x i.

Ja und dann noch eine Menge, die den Namen Konstruktion nicht so wirklich

verdient, die wir aber trotzdem brauchen. Das ist eine Menge, die schreiben wir

einfach 1 und das ist einfach eine ein elementige Menge aus, ja mit irgendeinem