Teoria kategorii dla informatyków

Z Studia Informatyczne
Wersja z dnia 18:39, 10 cze 2006 autorstwa Pqw (dyskusja | edycje) (sylabus: 10.06.06)
(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Przejdź do nawigacjiPrzejdź do wyszukiwania

Forma zajęć

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

Autor

Paweł Waszkiewicz

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.

Cel wykładu

Po pierwsze, 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. Po drugie, zbadamy zastosowania teorii kategorii w informatyce. Nie wymagamy od słuchaczy wykładu specjalnego przygotowania, ale pewna ich erudycja i dojrzałość matematyczna będą nieocenione, gdyż 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

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.

  • Kategorie jako abstrakcyjny język funkcyjny
    • definicja
    • izomorfizmy
    • grafy i kategorie wolne
    • przykłady: k.dyskretne, k.konkretne, Pos, monoidy, grupy jako kategorie, etc.
    • podstawy teoriomnogościowe: kategorie małe, duże, lokalnie małe
  • Morfizmy specjalne
    • mono- i epimorfizmy
    • sekcje i retrakcje, przykłady w Pos, Top
    • uogólnione elementy, listy
  • Zasada dualności i proste konstrukcje uniwersalne
    • produkty i koprodukty
    • pullbacki i pushouty
    • ekwalizatory i koekwalizatory
    • obiekt końcowy i początkowy
    • podobiekty
  • Zaawansowane konstrukcje uniwersalne
    • eksponent
    • kategorie kartezjańsko zamknięte; algebry Heytinga
    • teoria zbiorów abstrakcyjnych: program Lawverego
  • Funktory i transformacje naturalne
    • pojecie funktora, przykłady
    • funktory wolne i funktory zapominania
    • funktory pełne i wierne
    • transformacje naturalne; naturalne izomorfizmy
  • Równoważność kategorii
    • dualność Stone'a
  • Lemat Yonedy i funktory reprezentowalne
    • przykłady
    • 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
    • kartezjańsko zamknięte kategorie dziedzin; posety bc-zupełne
  • Teoria dziedzin II
    • dziedziny Scotta jako modele języków funkcyjnych
    • równania na dziedzinach typu
  • Ilościowa teoria dziedzin
    • uogólnione przestrzenie metryczne
    • dziedziny quasimetryzowalne
    • problemy otwarte ilościowej teorii dziedzin
  • 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. M. Barr, C. Wells, Category Theory for Computing Science, Cambridge University Press, 1995.
  3. S. MacLane, Categories for the Working Mathematician, Springer 1991.
  4. D. Turi, Category Theory Lecture Notes, Uniwersity of Edinburgh. Dostępne z: www.dcs.ed.ac.uk/home/dt/CT/categories.ps

Moduły