Teoria kategorii w podstawach informatyki

monograficzne

w sali

Algebra ogólna i teoria kategorii to klasyczne juz działy matematyki oferujące abstrakcyjne pojęcia, metody i wyniki, które zaadoptowane zostały przez podstawy informatyki i stanowią dziś standardowy język mówienia między innymi o modelowaniu, projektowaniu i systematycznym konstruowaniu złożonych systemów oprogramowania.

Wykład przypomni podstawowe pojęcia algebry ogólnej i od podstaw wprowadzi język teorii kategorii, z konieczności ograniczając sie do pojęć najważniejszych i dotyczących ich podstawowych wyników. Zasygnalizujemy przynajmniej, jak język ten wykorzystywany jest w różnych dziedzinach informatyki, między innymi w teorii typów czy w teorii specyfikacji algebraicznych.

Do wykładu przewidziane są ćwiczenia, w praktyce przeplatane z wykładem. Wykład może być prowadzony w języku angielskim, ale w przypadku braku studentów obcojęzycznych, zajęcia zapewne będą prowadzone po polsku.

Plan:

 Zbiory wielorodzajowe, podstawowe pojęcia i notacje teorii mnogości.

 Algebry wielorodzajowe i podstawowe pojęcia algebraiczne.

 Termy, równości, rozmaitości algebr; rachunek równościowy.

 Algebry początkowe, specyfikacje algebraiczne z początkową semantyką.

 Pokrewne środowiska algebraiczne.

 Pojęcie kategorii i najprostsze definicje kategoryjne.

 Granice i kogranice.

 Funktory i transformacje naturalne.

 Funktory sprzężone.

 Monady i algebry funktorów.

 Kategorie kartezjańsko domknięte i semantyka rachunku lambda z typami.

 G. Graetzer, Universla Algebra, Springer, 1979.

 S. MacLane, Categories for the Working Mathematician, Springer, 1971

 D.T. Sannella, A. Tarlecki, Foundations of Algebraic Specificiations and Formal Program Development, Springer, 2012.

Wiedza:

 Zna podstawowe pojęcia oraz najważniejsze klasyczne wyniki algebry ogólnej (K_W01, K_W02).

 Zna podstawowe pojęcia oraz proste wyniki teorii kategorii (K_W01, K_W02).

 Zna i rozumie niektóre zastosowania algebry ogólnej i teorii kategorii w podstawach informatyki (K_W01, K_W02).

Umiejętności:

 Potrafi potrafi udowodnić niektóre klasyczne wyniki algebry ogólnej i proste wyniki teorii kategorii (K_U01).

 Potrafi znależć interpretację abstrakcyjnych pojęć algebry ogólnej i teorii kategorii w konkretnych środowiskach logicznych (K_U01, K_U09, K_U10).

 Potrafi znależć uogólnienie pojęć i własności konkretnych środowisk logicznych w terminach algebry ogólnej i teorii kategorii (K_U01, K_U09, K_U10).

 Potrafi uzasadnić metody budowania modularnych programów funkcyjnych w terminach algebry ogólnej i teorii kategorii (K_U01, K_U02, K_U10).

Kompetencje:

 Zna ograniczenia własnej wiedzy i rozumie potrzebę dalszego kształcenia, w tym zdobywania wiedzy pozadziedzinowej (K_K01).

 Potrafi precyzyjnie formułować pytania, służące pogłębieniu własnego zrozumienia danego tematu lub odnalezieniu brakujących elementów rozumowania (K_K02).

Egzamin pisemny, oceniany przez prowadzącego, może mieć formę większego zadania o wielu podzadaniach, do samodzielnego rozwiązania w domu.

Ewentualną chęć zdawania we wcześniejszym terminie proszę zgłosić prowadzącemu.

Dla zaliczających ten przedmiot doktorantów zostanie dodane trudniejsze podzadanie lub odrębne zadanie na bardziej zaawansowanym poziomie.