Homotópia típusú elmélet

A homotópia típuselmélet ( HoTT , angolul homotopy type theory ) egy matematikai elmélet, a típuselmélet egy speciális változata , amely kategóriaelmélet , algebrai topológia , homológ algebra fogalmaival van felszerelve ; a homotópia tértípus , a magasabb kategóriák és a logikai és programozási nyelvek típusai közötti kapcsolaton alapul .

Az Univalent Foundations of Mathematics egy univerzális formális nyelv felépítésére szolgáló program a homotópia típusú elmélet segítségével, amely konstruktív alapja a modern matematika ágainak, és lehetővé teszi a bizonyítások helyességének automatikus ellenőrzését számítógépen . Vlagyimir Voevodszkij kezdeményezte a 2000-es évek végén; Az univalens alapok iránti szélesebb körű érdeklődés ösztönzője a Voevodsky által írt formalizált matematikai „Alapok” könyvtár volt, amely a 2010-es évek közepére az UniMath könyvtár részévé vált, és sok más könyvtár alapjául szolgált ; írt matematikusok nagy csapata .

A matematikai bizonyítás a homotópia típuselméletben a kívánt típus „lakhatóságának” megállapításából, vagyis a megfelelő típus kifejezésének megalkotásából áll. Az automatikus bizonyítási rendszerek elméleti alkalmazása a Curry-Howard izomorfizmus gondolatát aknázza ki , és a típuselméleti fogalmakba ágyazott matematikai tartalomnak köszönhetően az elmélet formális nyelvezetében inkább kifejezhető és ellenőrizhető. összetett eredmények a matematika absztrakt részeiből, amelyeket korábban szoftveresen nem formalizálhatónak tartottak.

Az elmélet kulcsgondolata az univalencia axiómája , amely az objektumok egyenlőségét feltételezi, amelyek között ekvivalencia állapítható meg, vagyis a homotópia típuselméletben az izomorf, homeomorf, homotopikusan ekvivalens struktúrákat tekintik egyenlőnek; ez az axióma a magasabb kategóriájú értelmezés fontos tulajdonságait ragadja meg, és a formális nyelv technikai leegyszerűsítését is biztosítja.

Történelem

Az ötlet, hogy Per Martin-Löf intuicionista típuselméletét magasabb kategóriák formalizálására használjuk, Makkai Mihai ( Hung. Makkai Mihály ) munkásságáig nyúlik vissza, amelyben a FOLDS ( elsőrendű logika függő fajtákkal ) rendszerét építették. [1] . A legfontosabb különbség az univalens alapok és Mackay elképzelései között az az elv, hogy a matematika alapvető tárgyai nem magasabb kategóriák, hanem magasabb csoportoidok. Mivel a magasabb csoportoidok megfelelnek a Grothendieck homotópiatípusoknak való megfelelésnek , elmondható, hogy a matematika az univalens bázisok szempontjából homotópiatípusokon vizsgálja a struktúrákat. A Martin-Löf típuselmélet közvetlen felhasználásának lehetősége a homotópiatípusok struktúráinak leírására Voevodsky egy univalens típuselméleti modelljének a következménye. Ennek a modellnek a felépítése számos, az úgynevezett koherencia-tulajdonságokkal kapcsolatos technikai probléma megoldását követelte meg, és bár az univalens bázisok fő gondolatait 2005–2006-ban fogalmazta meg, a teljes univalens modell az egyszerűsített halmazok kategóriájában csak akkor jelent meg . 2009 - ben . Voevodszkij ezen tanulmányaival egyidőben más munkákat is végeztek a típuselmélet és a homotópiaelmélet közötti különféle összefüggések tanulmányozására, különösen az egyik történelmileg fontos esemény, amely összehozta az ebben az irányban dolgozó tudósokat, egy novemberi uppsalai szeminárium volt. 2006 év [2] .

2010 februárjában Voevodsky könyvtárat kezdett létrehozni a Coq -on , amely később „egyértékű bázisok könyvtárává” nőtt , amelyet a tudósok széles köre közösen fejlesztett ki .

Voevodsky kezdeményezésére az Institute for Advanced Study 2012–2013-as tanévét „az egyenértékű alapok évének” nyilvánították, az Audival és a Kokannal együttműködve speciális kutatási programot nyitottak, ennek keretében matematikusok, ill. informatikusok dolgoztak az elmélet kidolgozásán. Az év egyik eredménye volt, hogy a résztvevők közösen elkészítették a hatszáz oldalas „ Homotopikus típuselmélet: a matematika egyértelmű alapjai ” című könyvet , amelyet a program honlapján tettek közzé ingyenesen a CC-SA licenc alatt ; egy projektet hoztak létre a GitHubon [3] , hogy együttműködjenek a könyvön .

A program résztvevői a könyv bevezetőjében [4] :

Thorsten Altenkirch ( angolul Thorsten Altenkirch )
Benedikt Ahrens ( Benedikt Ahrens )
Steve Audi _ _ _
Bruno Barras ( Bruno Barras )
Andrej Bauer ( szlovén Andrej Bauer )
Marc Bezem ( Marc Bezem )
Yves Bertot ( Yves Bertot )
Benno van den Berg
Vlagyimir Voevodszkij
Daniel Grayson ( Daniel Grayson , a Macaulay2 számítógépes algebrarendszer megalkotója )
André Joyal ( francia André Joyal )
Thierry Cocan
Dan Licata ( Dan Licata )
Peter Lumsdaine ( Peter Lumsdaine )
Per Martin-Löf
Assia Mahboubi ( Assia Mahboubi )
Szergej 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 _ _ _
Aczel Péter _ _ _
Hugo Herbelin , a Coq fejlesztési projektvezetője

Emellett a bevezető utal arra, hogy hat hallgató is jelentős mértékben hozzájárult, és megjegyzi több mint 20 tudós és gyakorlati szakember közreműködését, akik az „egyvalens alapok évében” látogattak el a Felsőoktatási Intézetbe (köztük az egyetem szemantikájának megalkotója) . λ-számítás Dana Scott és a fejlesztői formalizálások Coq-on a négy színprobléma és a Feit-Thompson tétel bizonyítására ( Georges Gontier ). A könyv két részből áll - "Alapok" és "Matematika", az első részben a főbb rendelkezéseket és az eszközöket ismertetjük, a második részben a homotópia-elmélet, a kategóriaelmélet , a halmazelmélet megvalósításai , a valós számok . a bevezetett eszközök felhasználásával épült .

Alapok

Az elmélet Martin-Löf intuicionista típuselméletének egy intenzionális változatán alapul, és a típusok értelmezését használja a homotópiaelmélet és a magasabb kategóriák tárgyaként. Ebből a szempontból tehát egy pontnak a térhez tartozás viszonyát a megfelelő típusú tagnak tekintjük : , köteg alappal - függő típusnak . Ebben az esetben nincs szükség a tereket topológiával ellátott ponthalmazok formájában ábrázolni, és a terek közötti folyamatos leképezéseket olyan függvényekként ábrázolni, amelyek megőrzik vagy tükrözik a terek megfelelő pontszerű tulajdonságait. A homotópiatípus-elmélet a típustereket és az ilyen típusú terminusokat (pontokat) elemi fogalomnak tekinti, a terek feletti konstrukciókat, például homotópiákat és kötegeket, függő típusoknak. $a\in A$ $a:A$ $x$ $Fejsze)$

A típuselmélet formális felépítésében a típusuniverzumot használjuk , amelynek minden más nem univerzális ("kicsi") típusa a kifejezés, majd a típusokat úgy építjük fel , hogy ráadásul a típus minden tagja egyben terminus is . a típusból . A függő típusokat (típuscsaládokat) olyan függvényekként határozzuk meg, amelyek kódtartománya valamilyen típus-univerzum. ${\mathcal U}_{0}$ ${\mathcal U}_{1},{\mathcal U}_{2},\pontok$ $U_{i}:U_{{i+1}}$ ${\mathcal U}_{i}$ ${\mathcal U}_{{i+1}}$ $B:A\ to {\mathcal U}$

A homotópia típuselméletben többféle módon lehet új típusokat építeni a meglévőkből. Az ilyen típusú alapvető példák a -types (függő funkcionális típusok, terméktípusok ) és a -types (függő összeg típusok ). Egy adott típushoz és családhoz létrehozhatunk olyan típust, amelynek tagjai olyan függvények, amelyek kódtartománya a definíciós tartomány egy elemétől függ (geometriailag az ilyen függvények valamilyen köteg szakaszaiként ábrázolhatók), valamint olyan típust, amelynek tagjai geometriailag megfelelnek a köteg teljes területének elemeinek . ${\boldsymbol \Pi }$ ${\boldsymbol \Sigma }$ $V:{\mathcal U}$ $B:A\ to {\mathcal U}$ ${\boldsymbol \Pi }_{{x:A}}B(x)$ ${\boldsymbol \Sigma }_{{x:A}}B(x)$

Az azonos típusú kifejezések egyenlősége a homotópia típuselméletben lehet „definíció szerint” egyenlőség ( ) vagy propozíciós egyenlőség. Az egyenlőség definíció szerint magában foglalja a propozíciós egyenlőséget, de fordítva nem. Általánosságban elmondható, hogy a kifejezések és a típus propozíciós egyenlőségét nem üres típusként ábrázoljuk , amelyet azonosságtípusnak nevezünk; ez utóbbi típus kifejezései a nézet útjai a térben ; így az identitástípust az utak tereként tekintjük (azaz az egységszegmens folyamatos leképezéseit pontról pontra ) . $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}$

Az univalencia axiómája

A típusok intuicionista elmélete lehetővé teszi, hogy meghatározzuk a típusekvivalencia fogalmát (az azonos univerzumhoz tartozó típusokra), és egy függvényt kanonikus módon konstruáljunk identitástípusból ekvivalenciatípusba : $A=B$ $A\simeq B$

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

Az univalencia axiómája , amelyet Voevodsky fogalmazott meg, kimondja, hogy ez a függvény egyben ekvivalencia is:

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

vagyis két adott típus azonosságtípusa egyenértékű azon típusok ekvivalenciatípusával. Ha és propozíciós típusok, az axióma különösen átlátszó jelentéssel bír, és az olykor Church extenzionalitás-elvének nevezettre csapódik le: a propozíciók egyenlősége logikailag egyenértékű logikai ekvivalenciájukkal; ennek az elvnek a használata azt jelenti, hogy csak az állítások igazságértékét veszik figyelembe, de jelentésüket nem. Az axióma következménye a funkcionális extenzionalitás , vagyis az az állítás, hogy azok a függvények, amelyek értéke egyenlő argumentumaik minden egyenlő értékére, egyenlők egymással. A függvényeknek ez a tulajdonsága fontos a számítástechnikában. $A$ $B$

Az axiómát egyes matematikafilozófusok a matematikai strukturalizmus filozófiája fő tézisének egzakt matematikai megfogalmazásának tekintik , amely a matematikai érvelés általános gyakorlatán alapul "az izomorfizmusig " vagy "az ekvivalenciáig " . 5] .

Logika, halmazok, csoportoidok

A propozíciót ( puszta proposition , " puszta propozíció " ) a homotópia típuselméletben olyan típusként határozzák meg , amely vagy üres , vagy egyetlen kifejezést tartalmaz ; az ilyen típusokat propozicionálisnak nevezzük. Ha a típus üres, akkor a megfelelő állítás hamis, ha tartalmaz egy kifejezést (szimbolikusan - ), akkor a megfelelő állítás igaz, és a kifejezést annak bizonyítékának tekintjük. Így az elmélet az igazság intuicionista fogalmát használja, amely szerint egy állítás igazsága alatt az állítás bizonyításának lehetőségét értjük. $P$ $p$ $P$ $P$ $p$ $p:P$ $P$ $p$

A homotópiatípus-elmélet egy töredéke, amely a propozíciótípusokkal, azaz propozíciókkal végzett műveletekre korlátozódik, ennek az elméletnek a logikai töredékeként (logikájaként) írható le. A propozíciós töredék logikai diszjunkciója megfelel az összeg típusnak , a konjunkció a szorzat típusnak , az implikáció a funkcionális típusnak , a tagadás a típusnak , ahol az üres típus (null típusú). Az ilyen konstrukcióknak megfelelő logika az intuicionista logika egy változata , különösen nem szerepelnek benne olyan kijelentések, mint a kettős tagadás törvénye vagy a kizárt közép . $A\vee B$ $A+B$ $A\wedge B$ $A\-szer B$ $A\jobbra nyíl B$ $A-tól B-ig$ $\lnem A$ $A\to \mathbf {0}$ ${\mathbf 0}$

Bármely típus , amely két vagy több különálló kifejezést tartalmaz , egy az egyhez megfeleltetésbe helyezhető egy propozíciótípussal, amelyet a típus összes tagjának azonosításával kapunk. Az ilyen műveletet propozíciós csonkításnak ( propozíciós csonkítás ) nevezik. Ez lehetővé teszi, hogy különbséget tegyünk egy elmélet „propozíciós szintje” (állítási szint) és „magasabb” nem propozíciós szintjei homotópia-hierarchiája között. $x$ $x,y,\dots$ $x$

A propozíciók szintjét a halmazok szintje követi . A homotópia típuselméletben egy halmazt diszkrét topológiájú térként (típusként) definiálunk . Ezzel egyenértékűen egy halmaz elméletben leírható típusként úgy, hogy bármelyik kifejezésére a típus egy propozíció, azaz vagy üres (az az eset, amikor és a halmaz különböző elemei ), vagy egyetlen elemet tartalmaz (a eset, amikor és ugyanaz az elem). A halmazok szintje után következik a csoportoidok szintje (a pontok halmaza és az egyes pontpárok közötti utak halmaza), valamint az összes rendű -groupoidok szintjei . $A$ $a_{1},a_{2}:A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $a_{1}$ $a_{2}$ $A$ $a_{1}$ $a_{2}$

A típuselméleti fogalmak különféle értelmezései

A HoTT könyvtárai és megvalósításai

A HoTT Libraries több, a GitHubon üzemeltetett projekt ( ugyanabban a tárhelyen, ahol a könyv forráskódja is található), amelyek a matematika különböző ágainak formális leírását hoznak létre automatikus bizonyítási rendszerekkel, homotópia típusú elmélet konstrukcióit használva.

Vlagyimir Voevodszkij "Egyértékű bázisok könyvtára" [6] nevű projektjében egy speciálisan kifejlesztett minimális biztonságos Coq részhalmazt használnak , amely az elmélettel összhangban biztosítja a konstrukciók ideológiai tisztaságát és megbízhatóságát. A HoTT projekt [7] szabványos Coq eszközökkel valósul meg, az Institute for Advanced Study kutatási programjának részeként valósult meg, és általában a könyvet követi , 2020-ig 48 fejlesztő vesz részt a projektben, a legtöbb aktívak Jason Gross, Michael Shulman, Ali Kaglayan és Andrey Bauer [8] . Agdában is van egy párhuzamos projekt [9] .

Számos kísérleti interaktív bizonyító rendszer létezik , amelyek teljes egészében HoTT-re épülnek: Arend , RedPRL, redtt, cooltt, és az Agda 2.6.0-s verziójában bekerült az úgynevezett "cubic mode", amely lehetővé teszi a homotópia típusok teljes körű használatát.

Jegyzetek

↑ Makkai Mihály. Elsőrendű logika függő rendezésekkel, alkalmazásokkal a kategóriaelmélethez (angol) (1995). Letöltve: 2014. december 5. Az eredetiből archiválva : 2015. október 10.
↑ Identitástípusok – topológiai és kategorikus struktúra . Workshop, Uppsala, 2006. november 13-14. (2006) . Hozzáférés időpontja: 2013. december 5. Az eredetiből archiválva : 2014. december 18. (határozatlan)
↑ Homotópiatípuselmélet: A matematika univalens alapjai, projektforráskódok a GitHubon
↑ HoTT, 2013 , p. iii.
↑ Steve Avodey. Strukturalizmus, változatlanság és univalencia // Philosophia Mathematica . - Oxford University Press , 2014. - V. 22 , 1. szám . — ISSN 0031-8019 . - doi : 10.1093/philmat/nkt030 .
↑ Univalent Base Library Project a GitHubon
↑ Homotopy Type Theory Project a GitHubon
↑ HoTT 2011. március 20. – 2020. október 02. Hozzájárulás a masterhez, az összevonási kötelezettségvállalások kivételével .
↑ Agda HoTT könyvtárprojekt a GitHubon

Irodalom

Homotópiatípuselmélet: A matematika univalens alapjai . - Princeton : Institute for Advanced Study , 2013. - 603 p.
Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodsky univalencia-axiómája a homotópiatípus-elméletben (angol) // Notices of the AMS . - 2013. - Kt. 60 , sz. 9 . - P. 1164-1167 .
Hannes Hummel. A számítógépek újradefiniálják a matematika gyökereit? . Amikor egy legendás matematikus hibát talált saját munkájában, számítógépes kutatásba kezdett, hogy kiküszöbölje az emberi hibákat. Ehhez át kell írnia az egész matematika alapjául szolgáló évszázados szabályokat . Quanta Magazine (2015. május 19. ) Letöltve: 2017. december 31.
Don Monroe. Egy új típusú matematika? (angol) // Az ACM kommunikációja . - 2014. - Kt. 57 , sz. 2 . - 13-15 . o . - doi : 10.1145/2557446 .
Andrej Rodin. Logikai és geometriai atomizmus Leibniztől Voevodskyig // A filozófia problémái . - 2016. - 6. sz . - S. 134-142 .

Linkek

cs.cmu.edu/~rwh/courses/hott/ - kurzusanyagok a homotópia típuselméletről , amelyet Robert Harper tanított a Carnegie Mellon Egyetemen