data List A ::= Nil | Cons A (List A)
Greife vor auf F-Algebren und sage, dass das Schema eine F-Algebra-Struktur (mit F: Set → Set via FX := 1 + A x X) benötigt und den initialen Morphismus aus der Termalgebra List A zurückgibt.
fold (c, h) Nil = c fold (c, h) (Cons a xs) = h (a, fold (c, h) xs)
c und h sind von der F-Algebra-Struktur, d.h. 1 + A x X → X für ein bestimmtes X, d.h. c: 1 → X, h: A x X → X. fold ist polymorph in X.
1. Identitätsregel: der eindeutige Morphismus von der initialen F-Algebra in sich selbst ist die Identität, in Formeln: fold (Nil, Cons) = id_{List A}
2. Fusionsregel: kategoriell in einem recht unübersichtlichen kommutativen Diagramm erklärt. Die „folds“ sind genau die eindeutigen Morphismen, die per Initialität existieren von List A in andere Trägerobjekte.
Fixiere eine Kategorie C, einen Endofunktior F: C → C, dann betrachte die Menge der Algebrastrukturen FX → X für beliebige X aus C. Morphismen in dieser F-Algebra-Kategorie sind Homomorphismen, d.h. sie bringen folgendes Quadrat zum Kommutieren:
FX -> X |Fh | h v v FY -> Y
Initialobjekte in oben erwähnter Kategorie, d.h. für jede andere Algebrastruktur existiert genau ein Homomorphismus in diese.
Nein, betrachte F: Set → Set, FX := Powerset(X). Existierte eine initiale Algebrastruktur i: FI → I, dann wäre nach Lambeks Lemma i ein Isomorphismus. Das kann bekanntermaßen nicht sein.
Satz von Cantor.
Siehe Beweis aus dem Skript.
Bilde omega-Kette 0 → F0 → F^2 0 → …, bilde Kolimes (Kategorie kovollständig), nenne diesen I. Wende Funktor auf dasselbe Diagramm an und erhalte F0 → F^2 0 → F^3 0 → …, davon ist FI Kolimes (da F omega-kostetig). Nun ist I auch Kokegel von letzterem Diagramm via dieser Morphismen (schreibe Morphismen auf und zeige anhand Skizze).
FI → I nun initiale F-Algebra?
Sei FA → A andere F-Algebra. Nun konstruiere A als Kokegel von 0 → F0 → F^2 0 → …, um Morphismus I → A zu bekommen. Der Rest des Beweises ist etwas länglich.
Ja, CPOs und Kleene'scher FP-Satz. Ein CPO ist ein Poset mit einem kleinsten Element \bot und Suprema \sup von omega-Ketten. Der Kleene'sche FP-Satz sagt nun aus, dass wenn man eine stetige Endofunktion f auf einem CPO hat, dass das der kleinste FP mit µf := \sup_{i \in \mathbb{i}} f^i(\bot). Eine solche Funktion heißt stetig, wenn sie (a) monoton ist und (b) Suprema von omega-Ketten erhält.
Nun Koalgebrastruktur andersherum X → FX. Sie bilden gut zustandsbasierte Systeme ab, etwa Automaten.
Ja, terminale F-Koalgebren.
FX := A x X^\Sigma // Moore-Automaten.
Terminale Koalgebren erfassen ja das Verhalten aller möglichen Koalgebren. Sprich hier kann man erfassen, was man für einen bestimmten Sigma-String als Eingabe für einen String an As herausbekommt. Oder alternativ (isomorph, siehe Übung WS 18/19) was für ein letztes A man herausbekommt.
In Formeln:
T := A^(\Sigma^*) -> A x (A^(\Sigma^*))^\Sigma := <o, t>
o(h) := h(\varepsilon) t(h) := \lambda \sigma: \Sigma. \lambda w: \Sigma^*. h(\sigma w)
Hier war ich mir unsicher, ob es „h(\sigma w)“ oder „h(w \sigma)“ war und sagte das auch. Laut Prüfern ginge aber beides, die resultierenden Koalgebren müssten isomorph sein.
FX := (A x X)^\Sigma // Mealy-Automaten
Vollkommen analog zu initialen F-Algebren. Beachte nun, dass nicht alle finitären Funktoren Limites von omega^{op}-Ketten erhalten.
Man muss nach omega-Schritten noch omega-Schritte mehr machen, d.h. omega + omega Schritte.
Man beginnt also mit 1 ← F1 ← F^2 1 ← … Sei T davon der Limes. Dann bilde 1 ← T ← FT ← F^2 T. Der Morphismus t_1: FT → 1 ist trivial gegeben. Der Morphismus t_2: FT → T dadurch, dass FT ein Kegel vom erst genannten Diagramm ist. Dazu benötigt man Morphismen FT → 1, FT → F1, FT → F^2 1, … FT → 1 bekommt man wieder trivial. FT → F1 bekommt man via F(T → 1). FT → F^2 1 via F(T → F1).
Hier geriet ich schon sehr ins Straucheln, da ich mehr oder weniger geschickt raten musste, denn die Konstruktion war nicht in der VL besprochen. Nach der Prüfung wurde gefragt, ob denn die Konstruktion (und nicht nur das Resultat - so wie es war) in der VL besprochen wurde, was ich verneinte. Das wird also so genau vielleicht nicht mehr gefragt.
Eine Relation R \subseteq C x D für zwei Trägerobjekte C, D von zwei F-Koalgebren, sodass die Rechteckte […] (siehe Definition in VL) kommutieren.
Siehe Definition in VL.
Wenn zwei Zustände bisimilar sind, so auch verhaltensäquivalent. Außerdem ist beim Spezialfall von einer Bisimulation auf der terminalen F-Koalgebra die Relation eine Untermenge der Diagonale, d.h. so beweist man Zustandsgleichheit auf der terminalen F-Koalgebra.
Wenn der Funktor Pullbacks schwach erhält.
Siehe Beweis aus VL. Insbesondere nehmen wir an, dass die Grundkategorie Pushouts hat, welche Pushouts in der F-Koalgebra-Kategorie induziert. (Das war eine der Übungsaufgaben mit Titel „F-Koalgebren sind abgeschlossen unter Kolimites“.)