Behörighetskrav

120 högskolepoäng varav 90 högskolepoäng i matematik och datavetenskap. Vana vid algebraiska strukturer motsvarande Algebra II. Algebraiska strukturer och Logik II eller Mängdlära är en fördel. Bakgrund inom programsemantik eller beräkningsteori kan underlätta förståelsen.

Mål

Efter godkänd kurs ska studenten kunna

• använda gitterteoretiska begrepp;
• redogöra för olika fixpunktsatser, samt deras samband med rekursiva procedurer;
• redogöra för olika kategorier av domäner och för vanliga konstruktioner av domäner såsom funktionsrum, produkt och summa inom olika kategorier;
• redogöra för tolkning av enkel typad lambdakalkyl i kartesiskt slutna kategorier;
• redogöra för sambandet mellan beräkningsbarhet och kontinuitet;
• resonera i en abstrakt kategori om begrepp som produkt, exponent och monader;
• redogöra för datastrukturer som lösningen till domänekvationer eller som initiala eller finala algebror;
• lösa domänekvationer och ge en modell för otypad lambdakalkyl;
• redogöra i stora drag för PCF och sambandet mellan dess operationella och denotationella semantik.

Innehåll

Fixpunkter. Olika domänbegrepp: cpo, algebraisk cpo, Scott-Ershovdomäner. Domänkonstruktioner, domänekvationer och teorin för deras lösningar. Något om topologiska begrepp med anknytning till domänteori. Alternativa sätt att presentera domäner: omgivningssystem, informationssystem. Något om beräkningsbara domäner, potensdomäner, universaldomäner eller formella topologiska rum.

Kategoriteoretiska begrepp: Adjunktioner, initiala och finala algebror, monader, monoidala kategorier och funktorkategorier.

Modeller för lambdakalkyl. Operationell och denotationell för PCF. Eventuellt något om spelsemantik. Semantik för kvantprogrammeringsspråk.

Undervisning

Föreläsningar och räkneövningar.

Examination

Skriftligt och eventuellt muntligt prov vid kursens slut eventuellt kombinerat med inlämningsuppgifter under kursen enligt anvisningar som lämnas vid kursens start.