Direkt zum Inhalt | Direkt zur Navigation

Sektionen
Benutzerspezifische Werkzeuge
Sie sind hier: Startseite Willkommen Professuren Ordentliche Professuren Theoretische Informatik Lehrveranstaltungen Sommersemester 2015 Kategorientheorie und Typen

Kategorientheorie und Typen

  • Vorlesung, Dr. E. Richter, Mi. 10:00-12:00, wechselnde Räume, siehe unten!
  • Übung, T. Richter, Fr. 10:00-12:00, wechselnde Räume, siehe unten!

Die Veranstaltung ist in PULS fälschlich als "KATEGORIENTHEORIE UND LOGIK" ausgewiesen. Eine Korrektur ist in Bearbeitung.

Vorlesung und Übung finden in z.T. wöchentlich wechselnden Räumen statt. Hier der genaue Raumplan:

Vorlesung Übung
V 15.04. -
U 17.04. S27
V 22.04. S12 U 24.04. S14
V 29.04. S18 U 01.05. S12
V 06.05. S12 U 08.05. 1.02
V 13.05. S12 U 15.05. fällt aus
V 20.05. S21 U 22.05. S13
V 27.05. S12 U 29.05. S15
V 03.06. S13 U 05.06. S22
V 10.06. S12 U 12.06. 1.02
V 17.06. S13 U 19.06. 1.02
V 24.06. S12 U 26.06. S14
V 01.07. S12 U 03.07. S18
V 08.07. S12 U 10.07. S19
V 15.07. S12 U 17.07. S19
V 22.07. S12 U 22.07. S19


Seit der ersten Erwähnung der Kategorien als Semantik für den Lambda-Kalkül sind fast 50 Jahre vergangen. Heutzutage kann man kaum noch einen Text über die Theorie der Programmiersprachen finden, in denen keine Kategorien erwähnt werden. Der Grund dafür  ist die Tatsache, dass sowohl Kategorientheorie als auch die Theorie der Programmiersprachen im Wesentlichen "Funktionentheorien" sind. 

Dabei ist der Begriff eines Morphismus' -- das ist die kategoriale  Entsprechung von Funktionen -- eine großzügige  Verallgemeinerung des  mengentheoretischen Funktionenbegriffs und bildet ein Art Universalwerkzeug, mit dessen Hilfe man verschiedene Aspekte der Theorie der Programmiersprachen wie Typentheorie, generische Programmierung und  Optimierung in einer einheitlichen Sprache beschreiben kann.

Der Einfluss der Kategorientheorie  ist  jedoch in den letzten Jahren auch in anderen Bereichen  der Informatik immer wichtiger geworden. So  findet man häufig  kategoriale Ansätze  z.B.  in der Softwareentwicklung, der KI, der  Automatentheorie und anderen theoretischen Bereichen. Dabei werden nicht nur die  Resultate über kategoriale Konstruktionen direkt verwendet, sondern man nutzt die Kategorientheorie als mathematische Sprache.

Eine der Kernideen der Kategorientheorie, abstrakte Strukturen stets zusammen mit den dazugehörigen (d.h. strukturerhaltenden) Beziehungen zu betrachten, hat sich als äußerst fruchtbar erwiesen; sie erleichtert die Schaffung einer mathematischen Taxonomie, häufig ein erstes Ziel einer wissenschaftlichen Analyse. Oft gibt es mehrere Formalismen und Strukturen für etwas, das im Grunde dasselbe Konzept ist. Die kategoriale Sprache vereinfacht durch Abstraktion und häufig stellt sich heraus, dass das gesuchte Konzept eine kategoriale Konstruktion ist und die verschiedenen Formalismen deren Realisierungen in verschiedenen Kategorien sind.

Unsere Vorlesung  verfolgt  eine doppelte Absicht. Sie soll einerseits den Zusammenhang zwischen Kategorientheorie und Typentheorie erläutern, andererseits aber auch mit der  kategorialen Denkweise als Werkzeug vertraut  machen.

Die Vorlesung gliedert sich in 4 Kapitel. Im einleitenden Kapitel geht es um Ordnungen, Verbände und Grundlagen der Semantik funktionaler Programmiersprachen. Damit werden einerseits  konkrete mathematische Strukturen eingeführt, andererseits aber auch die in der Kategorientheorie üblichen Denkschemata sozusagen im Konkreten ausgeführt. Auf die in diesem Kapitel behandelten Begriffe werden wir als "running examples" immer wieder zurückgreifen.

Im zweiten Kapitel definieren wir die Grundbegriffe wie z.B. Kategorie, Funktor, natürliche Transformation, Adjunktion und Monade. Wir führen verschiedene kategoriale Konstruktionen ein und beweisen einige grundlegende  Zusammenhänge.  Viele Bücher über Kategorientheorie verwenden  Beispiele und Motivationen aus  Algebra und  Geometrie, die natürlich nur Lesern helfen, die mit den entsprechenden Gebieten der Mathematik vetraut sind. Stattdessen werden wir uns zur Illustration der Konzepte  auf die in Kapitel 1 eingeführten Begriffe sowie auf elementare  mathematische Strukturen,  die jedem
Informatikstudenten vertraut sind, konzentrieren. Auch einige Techniken der funktionalen Programmierung  und Resultate der Berechenbarkeitstheorie werden wir als Realisierung bestimmter kategorialer Konstruktionen neu betrachten. Zum Beispiel werden wir sehen, dass das s-n-m Theorem nur eine konkrete Formulierung der Existenz des Exponentials in der Kategorie der partiell berechenbaren Funktionen ist.

Das dritte Kapitel beginnt damit, dass wir zeigen, wie die Definition einer Kategorie mit der Herleitung von Urteilen (d.h. Termen-im-Kontext) einer algebraischen Typentheorie verbunden ist, was uns einen ersten Blick auf die enge Beziehung zwischen Kategorientheorie und Typentheorie liefert.

In Kapitel 4 schließlich führen wir funktionale Typentheorie basierend auf dem einfach getypten Lambda-Kalkül ein. Dieser stellt eine formale syntaktische Sprache dar und kann als sehr einfache Programmiersprache aufgefasst werden. Abschließend charakterisieren wir  Kategorien, die sich als Semantik für  Programmiersprachen mit erweiterten Typkonstrukten, wie z.B. abhängigen Datentypen und polymorphen Funktionen eignen.

Kategorientheorie ist eine sehr abstrakte Sprache.  Um sich ihre Begriffe anzueignen und deren Tragweite zu erfassen, ist es erforderlich, dass der Lernende
möglichst viele  Beispiele selbst durcharbeitet. Daher wird die Vorlesung durch eine Übungsveranstaltung ergänzt. Während des ersten Teils beinhalten die Aufgaben hauptsächlich das Ausführen von kategorialen Konstruktionen als sogenannte Diagrammjagden auf dem Papier. Im weiteren Verlauf wird dieser Teil ergänzt durch praktische Übungen mit einem formalen System, d.h. Programmieren von Konzepten in einer funktionalen Sprache.

Literatur

Der Leittext ist

  • Crole: "Categories for Types", Cambridge Mathematical Textbooks, 1993

Weitere informatikerfreundliche Einführungen sind

  • Awodey: "Category Theory", Clarendon Press, Oxford 2006
  • Adámek, Herrlich, Strecker: "Abstract and Concrete Categories - The Joy of Cats", Online Edition 2004

Nach wie vor die Standardeinführung in die Kategorientheorie:

  • MacLane: "Categories for the Working Mathematician", 2nd edition, Springer 1998
Artikelaktionen
Auf einen Blick
Lehrform Vorlesung/Übung
Empfohlen ab FS 5
Voraussetzungen

Kenntnisse in Logik empfehlenswert, aber nicht zwingend nötig.

Benotet Ja
Punkte gesamt 6
davon praktisch 0
Sprache deutsch
Fremdhörer zugelassen? Nein
Teilgebiete Theoretische Informatik(2000), Angewandte Informatik(4000), Wahlfrei(7000)
Studiengang Bachelor, Master
Belegung via PULS