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

Ja, herzlich willkommen.

Wir setzen fort das Kapitel über induktive Datentypen.

Ich erinnere noch mal daran, wo wir beim letzten Mal aufgehört haben. Wir haben letztes Mal einen Satz

Mengen theoretische Notationsweisen eingeführt.

Insbesondere, was sicher alle noch kennen, das kathesische Produkt zweier Mengen.

Wenn wir das jetzt mal mit Bezeichnung für C-Datentypen belegen, dann ist so ein kathesisches Produkt ein Struct.

Das hat zwei Felder und in beide Felder trage ich was ein.

Der Typ von dem, was ich da eintrage, das sind eben meine Mengen x1, x2.

Etwas weniger geläufig war die disjunkte Summe zweier Mengen, die wir dadurch erzeugen,

dass wir die Mengen absichtlich disjunkt machen, indem wir jeweils ein Index vorne dran schreiben,

eins bzw. zwei, an die Elemente von x1 bzw. x2 und das dann zusammen in eine Menge schmeißen.

Auch das hat eine Analogie als C-Datentyp.

In C ist sowas eine Union.

Das ist also ein Feld, wo ich nur eine Sache reinschreiben kann.

Ich habe nur ein Datenfeld, aber dieses eine Datenfeld kann halt einen von zwei ausgewählten Typen haben.

Dann hatten wir entsprechende Konstruktionen auf Abbildungen.

Zum Beispiel ist das hier eine Abbildung zwischen zwei so kathesischen Produkten,

wo ich also praktisch für jedes Feld eine Abbildung habe und jeweils die,

wo ich also beide Abbildungen anwende, f1 aufs erste Feld, f2 aufs zweite Feld.

Entsprechend dann auch eine Summe von Abbildungen.

Das ist jetzt praktisch so eine Art Fallunterscheidung,

je nachdem welcher Art Wert in meinem Feld in der Union steht.

Also vom ersten oder vom zweiten Typ verwende ich die erste Abbildung oder die zweite.

Was ich rauskriege, ist wieder von so einem Union-Typ,

abhängig eben von dem Resultattyp hier, dieser f1 bzw. f2.

Und eng verwandt damit so Paar-Abbildungen wie diese hier,

wo ich also praktisch einfach nur in zwei Funktionen jeweils Werte aus z rein schiebe

und ich bekomme raus einmal einen Wert von Typ x1 sagen,

wäre einmal ein Wert von Typ x2.

Und wenn ich die zusammen verpaare, habe ich eben ein Element des kathesischen Produkts und dual dazu.

Hier das sogenannte Co-Paar von zwei Abbildungen,

wieder eine Fallunterscheidung mit dem einen Unterschied,

dass ich jetzt mit beiden Abbildungen hier in derselben Menge lande,

egal in welcher Alternative meiner Union ich anfänge,

aber ich habe eben weiterhin die Fallunterscheidung,

je nachdem auf welcher Seite ich bin, verwende ich halt g1 oder g2.

So, dann hatten wir uns ein paar einfache Rechengesetze für die Dinger überlegt

und wenn einem so ein Rechengesetz einfällt und man sich fragt, ob es gilt,

dann kann man sofort einfach in die Definitionen der Dinger reingehen und das mal ausrechnen,

das ist also schnell durchverifiziert.

So, mit dieser Notation sehen wir uns jetzt das mit den Algebren und den Homomorphismen nochmal an.

Und dazu nehmen wir uns mal als Beispiel folgende Datentyp-Deklaration von binären Bäumen.

Das soll jetzt mal Bäume ohne Einträge sein, die verzweigen sich einfach nur irgendwie binär

und haben dann sowohl an den inneren Knoten als auch an den Blättern schlicht und schlicht nichts stehen.

Das ist trotzdem noch ein sinnvoller Datentyp in dem Sinne, dass sich die Dinger

also voneinander unterscheiden können, auch wenn nichts dran steht.

Also die sehen dann einfach so aus.

Hier ist, weiß ich, so.

Das wäre ein so ein binärer Baum zum Beispiel.