Natürliche Zahlen, Listen, Binäre Bäume.

Ich schreibe:

data List A := Nil : () -> List A | Cons : A -> List A -> List A

Ich notiere:

foldl (c : () -> C, f : A -> C -> C) : List A -> C
foldl (c, f) (Nil) = c
foldl (c, f) (Cons a l) = f(a, foldl (c, f) l)

• Identitätsgesetzp foldl (Nil, Cons) = id
• Fusionsregel Hier erwähne ich F-Algebren, und wir springen daher gleich vor.

Für eine Kategorie C und Endofunktor F : C -> C können wir eine Kategorie Alg(F) definieren, wo die Objekte Morphismen der Form FA -> A oder (A, a) in der Basiskategorie C sind, und Morphismen F-Algebra Homomorphismen, sodass das Quadrat aus der Vorlesung kommutiert.

Initiale Objekte in C sind Initiale F-Algebren (I, i), für die ein eindeutiger Morphismus h : (I, i) -> (A, a) zu jedem Objekt (A, a).

Wenn wir (|a|) als Notation benutzen für den eindeutigen Morphismus, dann gilt für ein f : (A,a) -> (B,b) das kommutative Diagramm f o (|a|) = (|b|).

Hier stolpere ich, aber schaffe mit einem Hinweis darauf zu kommen, dass es aufgrund der Eindeutigkeit von (|b|) ist.

Dass (|i|) = id_(I,i), wobei ich zuerst id_Alg(F) geschrieben hab aufgrund meiner vorherigen Verwirrung.

Nein, weil wir wegen Lambek wissen, dass der Strukturmorphismus i von (I, i) ein Isomorphismus sein muss. Dieses ist beispielsweise so bei dem Potenzmengenfunktor nicht gegeben, weil wir aufgrund von Cantors Gesetz wissen, dass die Kardinalität von einer beliebigen Menge M strikt kleiner ist als PM.

Wir benötigen, dass F Kolimiten von omega-Ketten erhält und die Kategorie initiale Objekte hat. Hier hab ich wohl angenommen, dass „omega-Ketten erhällt“ impliziert, dass C Kolimiten von omega-Ketten besitzt, wo nachgefragt werden musste.

Ich habe dann die 0 -> F0 -> FF0 -> ... Kette aufgezeichnet und den besagten Kolimes colim F davon gebildet. Aufgrund der Eigenschaften vom Funktor können wir F (colim F) bilden, wo ein eindeutiger Morphismus zu colim F existieren muss.

Hier wird nachgehakt wieso das der Fall ist, weil ja vorher colim F der Kolimes war. Hier bin ich verwirrt und werde darauf hingewiesen, dass colim F nicht mehr das initiale Objekt in der Kokegel-Kategorie von dem Diagram F0 -> FF0 -> ... ist. Duh.

Ich dachte dieser Teil würde nicht in der Prüfung erwähnt werden, auch wenn es im Nachhinein in dem alten Braindump explizit angebracht wurde. Ich meine das gerade nicht zu können, und es wird vom Prüfer geleugnet. Jedenfalls schaffe ich es noch aus dem Gedächtnis ungefähr darauf zu kommen, wie man für ein Objekt FA -> A den Kegel aus der omega-Kette konstruiert, und dass es kommutiert aufgrund der Eindeutigkeit von ¡ : I -> A.

Eine Relation von zweier Koalgebra Trägermengen, für welche das Diagramm aus der Vorlesung kommutiert.

Ich komme nicht direkt darauf, weil ich meine etwas im Skript vergessen zu haben. Ich erwähne, dass es in ThProg benutzt wird bei der Minimierung von Automaten, aber nach einem kleinem Hinweis verstehe ich, dass hier gemeint ist, dass wir Verhaltensäquivalenz folgern können aus Bisimulation. Aufgrund von zeitlicher Knappheit skizziere ich nur den dafür notwendigen Pushout und die Abbildungen auf die Terminale Koalgebra, aber komme nicht mehr dazu es genauer zu erklären.

Beschämt, Blamiert und Beschmutzt bedulde ich mich auf meine Note, während ich verzweifelt versuche zu vermeiden meinen Nachprüfling zu verunsichern.

„Sie schienen nervös zu sein, was nicht berechtigt war, weil Sie ja den ganzen Stoff verstehen“, paraphrasiere ich den Prüfer nun im Nachhinein. Weil ich aber dennoch hier und da gehakt habe, ist es „nur“ eine 1.3.