Behörighetskrav

120 hp varav 90 hp 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. Engelska 6. (Med en svensk kandidatexamen uppfylls kravet på engelska.)

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 prov vid kursens slut kombinerat med inlämningsuppgifter under kursen enligt anvisningar som lämnas vid kursens start.

Om särskilda skäl finns får examinator göra undantag från det angivna examinationssättet och medge att en enskild student examineras på annat sätt. Särskilda skäl kan t.ex. vara besked om särskilt pedagogiskt stöd från universitetets samordnare för studenter med funktionsnedsättning.