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

Also wir hatten gesehen, wie man auf einem inaktiven Datentyp Funktionen definiert durch Rekursionen.

Und wir hatten letztes Mal gesehen, dual dazu kann man auf einem Codatentyp, wie z.B. Streams, Funktionen definieren durch etwas, das könnte man eben Corecursion nennen.

Wir sehen gleich noch ein Beispiel dieses Definitionsschemas.

Wir haben im induktiven Fall gesehen, dass man Eigenschaften solcher rekursiv definierten Funktionen beweist durch strukturelle Induktion.

So, jetzt brauchen wir ein Beweisprinzip, das entsprechend funktioniert für unsere corecursiv definierten Funktionen.

In der Tat, das heißt Coreinduktion.

Ich erinnere nochmal an so eine corecursive Definition.

Das war diese Blink-Funktion, die also ein Stream nimmt und jedes zweite Mal entweder an geraden oder ungeraden Stellen so einen vorgegebenen Buchstaben X einfügt in den Stream.

Das heißt, wenn ich mir als Fernsehbild vorstelle, da plötzlich ein Bild blinkt oder so etwas dazwischen oder ich setze ein Trendzeichen dazwischen, was mir immer als Anwendung einfällt.

Der kürze Halber hatte ich also die eine von den beiden Funktionen f genannt und die andere g eben zwei Funktionen, also bei f eben dieses x, das das Argument ist das erste gerade immer an die geraden Stellen von s setzt,

weil ich mich entsinnen muss, dass also die Einträge in s angefangen werden zu nummerieren bei 0, das heißt also das erste Element in f x s, das wäre dann dementsprechend das x.

Die zweite Funktion hatte ich g genannt, das war also die, die nun gerade das x an die ungeraden Stellen setzt, insofern fängt also g x s zunächst mal an wie s selber mit dem Kopf von s, also hier kommt raus het s, dann der tail.

Ja, jetzt kommt das Entscheidende, das war ja, also das Definitionsprinzip, was wir hier ausnutzen ist eben, dass dasjenige, das wir eine Abbildung definieren als den eindeutig bestimmten Co-Algebra-Morphismus in den Co-Datentyp rein.

So und dazu gehört, dass wir also jetzt das f nach außen schalten hier, ja also hier bei dem het sieht man das nicht, weil da das ist praktisch auf einer vorher vorhandenen festgewählten Sorte, wo also der Morphismus wie auch schon im induktiven Falle immer Identität ist, deswegen sieht man ihn hier nicht.

Hier im Falle von tail, da wo also was der Co-Datentyp selber wieder rauskommt, da sieht man ihn, hier kommt also jetzt raus f x, also das hier ist jetzt x, na nicht f natürlich g.

Wir haben jetzt das x einmal eingesetzt und wir machen weiter mit einem Stream, wo wir das x an ungrader Stelle einsetzen, also g, x und dann s selbst, denn das erste Element von s, das haben wir ja noch gar nicht eingebaut.

So und jetzt hier entsprechend tail von g x, s, nun bei g, da haben wir hier das erste Element von s schon verbraten, das heißt wir wenden den korekursiven Aufruf auf tail von s an und zwar natürlich wieder g mit dem selben Argument x.

Das war jetzt eine korekursive Definition, die uns zwei Funktionen f und g definiert, die nach dem Satz, den wir gezeigt hatten jetzt eindeutig bestimmt sind, also existieren und eindeutig sind.

So, ja auf dem Zettel sind also zahlreiche Übungen zu diesem Definitionsprinzip auch mit schönen Anwendungsbeispielen, die also einem zeigen, wie man sowas im Rahmen von Video Streaming oder Stateless Servers und sowas verwendet und das sind tatsächlich auch realistische Anwendungen. Bitte sehr.

F natürlich, danke schön, f, weil wir jetzt ja anfangen das x an gerade Stellen reinzusetzen, sehr richtig, danke schön.

So, okay, ja die Funktion brauchen wir gleich, um aber jetzt ein bisschen was anständig an Eigenschaften über das Ding überhaupt mal formulieren zu können, brauchen wir noch mehr Funktionen, nehmen wir erstmal diese hier.

Wir definieren zwei Funktionen, even und odd über dasselbe Prinzip der korekursion.

Die Idee ist, dass even uns immer gerade die geraden Elemente aus dem Stream rausgreift und odd die ungeraden Elemente.

Also, wie sieht das aus?

Wenn even die geraden Elemente rausgreift und wir bei null anfangen zu nummerieren, was ist head von even von s?

Ja, von null, von null.

Head von s.

Das ist head von odd von s.

Ja?

Head von tail von s.

Ja, das war soweit so klar.

Das ist tail von even von s.

Ja?

Na, wenn das hier head und tail wäre, dann würde ich ja dann mit even praktisch s genau reproduzieren.

Ich lese den Kopf und schalte genau einen weiter.

Odd von s.

Danke schön. Das ist odd von tail von s, sehr richtig.

Ist das richtig? Ist das nicht? Moment, ist hier falsch? Moment, wer hat jetzt recht?

Ich glaube, wir haben beide recht, weil die beiden Termine, die man hinschreiben kann, dann die gleichen sind.

Ja, odd von tail von s tut es gut. Also den ersten habe ich verbraten, lasse ihn weg, sage aber dann noch einmal tail und nehme ab da aber die ungeraden.

Das haut hin.

Und entsprechend nicht tail von odd von s ist dann gleich even von tail von s. Ist das richtig?

Moment, ich habe es selber jetzt anders aufgeschrieben, deswegen muss ich kurz mal nachdenken, ob das stimmt.

Also even von tail von s, also wir haben.

Ne, das klappt jetzt so nicht, dann würde sich das erste Element ja wiederholen.

Jetzt müssen wir drei tails hier hinschreiben. Meine eigene Lösung war eine andere.

Meine Lösung war diese hier.

Also wir lassen zwei weg und wenden dann wieder odd an. Wieso was andersrum?

Ja, also meine Lösung sagte hier eigentlich, äquivalenterweise, even von tail von tail von s.