Behörighetskrav

120 hp samt Logik II eller Tillämpad logik. Engelska 6. (Med en svensk kandidatexamen uppfylls kravet på engelska.)

Mål

Efter godkänd kurs ska studenten kunna:

• behärska lambdakalkyl och typinferens;
• kunna redogöra för huvuddragen i bevisen för konfluens och normalisering för en typad lambdakalkyl;
• vara förtrogen med algoritmisk tolkning av logik;
• kunna genomföra formella bevis i typteori och logiska system baserade på intuitionistisk logik;
• känna till grunderna och principerna i konstruktiv matematik;
• kunna motivera typkonstruktioner genom informella meningsförklaringar;
• känna till de viktigaste metamatematiska egenskaperna hos typteorier.

Innehåll

Lambdakalkyl: otypad lambdakalkyl, reduktion och konversion, Church-Rosseregenskapen, normalformer, Churchnummer och representation av rekursiva funktioner. Lat och ivrig evaluering. Böhmträd. Typad lambakalkyl: typinferens, typkonstruktioner. Beroende typer. Stark och svag normalisering. Modeller för lambdakalkyl.

Typteori: kontext, kontextavbildningar, omdömesformer, meningsförklaringar. BHK-tolkningen. Beroende produkt- och summatyper. Induktiva typer. Likhetstypen. Typuniversum. Induktivt rekursiva typer. Bevisteoretiska egenskaper och modeller för typteori. Logiska ramverk.

Konstruktiv matematik i typteori: mängder som typer med ekvivalensrelationer. Egenskaper hos mängdteorin. Intuitionistisk logik. Exempel från konstruktiv matematik: algebra, analys och topologi. Exekverbara bevis.

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.