vorrechnen der letzten hausaufgabe an sondern das können wir ganz gut auch einordnen nach dem

abschluss des kapitels über korekursion und koinduktion weil so ein bisschen was ist da

noch offen das machen wir jetzt noch zu ende mich erinnere zunächst mal noch mal dran was hier eine

bisimulation war wir hatten ja ein so ein beispiel bisimulationsbeweis für streams fast fertig

gemacht bis so auf ein lema wenn ich kreide hätte könnte ich das tatsächlich auch machen so

also allgemein ist es ja so dass man bei einer bisimulation jetzt also zunächst mal ein endofunkto

anguckt und dann koalgebren c und d wir hatten es glaube ich nur für mengen gemacht damit wir auch

wirklich sagen können relation ist eine teilmenge von c kreuz d also relation hier ist also so eine

teilmenge von c kreuz d und das heißt dass man jetzt auch im prinzip hier die projektionsfunktionen

hat p0 und p1 und das r ist jetzt also eine bisimulation wenn es so eine abbildung hier

gibt klein r so dass dann diese beiden hier entstehen wollenden quadrate zu einer ja

komputieren das heißt also die beiden projektionsfunktionen werden koalgebra homophysen

das ist erstmal die abstrakte definition was eine bisimulation ist bisimulation

und bei streams war es dann ebenso dass wenn ich also jetzt sozusagen spezialisieren auf den

funktoren ich hatte mal den hier a kreuz x eigentlich nur interessant wieder

ja wir hatten a kreuz x da ist es dann so also so eine relation bis bisimulation genau dann wenn

zwei eigenschaften erfüllt sind nehme ich also wenn ich zwei wenn ich zwei elemente in dieser

relation habe dann muss daraus folgen dass also erstens deren hat gleich ist also das heißt was

jetzt hier passiert ist natürlich dass bei diesem funktor wenn ich hier also koalgebra habe die sich

zerlegen lassen ja also das c das ist ein pairing aus einem h und einem t und das d ist dann so ein

h-strich t-strich ja weil das hier in so ein produkt geht jeweils also die beiden müssen

gleich sein und die andere bedingung ist dass also t x wieder in relation steht zu t-strich von y

das ist also was man im prinzip aus analyse der kommutativität dieser beiden quadrate in

dem spezialfall erhält und was wir dann aus außerdem noch gesehen hatten war denn das ist

eigentlich wieder allgemein dass wenn ich eine bisimulation habe auf der finalen koalgebra dann

ist es immer eine untermenge der der gleichheitsrelation also der diagonale also wenn er

bisimulation ist auf der finalen koalgebra dann gilt das aus x ry folgt x gleich y

und das ist im prinzip die das liefert im prinzip die bisimulations beweismethode oder die

koinduktions beweismethode wie man sie tatsächlich benutzt nämlich indem man ja gleichheit von

elementen in der finalen koalgebra beweisen will indem man eine bisimulation zwischen den elementen

findet was halt einfacher ist als das direkt zu versuchen per irgendwelchen induktions beweisen

oder so die dann auf elemente unterbrechen müssen oder auf komponenten von streams beispielsweise

so das sozusagen der stand und wir hatten uns dann eben angeguckt dieses dieses zip even und odd und

da hatten wir schon fast bewiesen dass wenn man also diese funktionen so verketten war die funktion

die aus dem stream die graden komponenten auswählt die ungraden und zipp das macht so einen reißverschluss

also wenn man so die hände hält dann die beiden streams werden also so miteinander verzahnt und

das muss natürlich wenn man so anschaut wieder das geben was man vorher hatte also das muss die

identitätsfunktion sein auf jetzt den streams über so das hatten wir schon fast bewiesen außer

es fehlte noch ein lemma und das können wir jetzt gleich noch mal nachreichen und dann sehen wir

auch diese bisimulations beweismethode noch einmal an der arbeit und zwar brauchten wir noch dass

also für alle streams aus a hoch omega gilt dass wenn man jetzt die ungraden davon anguckt

odd von sigma dann gilt das ist dasselbe wie eben von tail sigma tail das war noch mal zur

erinnerung die teil der koalgebra struktur auf der auf den streams hier also da gibt es halt

diese üblichen hat und tail funktionen hat und tail von stream und das sind hier quasi die beiden

destruktoren auch die man da benutzt um korekursive definition zu machen hat und tail und so waren

also eben auch even und odd definierte das werden wir jetzt gleich benutzen müssen noch mal das werde

ich aber jetzt nicht noch mal wiederholen das hatten wir an der tafel zu stehen so und so ein

bisimulations beweis den kann man immer erst mal starten indem man sagt also ich will jetzt hier

eine gleichung beweisen deshalb mache ich jetzt eine relation auf a hoch omega das ist die finale

oder terminale koalgebra die erst mal alle diese elemente enthält ja für alle sigma also würde