Homotopi typteori

Homotopy type theory ( HoTT , från engelska homotopy type theory ) är en matematisk teori, en specialversion av typteori , utrustad med begrepp från kategoriteori , algebraisk topologi , homologisk algebra ; bygger på förhållandet mellan begreppen homotopityp av rymd, högre kategorier och typer i logik och programmeringsspråk .

Univalent Foundations of Mathematics är ett program för att konstruera ett universellt formellt språk med hjälp av homotopitypteori, som är en konstruktiv grund för moderna grenar av matematik och ger möjligheten att automatiskt kontrollera korrektheten av bevis på en dator . Initierad av Vladimir Voevodsky i slutet av 2000-talet; drivkraften för ett bredare intresse för univalenta stiftelser var biblioteket för formaliserad matematik "Foundations" skrivet av Voevodsky, som blev en del av UniMath- biblioteket i mitten av 2010-talet och fungerade som basen för många andra bibliotek ; av ett stort team av matematiker .

Matematiska bevis inom homotopitypteorin består i att fastställa "bebobarheten" för den önskade typen, det vill säga att konstruera ett uttryck av motsvarande typ. Användningen av automatiska bevissystem för teorin utnyttjar idén om Curry-Howard-isomorfism , och tack vare det matematiska innehållet inbäddat i de typteoretiska begreppen, i teorins formella språk, är det möjligt att uttrycka och verifiera snarare komplexa resultat från abstrakta delar av matematiken som tidigare ansågs inte kunna formaliseras av programvara.

Teorins nyckelidé är univalensaxiomet , som postulerar likheten mellan objekt mellan vilka ekvivalens kan fastställas, det vill säga i homotopitypteori anses isomorfa, homeomorfa, homotopiskt ekvivalenta strukturer vara lika; detta axiom fångar viktiga egenskaper för tolkning av högre kategori och ger också en teknisk förenkling av det formella språket.

Historik

Tanken på att använda Per Martin-Löfs intuitionistiska typteori för att formalisera högre kategorier går tillbaka till Mihai Makkais ( Hung. Makkai Mihály ) arbete, där FOLDS ( första ordningens logik med beroende sorter ) byggdes upp. [1] . Den viktigaste skillnaden mellan univalenta baser och Mackays idéer är principen att matematikens grundläggande objekt inte är högre kategorier, utan högre gruppoider. Eftersom de högre groupoiderna motsvarar Grothendieck-överensstämmelsen med homotopityper , kan man säga att matematik, i termer av univalenta baser, studerar strukturer på homotopityper. Möjligheten att direkt använda Martin-Löfs typteori för att beskriva strukturer på homotopityper är en konsekvens av Voevodskys konstruktion av en univalent modell av typteori. Konstruktionen av denna modell krävde lösningen av många tekniska problem förknippade med de så kallade koherensegenskaperna, och även om huvudidéerna för univalenta baser formulerades av honom 2005–2006, dök bara en komplett univalent modell i kategorin för enkla uppsättningar upp. år 2009 . Under samma år som dessa studier av Voevodsky genomfördes andra arbeten för att studera olika kopplingar mellan typteori och homotopiteori, i synnerhet en av de historiskt viktiga händelserna som förde samman forskare som arbetade i denna riktning var ett seminarium i Uppsala i november 2006 år [2] .

I februari 2010 började Voevodsky att skapa ett bibliotek på Coq , som sedan växte till ett "bibliotek med univalenta baser" gemensamt utvecklat av ett brett spektrum av forskare .

På initiativ av Voevodsky utropades läsåret 2012–2013 vid Institutet för avancerade studier till "året för univalenta stiftelser", ett särskilt forskningsprogram öppnades i samarbete med Audi och Kokan , och inom dess ram en grupp matematiker och datavetare arbetade med teoriutveckling. Ett av årets resultat var deltagarnas gemensamma skapande av den sex hundra sidor långa boken " Homotopic Type Theory: Univalent Foundations of Mathematics ", som publicerades på programmets webbplats för fri tillgång under CC-SA-licensen ; ett projekt på GitHub [3] skapades för att samarbeta om boken .

Deltagare i programmet, presenterade i inledningen till boken [4] :

Thorsten Altenkirch ( engelska Thorsten Altenkirch )
Benedikt Ahrens ( Benedikt Ahrens )
Steve Audi _ _ _
Bruno Barras ( Bruno Barras )
Andrej Bauer ( slovenska Andrej Bauer )
Marc Bezem ( Marc Bezem )
Yves Bertot ( Yves Bertot )
Benno van den Berg
Vladimir Voevodsky
Daniel Grayson ( Daniel Grayson , skapare av Macaulay2 datoralgebrasystem )
André Joyal ( franska André Joyal )
Thierry Cocan
Dan Licata ( Dan Licata )
Peter Lumsdaine ( Peter Lumsdaine )
Per Martin-Löf
Assia Mahboubi ( Assia Mahboubi )
Sergei Melikhov
Alvaro Pelayo ( Alvaro Pelayo )
Andrew Polonsky _ _
Matthieu Sozeau _ _
Bas Spitters ( Bas Spitters )
Michael Warren ( Michael Warren )
Eric Finster ( Eric Finster )
Noam Zeilberger ( Noam Zeilberger )
Michael Shulman _ _ _
Peter Aczel _ _ _
Hugo Herbelin , Coq utvecklingsprojektledare

Dessutom indikerar inledningen att sex studenter också gjorde betydande bidrag, och noterar också bidraget från mer än 20 vetenskapsmän och praktiker som besökte Institutet för högre studier under "året av univalenta grunder" (inklusive skaparen av semantiken i λ-kalkyl Dana Scott och utvecklarens formaliseringar på Coq av bevisen för fyrfärgsproblemet och Feit-Thompson-satsen ( Georges Gontier ). Boken är uppbyggd i två delar - "Fundamentals" och "Matematik", i den första delen anges huvudbestämmelserna och verktygen definieras, i den andra - implementeringar av homotopiteorin, kategoriteorin , mängdläran , reella tal är byggd med de införda medlen .

Grunderna

Teorin bygger på en intensional variant av Martin-Löfs intuitionistiska typteori och använder tolkningen av typer som objekt för homotopiteorin och högre kategorier. Så ur denna synvinkel anses förhållandet att tillhöra en punkt till rymden som en term av motsvarande typ: , en bunt med en bas - som en beroende typ . I det här fallet finns det inget behov av att representera utrymmen i form av uppsättningar av punkter utrustade med topologin , och att representera kontinuerliga avbildningar mellan utrymmen som funktioner som bevarar eller reflekterar motsvarande punktvisa egenskaper hos utrymmen. Homotopi typteori betraktar typrum och termer av dessa typer (punkter) som elementära begrepp, och konstruktioner över rum, såsom homotopier och buntar, som beroende typer. $a\i A$ $a:A$ $X$ $Yxa)$

I den formella konstruktionen av typteorin används typuniversumet, vars termer är alla andra icke-universella ("små") typer, sedan konstrueras typer så att dessutom alla termer för typen också är termer av typen . Beroende typer (typfamiljer) definieras som funktioner vars koddomän är något typuniversum. ${\mathcal U}_{0}$ ${\mathcal U}_{1},{\mathcal U}_{2},\dots$ $U_{i}:U_{{i+1}}$ ${\mathcal U}_{i}$ ${\mathcal U}_{{i+1}}$ $B:A\to {\mathcal U}$

Inom homotopitypteori finns det flera sätt att konstruera nya typer från befintliga. Grundläggande exempel av detta slag är -typer (beroende funktionstyper, produkttyper ) och -typer (beroende summatyper ) . För en given typ och familj kan man konstruera en typ vars termer är funktioner vars koddomän beror på ett element i definitionsdomänen (geometriskt kan sådana funktioner representeras som sektioner av någon bunt), såväl som en typ vars termer geometriskt motsvarar delar av buntens totala utrymme . ${\boldsymbol \Pi }$ ${\boldsymbol \Sigma }$ $A:{\mathcal U}$ $B:A\to {\mathcal U}$ ${\boldsymbol \Pi }_{{x:A}}B(x)$ ${\boldsymbol \Sigma }_{{x:A}}B(x)$

Likhet mellan termer av samma typ i teorin om homotopityp kan antingen vara en likhet "per definition" ( ) eller en propositionell likhet. Jämlikhet innebär per definition propositionell jämlikhet, men inte vice versa. I allmänhet representeras den propositionella likheten mellan termer och typ som en icke-tom typ , som kallas en identitetstyp; termerna för denna sista typ är synens vägar i rymden ; identitetstypen ses alltså som utrymmet av vägar (d.v.s. kontinuerliga avbildningar av enhetssegmentet till ) från punkt till punkt . $a_{1}:=a_{2}$ $a_{1}$ $a_{2}$ $A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $p:a_{1}\rightsquigarrow a_{2}$ $A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $\mathbb {I}$ $A$ $a_{1}$ $a_{2}$

Axiom för univalens

Den intuitionistiska teorin om typer tillåter oss att definiera begreppet typekvivalens (för typer som tillhör samma universum) och att konstruera en funktion på ett kanoniskt sätt från en identitetstyp till en ekvivalenstyp : $A=B$ $A\simeq B$

(A=B)\to (A\simeq B)

Univalensaxiomet , formulerat av Voevodsky, säger att denna funktion också är en ekvivalens:

(A=B)\simeq (A\simeq B)

det vill säga identitetstypen för två givna typer är ekvivalent med ekvivalenstypen för dessa typer. Om och är satstyper, har axiomet en särskilt genomskinlig innebörd och kokar ner till vad som ibland kallas kyrkans princip om extensionalitet: satsernas likhet är logiskt likvärdig med deras logiska likvärdighet; Användningen av denna princip innebär att endast sanningsvärdena för uttalanden beaktas, men inte deras betydelse. En konsekvens av axiomet är funktionell extensionalitet , det vill säga påståendet att funktioner vars värden är lika för alla lika värden av deras argument är lika med varandra. Denna egenskap hos funktioner är viktig inom datavetenskap. $A$ $B$

Axiomet anses av vissa matematikfilosofer som en exakt matematisk formulering av huvuduppsatsen i filosofin om matematisk strukturalism , som är baserad på den vanliga praktiken av matematiska resonemang "upp till isomorfism " eller "upp till ekvivalens " [ 5] .

Logik, uppsättningar, gruppoider

En proposition ( enbart proposition , " bar proposition ") i homotopitypteori definieras som en typ som antingen är tom eller innehåller en enda term ; sådana typer kallas propositionella. Om typen är tom är motsvarande proposition falsk; om den innehåller en term (symboliskt - ), är motsvarande proposition sann och termen anses vara dess bevis. Således använder teorin det intuitionistiska sanningsbegreppet, enligt vilket sanningen i ett påstående förstås som möjligheten att presentera ett bevis på detta påstående. $P$ $sid$ $P$ $P$ $sid$ $p:P$ $P$ $sid$

Ett fragment av teorin om homotopityp, som är begränsad till operationer med propositionstyper, det vill säga med propositioner, kan beskrivas som ett logiskt fragment (logik) av denna teori. Den logiska disjunktionen i propositionsfragmentet motsvarar summatypen , konjunktionen produkttypen , implikationen till funktionstypen , negationen till typen , där är den tomma typen (noll-typen). Logiken som motsvarar sådana konstruktioner är en variant av intuitionistisk logik , i synnerhet påståenden som lagen om dubbel negation eller den uteslutna mitten äger inte rum i den . $A\vee B$ $A+B$ $A\wedge B$ $A\ gånger B$ $A\högerpil B$ $A till B$ $\linte A$ $A\to \mathbf {0}$ ${\mathbf 0}$

Vilken typ som helst som innehåller två eller flera distinkta termer kan sättas i en-till-en-korrespondens med en propositionell typ, som erhålls genom att identifiera alla termer av typ , en sådan operation kallas propositionell trunkering ( propositionell trunkering ). Detta gör det möjligt att skilja mellan en teoris "propositionella nivå" (påståendenivå) och homotophierarkin för dess "högre" icke-propositionella nivåer. $X$ $x,y,\dots$ $X$

Nivån på propositioner följs av nivån på uppsättningar . En mängd i homotopitypteori definieras som ett utrymme (typ) med en diskret topologi . På motsvarande sätt kan en mängd i teorin beskrivas som en typ så att typen för någon av dess termer är en proposition, det vill säga antingen tom (fallet när och är olika element i mängden ) eller så innehåller den ett enda element (den fall när och är samma element). Efter nivån av uppsättningar kommer nivån av groupoids (uppsättningen av punkter och uppsättningen av banor mellan varje par av punkter), och nivåerna av -groupoids av alla ordningar. $A$ $a_{1},a_{2}:A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $a_{1}$ $a_{2}$ $A$ $a_{1}$ $a_{2}$

Olika tolkningar av typteoretiska begrepp

Bibliotek och implementeringar av HoTT

HoTT-biblioteken är flera projekt som finns på GitHub (i samma arkiv där bokens källkod finns) som skapar formella beskrivningar av olika grenar av matematiken med hjälp av automatiska bevissystem med konstruktioner av homotopitypteori.

I Vladimir Voevodskys projekt, kallat "Library of univalent bases" [6] , används en speciellt utvecklad minimal säker delmängd Coq , som ger ideologisk renhet och tillförlitlighet av konstruktioner i enlighet med teorin. HoTT-projektet [7] drivs av standardverktyg från Coq, implementerade som en del av forskningsprogrammet för Institute for Advanced Study, och följer i allmänhet boken , från och med 2020 deltar 48 utvecklare i projektet, de flesta aktiva är Jason Gross, Michael Shulman, Ali Kaglayan och Andrey Bauer [8] . Det finns också ett parallellt projekt i Agda [9] .

Det finns flera experimentella interaktiva bevissystem helt baserade på HoTT: Arend , RedPRL, redtt, cooltt, och i Agda version 2.6.0 lades det så kallade "kubiska läget" till, vilket tillåter full användning av homotopityper.

Anteckningar

↑ Makkai Mihaly. Första ordningens logik med beroende sorteringar, med tillämpningar till kategoriteori (engelska) (1995). Hämtad 5 december 2014. Arkiverad från originalet 10 oktober 2015.
↑ Identitetstyper - Topologisk och kategorisk struktur . Verkstad, Uppsala, 13-14 november 2006 (2006) . Datum för åtkomst: 5 december 2013. Arkiverad från originalet 18 december 2014. (obestämd)
↑ Homotopy Type Theory: Univalent Foundations of Mathematics Projektkällkoder på GitHub
↑ HoTT, 2013 , sid. iii.
↑ Steve Avodey. Strukturalism, invarians och univalens // Philosophia Mathematica . - Oxford University Press , 2014. - V. 22 , nr 1 . — ISSN 0031-8019 . - doi : 10.1093/philmat/nkt030 .
↑ Univalent Base Library Project på GitHub
↑ Homotopy Type Theory Project på GitHub
↑ HoTT 20 mars 2011 – 2 oktober 2020 Bidrag till master, exklusive sammanslagningar .
↑ Agda HoTT-biblioteksprojekt på GitHub

Litteratur

Homotopy Type Theory: Univalent Foundations of Mathematics . - Princeton : Institute for Advanced Study , 2013. - 603 sid.
Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodskys Univalence Axiom in Homotopy Type Theory (engelska) // Notices of the AMS . - 2013. - Vol. 60 , nej. 9 . - P. 1164-1167 .
Hannes Hummel. Kommer datorer att omdefiniera matematikens rötter? . När en legendarisk matematiker hittade ett misstag i sitt eget arbete, inledde han en datorstödd strävan att eliminera mänskliga misstag. För att han måste skriva om de hundra gamla reglerna som ligger till grund för all matematik . Quanta Magazine (19 maj 2015) . Hämtad: 31 december 2017.
Don Monroe. En ny typ av matematik? (engelska) // Kommunikation från ACM . - 2014. - Vol. 57 , nr. 2 . - S. 13-15 . - doi : 10.1145/2557446 .
Andrey Rodin. Logisk och geometrisk atomism från Leibniz till Voevodsky // Filosofiens problem . - 2016. - Nr 6 . - S. 134-142 .

Länkar

cs.cmu.edu/~rwh/courses/hott/ - kursmaterial om homotopi typteori som undervisas av Robert Harper vid Carnegie Mellon University