Kategorientheorie und Logik - Einzelansicht

Die Kategorientheorie ist eine "allgemeine Theorie mathematischer Strukturen" (Wikipedia).
In den 1940er Jahren als Zweig der reinen Mathematik entstanden, wird sie heute auch für
Physiker, Philosophen, Theoretische Informatiker und nicht zuletzt Programmierer immer
wichtiger: als Systematisierungswerkzeug, aber auch als Inspirationsquelle.

Der Begriff der Kategorie abstrahiert den mengentheoretischen Funktionsbegriff:  Funktionen
f: B -> C und g: A -> B zwischen Mengen A,B,C können zu einer Funktion f . g : A -> C
"komponiert" werden. Als Kategorie bezeichnet man nun eine Kollektion von "Pfeilen" mit
einer Kompositionsstruktur, die die wesentlichen Eigenschaften der Funktionenkomposition erfüllt.
Viele "strukturerhaltende" Abbildungen wie etwa lineare Abbildungen zwischen Vektorräumen,
stetige Abbildungen zwischen topologischen Räumen, Homomorphismen algebraischer Strukturen
usw. können wie Mengenfunktionen komponiert werden und bilden auf diese Weise Kategorien.
Aber Pfeile müssen keine Funktionen sein: Man untersucht z.B. Kategorien, deren Pfeile die
Pfade in einem gerichteten Graphen, Wörter über einem Alphabet, Relationen zwischen Mengen
oder Programme einer funktionalen Programmiersprache sind.

Informatiker benutzen die Kategorientheorie z.B. im Programmiersprachendesign und für die
Spezifikation und Verifikation von Software. Für viele funktionale Programmierer gehört das
Denken in kategorientheoretischen Begriffe heute zum Tagesgeschäft.

Die Veranstaltung wird zunächst die grundlegenden Konzepte der Kategorientheorie einführen:
Kategorie, Funktor, natürliche Transformation, Limes und Kolimes, Adjunktion, Monade.
Im zweiten Teil werden wir die Beziehung cartesisch abgeschlossener Kategorien zu einfach
getypten Lambda-Kalkülen und zur intuitionistischen Logik untersuchen.

Die Beweise der Kategorientheorie sind zuweilen länglich, meist aber sehr geradlinig. Wir werden
deshalb einen guten Teil der Beweise nicht in der Vorlesung präsentieren, sondern im Rahmen der
Übungen gemeinsam erarbeiten. Zum Verständnis der Vorlesung ist daher eine aktive Teilnahme
an den Übungen essentiell.

siehe https://www.logicmatters.net/categories/

Vorkenntnisse in formaler Logik und funktionaler Programmierung sind von Vorteil, aber nicht zwingend nötig.