Ja, herzlich willkommen.

Ja, wir kommen jetzt zu einem neuen Kapitel im Fortgang der Veranstaltung.

Weiter im Geiste einer Durchdringung der Semantik von Programmersprachen kommen wir jetzt zum Thema inductive Datentypen.

Ja, mit unserem bisherigen Vokabular können wir das Wort inductiv durch etwas vielleicht weniger Bekanntes, aber dafür an dieser Stelle technisch Schlagenes, ergänzen.

Induktiv ist im Wesentlichen gemein wohlfundiert.

Kurz gesagt, alle inductiven Datentypen, die wir uns ansehen werden, werden Ansammlungen von Bäumen irgendeiner Art sein.

Und ein solcher Baum ist wohlfundiert, wenn ich da nicht endlos absteigen kann in der Kinderstruktur des Baums.

Das ist also kurz gesagt der Geist des Ganzen.

Eine charakterisierende Eigenschaft von inductiven Datentypen wird sein, dass man ein Definitionsprinzip hat für aus dem Typ rausgehende Funktionen per Rekursion.

Und begleitend haben wir ein Beweisprinzip

für Aussagen der Form, alle Bewohner meines Typs erfüllen irgendeine Eigenschaft per Induktion.

Und weil man Rekursive Definitionen auch als inductive Definition bezeichnet, heißen solche Dinge eben deswegen inductive Datentypen.

Wir werden für solche Datentypen einigermaßen konsequent eine ausgemachte Sündtags-Einhalten, die in etwa so aussieht wie Haskell oder eine bestimmte Farbe Haskell.

Wir werden Datentyp-Deklarationen immer einleiten mit dem Wort data, so wie in Haskell auch.

Dann kommt der Name des Typs, ich definiere jetzt mal scherzeseilbar die natürlichen Zahlen.

Dann kommt ein WHERE.

Und dann kommt eine Serie von Operationsdeklarationen, in diesem Falle, ich will es jetzt gar nicht zero schreiben, sondern richtig gleich als null.

Und ich gebe einfach direkt das Profil dieser Operation an, also in diesem Falle ist zero oder null eine Operation, die keine Argumente nimmt, das deute ich hier durch zwei leere Klammern an.

Und mir eine natürliche Zahl zurückliefert.

Dann natürlich die Successor-Funktion, die eine natürliche Zahl nimmt als Argument und mir eine neue natürliche Zahl zurückliefert.

So, das ist also der Stil unserer Datentyp-Deklarationen, es wird vermutlich jeder in der Lage sein, jetzt kompliziertere Datentypen anhand dieses Beispiels hinzuschreiben.

Dann sehen wir einmal fest, was der Effekt so einer Deklaration ist.

Und zwar, das Ganze deklariert mir eine Signatur, hier die Signatur der natürlichen Zahlen, die nenne ich mal sigma-natt, im Allgemeinen schreibe ich da also hier den Typen, den ich da deklariere, in den Index.

Gut, diese Signatur, die deklariert nur Funktionssymbole natürlich, keine Prädikate, weil ich eben immer nur Operationen angebe.

Und diese Operatoren, die nenne ich Konstruktoren. Also jeder Datentyp hat eine gewisse Anzahl Konstruktoren.

Gut, und dann gibt es eine Semantik, die ich jetzt auch zunächst mal nur beispielhaft aufschreibe.

In diesem Fall werde also die Semantik anzugeben durch Semantikklammern um den Datentyp-Namen herum.

Und die Semantik ist sehr einfach. Sie besteht einfach aus allen Termen, die ich aus diesen Konstruktoren bilden kann.

Also Null ist ein solcher Term, Suc von Null ist ein solcher Term und so weiter.

Das haben wir alles schon mal gesehen. Diese Signatur aus einer unähren und einer nullären Operation,

dass das uns nun genau hier eine Termmenge generiert, die im Wesentlichen so aussieht wie die natürlichen Zahlen.

Das hatten wir uns in Gleun schon angesehen.

Wir werden jetzt ebenfalls aus Gleun importieren, aber für die, die nicht da waren, keine Angst, ich wiederhole also die Definition nochmal vollständig.

Sind wir also allgemeiner, also für Zwecke der Meta-Theorie solcher Datentypen interessiert an beliebigen Modellen dieser Konstruktorsignatur.

Vollständiger heißt so ein Ding ein Sigma-Modell.

Und weil wir eine algebraische Sichtweise auf diese Dinge jetzt verfolgen werden, denn wir es auch eine Sigma-Algebra.

Das Ganze eben für eine gegebene Signatur Sigma.

Ich füge als erinnernden Kommentar nochmal hinzu, eine Signatur Sigma, die nur aus Funktionssymbolen besteht,

die ja so keine Prädikate hat, sonst ist der Begriff noch ein komplizierter.

So ein Ding besteht aus zweierlei Zutaten.

Erstens dem sogenannten Grundbereich.

Den schreiben wir Groß-M, also das Gesamtmodell, das Gesamtmodell schreiben wir Deutsch-M.

Und wir verwenden immer für den Grundbereich den entsprechenden lateinischen Buchstaben zu diesen deutschen Buchstaben hier.

Und dieses M ist einfach irgendeine Menge ohne weitere Einschränkung.

Und dann einer zweiten Zutat, die allerdings nochmal wieder indiziert ist, also eine Zutat für jedes Funktionssymbol F in Sigma.

Und hier zur Erinnerung, diese Schreibweise F'n in Sigma heißt F ist ein Symbol in Sigma und hat Arität n.

Und wir schreiben die Interpretation eines solchen Funktionssymbols in der Form Deutsch-M, also Name des Modells,

dann Semantikklammern, dann F, also Name des Symbols und das ist jeweils eine Abbildung der richtigen Stelligkeit, also von M'n nach N.

Dann fang ich gerade selber mitzubringen hier.

Gut.