Leírás
BME Algebra Tanszék szemináriuma
ABSZTRAKT:
Martin-Löf típuselmélete egy programozási nyelv, melyben matematikai
bizonyítások is formalizálhatók. A logikai állítások típusoknak
felelnek meg, a bizonyítások adott típusú programoknak. Így a
programok típusellenőrzése bizonyításellenőrzésre is használható. A
típusok két fő csoportba sorolhatók: induktív és koinduktív
típusok. Induktív például a természetes számok típusa, a logikai
hamis, a logikai vagy, az egzisztenciális kvantor, általánosságban a
szabad algebrák típusa tetszőleges algebrai struktúrára. Koinduktív az
implikáció, az univerzális kvantor, a logikai és, a Turing-gépek
típusa. Hagyományosan az egyenlőség típus is induktív, ennek néhány
negatív következményével. Az előadásban bevezetést adok Martin-Löf
típuselméletébe, majd bemutatom a típuselmélet egy továbbfejlesztését,
melyben az induktív típusok egyenlősége induktív, a koinduktív típusok
egyenlősége koinduktív, és teljesül Vladimir Voevodsky univalence
axiómája. (Még nem befejezett közös munka Thorsten Altenkirch-el és
Michael Shulman-nal.)