Behörighetskrav

120 högskolepoäng samt Logik II eller Tillämpad logik.

Mål

För godkänt betyg på kursen skall studenten

• 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.