Herzlich willkommen! Wir beschäftigen uns heute mit einem allseitigen Lieblingsthema Induktion.

Ja, wir stellen es unter eine etwas neue Überschrift. Wir machen eben Induktion über

Datentypen. Was wir heute machen, ist in Wirklichkeit nicht neu, aber man kann eben nicht behaupten,

dass es vom letzten Semester noch so fest sitzt, dass es sich nicht lohnen würde,

vielleicht noch mal eine Sitzung darauf zu verwenden. Also, Induktion über Datentypen,

das ist im Prinzip die gute alte strukturelle Induktion über Grammatiken, wie wir sie letztes

Semester kennengelernt haben. Wir machen das jetzt in unserer etwas neuen Notation,

also angepasst auf unsere Syntax für Datentypen. Das, was dann tatsächlich vielleicht ein bisschen

neu ist, ist das, was ich letztes Mal schon angekündigt habe, dass wir eben eine Version

des Ganzen für mehrsortige Datentypen uns nochmal sorgfältiger angucken. Wer ganz genau im

Gleun-Skript nachliest, beziehungsweise in der Handreichung auch zur Induktion dazu,

aber insbesondere auch das Kapitel über strukturelle Induktion im Skript, der sieht

da den Inhalt der heutigen Veranstaltung auch schon drin. Das haben wir nur in Gleunen nicht

so besonders betont. Also, im Prinzip besteht fast alles, was ich heute mache, aus Beispielen. Also,

ich führe diese Prinzipien jetzt nicht nochmal ein. Wie gesagt, durchargumentiert, warum das

korrekte Prinzipien sind, haben wir an sich schon. Wir sehen uns also nur Beispiele an.

Und führen zu diesen Berufe erstmal wieder einen neuen Beispiel-Datentyp ein, den wir bisher nicht

eingeführt hatten, also vor der letzten Sitzung, deswegen nicht, weil er parametrisiert ist. Wir

hatten im einsortigen Fall uns die natürlichen Zahlen angeguckt. Im mehrsortigen Fall gleich

dieses kompliziertere Beispiel eines Datentypen mit zwei gegenseitig rekursiv definierten Anteilen,

deutlich harmloser, aber trotzdem zweisortig ist der Datentyp der Listen. Ich schreibe die

Sortenmenge jetzt nicht nochmal hin, aber man sieht eben, dieser Datentyp ist eben insgesamt

zweisortig. Also, es gibt einmal den Typ der Listen und es gibt dann diese Sorte der Datenelemente

in der Liste, die wir als Parameter markieren und die deswegen nicht induktiv generiert wird,

sondern einfach als gegeben angesehen ist. So, dieser Datentyp hat hoffentlich bekannte

Konstruktoren, einmal eine konstante NIL, die wir uns als die leere Liste vorstellen und dann

ein Konstruktor cons, der ist binär, er nimmt sich ein Datenelement und eine Liste und produziert

daraus wieder eine Liste. So, ich füre den nur deswegen ein, um jetzt gleich eine rekursive

Definition einer Funktion darüber hinschreiben zu können, für die ich dann einen einfachen,

induktiven Beweis führen will. Ja, und die rekursive Funktion, die ich hinschreiben will,

ist einfach die Konkatenation von Listen. So, ich will jetzt mal Curry-Schreibweise verwenden,

um gleich so ein bisschen Klammern zu sparen. Ja, also ich schreibe das jetzt so, wie ich es in

Haskell auch schreiben würde, das heißt, der Typ des Ganzen ist so ein gecurrieder Typ hier mit

zwei Funktionspfeilen statt ein endcurrieder Typ, wo also hier, also cons schreibe ich gemäß

unserer Konvention der Datentyp-Syntax hier in, erstmal uncurried, also mit zwei expliziten

Argumenten. Sie werden gleich feststellen, dass ich, also wenn ich das tatsächlich schreibe,

ich in Wirklichkeit das curried verwende, das verursacht hoffentlich keine allzu großen

Irritationen. So, na, ja, wir haben das im Prinzip schonmal angedeutet, wir machen jetzt also

primitive Rekursion und zwar primitive Rekursion über das erste Argument. Konkert hat ja zwei

Argumente, wir können uns im Prinzip aussuchen, worüber wir Rekursion machen. Wir stellen fest,

dass also Rekursion über das zweite Argument hier nicht so richtig zielführend ist, weil dann das

Element, das wir von der einen Liste abspalten, in der Mitte des Ganzen steht. Wir machen also

primitive Rekursion über das erste Argument, das heißt unser erster Fall ist hier, dass wir nil

von links mit irgendeiner Liste konkatenieren. Gut, was rauskommt, ist offensichtlich einfach

wieder die Liste selbst. So, und der andere Fall ist, dass wir hier einen Konstruktor-Pattern

bekommen mit diesem Const-Konstruktor. Sagen wir Const X K vielleicht, damit hier das zweite

Argument wieder L heißen kann. Also, Const X K und das Ganze komponiert oder konkateniert mit L

müssen wir definieren. Gut, müsste bekannt sein. Wir konkatenieren zunächst mal hier die Restliste

K mit L und an das, was wir dann kriegen, hängen wir nochmal das Element X vorne dran.

Muss auch mal sein. Ja, und jetzt wollen wir eben über Konkatenation einen einfachen Beweis