Homotopytyyppinen teoria

Homotopy tyyppiteoria ( HoTT , englannista homotopy type theory ) on matemaattinen teoria ,erityinen versio tyyppiteoriasta , joka on varustettu käsitteillä luokkateoriasta , algebrallinen topologia , homologinen algebra ; perustuu homotopian avaruuden käsitteiden, korkeampien luokkien ja logiikka- ja ohjelmointikielten tyyppien väliseen suhteeseen .

Univalent Foundations of Mathematics on ohjelma universaalin muodollisen kielen rakentamiseen homotopy-tyyppiteorian avulla, joka on rakentava perusta nykyaikaisille matematiikan aloille ja tarjoaa mahdollisuuden automaattisesti tarkistaa todisteiden oikeellisuus tietokoneella . Vladimir Voevodskyn aloitteesta 2000-luvun lopulla; sysäys laajemmalle kiinnostukselle univalenttisia perusteita kohtaan oli Voevodskyn kirjoittama formalisoidun matematiikan "Foundations" kirjasto, josta tuli osa UniMath -kirjastoa 2010-luvun puoliväliin mennessä ja joka toimi perustana monille muille kirjastoille ; kirjoitti suuri joukko matemaatikoita .

Matemaattinen todistus homotopian tyyppiteoriassa koostuu vaaditun tyypin "asutettavuuden" toteamisesta, eli vastaavan tyypin lausekkeen rakentamisesta. Automaattisten todistusjärjestelmien käyttö teoriassa hyödyntää Curry-Howard-isomorfismin ideaa , ja tyyppiteoreettisiin käsitteisiin upotetun matemaattisen sisällön ansiosta teorian muodollisella kielellä on mahdollista ilmaista ja todentaa pikemminkin monimutkaisia tuloksia matematiikan abstrakteista osista, joita ei aiemmin pidetty ohjelmiston formalisoitavissa.

Teorian keskeisenä ajatuksena on univalenssiaksiooma , joka postuloi objektien yhtäläisyyden, joiden välille voidaan todeta ekvivalenssi, eli homotopiatyyppiteoriassa isomorfisia, homeomorfisia, homotooppisesti ekvivalentteja rakenteita pidetään samanarvoisina; tämä aksiooma kaappaa korkeamman kategorian tulkinnan tärkeitä ominaisuuksia ja tarjoaa myös teknisen yksinkertaistuksen muodollisesta kielestä.

Historia

Ajatus Per Martin- Löfin intuitionistisen tyyppiteorian käyttämisestä korkeampien kategorioiden formalisoimiseen juontaa juurensa Mihai Makkain ( Hung. Makkai Mihály ) työhön, jossa rakennettiin FOLDS ( ensimmäisen asteen logiikka riippuvaisilla lajeilla ) -järjestelmä. [1] . Keskeinen ero univalenttien ja Mackayn ideoiden välillä on periaate, jonka mukaan matematiikan perusobjektit eivät ole korkeampia kategorioita, vaan korkeampia ryhmiä. Koska korkeammat groupoidit vastaavat Grothendieck-vastaavuutta homotopiatyypeille , voidaan sanoa, että matematiikka tutkii univalenttisten perusteiden suhteen homotoopiatyyppien rakenteita. Mahdollisuus käyttää Martin-Löfin tyyppiteoriaa suoraan kuvaamaan homotoopiatyyppien rakenteita on seurausta Voevodskyn rakentamasta univalenttisesta tyyppiteorian mallista. Tämän mallin rakentaminen edellytti lukuisten ns. koherenssiominaisuuksiin liittyvien teknisten ongelmien ratkaisemista, ja vaikka hän muotoili pääideat univalenttisista emäksistä vuosina 2005–2006, täydellinen univalenttinen malli yksinkertaisten joukkojen kategoriaan ilmestyi vasta vuonna 2009 . Samoihin vuosiin kuin nämä Voevodsky-tutkimukset tehtiin muitakin töitä tyyppiteorian ja homotopiateorian välisten erilaisten yhteyksien tutkimiseksi, erityisesti yksi historiallisesti merkittävistä tapahtumista, joka kokosi yhteen tähän suuntaan työskenteleviä tiedemiehiä, oli seminaari Uppsalassa marraskuussa. 2006 vuotta [2] .

Helmikuussa 2010 Voevodsky alkoi luoda Coqiin kirjastoa , joka myöhemmin kasvoi "yksiarvoisten tukikohtien kirjastoksi" , jonka useat tutkijat ovat kehittäneet yhdessä .

Voevodskyn aloitteesta Syventävän tutkimuksen instituutin lukuvuosi 2012–2013 julistettiin "yksiarvoisten perusteiden vuodeksi", yhteistyössä Audin ja Kokanin kanssa avattiin erityinen tutkimusohjelma ja sen puitteissa ryhmä matemaatikoita ja tietotekniikan tutkijat työskentelivät teorian kehittämisen parissa. Yksi vuoden tuloksista oli osallistujien yhteinen kuusisataasivuinen kirja " Homotopic Type Theory: Univalent Foundations of Mathematics ", joka julkaistiin ohjelman verkkosivuilla vapaaseen käyttöön CC-SA-lisenssillä ; GitHubille [3] luotiin projekti yhteistyössä kirjan parissa .

Ohjelman osallistujat, esitelty kirjan johdannossa [4] :

Thorsten Altenkirch ( englanniksi Thorsten Altenkirch )
Benedikt Ahrens ( Benedikt Ahrens )
Steve Audi _ _ _
Bruno Barras ( Bruno Barras )
Andrej Bauer ( slovenialainen Andrej Bauer )
Marc Bezem ( Marc Bezem )
Yves Bertot ( Yves Bertot )
Benno van den Berg
Vladimir Voevodsky
Daniel Grayson ( Daniel Grayson , Macaulay2 tietokonealgebrajärjestelmän luoja )
André Joyal ( ranskalainen 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 , Coqin kehitysprojektipäällikkö

Lisäksi johdannossa todetaan, että myös kuusi opiskelijaa teki merkittävän panoksen, ja panee merkille myös yli 20 korkeakoulututkinnon instituutissa vierailleen "yksiarvoisen perustan vuoden" aikana (mukaan lukien instituutin semantiikan luojan) panoksen . λ-laskenta Dana Scott ja Coqin kehittäjäformalisaatiot neljän värin ongelman ja Feit-Thompsonin lauseen todisteille ( Georges Gontier ). Kirja on rakennettu kahteen osaan - "Perusasiat" ja "Matematiikka", ensimmäisessä osassa esitetään pääsäännöt ja määritellään työkalut, toisessa - homotopiateorian, kategoriateorian , joukkoteorian toteutukset , reaaliluvut . rakennettu käyttäen käyttöön otettuja keinoja .

Perusteet

Teoria perustuu Martin-Löfin intuitionistisen tyyppiteorian intensionaaliseen muunnelmaan ja käyttää tyyppien tulkintaa homotopiateorian ja korkeampien kategorioiden kohteina. Tästä näkökulmasta katsottuna pisteen kuuluvuuden suhdetta avaruuteen pidetään siis vastaavan tyyppisenä terminä : , nipu , jossa on kanta - riippuvaisena tyyppinä . Tässä tapauksessa ei tarvitse esittää avaruuksia pistejoukkojen muodossa, jotka on varustettu topologialla , ja esittää jatkuvia avaruuksien välisiä kuvauksia funktioina, jotka säilyttävät tai heijastavat avaruuksien vastaavat pistemäiset ominaisuudet. Homotoopiatyyppiteoria pitää tyyppiavaruutta ja näiden tyyppien termejä (pisteitä) alkeiskäsitteinä ja tilojen yli olevia konstruktioita, kuten homotopioita ja nippuja, riippuvaisina tyypeinä. $a\in A$ $a:A$ $X$ $Kirves)$

Tyyppiteorian muodollisessa konstruktiossa käytetään tyyppiuniversumia , jonka termit ovat kaikki muut ei-universaalit ("pienet") tyypit, sitten tyypit rakennetaan siten, että lisäksi kaikki tyypin termit ovat myös termejä . tyypistä . Riippuvaiset tyypit (tyyppiperheet) määritellään funktioiksi, joiden koodialue on jokin tyyppiuniversumi. ${\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}$

Homotopian tyyppiteoriassa on useita tapoja rakentaa uusia tyyppejä olemassa olevista. Perusesimerkkejä tällaisista ovat -tyypit (riippuvaiset toiminnalliset tyypit, tuotetyypit ) ja -tyypit (riippuvaiset summatyypit ) . Tietylle tyypille ja perheelle voidaan rakentaa tyyppi, jonka termit ovat funktioita, joiden koodialue riippuu määrittelyalueen elementistä (geometrisesti tällaiset funktiot voidaan esittää jonkin nipun osina), sekä tyyppi, jonka termit geometrisesti vastaavat nipun kokonaistilan osia . ${\boldsymbol \Pi }$ ${\boldsymbol \Sigma }$ $V:{\mathcal U}$ $B:A\to {\mathcal U}$ ${\boldsymbol \Pi }_{{x:A}}B(x)$ ${\boldsymbol \Sigma }_{{x:A}}B(x)$

Samantyyppisten termien yhtäläisyys homotopian tyyppiteoriassa voi olla joko "määritelmän mukaan" ( ) tai propositionaalinen yhtäläisyys. Tasa-arvo tarkoittaa määritelmän mukaan propositionaalista tasa-arvoa, mutta ei päinvastoin. Yleensä termien ja tyypin propositionaalinen yhtäläisyys esitetään ei-tyhjänä tyyppinä , jota kutsutaan identiteettityypiksi; tämän viimeisen tyypin termit ovat näkymän polut avaruudessa ; identiteettityyppiä tarkastellaan siten polkujen (eli yksikkösegmentin jatkuvien kartoitusten ) tilana pisteestä pisteeseen . $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}$

Univalenssin aksiooma

Intuitionistinen tyyppiteoria mahdollistaa tyyppiekvivalenssin käsitteen määrittelemisen (samaan universumiin kuuluville tyypeille) ja funktion rakentamisen kanonisella tavalla identiteettityypistä ekvivalenssityyppiin : $A=B$ $A\simeq B$

{\näyttötyyli (A=B)\to (A\simeq B)}

Voevodskyn muotoilema univalenssiaksiooma sanoo, että tämä funktio on myös ekvivalenssi :

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

eli kahden tietyn tyypin identiteettityyppi vastaa näiden tyyppien ekvivalenssityyppiä. Jos ja ovat propositionaalisia tyyppejä, aksioomalla on erityisen läpinäkyvä merkitys ja se tiivistyy siihen, mitä joskus kutsutaan Churchin ekstensiaalisuuden periaatteeksi: lauseiden tasa-arvo vastaa loogisesti niiden loogista ekvivalenssia; Tämän periaatteen käyttö tarkoittaa, että vain lausuntojen totuusarvot otetaan huomioon, mutta ei niiden merkitystä. Aksiooman seurauksena on funktionaalinen ekstensioisuus eli väite, jonka mukaan funktiot, joiden arvot ovat samat kaikille argumenttiensa yhtäläisille arvoille, ovat keskenään samanarvoisia. Tämä funktioiden ominaisuus on tärkeä tietojenkäsittelytieteessä. $A$ $B$

Jotkut matematiikan filosofit pitävät aksioomaa täsmällisenä matemaattisena muotoiluna matemaattisen strukturalismin filosofian , joka perustuu matemaattisen päättelyn yleiseen käytäntöön " isomorfismiin asti " tai " ekvivalenssiin asti " . 5] .

Logiikka, joukot, ryhmäoidit

Homotopian tyyppiteoriassa lause ( pelkkä proposition , " paljas proposition " ) määritellään tyypiksi , joka on joko tyhjä tai sisältää yhden termin ; tällaisia tyyppejä kutsutaan propositioksi. Jos tyyppi on tyhjä, vastaava lause on epätosi, jos se sisältää termin (symbolisesti - ), niin vastaava lause on tosi, ja termiä pidetään sen todisteena. Siten teoriassa käytetään intuitionistista totuuskäsitettä, jonka mukaan väitteen totuus ymmärretään mahdollisuutena esittää todiste tästä väitteestä. $P$ $s$ $P$ $P$ $s$ $p:P$ $P$ $s$

Fragmentti homotopy-tyyppisestä teoriasta, joka rajoittuu operaatioihin lausetyyppien eli proposioiden kanssa, voidaan kuvata tämän teorian loogiseksi fragmentiksi (logiikaksi). Lausuntofragmentin looginen disjunktio vastaa summa-tyyppiä , konjunktio tulo - tyyppiä , implikaatio funktionaalista tyyppiä , negaatio tyyppiä , missä on tyhjä tyyppi (nolla-tyyppi). Tällaisia rakenteita vastaava logiikka on intuitionistisen logiikan muunnelma, jossa ei esiinny erityisesti sellaisia väitteitä kuin kaksoisnegaation laki tai poissuljettu keskikohta . $A\vee B$ $A+B$ $A\wedge B$ $A\ kertaa B$ $A\Nuoli oikealle B$ $A:sta B:hen$ $\l ei A$ $A\to \mathbf {0}$ ${\mathbf 0}$

Mikä tahansa tyyppi , joka sisältää kaksi tai useampia erillisiä termejä, voidaan asettaa yksi-yhteen-vastaavuuteen lausetyypin kanssa, joka saadaan tunnistamalla kaikki tyypin termit. Tällaista operaatiota kutsutaan propositional truncationiksi ( propositional truncation ). Tämä tekee mahdolliseksi erottaa teorian "ehdotustason" (lausuntotason) ja sen "korkeampien" ei-propositionaalisten tasojen homotopiahierarkian. $X$ ${\näyttötyyli x,y,\pisteet }$ $X$

Ehdotusten tasoa seuraa joukkojen taso . Homotopian tyyppiteoriassa joukko määritellään avaruudeksi (tyypiksi), jolla on diskreetti topologia . Vastaavasti joukko voidaan kuvata teoriassa tyypiksi siten, että mille tahansa sen termille tyyppi on lause, eli joko tyhjä (tapaus, kun ja ovat joukon eri elementtejä ) tai se sisältää yhden elementin ( tapaus, jolloin ja ovat sama elementti). Joukkotason jälkeen tulee ryhmittymien taso (pistejoukko ja kunkin pisteparin välinen polkujoukko) ja kaikkien kertalukujen -ryhmätasot . $A$ $a_{1},a_{2}:A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $a_{1}$ $a_{2}$ $A$ $a_{1}$ $a_{2}$

Erilaisia tulkintoja tyyppiteoreettisista käsitteistä

HoTT:n kirjastot ja toteutukset

HoTT-kirjastot ovat useita GitHubissa isännöityjä projekteja (samassa arkistossa, jossa kirjan lähdekoodi sijaitsee), jotka luovat muodollisia kuvauksia matematiikan eri aloille käyttämällä automaattisia todistusjärjestelmiä käyttäen homotopy-tyyppisen teorian rakenteita.

Vladimir Voevodskyn hankkeessa, nimeltään "Yksivalenttien tukikohtien kirjasto" [6] , käytetään erityisesti kehitettyä vähimmäisturvallista alajoukkoa Coq , joka tarjoaa ideologisen puhtauden ja rakenteille teorian mukaisen luotettavuuden. HoTT-projekti [7] toteutetaan Coq-standardin työkaluilla, osana Institute for Advanced Study -tutkimusohjelmaa, ja se noudattaa pääsääntöisesti kirjaa , vuoden 2020 mukaan projektissa on mukana 48 kehittäjää, eniten. aktiivisia ovat Jason Gross, Michael Shulman, Ali Kaglayan ja Andrey Bauer [8] . Agdassa on myös rinnakkainen hanke [9] .

On olemassa useita kokeellisia interaktiivisia todistusjärjestelmiä, jotka perustuvat kokonaan HoTT:hen: Arend , RedPRL, redtt, cooltt ja Agda-versioon 2.6.0 lisättiin ns. "kuutiotila", joka mahdollistaa homotopiatyyppien täyden käytön.

Muistiinpanot

↑ Makkai Mihaly. First Order Logic with Dependent Sorts, with Applications to Category Theory (Englanti) (1995). Haettu 5. joulukuuta 2014. Arkistoitu alkuperäisestä 10. lokakuuta 2015.
↑ Identiteettityypit – topologinen ja kategorinen rakenne . Workshop, Uppsala, 13.-14.11.2006 (2006) . Käyttöpäivä: 5. joulukuuta 2013. Arkistoitu alkuperäisestä 18. joulukuuta 2014. (määrätön)
↑ Homotopy Type Theory: Univalent Funds of Mathematics Project lähdekoodit GitHubissa
↑ HoTT, 2013 , s. iii.
↑ Steve Avodey. Strukturalismi, muuttumattomuus ja univalenssi // Philosophia Mathematica . - Oxford University Press , 2014. - V. 22 , nro 1 . — ISSN 0031-8019 . - doi : 10.1093/philmat/nkt030 .
↑ Univalent Base Library Project GitHubissa
↑ Homotopy Type Theory Project GitHubissa
↑ HoTT 20. maaliskuuta 2011 – 2. lokakuuta 2020 Osallistuminen master-versioon, lukuun ottamatta yhdistämissitoumuksia .
↑ Agda HoTT -kirjastoprojekti GitHubissa

Kirjallisuus

Homotopy Type Theory: Univalent Foundations of Mathematics . - Princeton : Institute for Advanced Study , 2013. - 603 s.
Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodskyn univalenssiaksiooma homotopian tyyppiteoriassa (englanniksi) // AMS:n huomautuksia . - 2013. - Vol. 60 , ei. 9 . - s. 1164-1167 .
Hannes Hummel. Määrittävätkö tietokoneet matematiikan juuret uudelleen? . Kun legendaarinen matemaatikko havaitsi virheen omassa työssään, hän ryhtyi tietokoneavusteiseen pyrkimykseen eliminoida inhimilliset erehdykset. Hänen on kirjoitettava uudelleen koko matematiikan taustalla olleet vuosisadan vanhat säännöt . Quanta Magazine (19. toukokuuta 2015) . Haettu: 31. joulukuuta 2017.
Don Monroe. Uudenlainen matematiikka? (englanti) // ACM:n viestintä . - 2014. - Vol. 57 , no. 2 . - s. 13-15 . - doi : 10.1145/2557446 .
Andrei Rodin. Looginen ja geometrinen atomismi Leibnizistä Voevodskyyn // Filosofian ongelmat . - 2016. - Nro 6 . - S. 134-142 .

Linkit

cs.cmu.edu/~rwh/courses/hott/ - Robert Harperin Carnegie Mellonin yliopistossa opettaman homotopian tyyppiteorian kurssimateriaalit