Algebra des Programmierens Prüfung WS 2018/19

• Fach: Algebra des Programmierens vom WS 2018/19
• Datum: vergessen, Prüfungszeitraum WS 2018/19
• Prüfungsart: Mündliche Prüfung
• Prüfer: Prof. Dr. Milius
• Beisitzer: Dr. Henning Urbat
• Note: 1.0
• Vorbereitungsstil:
  • 1.5 Wochen VL und Übung durchgearbeitet. Einige der Beweise (insb. Konstruktionen!) aus der VL habe ich selbst nachgerechnet, einige auch aus der Übung.
  • Ich habe mich an die von Prof. Milius ausgeteilte Themenliste gehalten. Anmerkung: Das Resultat, dass finitäre Funktoren auch eine initiale F-Koalgebra besitzen nach omega+omega Schritten [siehe unten] war darin nicht enthalten. Mit der Liste kann man wohl locker bestehen, aber für die 1.0 wird anscheinend noch etwas mehr gefragt.
• Einschätzung
  • Es werden erstaunlich viele Details für eine VL gefragt, bei der man in der Übung sowieso regelmäßig an der Tafel vorstellen musste. Aufgrund früherer anderer VLs aus der theoretischen Informatik hatte ich mir das weniger vorgestellt.
  • Es wurde einem nicht viel Zeit eingeräumt, wenn man über etwas nachdenken wollte, wie z. B. in welche Richtung jetzt die Pfeile gehen oder ob das jetzt eine Prä- oder Postkomposition ist [siehe „\sigma w vs. w \sigma w“]. Übt das also auch ein und denkt am besten laut während der Prüfung, sodass ihr nicht zu schnell unterbrochen werdet und das dann als 'ungenügende Antwort' gewertet wird.
  • Es gibt ja an der FAU auch theoretische Fächer, bei denen man die Prüfung besteht, auch wenn man viele Beweise/Details nicht weiß. Das ist bei „Algebra des Programmierens“ definitiv nicht der Fall. Wer das also belegen möchte, sollte definitiv auch Interesse an Eigenausarbeitung von Beweisen und Details haben! Sonst würde ich strikt von dem Fach abraten.

• Datentypen: Erklären Sie, was Datentypen beispielhaft an Listen.

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

• Wie sieht das fold-Rekursionsschema darauf aus?

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.

• Wie sieht das genau in Gleichungen mit fold aus?

fold (c, h) Nil = c
fold (c, h) (Cons a xs) = h (a, fold (c, h) xs)

• Was sind die Typen von c und h?

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.

• Wir hatten da zwei Regeln, welche waren das?

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.

• Da Sie schon auf F-Algebren vorgegriffen haben, gehen wir gleich dazu über. Was sind F-Algebren?

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

• Sie erwähnten bereits initiale Algebren. Was sind initiale Algebren?

Initialobjekte in oben erwähnter Kategorie, d.h. für jede andere Algebrastruktur existiert genau ein Homomorphismus in diese.

• Hat jede F-Algebra-Kategorie eine initiale Algebra?

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.

• Wissen Sie, wie das Resultat aus der Mathematik heißt?

Satz von Cantor.

• Wie beweist man Lambeks Lemma?

Siehe Beweis aus dem Skript.

• Wie konstruiert man initiale F-Algebren?

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).

• Warum ist 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, den sparen wir uns, mit genügend Zeit bekommen Sie den sicher hin. Bevor wir zu F-Algebren kamen, hatten wir noch einen ordnungstheoretischen Spezialfall diskutiert. Erinnern Sie sich?

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.

• Kommen wir zu F-Koalgebren. Was sind diese und wofür wendet man sie an?

Nun Koalgebrastruktur andersherum X → FX. Sie bilden gut zustandsbasierte Systeme ab, etwa Automaten.

• Gibt es etwas Ähnliches zu initialen F-Algebren?

Ja, terminale F-Koalgebren.

• Ich glaube Ihnen mal, dass Sie wissen, was Terminalität daran konkret bedeutet, nachdem Sie Initialität ja vorhin schon erklärt hatten. Nennen Sie einen konkreten Funktor als Beispiel.

FX := A x X^\Sigma  // Moore-Automaten.

• Wie sieht die terminale Koalgebra inkl. Struktur (!) aus?

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.

• Können Sie noch ein anderes Beispiel sagen?

FX := (A x X)^\Sigma  // Mealy-Automaten

• Wie funktioniert die Konstruktion von terminalen Koalgebren?

Vollkommen analog zu initialen F-Algebren. Beachte nun, dass nicht alle finitären Funktoren Limites von omega^{op}-Ketten erhalten.

• Nun sind viele Funktoren nicht finitär. Was kann man da machen? Erinnern Sie sich an das Resultat von Worrell?

Man muss nach omega-Schritten noch omega-Schritte mehr machen, d.h. omega + omega Schritte.

• Wie genau?

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.

• Zum Schluss noch Korekursion und Koinduktion. Was ist eine Bisimulation?

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.

• Wann sind nun zwei Zustände bisimilar?

Siehe Definition in VL.

• Was bringt nun Bisimilarität?

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.

• Erinnern Sie sich, wann aus Verhaltensäquivalenz auch Bisimilarität folgt?

Wenn der Funktor Pullbacks schwach erhält.

• Und wie genau folgt aus Bisimilarität Verhaltensäquivalenz?

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“.)