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

Ja, herzlich willkommen.

Wir haben ja letztes Mal gesehen, wie man Funktionen in einen Kodatentyp hinein,

also zum Beispiel zur Erzeugung von Streams mittels Korekursion definiert,

also mit etwas, was wir erst mal das Unfold Schema genannt haben.

Das haben wir uns bisher nur angeschaut auf Streams.

Und ich bleibe heute beim Beweisprinzip auch erst mal rein bei den Streams.

Wir gehen dann ab Donnerstag auf allgemeinere Kodatentypen über,

da macht die Einführung dann der Herr Hausmann.

Ich selber bin mit fast dem gesamten restlichen Dish-Wolfkonferenz.

Das heißt, wir sehen uns jetzt an einem Beweisprinzip, mit dem wir über solche

korekursiv definierten Funktionen auch mal was sagen können.

Und das heißt, wie soll das anders sein?

Koinduktion.

Ja, also wir entsinnen uns an das letzte Mal, wo wir diese Blink-Funktion definiert hatten,

die wir nachher mit drei Argumenten definiert hatten.

Also eine Funktion, die an die geraden Stellen im Stream eben dieses Füllsymbol x einfügt

und eine mit der 1 dran, die dann in die ungeraden Stellen das einfügt.

Das war folgendermaßen korekursiv definiert.

Einmal müssen wir sagen, was der Head von dem Ding ist.

Gut, das ist, weil wir an die geraden Stellen einfügen und wir eben bei 0 anfangen zu zählen,

ist das gerade x und Tail von demselben Ding ist, naja, was kommt als nächstes?

Ne, jetzt kam als erstes das x, jetzt kommt der restliche Stream s, wieder natürlich

mit x zwischendurch eingefügt, aber jetzt an den ungeraden Stellen.

Also Blink 1 xs.

Und dann die Fälle für 1, Head von Blink 1 xs.

Da steht jetzt vorne, weil x erst an der nächsten Stelle kommt, der Kopf von s, also

Head s und Tail vom gleichen Ding.

Nun, da haben wir jetzt ja von s schon ein Symbol verbraucht, das heißt, da kommt jetzt

nur noch Tail s vor und natürlich wollen wir weiter blinken.

Jetzt natürlich wieder mit einer 0 vorne, weil jetzt als nächstes das x dran ist und

immer noch mit demselben Symbol x.

Definieren wir uns mal einen zweiten Satzfunktion dazu, und zwar solche, die jetzt gerade oder

ungerade Elemente aus so einem Stream wieder rausgreifen, also immer gerade auf gewisse

Maßen die Hälfte des Streams zurückliefern, also zum Beispiel diese hier.

Das sind jetzt neue Definitionen, die ich letztes Mal noch nicht angeschrieben hatte.

Sagen wir, wir wollen eine Funktion odd definieren, die also gerade die ungeraden Elemente aus

dem Stream rausgreift, also die gerade Elemente aus dem Stream rausgreift.

Nun, das erste gerade Element ist ja gerade das erste, weil die 0 anfangen zu indizieren,

das heißt Head von even s ist gerade einfach gleich Head von s.

Muss man noch sagen, was der Tail von even s ist.

Ja, überlegen wir uns was da passiert, also wir haben hier unsere Positionen, wir wollen

die gerade rausgreifen, also diese hier, diese hier, diese hier und so weiter.

Wenn wir also davon den Tail nehmen, dann ist das etwas, was hier bei 2 anfängt und

davon aber natürlich wieder nur die gerade, das heißt, was hier rauskommt ist even von

2 mal Tail von s, 2 mal Tail schaltet mir hier hin um und dann muss ich wieder even anwenden.

Und dann will ich analog dazu eine Funktion odd definieren, nehme ja eben gerade die ungeraden

Elemente immer rausgreift, gut der Head ist klar, der ist dann also das zweite Element

des Streams, sprich Head von Tail von s, das zweite Element, sprich das mit der laufenden

Nummer 1.