Teoria kategorii dla informatyków

Forma zajęć

Wykład (30 godzin) + ćwiczenia (30 godzin)

Opis

Stefan Banach powiedział kiedyś, ze dobry matematyk to taki, który potrafi znaleźć analogie pomiędzy twierdzeniami, zaś wybitny matematyk to ten, który widzi analogie pomiędzy analogiami. Teoria kategorii jest nauką o analogiach między teoriami matematycznymi. Daje ona jednolity obraz różnorodnych (tzw. uniwersalnych) konstrukcji, które pod wieloma postaciami i nazwami pojawiają się w różnorodnych gałęziach matematyki.

Teoria kategorii wyrosła z prac Samuela Eilenberga i Saundersa MacLane'a w topologii algebraicznej i algebrze homologicznej prowadzonych w latach 40tych ubiegłego stulecia. Od tamtego czasu zarówno język, jak i metody teorii kategorii spowodowały ujednolicenie i uproszczenie wielu pojęć algebry, topologii, geometrii algebraicznej, analizy funkcjonalnej, a także, ostatnimi czasy, logiki matematycznej i informatyki teoretycznej.

Wykład ma za cel uświadomienie słuchaczom jedności wielu dyscyplin matematycznych, które są często prezentowane jako oddzielne, niezwiązane ze sobą przedmioty. Zbadamy zastosowania teorii kategorii w informatyce. Omawiamy przykłady konstrukcji uniwersalnych z różnorodnych gałęzi matematyki i informatyki: analizy, algebry, logiki, topologii, teorii dziedzin i semantyki języków programowania, lambda rachunku, teorii obliczalności. Student, który ukończy kurs z ocena pozytywna powinien sprawnie posługiwać się podstawowym aparatem pojęciowym teorii kategorii, który jest często oficjalnym językiem wielu prac naukowych w informatyce teoretycznej.

Sylabus

Autor

• Paweł Waszkiewicz

Wymagania wstępne

• Logika i teoria mnogości

Zawartość

Część pierwsza wykładu obejmuje tematy fundamentalne: kategorie, funktory, transformacje naturalne, równoważność kategorii, zasadę dualności, granice i kogranice, lemat Yonedy i funktory reprezentowalne, sprzężenia i monady. Część druga skupia się na zastosowaniach teorii kategorii w informatyce, wybierając spośród tematów dotyczących: kategorii kartezjańsko zamkniętych i lambda rachunku, koalgebr, koindukcji i bisymulacji, teorii dziedzin i rozwiązywania równań na dziedzinach. Ćwiczenia, ilustrujące wykład, budują zestaw sztandarowych przykładów konkretnych kategorii, funktorów i ich własności.

• Teoria kategorii jako abstrakcyjna teoria funkcji
  • definicja
  • przykłady: k.dyskretne, k.konkretne, Pos, monoidy, grupy jako kategorie, etc.
  • izomorfizmy
  • podstawy teoriomnogościowe: kategorie małe, duże, lokalnie małe

• Morfizmy specjalne
  • mono- i epimorfizmy
  • sekcje i retrakcje
  • uogólnione elementy

• Zasada dualności i proste konstrukcje uniwersalne
  • produkty i koprodukty
  • pullbacki i pushouty
  • ekwalizatory i koekwalizatory
  • obiekt końcowy i początkowy

• Zaawansowane konstrukcje uniwersalne
  • eksponent
  • kategorie kartezjańsko zamknięte; algebry Heytinga

• Funktory i transformacje naturalne
  • pojecie funktora, przykłady
  • funktory zapominania
  • funktory pełne i wierne
  • transformacje naturalne; naturalne izomorfizmy

• Równoważność kategorii
  • dualność Stone'a

• Lemat Yonedy i funktory reprezentowalne
  • Lemat Yonedy, funktor Yonedy
  • funktory reprezentowalne
  • kategorie funktorów

• Diagramy, granice i kogranice
  • konstrukcje uniwersalne jako granice
  • granice jako funktory
  • zachowywanie granic przez funktory; funktory ciągłe
  • kogranice i eksponent w kategoriach diagramów
  • kategorie zupełne i kozupełne

• Sprzężenia I
  • trzy równoważne opisy zjawiska sprzężenia
  • sprzężenia w teoriach matematycznych: przykłady
  • sprzężenia jako fundamentalne pojęcie teorii kategorii

• Sprzężenia II
  • sprzężenia między posetami
  • kwantyfikatory jako sprzężenia
  • twierdzenie Freyda (zachowywanie granic przez sprzężenia)

• Monady
  • monady a sprzężenia
  • algebry dla monad
  • zastosowania teorii monad w semantyce języków programowania

• Teoria dziedzin I
  • ciągłość, zupełność i aproksymacja
  • topologia Scotta

• Teoria dziedzin II
  • dziedziny Scotta jako modele języków funkcyjnych
  • kartezjańsko zamknięte kategorie dziedzin

• Teoria dziedzin III
  • równania na dziedzinach typu $D\cong [D\to D]$

• Algebry i koalgebry endofunktorów
  • indukcja i koindukcja
  • analiza na nieskończonych listach
  • weryfikacja algorytmów sortujących listy

Literatura

1. A. Asperti, G.Longo, Categories, Types and Structures. An introduction to Category Theory for the working Computer Scientist, MIT Press, 1991.
2. S. Awodey Category theory. Wykład z uniwersytetu Carnegie Mellon. Dostępny tutaj.
3. M. Barr, C. Wells, Category Theory for Computing Science, Cambridge University Press, 1995.
4. S. MacLane, Categories for the Working Mathematician, Springer 1991.
5. D. Turi, Category Theory Lecture Notes. Wykład z uniwersytetu w Edynburgu. Dostępny tutaj.

Moduły

• Teoria kategorii jako abstrakcyjna teoria funkcji (Ćwiczenia)
• Morfizmy specjalne (Ćwiczenia)
• Zasada dualności i proste konstrukcje uniwersalne (Ćwiczenia)
• Zaawansowane konstrukcje uniwersalne (Ćwiczenia)
• Funktory i transformacje naturalne (Ćwiczenia)
• Równoważność kategorii (Ćwiczenia)
• Lemat Yonedy i funktory reprezentowalne (Ćwiczenia)
• Diagramy, granice i kogranice (Ćwiczenia)
• Sprzężenia I (Ćwiczenia)
• Sprzężenia II (Ćwiczenia)
• Monady (Ćwiczenia)
• Teoria dziedzin I (Ćwiczenia)
• Teoria dziedzin II (Ćwiczenia)
• Teoria dziedzin III (Ćwiczenia)
• Algebry i koalgebry endofunktorów (Ćwiczenia)