Braindump für Algebra des Programmierens im WS23/24
| Prüfer | Stefan Milius |
| Beisitzer | Thorsten Wißmann |
| Datum |
Wir haben anfangs in der Vorlesung rekursive Datentypen behandelt. Welche denn?
- \(\mathbb{N}\)
list Atree A
Wie schauen denn z.B. Listen aus?
data list A where nil : () -> list A | cons : (A, list A) -> list A
Wie definiere ich mir fold?
fold (c,h) nil = c fold (c,h) (cons x xs) = h (x, fold (c,h) xs)
Es gab da immer zwei Regeln. Welche?
- Identity
- \[
\mathrm{fold} (\mathrm{nil}, \mathrm{cons}) = \mathrm{id}_{\mathrm{list A}}
\]
- Fusion
- Ich will auf \(F\)-Algebren vorgreifen, werde unterbrochen
Ok, dann erklär mal \(F\)-Algebren
Eine \(F\)-Algebra von einem Funktor \(F : \mathcal{C} \to \mathcal{C}\) ist ein Tupel \(A \in \mathrm{Ob}~\mathcal{C}, a : F A \to A\).
Ein \(F\)-Algebra-Homomorphismus zwischen \(F\)-Algebren \((A,a), (B,b)\) ist ein \(f \in \mathrm{Hom}_{\mathcal{C}}(A,B)\) sodass
kommutiert.
Beides zusammen formt die Kategorie \(\mathsf{Alg}(F)\).
Da gab es doch eine besondere \(F\)-Algebra
Die initiale \(F\)-Algebra. Die ist das initiale Objekt in \(\mathsf{Alg}(F)\).
Ich erkläre noch Initialität (beim ersten Versprecher noch Terminalität).
Was ist jetzt die Aussage von der Fusionsregel?
Wenn \(f : A \to B\) \(F\)-Algebra-Homomorphismus, dann kommutiert das innere Dreieck in
Wie kommt das?
Durch die universelle Eigenschaft von \(I\) angewandt auf \(m : I \to B\) und \(f \circ h : I \to B\).
Welchen Funktor benutzt ich jetzt bei Listen? Was ist die initiale Algebra davon?
list A ist die initiale Algebra von dem Funktor \(F X = 1 + A \times X\).
Hat denn jeder Funktor eine initiale Algebra?
Nein, da eine initiale Algebra von \(\mathcal{P}\) ja über Lambek's Lemma im Widerspruch zu Cantor wäre.
Was ist die Aussage des Satzes von Cantor?
Es gibt keine Bijektion zwischen einer Menge und ihrer Potenzmenge.
Was ist die Aussage von Lambek's Lemma? Wie beweist man das?
Sei \((I,i)\) die initiale Algebra eines Funktors \(F : \mathcal{C} \to \mathcal{C}\). Dann ist \(i\) ein Isomorphismus in \(\mathcal{C}\).
Der Beweis folgt aus dem Diagramm:
wobei \(h \circ i = \mathrm{id}_{FI}\) folgt aus der Funktorialität von \(F\).
Wie kann ich mir so eine initiale Algebra konstruieren? Was gibt es da für Voraussetzungen?
Die Kategorie muss kovollständig (bzw. ein initiales Objekt und Kolimiten von \(\omega\)-Ketten haben) sein, der Funktor \(\omega\)-kostetig.
Wie funktioniert dann die Konstruktion?
Ich bilde den Kolimes der \(\omega\)-Kette
als Kanditat für die Trägermenge der initialen Algebra.
Den Strukturmorphismus konstruieren ich durch anwenden von \(F\) auf das Diagramm, was mir aufgrund der Annahme das \(F\) \(\omega\)-kostetig ist widerrum einen Kolimes gibt:
Hier nutze ich aus, dass nach dem vorherigen Diagramm auch ein Kokegel der neuen \(\omega\)-Kette über \(I\) existiert.
Nach Initialität von \(FI\) in der Kokegelkategorie gibt es also einen eindeutigen Strukturmorphismus \(s : FI \to I\).
Die \(F\)-Algebra ist also konstruiert, nun zum Beweis der Initialität:
Sei \(A,a\) nun eine andere \(F\)-Algebra…
Naja, sie kann ja auch gleich sein!
Solch Pedanterie weise ich mit dem Kommentar "Ich meine natürlich \(\forall\)-Introduction" ab.
Weiter im Text:
Ich will mir nun einen Kokegel der ersten \(\omega\)-Kette konstruieren, um dann über die Initialität von \(I\) in der Kokegelkategorie einen Morphismus \(h : I \to A\) zu bekommen. Das mache ich induktiv:
- \(a_0 : \bot \to A\) ist gegeben durch Initialität.
- \(a_{n+1} = a \circ F a_{n}\)
Das die \(a_n\) einen Kokegel bilden folgt dann per Induktion über \(n\).
Warum ist \(h\) dann ein \(F\)-Algebra-Homomorphismus?
Hier brauche ich etwas Hilfe für das Argument.
Man verwendet natürlich die Initialität von \(FI\) in der Kokegelkategorie über der zweiten Kette.
Gut, das langt. Dann machen wir mal weiter mit Koalgebren. Was ist eine Bisimulation?
Eine Bisimulation ist eine Relation \(R \subseteq C \times D\), wobei \((C,c), (D,d)\) Koalgebren über einen Funktor \(F : \mathsf{Set} \to \mathsf{Set}\) sodass \(r : R \to FR\) existiert mit
Woher kommen diese Projektionen?
Über Injektion \(\iota : R \hookrightarrow C\times D\).
Was heißt es jetzt wenn \(x \in C, y \in D\) bisimilar sind?
Es existstiert eine Bisimulation \(R \subseteq C \times D\) mit \((x,y) \in R\).
Was bringt mir denn eine Bisimulation?
Es gab da so ein Lemma das \(x,y\) bisimilar ⇒ x ∼ y
Definiere doch mal Verhaltensäquivalenz
Für \((C,c), (D,d)\) Koalgebren sind \(x \in C, y \in D\) verhaltensäquivalent \((x \sim y)\) wenn eine Koalgebra \((E,e)\) mit Koalgebrahomomorphismen \(h_C : C \to E, h_D : D \to E\) existiert mit \(h_C(x) = h_D (y)\).
Und der Beweis?
\(\mathsf{Set}\) ist ja kovollständig, also kann ich den Pushout der Projektionen bilden. Dann wende ich die universelle Eigenschaft davon auf die terminale Koalgebra an…
Die terminale Koalgebra muss ja aber nicht existieren. Was mach ich dann?
Nach etwas Unterstützung produziere ich dieses Diagramm:
Woher bekomm ich dann die Bedingung der Verhaltensäquivalenz?
Ich zögere…
(Thorsten) Wenn mich jemand auf der Straße fragt was ein Pushout ist, was erzähl ich dann?
Die Absurdität des Szenarios ignoriere ich und komme endlich darauf das die Bedingung ja aus Kommutieren des oberen Quadrats folgt.
Fazit
"Das lief ja ganz gut, bis auf das Ende." Es ist also "noch" eine 1.0