Herzlich Willkommen.

Wir befassen uns weiter mit Codaten, heute in erster Linie mit Beweismethoden für Codaten.

Ich schiebe noch ein Beispiel nach,

Erstens, um auch mal ein bisschen was nicht trivialeres zu sehen, was so unser Unfold Schema angeht,

also ein Beispiel einer koinduktiven oder korekursiven Definition,

die jetzt vielleicht ein bisschen aufwendiger ist als die sehr primitive Definition von Ones,

die wir gesehen haben, also dem Stream, der nur aus lauter Einzen besteht,

sowie der auch noch recht einfachen Funktion MapF,

die einfach einen Stream ummodelt, indem sie auf jedes seiner Datenelemente eine Funktion f anwendet.

So, das kommt jetzt.

Also noch weiter ein Beispiel zum Thema Korekursion und Unfold.

Wie gesagt, einerseits, um überhaupt das Prinzip zu illustrieren,

andererseits, weil wir den Beweis, den wir nachher machen, also zur Illustration unseres Beweisprinzips,

nämlich der Koinduktion, die wir heute einführen,

weil wir da genau die Funktion, die wir jetzt hier verwenden, brauchen werden.

Wir wollen definieren eine Funktion blink.

Das ist so, ich weiß nicht, ob Sie Lucky Luke gelesen haben damals,

das hat auch einen Gewichtwarenhändler auf, der anbietet,

Schnürsenkel, Whisky, Hosenträger, Whisky, Nägel, Whisky.

Also so eine Funktion soll das sein.

Das heißt, die kriegt ein Argument x, das ist der Whisky, also das Element, was immer wieder erscheint,

und ein Element s, einen Moment, ich reduziere mal den Geräuschlevel.

Und ein Stream s, der also der ist, wo ich immer dieses Element x dazwischen klemmen will.

Das heißt also,

das soll werden eine Funktion mit zwei Argumenten vom Typ a und Stream a,

die ein Stream wiederum mit Elementen aus dem Typ a ausspuckt.

Und wir definieren das Ding jetzt mal informell, also das heißt informell,

ich definiere es vollständig formal, aber nicht folgend irgendeinem Definitionsprinzip,

sondern auf der Meta-Ebene, also rein mathematisch.

Also was ich da reinstopfe neben dem x, ist ja ein Stream, also eine unendliche Sequenz von irgendwelchen Elementen von a,

die ich hier, naja gut, jetzt habe ich sie schon klein a geschrieben, ist vielleicht nicht 100 pro glücklich,

aber sie verwechseln es nicht mit Typen. Ja, also das hier sind Elemente von a.

So, und was da rauskommt,

soll sein, der Stream, wo also x immer da zwischengeklemmt wird, und zwar so, dass wir mit x anfangen, glaube ich,

mal gucken, dass ich da nichts falsch mache, hier.

Also, dass der Stream, der rauskommt, soll also an erster Stelle x haben, bzw. an nullter Stelle,

also wir merken uns jetzt mal alle ganz doll, dass die Numerierung bei null anfängt.

Also insbesondere, um das gleich zu verstehen, das hier, 0 und 2, sind die geraden Positionen des Streams,

und hier 1, 3 und so weiter sind die ungeraden Positionen des Streams, das ist, wenn man den Stream unnummeriert sieht,

vielleicht so ein bisschen kontraintuitiv.

Die Alternative wäre, anfangen bei 1 zu nummerieren, das ist irgendwie auch nicht gut.

Also, der hier vorne ist eine gerade Position.

Also, an die geraden Positionen kommt jetzt also dieses x, und dazwischen kommt der alte Stream, das heißt, hier kommt a0,

dann kommt wieder x, a1, dann wieder x und a2 und so weiter.

So, das soll also das Verhalten dieser Funktion sein.

Ja, wie sah das aus mit unserem Unfold Schema?

Unser Unfold Schema kam ja von der Finalitätseigenschaft unserer Stream Co-Algebra.

Ich erinnere nochmal daran, wie das aussah, das ist, ich male das Bild ein paar Mal hin,

damit man sich das Prinzip aus diesem Bild rekonstruiert.

Ich kann mir das Prinzip auch nicht merken, ich kann mir nur merken,