Wer hat schon evaluiert? Ah, einer mehr als am Samstag, da waren es erst zwei.

Wer braucht noch einen TAN zum evaluieren? Keiner? Okay, ich glaube es waren noch echt alle da.

Was wir heute machen, also heute, dem Tag vor den Hochschulwahlenmorgen, zu denen ihr alle gehen solltet,

ist noch B-Simulation besprechen. Das heißt, ich wiederhole so ein bisschen,

also wenn wir irgendein Q-induktiven Datentypen haben, zum Beispiel, man kann ihn üblicherweise definieren als Mengenoperation G,

die ein X zuordnet auf irgendeine Zone des Jungter Sommer mit irgendwelchen Outputwerten und irgendwelchen Nachfolgern,

also zum Beispiel bei Streams, also D-Stream X ist zum Beispiel irgendein A- und Nachfolger oder

wenn ich Binärbäume habe mit Blättern, in denen Werte stehen und sonst innere Knoten ohne Werten,

dann sieht dieser Funktur so aus, ich habe entweder ein Blatt, also das ist irgendwie so ein Blatt,

oder ich habe eine Verzweigung ohne Wert. Also das hier ist das gleiche wie X².

Das ist so die allgemeinste Schreibweise. Ich habe N plus 1-Ausfallmöglichkeiten, jeder hat irgendwie so ein Output ai und k i verschiedene Nachfolger.

Wenn ich sowas definieren kann, das ist auch äquivalent dazu, wenn ich zu irgendeiner Signatur mir was Ähnliches definiere,

also das entspricht irgendeiner Signatur. Was macht die? Die Signatur ist mehrsortig,

also mehrsortig mit irgendwelchen Sorten d 0 bis d n und was wir da jetzt haben,

ist, dass wir irgendwelche Beobachterfunktionen haben, um uns diesen Output zu geben,

zum Beispiel h i gibt uns zu einem d i irgendwie so ein ai und dieses ai entspricht, also ich sage jetzt mal entspricht, was jetzt das genau ist,

es geht nur darum so ein Gefühl dafür zu bekommen. Das ai von hier unten entspricht dem ai von hier oben, das gibt uns dieses hier

und ich kann mir auch den j-Nachfolger geben, das heißt jedem die i ordnet das was ist das genau, das ist irgendwas, das wissen wir nicht.

Also wir haben so ein Datentyp d und d ist entweder d 0 oder d 1 oder d n und das ist eine Möglichkeit das darzustellen,

das da oben ist eine andere Möglichkeit und wenn ich mir jetzt eine, wie heißt das, ich kann mir entweder solche d 0 bis d n definieren

mit irgendwelchen solchen Abbildungen, also ein Modell für diese Signatur angeben oder ich kann irgendeine Abbildung mir definieren

und das ist so mehr oder weniger das gleiche, also sagen wir so ein Modell der Signatur entspricht genau so einer Abbildung von x,

so eine Abbildung f, wenn ich das mal von x in so ein g x und das ist eben diese ewige Summe.

Das ist so der Hintergrund und wenn wir jetzt irgendwelche Morphismen, also irgendwelche Homomorphismen zwischen so Co-Algebren haben,

also zwischen Modellen, dann ist so ein, jetzt habe ich den einen, ich sag mal g ist Co-Algebrenmorphismus, wenn,

hast du schon einen Evaluationstand, oder? So ein Co-Algebrenmorphismus, wenn es gilt, dass, also wir sagen von irgendeinem Modell m in irgendein anderes Modell n,

wenn es egal ist, ob ich das h im einen zuerst aufführe, oder ob ich erst in das andere Modell gehe, also schauen wir mal wie das ist.

Es soll gelten h i von g, also das h i in diesem Modell, wenn ich das aufrufe von irgendwas, was ich von hier drüben bekomme,

also von irgendeinem m, soll das gleiche sein, wie wenn ich das hier drüben, wenn ich zuerst das einfach aufrufe, wo haben wir es, h i,

und für diese Nachfolgerfunktionen, die uns irgendwie zum Beispiel bei einem Binärbaum das linke und das rechte Kind geben, da vertauschen die sich,

für genaueres die Vorlesung, aber es soll vor allem, das vertauscht also,

m, i, j, und eben so mit m geben, es soll vor allem diese Beziehung darstellen, wenn wir zum einen irgendwie was mit Codata schreiben,

dann geben wir eigentlich sowas an, also zum Beispiel unser head ist so ein h und das t ist unser tail,

oder in den Animationen war das das sprite und das das advance, und in der Vorlesung haben wir eigentlich vor allem sowas gesehen,

wenn wir definiert haben, was ist überhaupt eine Bissimulation, dann wurde das eigentlich auf dem Ding da oben definiert,

wobei, beziehungsweise auch hier, also das ist so ein bisschen wie ich programmiere, und das ist ein bisschen kompakter,

und kam ein paar mal in der Vorlesung vor, und das soll euch auch dazu motivieren Fragen zu stellen, also hat jemand eine Frage?

Ich habe noch den ganzen Zusammenhang noch nicht so ganz verstanden, also, das bringt dir deshalb was, weil dir dieses Prinzip jetzt,

die Frage ist, wie kriegt man so einen Homomorphismus, und was bringt das einem,

und wir hatten zum Beispiel bei Algebren zwischen Listen, zwischen Listen-Algebren, einen Homomorphismus definiert, nämlich Länge,

es war so mehr oder weniger, wir haben die initiale, also die Liste war so mehr oder weniger so ein, entweder ist es Nil,

es ist ein Element A und Nachfolger, sowas hatten wir da, und wir hatten jetzt die initiale Algebra, also das hier ist Algebra,

wir hatten die initiale Algebra, das war, jetzt muss ich schauen, dass ich die Pfeilrichtung drehe, das war 1 plus A und eine Liste,

und eine A und List A nach List A, das ist die initiale Algebra, und wenn wir jetzt darauf auf List eine Funktion definieren wollten,

die uns die Länge einer Liste berechnet, haben wir eine Algebra hingeschrieben, auch wenn es keiner merkt, wenn man das rektorsiv definiert,

aber letztendlich hat man Folgendes gemacht, man hat definiert, was ist, also das hier ist so ein, hier hat man gesagt, die 1 ist sowas,

die 1, das entspricht dem Nil, der Lernliste, die hat Länge 0, und wenn ich so ein A und eine, wenn ich ein A habe, also irgendwie eine 5,

und eine ewig lange Liste, nehmen wir an, ich hätte die Länge der Liste schon berechnet, dann weiß ich jetzt, was 5, und das Rest ist, was das für eine Länge hat,

also das ist irgendwie so ein, mehr oder weniger ein 1 plus, und das ist so eine rektorsive Definition von einer Funktion Länge,

und was dieses Prinzip mir gegeben hat, war irgend so ein eindeutiger Algebra-Homomorphismus, aber effektiv war das die Funktion Length,