Herzlich willkommen!

Ja, vieles ist mal angekündigt, nachdem wir also kennengelernt haben, ein zur Rekursion

duales Definitionsprinzip für Funktionen, letztlich ein Prinzip der Co-Rekursion,

stellen wir dem jetzt gegenüber, ein Beweisprinzip, das dual ist zur Induktion und konsequenterweise

dann Co-Induktion heißt. Ja, wir fangen mal an und versuchen mal ein Beispiel, beweisen mal

irgendwie drauf los. Also wir definieren uns erstmal eine Funktion und zusätzlich zu den,

die wir schon gesehen haben. Ich versuche so ein bisschen Kreide zu sparen,

wenn nicht so rasend viel da ist, sonst hole ich noch welche. Gut, wir würden gerne jetzt

also definieren zwei Funktionen, even und odd auf Streams. Was sollen die tun? Die sollen uns

jeweils gerade die geraden Positionen des Streams rausgreifen oder die ungeraden Position. Gut,

das ist eine Übung, die sollten wir mittlerweile hinkriegen. Wir definieren die per Co-Rekursion,

das heißt, wir sagen zunächst mal, was ist der Kopf von even s. Naja, gut, wir müssen uns kurz

klar machen, was meint denn gerade und ungerade. Nun, wir indizieren ja ab Null, das heißt also,

der Kopf des Streams ist eine gerade Position, den wollen wir jetzt also haben, das heißt,

in der Lesart wäre das jetzt also head s und entsprechend können wir uns, wenn wir schon

dabei sind, auch gleich den Head von odd s überlegen. Nun, das ist dann eben der Head vom Tail. Ja,

und dann müssen wir sagen, was ist der Tail von even s. Naja, die Position eins, also die zweite,

wenn man so will, im Stream, die überspringen wir ja und, wenn wir uns das angucken, also wir

wollen immer die gepunkteten Positionen haben, die wo eine Null steht, die wo wir nicht haben,

Null heißt wird gestrichen, das heißt also, naja, hier haben wir den Kopf von even s und der Tail,

der beginnt hier, das heißt, wir nehmen also even von zweimal Tail von s, nicht zweimal Tail von s

ist das, was hier anfängt und davon natürlich dann wieder nur die geraden Positionen und ganz

entsprechend natürlich für odd, da müssen wir auch eben zwei Positionen überspringen.

Einmal spicken, ob ich mich nicht vertan habe, jawoll. Gut, wir können das jetzt verbinden mit

dieser blink-Funktion, die wir uns letztes Mal ausgedacht haben, die also immer jedes zweite Mal,

in jeder zweiten Position im Stream, irgend so ein Trendelement x einsetzt. Die hatten wir ja

letztlich parametrisiert, indem wir hier noch so ein bit angeben, was also angibt, ob jetzt unser

Element, das wir da einsetzen, an die geraden oder ungeraden Positionen soll, Null heißt,

es kommt an die geraden, dann bilden wir also blink x s, das ist also ein Stream,

der fängt mit x an, dann kommt das erste Element von s, dann kommt wieder x, dann kommt das zweite

Element von s und so weiter. So und wenn wir jetzt auf dieses Ding wieder odd loslassen,

dann müssten wir ja gerade die Einträge von s zurückbekommen, das heißt also,

das hier müsste hoffentlich gleich s sein. So, nun haben wir uns ja daran gewöhnt,

dass also die Art, wie wir so einen Stream angucken, die ist, dass wir einfach mal schauen,

was hat er für ein Head, was hat er für ein Tail und natürlich müssen die jeweils gleich sein,

damit zwei Streams gleich sind. Also zwei Streams sind offensichtlich genau dann gleich,

wenn sie gleich ein Head und gleich ein Tail haben. Probieren wir es das mal, also Head,

ich fange jetzt mal an blink immer als b abzukürzen, um gerade zu sparen,

wie letztes Mal, also letztes Mal hatte ich glaube ich den Space zwischen b und Null weggelassen,

das ist vielleicht egal. Also bilden wir also den Head von odd b 0 x s, so also Head von odd steht

da oben, ja das ist also gleich Head von was von, so, das wäre also Head von odd,

das ist Head von Tail von diesem Kram hier. So, das wäre also jetzt Head von Tail von blink 0 x s.

So, on Tail von blink kennen wir wieder auch, das wäre also jetzt Head von

blink 1 x s gemäß der korekursiven Definition von blink, denn das hier wäre die Funktion,

die also x jetzt an die ungeraden Positionen des Streams packt und s ist dabei noch unberührt

und der Head von dem Ding ist per Definition der Head von s. Aha, hat also hingehauen,

ja also Head von der linken Seite ist gleich Head von der rechten Seite, das sieht ja schon

mal gut aus. So und jetzt rechnen wir mal los mit dem Tail. So.

Also wir rechnen jetzt aus Tail von der linken Seite, ja also Tail von, Tail von odd von b 0 x s.

So Tail von odd steht da oben rechts, ja also das ist gleich, also Tail von odd ist gleich