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

Herzlich willkommen.

Wir machen ein neues Kapitel auf und beschäftigen uns jetzt eine Weile mit sogenannten induktiven

Datentypen. Das sind Dinge, die sie zumindest aus dieser Veranstaltung und aus Gleun im Grunde

kennen und die sie vermutlich auch aus hinreichend ausdrucksstarken Programmiersprachen kennen.

Wir verwenden hier für diese Datentypen so eine selbstgestrickte, halb erfundene Syntax,

sagen wir mal. Wir verwenden das Schlüsselwort Data wie in Haskell.

Dann kommt zunächst mal nur ein Datentyp, den wir dann deklarieren. Das werden später auch

noch mal mehrere. Dann kommt ein Where, auch angelehnt an Haskell, das auch gerne Where benutzt und dann

auch normalerweise nicht in Datentyp-Deklaration. Für diesen Datentyp führen wir dann nach dem

Where eben einen Konstruktoren an. Hier zum Beispiel die Null. Also klar, Nat soll ein

Datentyp natürlicher zahlen werden. Und dann gibt es eben eine Funktion Successor. Das haben wir

im Grunde so schon ein paar Mal gesehen. Der Grund, dass das induktiver Datentyp heißt,

ist, dass die Objekte, die hier definiert werden, ja, endliche Objekte sind oder allgemeiner wohl

fundiert. Bleiben wir mal im Moment bei endlich. Endlich heißt, naja, was denn, als Entschuldigung

dafür zu behaupten, dass etwas eine natürliche Zahl ist, dient mir zum Beispiel diese Successor-

Funktion. Also vier ist eine natürliche Zahl, weil es Successor von drei ist und so weiter.

So und diese Behauptung, dass irgendwas eine natürliche Zahl ist, die ich belege mittels,

naja, das ist ja Successor von was anderem, ja, das muss ich wohl fundiert reduzieren,

also in einer endlichen Herleitung gewissermaßen, darauf, dass ich irgendwann mal tatsächlich direkt

und ohne Voraussetzung zeige, dass irgendwas eine natürliche Zahl ist, nämlich Null. Ja, also wenn

ich bei vier anfange, sage ich, vier ist eine natürliche Zahl, denn vier ist ja Successor von

drei, das ist eine natürliche Zahl und so weiter. Und dann komme ich bei eins an und sage, und eins

ist eine natürliche Zahl, denn eins ist ja Successor von Null und Null ist eine natürliche Zahl. So,

nicht das. Alternativ, und das werden wir auch noch sehen, ja, kann man sich auch durchaus

Datentypen denken, wo ich also ad infinitum immer sage, ja, das ist jetzt eine natürliche Zahl,

weil es ja Successor von und so weiter ist und das mache ich einfach weiter, ohne jemals aufzuhören,

ja, das wäre dann nicht mehr wohl fundiert. Und das Wort induktiv, ja, das ist daher rührt,

ist vielleicht übertrieben zu sagen, aber das Wort induktiv klingt ja also nicht von ungefähr nach

Induktion, ja, man kann über solche endlichen Objekte eben Induktion betreiben und das kennen

wir ja auch schon. So eine Datentypdeklaration hier, die tut etwas, was wir eigentlich schon

kennen, das ist nur Notation, nämlich für eine Signatur, ja, das wir machen hier nichts anderes

als eine Signatur zu deklarieren in wohl organisierter Syntax. Die Signatur, die da deklariert wird,

die schreibe ich immer mit groß Sigma und unten dran der Name des Datentyps. Gut, und ich habe

jetzt hier einen eingeschränkten Begriff von Signatur, wo ich nur Funktionssymbole deklariere,

Prädikate kommen nicht vor. So, und Funktionssymbole unterscheiden sich dann nur noch durch ihre

Stelligkeit. Wir haben hier zwei, zero ist Nullstellig, ich deute das hier dadurch an,

dass ich hier Leere Klammer auf Leere Klammer zu schreibe, also Quart Klammer auf Klammer

zu schreibe ohne was dazwischen, ja, das ist also auch in Anlehnung an Hessgen Notation, ja,

für den Datentyp, der keine Informationen enthält gewissermaßen. Und Succesor ist einstellig,

also Succ Schrägstrich 1. Da haben wir also unsere Signatur deklariert. Und ja, Signatur ist ja gut

und schön, woher bekomme ich jetzt den Datentyp. Und der Datentyp, den ich dann definiere, den können

wir in unserer schon aufgelaufene Notation in deutlich weniger als einer Zeile hinschreiben.

Wir nennen ihn Semantik von Nat, ja, also jetzt meint natürlich von der ganzen Deklaration.

Und wir definieren ihn als T Sigma Nat von Leer. So, mal kurz nochmal schlucken, was das eigentlich

an Notation jetzt bedeutet. Ja, T heißt Menge von Termen. Sigma Nat gibt die Signatur an,

also Menge von Termen in der Signatur Sigma Nat, also sprich gebildet aus Null und Succesor,

über der leeren Variablenmenge. Also ich darf keine Variablen verwenden, ja, also Succesor von X

kommt da nicht vor, sondern, naja, wenn ich einen Term bilden will, dann muss ich also praktisch mit

Null anfangen. So, das heißt, ich weiß auch sofort jetzt, also ich kann sofort auflisten,