20 - Kategorien in der Programmierung [ID:10670]
50 von 599 angezeigt

war das Aufgabenblatt das letzte Prima, weil damit sind eigentlich fast alle

Voraussetzungen und Vorbereitungen abgeschlossen, um jetzt den Satz über

adjunctivierte Funktoren zu beweisen. Also das heißt, das Thema heute ist

adjunktion und limitis.

Und also was man in dem letzten Übungsplatz schon gesehen hat, ist eine

ganz wichtige Eigenschaft von adjungierten. Also wenn man jetzt

rechtsadjungierte anguckt, dann erhalten die limitis. Also falls G

rechtsadjungiert ist, dann folgt G erhält limitis. Und die Umkehrung gilt

nicht, das war glaube ich auch schon auf dem Aufgabenblatt drauf. Oder? Ja, also

zum Beispiel, wenn man jetzt den Vergissfunktor von den Funktoralgebungen

von der Potenzmengenfunktoren nach Mengen anguckt, der kann keinen

linksadjungierten haben. Also der ist deshalb kein rechtsadjungierter, weil

es sonst, also ein universeller Pfeil aus der leeren Menge, das müsste eine

initiale P-Algebra sein, die es ja nicht geben kann. Und der erhält aber

limitis. Davon muss man sich überzeugen, dass es so ist. Das ist aber so.

So und das heißt, man hätte gern, also diese angenehmen Eigenschaften von

rechtsadjungierten oder halt diese, eine Adjunktion heißt ja letztendlich, dass man

so eine Art Beziehung zwischen zwei Kategorien hat. Da entlang von

Adjungierten kann man so Strukturen und Ergebnisse übersetzen. Und was man jetzt

machen will, man möchte gerne hier diese rechte Seite so verstärken, dass diese

Implikation gilt. Also jetzt

rechte Seite verstärken.

So dass dort dann eben eine Äquivalenz steht.

Gut und da gibt es eben diesen rühmten Satz über adjungierte Funktoren von

Peter Freid. Ist der aus den 60er oder 70er Jahren stammt der. Und der hat eben

diese Bedingungen, die man da also zu der Limites Erhaltung noch hinzufügen

muss, sich überlegt. Und da gibt es also auch zwei Varianten von, nämlich den

allgemeinen Satz über adjungierte Funktoren und den speziellen. Die werden

wir uns beide angucken. Und bei dem allgemeinen Satz, genau bei dem, da

steckt zunächst mal ein einfaches Ergebnis dahinter, das eigentlich über

Initialobjekte geht. Also da geht es gar nicht um die darum, dass irgendwie ein

links adjungierter zu einem Funktor existiert, sondern spielt überhaupt

erstmal keine Funktorenrolle, sondern es geht darum, dass ein Initialobjekt existiert.

Und was man dazu braucht, ist den Begriff einer schwach initialen Menge zunächst

mal. Was ist das? Also das heißt, ich habe irgendwie eine Kategorie und ich

schwäche jetzt quasi die Eigenschaft von einem Initialobjekt in zweierlei

Hinsicht ab. Also erstens verlange ich nicht mehr Eindeutigkeit von einem

Morphismus und zweitens verlange ich nicht, dass es ein Objekt ist, was das

macht. Für jedes andere gibt es genau einen Morphismus, also das genaue einen

habe ich sowieso schon weggelassen, sondern ich sage, es gibt eine Menge von

Objekten, die das leistet. Und das nennt man dann schwach initialen Menge. Also M,

Script M ist eine Menge von C Objekten und die heißt jetzt schwach initial, wenn

die im Prinzip so eine schwache Initialeigenschaft im Hinblick auf alle

anderen Objekte hat. Also für alle Objekte von dem C x gibt es ein y aus

dieser Menge und ein Morphismus von y nach x.

Also kein genau eins, sondern es gibt einen. Das ist erstmal ein formaler Begriff,

diese schwach initialen Menge, aber das wird eine Rolle spielen über diesen

Satz über adjungierte Funktoren. Zunächst mal eine Bemerkung dazu, das Ganze hat

nur wirklich dann Gehalt, wenn wir hier über eine große Kategorie reden.

Wenn meine Kategorie C selbst klein ist, also alle Objekte davon sind nur

Teil einer Videoserie :

Zugänglich über

Offener Zugang

Dauer

01:27:47 Min

Aufnahmedatum

2018-01-29

Hochgeladen am

2019-04-20 20:19:03

Sprache

de-DE

Die behandelten Themen bauen auf den Stoff von Algebra des Programmierens auf und vertieft diesen. 
Folgende weiterführende Themen werden behandelt:

  • Kategorie der CPOs; insbesondere freie CPOs, Einbettungen/Projektionen, Limes-Kolimes-Koinzidenz

  • Lokal stetige Funktoren und deren kanonische Fixpunkte; Lösung rekursiver Bereichsgleichungen insbesondere Modell des ungetyptes Lambda-Kalküls

  • freie Konstruktionen, universelle Pfeile und adjungierte Funktoren

  • Äquivalenzfunktoren

  • Monaden: Eilenberg-Moore und Kleisli-Kategorien; Freie Monaden; Becks Satz

  • evtl. Distributivgesetze, verallgemeinerte Potenzmengenkonstruktion und abstrakte GSOS-Regeln

  • evtl. Algebren und Monaden für Iteration

Lernziele und Kompetenzen:

 

Fachkompetenz Verstehen Die Studierenden erklären grundlegende Begriffe und Konzepte der Kategorientheorie und beschreiben Beispiele. Sie erklären außerdem grundlegende kategorielle Ergebnisse. Anwenden Die Studierenden wenden kategorientheoretische Konzepte und Ergebnisse an, um semantische Modelle für Programmiersprachen und Spezifikationsformalismen aufzustellen. Analysieren Die Studierenden analysieren kategorientheoretische Beweise, dieskutieren die entsprechende Argumentationen und legen diese schriftlich klar nieder. Lern- bzw. Methodenkompetenz Die Studieren lesen und verstehen Fachliteratur, die die Sprache der Kategorientheorie benutzt.
Sie sind in der Lage entsprechende mathematische Argumentationen nachzuvollziehen, zu erklären und selbst zu führen und schriftlich darzus
Einbetten
Wordpress FAU Plugin
iFrame
Teilen