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

Ja, herzlich willkommen. Wir machen heute im Grunde genommen nichts Neues. Wir schauen uns

nur noch mal an, wie das denn nun eigentlich mal wieder geht. Nämlich das mit der strukturellen

Induktion, das wir uns schon ein paar Mal angesehen haben. Jetzt eben in diesem etwas

neuen Kontext. Strukturelle Induktion auf Datentypen. Ja, und zwar interessiert uns jetzt

die Verbindung zwischen Induktion und Rekursion. Also wir sehen Induktion hier jetzt als in

erster Linie ein Beweisprinzip für den Beweis von Eigenschaften rekursiv definierter Funktionen.

Und vieles von dem, was ich jetzt machen werde, ist also eher Heuristik als Wissenschaft. Ja,

also ich sage Ihnen, wie das denn, wenn sie tatsächlich vor so einem Problem stehen geht.

Und die Heuristik oder der Slogan, den wir hier verfolgen, ist dieser. Der lautet Folge

der rekursiven Definition. Also man hat eine rekursive Definition vor sich, die ist man meistens

dann doch eher in der Lage hinzuschreiben, als dass man jetzt einen freiwilligen,

induktiven Beweis anfängt. Und wenn man sich fragt, wie führe ich jetzt eine Induktion,

dann lautet der Slogan, man sehe sich die rekursive Definition an, die sagt einem,

wie man die Induktion führt. Beispiel. Ja, wir machen erstmal den einfachen Fall,

dass wir also eine, na, im Wesentlichen einsortige Struktur vor uns haben. Im wesentlichen

einsortig soll heißen, wir haben zwar eine Parametersorte, aber die stört nicht weiter,

wichtig ist, wir haben nur einen Datentyp, den wir definieren, statt zum Beispiel

gegenseitig rekursiver Datentypen wie in diesem Tree and Forest Beispiel. Also.

Wir haben das Beispiel schon gesehen, ich schreibe es noch mal an, damit wir die Konstruktoren noch

mal sehen. Also. Nicht der Datentyp, war der der Listen. Und wir hatten einen Konstruktor

nil für die leere Liste, der also kein Argument nimmt. Und einen Konstruktor cons, der einen

Eintrag und eine Liste nimmt und eine neue Liste ausspuckt, wo dieser Eintrag vorne dran gehängt

ist. Ich ändere hier absichtlich schon die Notation, um nachher kürzer schreiben zu können mit, ich

denke mal weniger Klammern und auch um näher an der Notation vom Zettel zu sein, nicht weil wir

jetzt also von der Meta-Theorie uns so ein bisschen wegbewegen, können wir also hier

wieder die Curry-Schreibweise benutzen. So, dann können wir auf die Idee kommen, einen

Konkretinationsoperator zu definieren. Ich nenne den mal an sich Konkret und schreibe aber,

weil ich den in Beweisen sehr oft schreiben muss, jetzt als CC, Abkürzung für Konkretination.

Ich deklariere noch mal, welchen Typ der hat. Der nimmt zwei Listen und spuckt wieder eine

Liste aus, die er aus beiden zusammenbaut. Das ist genau diese Append-Funktion, die wir in Glolab

also auch schon gesehen haben, nur jetzt tatsächlich eben Rekursiv programmiert als Funktion und nicht

mehr als Prädikat. So, das ist also dann natürlich relativ einfach. Wir haben also einmal die

Konkretination der Lehrenliste mit einer weiteren Liste K, das gibt wieder K selbst und wenn ich

die Konkretination von einer zusammengesetzten Liste mit ersten Element X und Restliste L habe

und das vorne an K dran hänge, dann hänge ich X vorne dran an die Liste, die ich durch Konkretination

von L und K bekomme. So, bekannte Definition, wie gesagt, jetzt nur in Funktionalschreibweise

statt in Prädikatenschreibweise.

Das erste, was man jetzt eigentlich fragen könnte ist, haben wir also hier so einen Tanz gemacht,

das hat darum aus Initialität unserer Datentypen noch mit diesem Trick der gleichzeitigen Programmierung

der Identität jetzt primitive Rekursion zu bekommen. Wenn man sich das Schema anguckt,

für primitive Rekursion passt das hier ja gar nicht rein. Warum nicht? Nun, weil primitive

Rekursion, so wie ich sie letztes Mal deklariert hatte, Funktionen mit einem Argument definiert.

Aber, naja, da kommt ja dann die Curry-Schreibweise. Also recht betrachtet definieren wir hier

in der Tat eine Funktion mit einem Argument, sie hat nur einen etwas komplexen Resultattyp.

Also, gucken wir uns das mal an. Also ich behaupte, das ist eine primitiv-rekursive

Definition in genau dem Sinne, den ich letztes Mal deklariert hatte, nämlich...

Hier habe ich im Grunde gar nichts geändert. Es steht zwar da drüben anders, ohne die

Klammern, aber die Klammern sind nur per impliziter Klammerung weggelassen da drüben.

Also das, was da drüben ohne Klammern steht, heißt genau das hier per Klammerkonvention.