Typteori och lambdakalkyl

10 hp

Kursplan, Avancerad nivå, 1MA059

Det finns en senare version av kursplanen.
Kod
1MA059
Utbildningsnivå
Avancerad nivå
Huvudområde(n) med fördjupning
Matematik A1F
Betygsskala
Med beröm godkänd (5), Icke utan beröm godkänd (4), Godkänd (3), Underkänd (U)
Fastställd av
Teknisk-naturvetenskapliga fakultetsnämnden, 6 november 2007
Ansvarig institution
Matematiska institutionen
Vad är en kursplan?

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