Kategorientheorie und Logik
- Vorlesung, Dr. rer. nat. Richter, Di. 10:00-12:00, 3.04.0.02
Ursprünglich wurde die Kategorientheorie entwickelt, um wiederkehrende Konzepte und Konstruktionen, die bei verschiedenen algebraischen Strukturen auftauchen, in einer einheitlichen Sprache zu beschreiben und so den Übergang von einer Struktur in eine andere transparenter zu machen. In den letzten 20 Jahren hat auch die Theoretische Informatik regen Gebrauch von dieser Sprache gemacht, insbesondere bei der Entwicklung von Programmiersprachen. Ein Grund dafür ist, dass sowohl die Theorie der Programmiersprachen als auch die Kategorientheorie im wesentllchen Theorien von Funktionen sind.
Das Ziel der Vorlesung besteht darin, den Hörern Konzepte aus der Kategorientheorie vorzustellen, die für Anwendungen in der Informatik besonders relevant sind. Es werden verschiedene kategoriale Konstruktionen wie Produkte und Summen, Differenzkerne und Pullbacks betrachtet. Eine zentrale Rolle bei der Beschreibung der Beziehungen zwischen verschiedenen Kategorien spielen Funktoren, insbesondere adjungierte Funktorpaare und Monaden. Funktoren verwendet man außerdem um komplexere Strukturen wie Algebren oder Automaten zu beschreiben. Im letzten Teil der Vorlesung wird die Beziehung zwischen kartesisch abgeschlossenen Kategorien, intuitionistischer Logik und getyptem Lambda-Kalkül untersucht.
Literatur
- Asperti, A., Longo, G. : Categories, Types and Structures
- Barr, M. , Wells, C.: Category Theory for Computer Science
- MacLane, S.: Categories for the Working Mathematician
- Goldblatt, R. : Topos Theory
