Homotopi type teori

Homotopy type theory ( HoTT , fra engelsk homotopy type theory ) er en matematisk teori, en speciel version af typeteori , udstyret med begreber fra kategoriteori , algebraisk topologi , homologisk algebra ; er baseret på forholdet mellem begreberne homotopi type rum, højere kategorier og typer i logik og programmeringssprog .

Univalent Foundations of Mathematics er et program til at konstruere et universelt formelt sprog ved hjælp af homotopi type teori, som er et konstruktivt grundlag for moderne grene af matematik og giver mulighed for automatisk at kontrollere korrektheden af beviser på en computer . Indledt af Vladimir Voevodsky i slutningen af 2000'erne; drivkraften til en bredere interesse for univalente fonde var biblioteket af formaliseret matematik "Foundations" skrevet af Voevodsky, som blev en del af UniMath -biblioteket i midten af 2010'erne og tjente som grundlag for mange andre biblioteker ; skrevet af et stort hold matematikere .

Matematisk bevis i homotopitypeteori består i at fastslå "beboeligheden" af den påkrævede type, det vil sige at konstruere et udtryk af den tilsvarende type. Brugen af automatiske bevissystemer til teorien udnytter ideen om Curry-Howard isomorfisme , og takket være det matematiske indhold, der er indlejret i de typeteoretiske begreber, i teoriens formelle sprog, er det muligt at udtrykke og verificere snarere komplekse resultater fra abstrakte dele af matematik, som tidligere blev anset for ikke at kunne formaliseres af software.

Teoriens nøgleide er univalensaksiomet , som postulerer ligheden af objekter, mellem hvilke ækvivalens kan etableres, det vil sige, i homotopitypeteori betragtes isomorfe, homøomorfe, homotopisk ækvivalente strukturer som ligeværdige; dette aksiom fanger vigtige egenskaber ved højere kategori fortolkning og giver også en teknisk forenkling af det formelle sprog.

Historie

Ideen om at bruge Per Martin- Löfs intuitionistiske typeteori til at formalisere højere kategorier går tilbage til Mihai Makkais arbejde ( Hung. Makkai Mihály ), hvor FOLDS ( førsteordens logik med afhængige sorter ) blev bygget. [1] . Den vigtigste forskel mellem univalente baser og Mackays ideer er princippet om, at matematikkens grundlæggende objekter ikke er højere kategorier, men højere gruppeoider. Da de højere groupoider svarer til Grothendieck-korrespondancen til homotopityper , kan man sige, at matematik, i form af univalente baser, studerer strukturer på homotopityper. Muligheden for direkte brug af Martin-Löf typeteori til at beskrive strukturer på homotopityper er en konsekvens af Voevodskys konstruktion af en univalent model for typeteori. Konstruktionen af denne model krævede løsningen af adskillige tekniske problemer forbundet med de såkaldte kohærensegenskaber, og selv om hovedideerne om univalente baser blev formuleret af ham i 2005-2006, dukkede en komplet univalent model i kategorien simple sæt kun op . i 2009 . I de samme år som disse undersøgelser af Voevodsky blev andre værker udført for at studere forskellige forbindelser mellem typeteori og homotopi-teori, især en af de historisk vigtige begivenheder, der samlede videnskabsmænd, der arbejdede i denne retning, var et seminar i Uppsala i november 2006 år [2] .

I februar 2010 begyndte Voevodsky at skabe et bibliotek på Coq , som efterfølgende voksede til et "bibliotek af univalente baser" i fællesskab udviklet af en bred vifte af videnskabsmænd .

På initiativ af Voevodsky blev studieåret 2012-2013 på Institute for Advanced Study erklæret "året for univalente fonde", et særligt forskningsprogram blev åbnet i samarbejde med Audi og Kokan , og inden for dets rammer en gruppe matematikere og dataloger arbejdede med udvikling af teori. Et af årets resultater var den fælles oprettelse af deltagerne af den seks hundrede sider lange bog " Homotopic Type Theory: Univalent Foundations of Mathematics ", der er lagt ud på programmets hjemmeside for gratis adgang under CC-SA-licensen ; et projekt på GitHub [3] blev oprettet for at samarbejde om bogen .

Deltagere i programmet, præsenteret i introduktionen til bogen [4] :

Thorsten Altenkirch ( engelsk Thorsten Altenkirch )
Benedikt Ahrens ( Benedikt Ahrens )
Steve Audi _ _ _
Bruno Barras ( Bruno Barras )
Andrej Bauer ( slovensk Andrej Bauer )
Marc Bezem ( Marc Bezem )
Yves Bertot ( Yves Bertot )
Benno van den Berg
Vladimir Voevodsky
Daniel Grayson ( Daniel Grayson , skaberen af Macaulay2 computeralgebrasystem )
André Joyal ( fransk 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 udviklingsprojektleder

Derudover indikerer introduktionen, at seks studerende også ydede betydelige bidrag, og bemærker også bidraget fra mere end 20 videnskabsmænd og praktikere, der besøgte Instituttet for Højere Studier i løbet af "året for univalente fonde" (inklusive skaberen af semantikken i λ-regning Dana Scott og udviklerens formaliseringer på Coq af beviserne for firefarveproblemet og Feit-Thompson-sætningen ( Georges Gontier ). Bogen er bygget op i to dele - "Fundamentals" og "Matematik", i den første del er hovedbestemmelserne angivet og værktøjerne defineret, i den anden - implementeringer af homotopi teorien, kategoriteori , mængdelære , reelle tal er bygget ved hjælp af de introducerede midler .

Grundlæggende

Teorien er baseret på en intensional variant af Martin-Löfs intuitionistiske typeteori og bruger fortolkningen af typer som objekter for homotopi-teori og højere kategorier. Så fra dette synspunkt betragtes forholdet mellem et punkts tilhørsforhold til rummet som et udtryk af den tilsvarende type: , et bundt med en base - som en afhængig type . I dette tilfælde er der ikke behov for at repræsentere rum i form af sæt af punkter udstyret med topologien , og at repræsentere kontinuerlige afbildninger mellem rum som funktioner, der bevarer eller afspejler de tilsvarende punktvise egenskaber af rum. Homotopi typeteori betragter typerum og termer af disse typer (punkter) som elementære begreber, og konstruktioner over rum, såsom homotoper og bundter, som afhængige typer. $a\i A$ $a:A$ $x$ $Økse)$

I den formelle konstruktion af typeteori bruges type-universet , hvis termer er alle andre ikke-universelle ("små") typer, derefter er typer konstrueret sådan , at desuden alle typens udtryk også er termer af typen . Afhængige typer (typefamilier) defineres som funktioner, hvis codomæne er et type-univers. ${\mathcal U}_{0}$ ${\mathcal U}_{1},{\mathcal U}_{2},\dots$ $U_{i}:U_{{i+1}}$ ${\mathcal U}_{i}$ ${\mathcal U}_{{i+1}}$ $B:A\til {\mathcal U}$

I homotopi type teori er der flere måder at konstruere nye typer fra eksisterende. Grundlæggende eksempler på denne art er -typer (afhængige funktionstyper, produkttyper ) og -typer (afhængige sumtyper ) . For en given type og familie kan man konstruere en type, hvis termer er funktioner, hvis codomæne afhænger af et element i definitionsdomænet (geometrisk kan sådanne funktioner repræsenteres som sektioner af et bundt), såvel som en type, hvis termer geometrisk svarer til elementer af det samlede rum i bundtet. ${\boldsymbol \Pi }$ ${\boldsymbol \Sigma }$ $A:{\mathcal U}$ $B:A\til {\mathcal U}$ ${\boldsymbol \Pi }_{{x:A}}B(x)$ ${\boldsymbol \Sigma }_{{x:A}}B(x)$

Ligheden af termer af samme type i homotopi type teori kan enten være en lighed "per definition" ( ) eller en propositionel lighed. Lighed indebærer per definition propositionel lighed, men ikke omvendt. Generelt er den propositionelle lighed af termer og type repræsenteret som en ikke-tom type , som kaldes en identitetstype; vilkårene for denne sidste type er udsigtens veje i rummet ; identitetstypen ses således som rummet af stier (dvs. kontinuerlige afbildninger af enhedssegmentet til ) fra punkt til punkt . $a_{1}:=a_{2}$ $a_{1}$ $a_{2}$ $EN$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $p:a_{1}\rightsquigarrow a_{2}$ $EN$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $\mathbb {I}$ $EN$ $a_{1}$ $a_{2}$

Aksiom for univalens

Den intuitionistiske teori om typer giver os mulighed for at definere begrebet typeækvivalens (for typer, der tilhører det samme univers) og at konstruere en funktion på en kanonisk måde fra en identitetstype til en ækvivalenstype : $A=B$ $A\simeq B$

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

Aksiomet for univalens , formuleret af Voevodsky, siger, at denne funktion også er en ækvivalens:

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

det vil sige, at identitetstypen for to givne typer svarer til ækvivalenstypen for disse typer. Hvis og er propositionelle typer, har aksiomet en særlig gennemsigtig betydning og bunder i det, der nogle gange kaldes kirkens ekstensionalitetsprincip: ligheden af propositioner er logisk ækvivalent med deres logiske ækvivalens; brugen af dette princip betyder, at kun sandhedsværdierne af udsagn tages i betragtning, men ikke deres betydning. En konsekvens af aksiomet er funktionel ekstensionalitet , det vil sige påstanden om, at funktioner, hvis værdier er ens for alle lige værdier af deres argumenter, er lig med hinanden. Denne egenskab ved funktioner er vigtig i datalogi. $EN$ $B$

Aksiomet betragtes af nogle matematiske filosoffer som en nøjagtig matematisk formulering af hovedtesen i filosofien om matematisk strukturalisme , som er baseret på den almindelige praksis for matematisk ræsonnement "op til isomorfisme " eller "op til ækvivalens " [ 5] .

Logik, sæt, gruppeoider

En proposition ( blot udsagn , " bare proposition ") i homotopitypeteori defineres som en type , der enten er tom eller indeholder et enkelt led ; sådanne typer kaldes propositionelle. Hvis typen er tom, så er den tilsvarende påstand falsk; hvis den indeholder en term (symbolsk - ), så er den tilsvarende påstand sand, og udtrykket betragtes som dets bevis. Teorien anvender således det intuitionistiske sandhedsbegreb, hvorefter sandheden af et udsagn forstås som muligheden for at fremlægge et bevis for dette udsagn. $P$ $s$ $P$ $P$ $s$ $p:P$ $P$ $s$

Et fragment af homotopitypeteori, som er begrænset til operationer med propositionelle typer, det vil sige med propositioner, kan beskrives som et logisk fragment (logik) af denne teori. Den logiske disjunktion i propositionsfragmentet svarer til sum-typen , konjunktion til produkt - typen , implikation til funktionstypen , negation til typen , hvor er den tomme type (nul-type). Logikken, der svarer til sådanne konstruktioner, er en variant af intuitionistisk logik , især udsagn som loven om dobbeltnegation eller den udelukkede midte finder ikke sted i den . $A\vee B$ $A+B$ $A\wedge B$ $A\ gange B$ $A\højrepil B$ $A til B$ $\ ikke A$ $A\to \mathbf {0}$ ${\mathbf 0}$

Enhver type , der indeholder to eller flere distinkte termer , kan sættes i en-til-en-korrespondance med en propositional type, som opnås ved at identificere alle termerne for type , en sådan operation kaldes propositional trunkering ( propositional trunkering ). Dette gør det muligt at skelne mellem det "propositionelle niveau" (udsagnsniveauet) af en teori og homotophierarkiet af dens "højere" ikke-propositionelle niveauer. $x$ $x,y,\dots$ $x$

Niveauet af propositioner efterfølges af niveauet af sæt . Et sæt i homotopi type teori er defineret som et rum (type) med en diskret topologi . Tilsvarende kan en mængde i teorien beskrives som en type, således at typen for enhver af dens termer er en proposition, det vil sige enten tom (tilfældet når og er forskellige elementer i sættet ) eller det indeholder et enkelt element (den tilfælde, når og er det samme element). Efter niveauet af sæt kommer niveauet af groupoids (sættet af punkter og sættet af stier mellem hvert par af punkter), og niveauerne af -groupoids af alle ordener. $EN$ $a_{1},a_{2}:A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $a_{1}$ $a_{2}$ $EN$ $a_{1}$ $a_{2}$

Forskellige fortolkninger af typeteoretiske begreber

Biblioteker og implementeringer af HoTT

HoTT-bibliotekerne er adskillige projekter, der hostes på GitHub (i det samme depot, hvor bogens kildekode er placeret), der skaber formelle beskrivelser af forskellige grene af matematikken ved hjælp af automatiske bevissystemer ved hjælp af konstruktioner af homotopi-typeteori.

I Vladimir Voevodskys projekt, kaldet "Bibliotek af univalente baser" [6] , bruges en specialudviklet minimal sikker delmængde Coq , som giver ideologisk renhed og pålidelighed af konstruktioner i overensstemmelse med teorien. HoTT-projektet [7] udføres af standard Coq-værktøjer, implementeret som en del af forskningsprogrammet for Institute for Advanced Study, og følger generelt bogen , fra 2020 deltager 48 udviklere i projektet, de fleste aktive er Jason Gross, Michael Shulman, Ali Kaglayan og Andrey Bauer [8] . Der er også et parallelt projekt i Agda [9] .

Der er flere eksperimentelle interaktive bevissystemer baseret udelukkende på HoTT: Arend , RedPRL, redtt, cooltt, og i Agda version 2.6.0 blev der tilføjet den såkaldte "cubic mode", som tillader fuld brug af homotopityper.

Noter

↑ Makkai Mihaly. Første ordens logik med afhængige sorteringer, med anvendelser til kategoriteori (engelsk) (1995). Hentet 5. december 2014. Arkiveret fra originalen 10. oktober 2015.
↑ Identitetstyper - Topologisk og kategorisk struktur . Værksted, Uppsala, 13.-14. november 2006 (2006) . Dato for adgang: 5. december 2013. Arkiveret fra originalen 18. december 2014. (ubestemt)
↑ Homotopy Type Theory: Univalent Foundations of Mathematics Projektkildekoder på GitHub
↑ HoTT, 2013 , s. iii.
↑ Steve Avodey. Strukturalisme, invarians og 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. marts 2011 – 02. okt. 2020 Bidrag til master, ekskl. fletteforpligtelser .
↑ Agda HoTT biblioteksprojekt på GitHub

Litteratur

Homotopi Type Theory: Univalent Foundations of Mathematics . - Princeton : Institute for Advanced Study , 2013. - 603 s.
Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodsky's Univalence Axiom in Homotopy Type Theory (engelsk) // Notices of the AMS . - 2013. - Bd. 60 , nr. 9 . - S. 1164-1167 .
Hannes Hummel. Vil computere omdefinere matematikkens rødder? . Da en legendarisk matematiker fandt en fejl i sit eget arbejde, begyndte han på en computerstøttet mission for at eliminere menneskelige fejl. For at han er nødt til at omskrive de århundrede gamle regler, der ligger til grund for al matematik . Quanta Magazine (19. maj 2015) . Hentet: 31. december 2017.
Don Monroe. En ny form for matematik? (engelsk) // Kommunikation af ACM . - 2014. - Bd. 57 , nr. 2 . - S. 13-15 . - doi : 10.1145/2557446 .
Andrey Rodin. Logisk og geometrisk atomisme fra Leibniz til Voevodsky // Filosofiens problemer . - 2016. - Nr. 6 . - S. 134-142 .